问题标签 [z3py]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
z3 - Z3 Python 中无法满足的核心
我正在使用 Z3 的 Python API，试图在我正在编写的研究工具中包含对它的支持。我有一个关于使用 Python 接口提取无法满足的核心的问题。
我有以下简单的查询：
通过 z3 可执行文件（对于Z3 4.1）运行此查询，我收到了预期的结果：
对于Z3 4.3，我得到一个分段错误：
这不是主要问题，尽管这是一个有趣的观察。然后我将查询（在文件内）修改为
使用文件处理程序，我将此文件的内容（在变量 `queryStr' 中）传递给以下 Python 代码：
我从“unsat_core”函数收到空列表：[]。我是否错误地使用了此功能？该函数的文档字符串表明我应该改为做类似的事情
但是，我想知道是否仍然可以按原样使用查询，因为它符合 SMT-LIB v2.0 标准（我相信），以及我是否遗漏了一些明显的东西。
z3 - 在 Z3 Python 中使用量词消除
g = And(ForAll([i, j, k], Implies(And(k <= 0, A * i + B * j + C * k + D <= 0), k + i - j <= 0)),Not(And(A==0,B==0,C==0))) 我尝试使用找到满足公式的 A、B、C、D 的值solve(g) 。这有很多可能的解决方案，一个是A=1,B=-1,C=D=0但 Z3 似乎无法做到这一点（solve(g)不会终止）。
Z3 可以做这种非线性（但简单）的公式吗？也许我可以为此指定一些量化宽松策略或其他东西？
z3 - Z3Py 不能做出一定的证明？
我试图证明
4*n^3*m+4*n*m^3 <= n^4+6*n^2*m^2+m^4
为所有n，m实数；在线使用 Z3Py。
我正在使用代码：
输出是： unknown。
请你告诉为什么Z3没有获得 "sat"。
z3 - MacOSX 上的 z3py：无法获取模型
我在 Mac 上看到 z3py 的一个奇怪问题，想知道是否有人以前见过这个：
模型中缺少 x 的值。我尝试了主分支和不稳定分支，结果相同。但是，如果在类似的 .smt2 文件上运行，z3 本身确实会给出正确的模型。我的配置是 Mac OSX 10.6.8，Python 2.7.4。
z3 - 有没有办法在 Z3 中获取默认上下文？
我正在使用 z3py API (4.3.0)。我可以轻松地将表达式expr从默认上下文转换为新上下文target_ctx，使用expr.translate(target_ctx). 但是如何从给定的上下文ctx转换为默认的 Z3 上下文？有没有办法Context从 Python API 获取默认值？
z3 - Z3py 中的数组和数据类型
我实际上使用 Z3py 来调度解决问题，并且我试图代表一个 2 处理器系统，其中必须完成 4 个不同执行时间的进程。
我的实际数据是： 进程 1：到达 0 和执行时间 4 进程 2：到达 1 和执行时间 3 进程 3：到达 3 和执行时间 5 进程 4：到达 1 和执行时间 2
我实际上是在尝试表示每个进程，同时在相同时间的子进程中分解每个进程，所以我的数据类型是这样的：
其中 pn 和 pt 是进程名称和进程的一部分（进程 1 分为 4 个部分，...）
但是现在我不知道如何代表我的处理器来添加我需要的 3 条规则：唯一性（每个子进程必须由 1 个处理器完成 1 次，并且只有 1 次）检查到达（进程的第一部分不能在到达之前处理）和顺序（流程的每个部分都必须在先例之后处理）所以我正在考虑使用数组来表示我的 2 个处理器与这种声明：
但是当我尝试执行它时，我收到一条错误消息：
并且知道我不知道如何处理它......我必须创建一个新的数据类型并想办法添加我的规则吗？或者有没有办法将数据类型添加到数组中，让我创建这样的规则：
提前致谢
z3 - Translating from Z3Py to SMT-LIB
Please let me know how to translate the following line from Z3Py to SMT-LIB:
Many thanks
int - Z3Py Bool 变量在模型中转换为 Int
我正在使用用于 Z3 的 python API 为我的研究构建一个工具。我遇到以下问题：我正在使用 Python 脚本生成一组 Z3 约束。由于集合可能不一致，我正在使用 assert_and_check 跟踪每个公式。例如，
当然，occWrites 被声明为布尔值：
但是，在模型中，Z3 将 occWrites 报告为整数。为什么会这样？模型中occWrites的值不应该是True还是False？
z3 - 在某些条件下证明 2 个公式等价？
两个公式a1 == a + b和a1 == b等价 if a == 0。我想a == 0用 Z3 python 找到这个必需的条件（）。我写了下面的代码：
但是，上面的代码总是"Not Equ"作为输出返回。那么显然我也无法将模型 ( a === 0) 作为"f"和"g"等价的条件。
关于代码哪里出错以及如何修复它的任何想法？非常感谢！
z3 - 找到两个公式相等的逻辑条件？
我发布了一个相关的问题，但后来我认为它不是很清楚。我想改写这样的问题：
如果 ，则两个公式a1 == a + b(1) 和a1 == b(2) 等价a == 0。给定这些公式 (1) 和 (2)，我如何使用 Z3 python 找出这个所需的条件 ( a == 0)，以便上述公式变得等价？
我想a1,a并且b都是BitVecs(32).
编辑：我想出了这样的代码：
输出是：a = 0，正如预期的那样。
但是，当我稍微修改代码以使用两个公式时，它不再起作用：
现在的输出不同了：a = 1314914305
所以问题是：
（1）为什么第二个代码会产生不同（错误）的结果？
(2) 有没有办法在不使用 ForAll （或量词）的情况下做到这一点？
谢谢