问题标签 [z3py]

谁能告诉我如何实现最小化整数问题，如下面的 Z3py？如何为所有语句定义？这里所有的变量都是 int 排序的。

Z3 中是否有专门的求解器可用于解决此类问题？如果有的话，那么我该如何为该求解器设置配置？

谢谢

我正在使用 z3py API 来计算一组归纳注释。我将我的约束映射到广义 Horn 子句的结合。在这些约束中，有几个关系（l6 和 iwc1）需要推断。涉及的变量（incr1、t1 和 wc1）都是整数。我希望推断的谓词是区间关系。谓词 l6(incr, t1) 应该捕捉到 incr = 0 和 t1 >= 0 的事实。我将其构建为以下规则：

推断谓词 l6 是：

同样，iwc1 是一个涉及变量 wc1 的谓词，它试图捕捉wc1 == incr + t1incr 和 t1 的值被 l6 过度逼近的事实。换句话说，

由于wc1 == incr + t1和 l6 推断 incr = 0 和 t1>=0，我预计 iwc1 为 wc1>=0。相反，推断的谓词是True。为什么 iwc1 变得如此弱？

此在线 z3py 代码中提供了完整的程序。

相反，如果我将 iwc1 的规则修改如下：

然后，我收到以下错误：

iwc1 规则已更改的程序可在此处获得。Z3Py 抱怨变量 incr 没有界限。我在哪里犯错？

当我尝试将定点引擎设置为 PDR 并尝试设置 pdr_use_farkas 选项时，我收到了 unknown_parameter 错误。

特别是，我在定点对象上使用以下选项：

这会导致错误：

使用 set_option 也无济于事。我试过了

我得到“未知选项”。

我在哪里犯错？

我正在使用 Z3 4.3.1 64 位。

我想将此 z3py 代码（在线代码）转换为标准 SMTLib 格式。除了设置选项属性 " (set-option :produce-models true) (set-option :timeout 4000)"之外，所有内容都转换为 SMTLib 格式。为什么不工作？转换代码由 Leonardo de Moura 提出。

我希望输出像 -

谢谢

我创建了大约 20k 个约束，在我的机器上解决它们大约需要 3 分钟。我有不同类型的约束，下面我给出例子并解释它们。我将断言上传到http://filebin.ca/vKcV1gvuGG3。

我对解决更大的约束系统很感兴趣，因此我想加快这个过程。我想问一下您是否有关于如何更快地解决它们的建议，例如通过使用适当的策略。从关于策略的教程中，我知道了策略，但我似乎没有通过应用策略获得积极的差异......

li是树的标签。第一种类型对标签的值进行了限制。标签值通常介于 10-20 个不同的值之间。

第二种类型将不同的标签相互关联。

第 3 种类型定义和关联函数f: Int --> Int（或f: BitVector --> BitVector，不完整），其中bound_{s, v}只是函数名称，n是节点的 ID。目标是找到令人满意的功能分配bound。

最后一种类型确定是否需要边界 ( >= 0) 或不需要 ( == -1, )

还有一个要求，对于某些初始状态，边界是必需的：

可执行文件的描述：在前 2-3 行中，脚本启动求解器，导入 z3 并在最后一行调用print s.check()

我必须使用 Z3 和 python 检索函数的 codomain。那可能吗？具体来说，我可能有一个表达式，如：f(var) = (var + 1) << 1，我想找出表达式可能假设的值的范围。有任何想法吗？

我必须使用 z3py 获得函数最大值的值（在它们的范围内）。例如：我有foo(x,y) = 2*x + 1 + y一个函数[x,y]（换句话说，我必须解决一个范围内的最大问题，这可能吗？lo <= foo(x,y) <= hifoo(x,y)

我在 python 中编写了这个简单的脚本：

如果我只使用一个变量（例如，foo(x) = 2*x + 1），那么给定的模型是正确的，并且 的值foo(x)是最高的。如果我使用多个变量（例如foo(x,y) = 2*x+y），则找到的结果是最小值。

范围内的所有点都在函数的域中。

编辑：显然，如果我删除关于 X 和 Y 的两个约束，我会得到最大值。

在之前的一篇文章中，使用 Z3Py 在线解决了一些涉及运算放大器的问题。但是现在 Z3Py online 已停止服务，我正在尝试使用 Z3 SMT-LIB online 解决此类问题。

示例 1：

在以下电路中找到 R 的值

使用以下代码解决此问题：

相应的输出是：

在此处在线运行此示例

如您所见，Z3 的输出是 x 上的二次方程。那么问题是：如何使用 Z3 求解这样的方程？

有没有办法将 SMT2 公式的 (check-sat ...) 语句中的假设传递给求解器？

考虑存储在 ex.smt2 中的以下示例公式：

正如预期的那样，在其上运行 z3 会产生 unsat。现在，我想通过 z3py 接口解决假设（p）：

是否有 API 可以从解析器获取假设（即本例中的 (p)）？或者更好的是，只是告诉求解器使用从输入文件中读取的假设来求解？

链接：
Z3 定理证明者
picosat 与 pyhton 绑定

我使用 Z3 作为 SAT 求解器。对于较大的公式，似乎存在性能问题，这就是为什么我想检查 picosat 看看它是否是一个更快的选择。我现有的 python 代码以 z3 语法生成一个命题公式：

输出/结果

然而，Picosat 使用数字列表/数组，如下例所示（“clauses1”：6 指变量 P，-6 表示“非 P”等）：

您推荐什么作为将表示 CNF 中的公式的 Z3 变量（如代码示例中的变量“f”）转换为上述格式 picosat 用于表示 CNF 中的公式的简单解决方案？我真的尝试使用Z3的python API，但是文档不足以自己解决问题。

（请注意，上面的例子只是说明概念。变量C表示的公式将是动态生成的，并且过于复杂，无法直接被z3高效处理）