问题标签 [smt]

我正在从事一个项目，其重点是使用术语重写来解决/简化固定大小的位向量算术问题，这对于一些决策过程（例如基于位爆破的决策过程）的前一步很有用。重写这个术语可能完全解决问题，或者产生一个更简单的等效问题，因此两者的结合可以带来相当大的加速。

我知道许多 SMT 求解器都实施了这种策略（例如 Boolector、Beaver、Alt-Ergo 或 Z3），但很难找到详细描述这些重写步骤的论文/技术报告/等。一般来说，我只找到作者在几段中描述这种简化步骤的论文。我想找到一些详细解释术语重写使用的文档：提供规则示例，讨论 AC 重写和/或其他等式公理的便利性，重写策略的使用等。

目前，我刚刚找到了技术报告A Decision Procedure for Fixed-Width Bit-Vectors，它描述了 CVC Lite 执行的规范化/简化步骤，我想找到更多这样的技术报告！我还找到了一张关于STP 中术语重写的海报，但这只是一个简短的总结。

我已经访问了那些 SMT 求解器的网站，并在他们的出版物页面中进行了搜索...

我将不胜感激任何参考或任何解释如何在当前版本的知名 SMT 求解器中使用术语重写。我对 Z3 特别感兴趣，因为它看起来拥有最智能的简化阶段之一。例如，Z3 3.* 引入了一个新的位向量决策过程，但不幸的是，我找不到任何描述它的论文。

如何使用 smt-lib2 获得公式的最大值？

我想要这样的东西：

当然，'max' 对 smtlibv2 来说是未知的。那么，如何做到这一点呢？

在 Z3 中表达枚举类型之间的子类型关系的最佳方式是什么？

具体来说，我想做以下事情：

然后创建一个新的子类型：

因此，有 4 个不同类型的 Animal 常量的断言是 SAT，但断言有 4 个不同类型的 Mammal 常量是 UNSAT。

如何计算属性值？这是一个例子：

有了这个我会得到2个模型：

现在，我想要的是这样的：

所以，我想得到属性总和大于6的模型：

也许使用数组是实现这一目标的一种方法......

我猜这主要是一个逻辑问题......

我使用这个 smtlib 公式：

这是这种结构的一个术语（至少在我看来）：

我的猜测：结果集看起来像这样：

但它使用 scala^z3 ctx.checkAndGetAllModels()：

为什么里面有ad和abcd？是否有可能只得到我期望的结果？

我有一个很大的布尔公式要解决，由于编辑的原因，我必须在此处粘贴图像：

另外，我已经有一个函数area来测量 4 个整数的维度：area(c,d,e,f)=|c−d|×|e−f|

我想做的不仅仅是弄清楚公式是否可以满足：我正在寻找一个最佳的 6 元组(a,b,c,d,e,f)，它可以构成大公式TRUE，并且area(c,d,e,f)大于或等于任何其他也满足公式的 6 元组的维度。

换句话说，找到Max(area(c,d,e,f))大公式的主题。

我想知道 SMT 求解器是否可以帮助解决这个问题。我知道Z3支持quantifiers，并且能够说布尔表达式是否可以满足。但问题是是否Z3可以帮助找到函数的最佳解决方案area。

有谁有想法吗？任何关于 SMT 求解器、Z3 或其他算法的评论将不胜感激......

我有一个代码z3，旨在解决布尔公式的优化问题

我猜是因为量词和含义，这段代码成本很高。当我在线测试时，它给了我2个警告，最终结果是unknown：

谁能告诉我这两个警告是否会避免获得良好的结果？有什么办法可以优化这段代码使其运行吗？

我有以下代码

代码应该在第一个（check-sat）返回 unsat 并在第二个（check-sat）返回，但我不知道。

有人可以告诉我有什么问题。我正在使用 Windows 7，使用 cygwin 的 jSMTLIB

谢谢赛义夫

在使用 SMTLIB 数组时，我注意到 Z3 对理论的理解与我的不同。我使用的是 SMTLIB 数组理论 [0]，可以在官方网站 [1] 上找到。

我认为我的问题最好用一个简单的例子来说明。

第一个数组应在索引 1 处返回 2，对所有其他索引返回 0，第二个数组应在索引 0 处返回 1，在索引 1 处返回 2，对所有其他索引返回 0。在索引 0 处调用select似乎证实了这一点：

Z3sat为两者返回。

正如预期的那样，Z3（如果重要的话，我在 linux-amd64 上使用 3.2 版）unsat在这种情况下回答。接下来，让我们比较这两个数组：

Z3 告诉我sat，我将其解释为“这两个数组比较相等”。但是，我希望这些数组不会比较相等。我基于 SMTLIB 阵列理论，它说：

因此，用简单的英语来说，这意味着“两个数组应该比较相等，当且仅当它们对于所有索引都相等”。有人可以向我解释一下吗？我是否遗漏了什么或误解了理论？如果您对这个问题有任何想法，我将不胜感激。

最好的问候，莱昂

[0] http://goedel.cs.uiowa.edu/smtlib/theories/ArraysEx.smt2 [1] http://smtlib.org

我想在 SMT 2.0 中定义一个函数，它返回 4 个整数值中的最小值。