问题标签 [smt]

在有界上下文（即所有基本排序都是位向量）中，我们将（2-dim）集合建模为数组。在某些公理中，我们需要对这个数组进行量化。一旦我们包含了这样的公理，求解器就会返回未知数。从句法的角度来看，这种量词超出了 的范围FOL，但我们期望求解器能够识别/使用有界上下文信息。

1. 为什么求解器不使用有界上下文信息？
2. 有没有可能在没有手动量词爆破的情况下将这个教给求解器？

这是一个最小的例子：

我使用以下策略来简化表达

原来的表达是：

应用该策略后，简化结果为：

但是，我认为第二个目标可以删除，因为它比第一个要强。那么如何使用 z3 来获得更简单的结果呢？

我有这段代码来检查其他元素是否包含集。

我的问题是您也想将此代码用于 8 位和 16 位的向量，但它不起作用。

例如，如果我将所有 (_BitVec 6) 替换为 (_BitVec 8)，上面的代码就不能正常工作，因为结果应该是 unsat 但它是 sat。

好像 6 位向量效果很好。

如何使它适用于不同大小的位向量？

据我了解，Z3 在遇到量化线性实数/有理算术时，应用了 Bjørner、IJCAR 2010 以及 Bjørner 和 Monniaux 最近的工作中描述的量词消除形式（qe_sat_tactic.cpp至少是这么说的）。

我想知道

1. 如果公式是多线性的，它是否仍然有效，因为“常数”是象征性的。例如∀x, ax≤b ⇒ ax≤0可以通过分离a<0、a=0和a>0的情况来处理。这可以使用 Weispfenning 的虚拟替换方法，但我不知道最终在 Z3 中实现了什么（也就是说，它是实现通用方法还是仅限于常数系数的方法）。

2. 是否有可能在 Z3 中输出消除结果，而不仅仅是求解一个模型。这样做可能有 Z3 策略，但我不知道应该如何请求。

3. 是否有可能在 Z3 中进行上述消除，然后使用新的非线性求解器来获得模型。同样，一连串的策略可能会奏效，但我不知道应该如何请求。

谢谢。

我一直在使用 (ML) z3 绑定和 API 函数

多年来一直忠实地服务。我现在正在尝试切换到 SMTLIB2 界面，但我发现distinct命令是unsupported. 例如，查询：

产生响应：

在网络演示上。有一些解决方法吗？

谢谢！

兰吉特。

我正在尝试使用 SMTLIB 接口为 Z3 定义集合理论（并集、交集等）。不幸的是，我当前的定义将 z3 挂起以进行微不足道的查询，所以我想我缺少一些简单的选项/标志。

这是永久链接： http ://rise4fun.com/Z3/JomY

关于我缺少什么的任何提示？

此外，据我所知，集合操作没有标准的 SMT-LIB2 编码，例如Z3.mk_set_{add,del,empty,...} （这就是我试图通过量词获得该功能的原因。）对吗？还是有其他路线？

谢谢！

兰吉特。

我打算做的是去所有的向量，并在每一位上做不同的事情。

我想知道的是我是否表现良好（in define-fun LT....）？

因为结果与预期不符：S

此链接中的代码：http ://rise4fun.com/Z3/xrFK

我正在使用 WordPunct Tokenizer 来标记这句话：

في_بيتنا كل شي لما تحتاجه يضيع ...ادور على شاحن فجأة يختفي ..لدرجة فسي ادور شيء

我的代码是：

我注意到打印输出与输入语句相同，那么为什么要使用分词器呢？此外，使用令牌文件或普通文本文件创建机器翻译系统 (MOSES) 会有什么不同吗？

我在 Z3 中得到以下统计数据。

我想知道每个结果行使用的指标。

你能帮助我吗？

如何使用 Z3 的 Python API 执行量词消除？尽管我检查了教程和 API，但无法做到。

我有一个具有存在量词的公式，我希望 Z3 给我一个新公式，这样这个量词就被消除了。我基本上想做与此相同的事情：

如何用 Z3 隐藏变量

但使用 Python 接口。我的公式也是线性算术。

谢谢！

加法：在完成量词消除后，我将“添加”另一个无量词公式。因此，如果我使用策略，有没有办法将子目标（即策略的输出）转换为线性算术表达式？