问题标签 [smt]

我阅读了有关 SAT 和 SMT 的信息。我一直想知道如何将它应用到实际的编程场景中。

这是一个例子：

鉴于这var a = 20; var b = a;是真的，我们想知道b = 20是真的还是假的。

我应该如何将其转换为布尔代数表达式并应用 SAT？

Z3 中是否有办法证明/显示给定模型是唯一的并且不存在其他解决方案？

一个小例子来演示

我知道以下模型是独一无二的，但我可以使用一些 Z3 选项或添加断言来确保这一点吗？

为了澄清起见，我通过 de JAVA API 使用 Z3

(get-assignment) 命令应该返回一个符号列表以及它们的真/假值，如果它们是布尔类型的话。据我了解，这只能在 :produce-assignments 设置为 true 并且 (check-sat) 返回 sat 时完成。但是，当我在 Z3 上运行一个小脚本来测试它时， (get-assignment) 只返回 () - 空白。这是我的脚本：

我有一个关于 Z3 如何逐步解决问题的问题。在这里阅读了一些答案后，我发现了以下内容：

1. 使用Z3进行增量求解有两种方式：一种是push/pop(stack)模式，另一种是使用假设。Z3 中的软/硬约束。
2. 在堆栈模式下，即使在一次局部“弹出”之后，z3 也会忘记全局（对吗？ ）范围内的所有学习引理SMT 求解器中约束加强的效率
3. 在假设模式下（我不知道名字，这是我想到的名字），z3 不会​​简化一些公式，例如值传播。z3 行为根据 unsat 核心的请求而改变

我做了一些比较（欢迎您询问公式，它们太大而无法放在rise4fun上），但这是我的观察：在一些公式上，包括量词，假设模式更快。在一些具有大量布尔变量（假设变量）的公式中，堆栈模式比假设模式更快。

它们是为特定目的而实施的吗？增量求解如何在 Z3 中工作？

我将集合编码为关系，并将集合上的操作编码为普遍量化的含义。我有一个集合上的选择运算符，它通过选择满足一元谓词 p 的元素（例如：v<4、v>4、..）来生成新集合。由于这个运算符，我的公式中有简单的算术谓词。下面给出了这种公式的示例 Z3 编码 -

正如预期的那样，Z3 为上述公式返回 UNSAT。但是，我的问题是——

1. 鉴于我可以用 prenex 范式编写我的公式，它还在 EPR 类中吗？
2. 这样的公式是可判定的吗？z3 是此类公式的决策程序吗？我应该如何约束我的谓词以使公式是可判定的？

更新 - 上述一组公式可以表示为关系代数中的联合查询，但不等式。

我需要使用 jSMTLIB 作为 API。

但我找不到任何可以帮助我的教程。

我唯一找到的是不完整的用户指南。（http://www.grammatech.com/resource/smt/jSMTLIBUserGuide.pdf）

任何人都知道在java中创建一个求解器并运行一些断言？

可以给我看一个它是如何工作的例子吗？

谢谢。

我有以下代码： (declare-const L4 (_ BitVec 6)) (declare-const L1 (_ BitVec 6)) (declare-const L0 (_ BitVec 6)) (declare-const l2 (_ BitVec 6) ))

当我运行此代码时，我得到的模型是： sat (model (define-fun min!0 () (_ BitVec 6) #b000011) (define-fun L1 () (_ BitVec 6) #b001000) (define-fun L0 () (_BitVec 6) #b000100) (define-fun L4 () (_BitVec 6) #b000100) (define-fun l2 () (_BitVec 6) #b001000) ) unsat

为什么结果min是：

而不是 b001000，因为 L1 的最小值是这个而不是 b000011。

有人可以解释一下吗？

最后，我定义了函数 Lt_l 来检查 S x < l 中的所有 x 是否存在，但现在我想做 GT_l 来检查 S l < x 中的所有 x 是否存在。我有以下代码：

但这不起作用为什么？

谢谢

我知道有几部作品试图处理 SMT 中的理论组合。但是，SMT-Lib 2.0 语言 ( http://smtlib.cs.uiowa.edu/docs.html ) 没有说明这一点。我的问题是它是否支持这一点，以及什么 Solvers 提供了同时处理多种理论的能力？

谢谢，

以下 SMT-LIB 代码在 Z3、MathSat 和 CVC4 中运行没有问题，但在 Alt-Ergo 中没有运行，请告诉我发生了什么，非常感谢：

使用最新版本的 IZ3 并运行 cpp_example 时出现段错误。

重现：

• 克隆 z3：git clone https://git01.codeplex.com/z3
• 切换到分支interp：git checkout interp
• 按照中的构建说明构建README
• 此外，构建cpp_example：cd build ; make cpp_example
• 跑过cpp_example

• 结果：

  /li>

如果cpp_example我建立在master.

我在 2012 年 12 月的某个邮件列表上阅读了一条消息，指出 Z3 的插值版本无法针对最新版本的 Z3 构建，但这是一项正在进行的工作。

IZ3 仍然不能与 Z3 版本 4 一起使用吗？

如果是，是否有关于如何针对早期版本的 Z3 构建插值源的说明？（开头：从哪里获得IZ3-3.2的源代码或其他什么？）

• 编辑：
• 操作系统：Linux __ 2.6.37.6-24-desktop #1 SMP PREEMPT __ i686 i686 i386 GNU/Linux

• 克++：

  /li>