z3py相关内容

如何以 smt2 格式示例获得 z3 求解器的多个解决方案?

如何使用 smt2 格式的 z3 求解器为位向量公式生成多个模型? 在为位向量实现 IDEA 代码时，它生成了一个模型. 如果存在，如何为相同的模型生成所有可能的模型? ex.smt2 文件 (设置逻辑 QF_BV)(设置信息:smt-lib-version 2.0)(declare-const A0 (_ BitVec 16))(declare-const A1 (_ Bit ..
发布时间：2021-10-04 20:33:09 Python

量词中的非零向量

我想验证以下形式的公式: 存在 p .ForAll x != 0 .f(x,p)＞0 一个实现(不起作用)如下: def f0(x0, x1, x, y):返回 x1 ** 2 * y + x0 ** 2 * xs = 求解器()x0, x1 = Reals('x0 x1')p0, p1 = Reals('p0 p1')s.add(存在([p0, p1],ForAll([x0, x1],f0 ..
发布时间：2021-10-04 20:32:37 其他开发

将 SMT 约束与 Z3 一起使用时获取合法范围信息的(次)最佳方法

这个问题与我之前的问题有关 在 Z3 中使用 SMT 约束时是否可以获得合法的范围信息 因此，考虑到典型的 32 位向量等，“有效地"找到最大范围信息似乎是不合适的.但另一方面，我在考虑找到某些“次最大"范围信息是否可行，这有望变得更有效率.另一件事是我们可能希望有一定的“安全"保证，比如对于次最大范围内的所有元素，它们必须满足约束，但可能存在一些其他解决方案满足也有约束. 我目 ..
发布时间：2021-10-04 20:32:32 其他开发

在 Z3Py 中获取布尔表达式的所有解永远不会结束

可能是与 Z3 相关的一个基本问题:我正在尝试获取布尔表达式的所有解决方案，例如对于 a OR b，我想得到 {(true, true),(false,true),(true,false)} 基于发现的其他回复，例如Z3:找到所有满意的模型，我有以下代码: a = Bool('a')b = Bool('b')f1=Or(a,b)s=求解器()s.add(f1)而 s.check() == ..
发布时间：2021-10-04 20:32:15 其他开发

使用布尔运算符在 Z3 中定义约束

比方说，我想将字符串的每个字符限制为字符集:[a-zA-Z0-9_] 使用 Z3 约束，我可以使用布尔运算符来指定吗? 举个例子: input = [BitVec("input%s" % i, 8) for i in range(10)]对于范围内的我(10):s.add(input[i] >= 0x30 and input[i] = 0x4 ..
发布时间：2021-10-04 20:31:45 Python

z3 的可扩展性

我想提高 SMT 求解的可扩展性.我实际上已经实现了增量求解.但我想提高更多.在不了解问题本身的情况下，还有其他一般方法可以改进它吗? 解决方案 没有单一的“技巧"可以让 z3 更好地解决任意问题.这实际上取决于实际问题是什么以及您有什么样的限制.当然，这适用于任何一般计算问题，但它确实适用于 SMT 求解器的上下文. 话虽如此，以下是基于我的经验的一些总体思路，大致按照易用性的顺序 ..
发布时间：2021-10-04 20:31:22 其他开发

如何从 Lambda 表达式中获取值?

我正在 python 中试验 z3.我有以下模型: (set-option :produce-models true)(设置逻辑 QF_AUFBV )(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8) ) )(declare-fun another () (Array (_ BitVec 32) (_ BitVec 8) ) )(assert ..
发布时间：2021-10-04 20:31:11 Python

如何使用 BitVector 建模有符号整数?

假设a是254的8位整数.如果a 是一个有符号整数，它实际上被认为是-2.相反，如果 a 是无符号的，它仍然是 254. 我试图用 Z3 用 BitVector 理论来模拟这个有符号/无符号整数问题，但似乎 BitVector 不允许这样做.这是真的?那么关于如何在 Z3py 中对此建模有什么想法吗? 非常感谢. 解决方案 Z3 具有用于签名和未签名解释的 API.例如，在 C ..
发布时间：2021-10-04 20:30:44 其他开发

Z3 的位向量中所有位的总和

给定 Z3 中的一个位向量，我想知道如何总结这个向量的每个位? 例如， a = BitVecVal(3, 2)sum_all_bit(a) = 2 是否有任何预先实现的 API/函数支持这一点?谢谢！ 解决方案 它不是位向量运算的一部分.您可以按如下方式创建表达式: def sub(b):n = b.size()bits = [ Extract(i, i, b) for i i ..
发布时间：2021-10-04 20:30:36 其他开发

使用 push 命令在 Z3 中增量求解

我正在使用 Z3 的 python api 进行某种增量求解.我使用 solver.push() 命令在每一步检查不满足性的同时，迭代地将约束推送到求解器.我想了解 Z3 是否会使用从先前约束中学习到的引理，或者使用新添加的约束求解时先前获得的令人满意的解决方案.我从不使用 solver.pop() 命令.在哪里可以获得有关如何使用先前迭代中完成的工作的更多详细信息? 解决方案 Z3 有多 ..
发布时间：2021-10-04 20:30:01 其他开发

Z3 生成模型值的随机性

我试图影响 Z3 生成的模型值的结果随机性.据我了解，此选项非常有限:在线性算术的情况下，单纯形求解器不允许仍然满足给定约束的随机结果.但是，有一个选项 smt.arith.random_initial_value(“在基于单纯形的程序中使用随机初始值进行线性算术(默认:false)")，我似乎无法使用: from z3 import *set_option('smt.arith.random_ ..
发布时间：2021-10-04 20:29:46 其他开发

如何按顺序打印 z3 求解器结果 print(s.model())?

假设我有一个包含 10 个变量的列表 v = [Real('v_%s' % (i+1)) for i in range(10)] 我想添加一个像这样的简单约束 s = Solver()对于范围内的我(10):s.add(v[i] == i)如果 s.check() == 坐:打印(s.model()) 所以一个令人满意的模型是v_1 = 0, v_2 = 1 .... v_10 = 9.然 ..
发布时间：2021-10-04 20:29:35 Python

Z3 Python 中无法满足的核心

我正在使用 Z3 的 Python API，试图在我正在编写的研究工具中包含对它的支持.我有一个关于使用 Python 接口提取不可满足的核心的问题. 我有以下简单查询: (set-option :produce-unsat-cores true)(断言(！(不是(=(_ bv0 32)(_ bv0 32))):命名为__constraint0))(检查周六)(获取未饱和核心)(出口) ..
发布时间：2021-10-04 20:29:32 其他开发

需要帮助理解等式

有等式 Pell x*x - 193 * y*y = 1 在 z3py 中: x = BitVec('x',64)y = BitVec('y',64)解决(x*x - 193 * y*y == 1，x > 0，y > 0) 结果:[y = 2744248620923429728, x = 8169167793018974721] 为什么? 附言有效答案:[y = 448036 ..
发布时间：2021-10-04 20:28:49 其他开发

用 Z3 检查溢出

我是 Z3 的新手，我正在查看在线 Python 教程. 然后我想我可以检查 BitVecs 中的溢出行为. 我写了这段代码: x = BitVec('x', 3)y = Int('y')解决(BV2Int(x)== y，不是(BV2Int(x + 1)==(y + 1))) 我期待 [y = 7, x = 7](即当值相等但后继者不相等时，因为 x + 1 将为 0 而 y + ..
发布时间：2021-10-04 20:28:46 其他开发

Z3py:如何从公式中获取变量列表?

在 Z3Py 中，我有一个公式.如何检索公式中使用的变量列表? 谢谢. 解决方案 Vu Nguyen 为 Z3Py 贡献了几个有用的过程.他实现了一个过程 get_vars 来收集使用过的变量列表.可以在此处找到此过程和许多其他过程.他的贡献将在下一个正式版本中提供.这是一个 get_vars 版本，可以在 rise4fun 上在线执行. # 允许将 Z3 AST 存储到 Pyth ..
发布时间：2021-10-04 20:28:29 其他开发

如何一起使用 Z3py 和 Sympy

我正在尝试对矩阵执行一些符号计算(使用符号作为矩阵的条目)，然后我将有许多可能的解决方案.我的目标是根据约束选择解决方案/解决方案. 例如，M是一个矩阵，它有一个元素作为symbol.该矩阵将有 2 个特征值，一个为正，一个为负.使用 z3 我试图仅找出负值，但我无法这样做，因为 a 被定义为一个符号，除非我将其转换为实数，否则我无法将其写为约束. 我该怎么办?有什么方法可以将(符号) ..
发布时间：2021-09-03 20:13:26 Python

如何将 z3py 表达式转换为 smtlib 2 格式

我的问题与:Z3:将 Z3py 表达式转换为 SMT-LIB2? 我正在尝试将 z3py 表达式从 smtlib2 格式转换.使用以下脚本，但转换后，当我将结果提供给 z3 或任何其他 SMT 时，我得到: “语法错误，意外的让" 有什么办法可以用z3py把它导入smtlib2格式，这样我就不用再写长表达式了. 以下是我用于转换的代码: def 转换器(f, status ..
发布时间：2021-06-26 19:51:59 Python

(Z3Py) 检查方程的所有解

在 Z3Py 中，如何检查给定约束的方程是否只有一个解? 如果有多个解决方案，我该如何枚举它们? 解决方案 您可以通过添加阻止 Z3 返回的模型的新约束来实现.例如，假设在 Z3 返回的模型中，我们有 x = 0 和 y = 1.然后，我们可以通过添加约束 Or(x != 0, y != 1) 来阻止这个模型.以下脚本可以解决问题.您可以在线试用:http://rise4fun.co ..
发布时间：2021-06-25 19:47:30 Python