问题标签 [z3]

我发现了一个问题，如下面的简单 SMT-LIB 程序所示。

SMT-LIB 代码：

这给出了以下警告：

我想知道警告信息。我知道我错过了一些东西，但我无法理解。任何人都可以在这个问题上帮助我吗？

嗨，我是 Z3 SMT 求解器的新手。我知道您可以使用相关 API 以编程方式调用 Z3。但我想用 Z3 SMT 求解器做以下事情：

1. 如何以编程方式为 Z3 提供一个输入文件？
2. 我怎样才能逐步获得解决方案？

例如：

最后，如何让Z3解完公式后将结果保存到一个输出文件中？

我可以查看任何想法或文件吗？

谢谢百万！！！

我正在使用 Z3-3.2 的 c-api（在 linux 上）来解决 QF_AUFBV 问题。

如果公式可以满足，我想从模型中读出自由数组变量的值。

我尝试了以下代码的一些内容，我想知道如何做到这一点的总体思路是否正确：

输入 Z3_ast 数组绝对是一个自由数组表达式。Z3_eval 返回 true，因此我们似乎已经成功评估了表达式，但随后 Z3_is_array_value 返回 false。我本来希望数组表达式上成功的 Z3_eval 的结果是数组值，那么为什么不是这样呢？

顺便说一句：我们通过遍历所有 model_func_decls 并尝试通过比较它们的 get_symbol_string 来尝试为该数组找到正确的信息，从而获得了所需的信息。所以这些信息似乎在 Z3 的某个地方可用，但这算不上一个好的解决方案。

感谢您对此的任何帮助。

最好的问候，弗洛里安

嗨 Leonardo：看起来 z3 (v3.2) 接受命令行开关“-T:10”来指定 Mac 和 Linux 上的超时，但忽略它。（还没有在 Windows 上尝试过。）如果 linux/mac 版本也支持超时，那就太好了。

（这是我第二次尝试寻求帮助。如果问题/方法没有意义或不清楚，请告诉我。我也会对任何小的提示或参考感到高兴，这可以帮助我理解Z3 和我的 SBA）

我正在使用 UFBV Z3 逻辑对关系规范进行有界验证。我正在调查的当前问题需要伪造所有可能的模型（因为对可达性谓词的否定使用），这会在更高的范围内扼杀求解器的性能。

因为只有一部分可能的模型确实很有趣（与其他模型不同构），所以我试图引入对称破坏技术（在 SAT 领域已知）。

然而，在某些情况下使用我所说的对称破坏公理可以提高 Z3 的性能，但求解器的一般行为变得不稳定。

我的一种方法（我认为最有前途的一种）基于打破其领域关系的对称性。它引入了关系 R 的每个域 D 和每个原子 a \in D 公理，它们对 R^{M} 和 R^{M[a+1/a]} 的二进制表示强制执行顺序，其中 M 是规范的模型。对于齐次关系，公理是放松的。

让 R \subset AxA 成为一个关系。我对 R 的宽松对称破缺公理如下所示：

我的问题是，使用此 SBA 的效果并不稳定/一致。它不同于从绑定到绑定和从形式规范到另一个。此外，使用所有或仅使用一个 SBA 会影响性能。

在 SAT 上下文中，所谓的对称破坏谓词 (SBP) 方法的成功基于 SAT 求解器的回溯能力，这（以某种方式）保证，如果求解器回溯，它将使用以下方法修剪搜索空间，其中包括 SBP。

• 在 Z3 的背景下有什么区别（如果有的话）？
• 如何强制使用这些公理来修剪搜索空间（当它回溯时）？
• 对我的 SBA 使用（量词）模式会有帮助吗？

问候，

Aboubakr Achraf El Ghazi

我是使用 Z3 的新手。但我想了解，在输入到Z3的以下程序中超时的原因：

我的另一个问题是，forall 3.2 版有什么新东西吗？我必须在 (x Int) 周围加上额外的括号，否则会引发错误。

谢谢。

基本上，我想要求 Z3 给我一个值大于 10 的任意整数。所以我写了以下语句：

如何将此量词应用于我的模型？我知道你可以写 (assert (> x 10)) 来实现这一点。但我的意思是我的模型中需要一个量词，所以每次我声明一个整数常量，其值保证超过 10。所以我不必为我的每个整数常量插入语句 (assert (> x 10))宣布。

我正在对 x86 指令进行符号解释。例如，对于 cmp 指令，比较的符号以及操作数是否相等都存储在 eflags 寄存器的两位中。

这是我的代码：

问题是我在 z3 API 中找不到将（假定的）布尔排序（在我的示例中为 ZF）转换为位向量（任意长度）的函数。

我曾考虑在 ZF 上创建一个带有 ite 语句的函数，该语句将返回一个位向量，但我想知道这样做的传统方式。

谢谢，

海吉。

如何创建包含一组其他对象的数据类型。基本上，我正在执行以下代码：

但是 Z3 告诉我 A 和 B 的未知排序。如果我删除“设置”，它就像指南所说的那样工作。我试图改用 List 但它不起作用。任何人都知道如何使它工作？

在 TPTP 文件上使用 Z3 时（例如http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Problems&Domain=SYN&File=SYN054+1.p）有没有办法找出哪些公理被用来证明猜想？或者，Z3 可以生成 TPTP 证明吗？

干杯