Z3Py 中的最大值模型不正确
我想找到一个最大区间，其中表达式 e 对所有 x 都为真.编写这样一个公式的方法应该是: Exists d : ForAll x in (-d,d) .e 和 ForAll x 不在 (-d,d) 中.!e. 要得到这样的 d，Z3 中的公式 f(看上面的那个)可能如下: from __future__ 导入师从 z3 导入 *x = Real('x')delta = Real('d')s
..
z3py相关内容
z3、z3py:是否可以从本质上减少Function的搜索空间?
我正在推断一个 Function(var1) 并且我只关心这个函数的值，当 0 (我猜)限制函数搜索空间的一种常见方法是像(在 z3py 中)断言约束一样: for i in range(11):solver.add(And(Function(i)>=0,Function(i) 我的问题是:有没有更好的方法来限制函数的搜索空间?像设置这个函数的上界/下界一样吗? 我的直觉是:由于我对这
..
可以从 Z3 得到最终的 CNF 公式吗?
这是我的简单编码.我想得到呈现所有这些约束的最终布尔 CNF.Z3求解器中是否有任何选项可以获得最终的布尔CNF? x = Int('x')y = Int('y')c1 = And(x >= 1, x 谢谢&问候 解决方案 正如 Ayrat 所说，使用目标和策略.这是一个例子:http://rise4fun.com/Z3Py/4I3 x = Int('x')y = Int('y')
..
Z3 python 对待 x**2 与 x*x 不同?
Z3 Python 接口似乎不喜欢 ** 运算符，它可以处理 x*x 但不能处理 x**2，如下例所示 >>>x,y = x,y=Reals('x y')>>>z3.prove(暗示(x -6 == 0,x**2 -36 == 0))未能证明[x = 6]>>>z3.prove(暗示(x -6 == 0,x*x -36 == 0))证实 解决方案 您可能在 Linux 或 OSX 上使用
..
如何解决 Z3 中的最小化约束?
谁能告诉我如何通过 Z3py 实现像下面这样的最小化整数问题?我如何定义所有语句?这里所有的变量都是 int 排序的. Z3 中是否有专门的求解器可以解决此类问题?如果有，那么我如何为该求解器设置配置? 谢谢 解决方案 以下是一些相关/类似的问题和答案: 变量的最小值和最大值 确定上/下任意命题公式中变量的界限 如何优化Z3中的一段代码?(PI_NON_NES
..
多线程Z3?
我正在处理一个 Python 项目，我目前正在尝试以一些可怕的方式加快速度:我设置了 Z3 求解器，然后我分叉了进程，并让 Z3 在子进程中执行求解并将模型的可腌制表示传回父级. 这很好用，代表了我正在尝试做的第一阶段:父进程现在不再受 CPU 限制.下一步是对父级进行多线程处理，以便我们可以并行求解多个 Z3 求解器. 我很确定我已经在设置阶段互斥了 Z3 的任何并发访问，并且在任何
..
Z3Py 中的模型计数
我正在尝试计算 Z3 的令人满意的分配数量.我想知道Z3是否提供了这样的信息.如果是这样，我如何计算 Z3 中的模型，尤其是 Z3Py 中的模型? 解决方案 虽然 Taylor 的回答会给出令人满意的作业数量，但它会遍历所有作业.原则上，没有如此昂贵的迭代是可以做到的，但 Z3 没有提供. 命题逻辑有高效的模型计数器，与SAT中使用的语言相同(搜索sharpSAT以找到这样的系统)，
..
为什么此代码返回 Unsat(使用 ForAll & Implies 的公式)?
给定2个方程c == a + 4和t == c + b，如果a == -4，则t == b.我正在尝试做相反的事情，这意味着 给定以上 2 个等式和 t == b，我尝试找到 a 的值. 我有以下代码可以使用 ForAll 和 Implies: from z3 import *a, b, c, t = BitVecs('a b c t', 32)g = 真g = And(g, c == (
..
Z3 中的地板和天花板功能实现
我尝试实现以下链接中定义的地板和天花板功能 https://math.stackexchange.com/questions/3619044/floor-or-ceiling-function-encoding-in-first-order-logic/3619320#3619320 但 Z3 查询返回反例. 地板功能 _X=Real('_X')_Y=Int('_Y')_W=I
..
使用 SMT-LIB 使用公式计算模块数量
我不确定使用 SMT-LIB 是否可行，如果不可能，是否存在可以做到的替代求解器? 考虑方程 a 和 a >5 b 和 b >0 b 使用a、b 和c 整数 a 和 b 的值，其中存在最大模型数，满足 a=9 和 b 时的方程=1. SMT-LIB 是否支持以下内容:对于 a 和 b 的每个值，计算满足公式的模型数量并给出 a 的值 和 b 使计数最大化. 解决
..
Z3py:打印包含 144 个变量的大型公式
我使用 Z3 定理证明器，并且我有一个很大的公式(114 个变量).我可以打印一个包含所有子句的大公式吗?普通的print str(f)会截断输出，最后只打印“..."，而不是所有子句. 我测试了 print f.sexpr() 并且这总是打印所有子句.但是仅在 sexpr 语法中. 我可以打印公式的所有子句但避免使用 s 表达式语法吗? 注意:代码示例很少能说明问题，但发布一个
..
从 z3py 获取证据
我一直在浏览 Z3Py 的文档，对于我这样的人，我无法弄清楚如何从求解器中获得证明(例如，如果我从德摩根定律的一个实例开始，我如何提取来自实例的 Z3Py 的证明，一步一步).我看到的唯一参考是 proof(self) 在 Solver 类中，如果启用了证明构造，它应该会获得上次检查的证明，但我一直在找回非常模糊的错误: 回溯(最近一次调用最后一次): 中的文件“example.py"，第 36
..
有没有办法在 Z3 中获取默认上下文?
我使用的是 z3py API (4.3.0).我可以使用 expr.translate(target_ctx) 轻松地将表达式 expr 从默认上下文转换为新上下文 target_ctx.但是如何从给定的上下文 ctx 转换为默认的 Z3 上下文?有没有办法从 Python API 中获取默认的 Context? 解决方案 可以通过main_ctx()访问. 以下是描述 main_c
..
证明 2 个公式在某些条件下等价?
如果a == 0，两个公式a1 == a + b 和a1 == b 是等价的.我想用 Z3 python 找到这个必需的条件(a == 0).我写了下面的代码: from z3 import *定义等价(F，G):s = 求解器()s.add(Not(F == G))r = s.check()如果 r == 未满足:打印 'Equ'打印 s.model()别的:打印 'Not Equ'a, b
..
如何在 Z3Py 中循环遍历数组
作为逆向工程练习的一部分，我正在尝试编写一个 Z3 求解器来查找满足以下程序的用户名和密码.这个特别难，因为大家参考的z3py教程(rise4fun)下线了. #include #include 使用命名空间标准；int main() {字符串名称，通过；cout>经过;整数总和 = 0;for (size_t i = 0;
..
z3:解决八皇后难题
我正在使用 Z3 来解决八皇后难题.我知道在这个问题中每个皇后都可以用一个整数表示.但是，当我用两个整数表示一个女王时，如下所示: from z3 import *X = [[Int("x_%s_%s" % (i+1, j+1)) for j in range(8)] for i in range(8)]cell_c = [Or(X[i][j] == 0, X[i][j] == 1) for i
..
Z3py 使用 pow() 函数返回未知方程
Z3py 使用 pow() 函数返回以下简单问题的未知数. import z3;目标 = z3.Goal();目标 = z3.Then('purify-arith','nlsat');求解器 = 目标.solver();x = z3.Real('x');solver.add(x 返回 未知 显然 x = 0, z = 1 是一个令人满意的解决方案.任何关于改变方程构建方式或修改策略的建议
..
我在哪里可以获得 z3py 教程
由于一些安全问题，rise4fun z3py 将在几周内不可用.我试图找出一些学习 z3py 的资源，但徒劳无功.请推荐一些学习z3py的资源 解决方案 我使用 Z3Py 教程源创建了一个 zip 文件.它基本上是几个 HTML 页面和一堆 python 文件.这是链接: https://github.com/leodemoura/leodemoura.github.com/blob/m
..
Z3/Python 从模型中获取 python 值
如何从 Z3 模型中获取真正的 Python 值? 例如 p = Bool('p')x = Real('x')s = 求解器()s.add(Or(x 10), Or(p, x**2 == 2), Not(p))s.check()打印 s.model()[x]打印 s.model()[p] 打印 -1.4142135623?错误的 但那些是 Z3 对象而不是 python float
..
Gecode branch() 函数的 z3 替代方案?
在像 Gecode 这样的约束求解器中，我们可以借助分支函数来控制搜索空间的探索.例如branch(home , x , INT_VAL_MIN ) 这将从变量 x 在其域中的最小可能值开始探索搜索空间并尝试找到解决方案.(有很多这样的替代方案.) 对于 z3，我们有这种内置的灵活性吗??任何可能的替代方案?? 解决方案 SMT 求解器通常不允许给出此类“提示"，它们更像是黑匣子.
..