问题标签 [smt]

我正在使用 Z3 的 ELIM_QUANTIFIERS 功能从位向量的公式中消除量词。我遇到了以下情况，Z3 产生了正确但过于复杂的结果，我想知道是否存在重写我的问题的方法，或者是否有配置选项会导致我期望的简单结果。

首先，这是一个按预期工作的示例。它指出，对于长度为 4 的位向量，存在一个与其相等的位向量。

Z3 为本示例生成以下输出。

但是，如果我添加一个否定：

然后 Z3 产生以下输出，其中列出了向量的所有可能值，而不是只返回“true”。

对于较长的位向量，例如大小为 32 或更大，Z3 不会在合理的时间内产生结果，因为它可能会枚举 32 位变量的所有可能值。

请注意，在这种特殊情况下，我可以只使用 check-sat 来检查公式的有效性；但是，在一般情况下，我有兴趣获得与原始公式等效的无量词表达式，而不仅仅是检查其有效性。

我正在为 Linux 使用 Z3 v3.2。

在调试 UNSAT 查询时，我注意到查询状态有一个有趣的差异。查询结构为：

查询中没有pop调用。触发此行为的查询在此处。

想法为什么？

注意：我实际上并不需要增量，它仅用于调试目的。Z3版本是3.2。

我正在使用 Microsoft 的 Z3 对动态观察进行一些简单的分析。作为其中的一部分，如果我可以将一些公式从使用一组变量转换为另一组目标变量，那将会很有帮助。

我对 Z3 真的很陌生，但我知道它有一些内部简化规则和其他转换公式的方法......基本上，我想知道是否可以进行一些转换，例如：

我认识到这并不是 Z3 的真正主要目标，但我知道它已经有一些简化/解决的能力......从帮助文本来看，我的印象是有一些方法可以设计目标状态和策略到达他们，但我真的无法根据 Z3 的(help)命令找到有关如何做到这一点的信息（除非我遗漏了一些东西......）。

我真的不想做任何复杂的事情——只是简单地替换/消除不在目标集中的符号......我想知道是否有某种方法可以诱使该工具执行此操作？

有没有办法让 z3 求解器发出“符号”解决方案？例如，对于方程：

1+x=c

解是 x=c-1，但 z3 总是发出一个特定的模型，比如[c = 0, x = -1]. 如何将 c“定义”为符号变量？

如何以 SMT-LIB2 格式输出使用 z3py 所做的断言？我在文档中找不到任何提及。我找到了一个标志Z3_PRINT_SMTLIB_FULL，但我不知道如何设置它。

我正在通过 IDLE GUI 在 Windows XP 上使用 Python 2.7.3，并且我正在尝试通过 Python API 在本地运行 Z3 4.0。

这条线工作正常：

此行没有：

任何人都知道问题可能是什么？

我的 PYTHONPATH 设置为“C:\Program Files\Microsoft Research\Z3-4.0\python”，不带引号。

解决优化问题的一种方法是使用 SMT 求解器来询问是否存在（坏）解决方案，然后逐步添加更严格的成本约束，直到该命题不再可满足。例如，http: //www.lsi.upc.edu/~oliveras/espai/papers/sat06.pdf和http://isi.uni-bremen.de/agra/doc/konf/讨论了这种方法08_isvlsi_optprob.pdf。

但是，这种方法有效吗？即，求解器在尝试使用附加约束求解时是否会重用来自先前解决方案的信息？

Traditionally most work with computational logic was either propositional, in which case you used a SAT (boolean satisfiability) solver, or first-order, in which case you used a first-order theorem prover.

In recent years, a lot of progress has been made on SMT (satisfiability modulo theory) solvers, which basically augment propositional logic with theories of arithmetic etc.; John Rushby of SRI International goes so far as to call them a disruptive technology.

What are the most important practical examples of problems that can be handled in first-order logic but still can't be handled by SMT? Most particularly, what sort of problems arise that can't be handled by SMT in the domain of software verification?

说给定一个公式

(t1>=2 或 t2>=3) 和 (t3>=1)

我希望得到它的析取范式 (t1>=2 and t3>=1) or (t2>=3 and t3>=1)

如何在 Z3 中实现这一点？

说我有

是否可以隐藏变量 x 以便 t1<t2 在 Z3 中？