标签: z3py

在Z3Py中,如何检查给定约束的方程是否只有一个解？

如果有多个解决方案,我该如何枚举它们？

如何从Z3模型中获取真正的python值？

例如

p = Bool('p')
x = Real('x')
s = Solver()
s.add(Or(x < 5, x > 10), Or(p, x**2 == 2), Not(p))
s.check()
print s.model()[x]
print s.model()[p]

版画

-1.4142135623?
False

但那些是Z3对象而不是python float/bool对象.

我知道我可以使用is_true/ 检查布尔值is_false,但是如何优雅地将ints/reals/...转换回可用值(例如,不通过字符串并删除这个额外的?符号).

我正在使用Python绑定Z3定理证明器(Z3Py).我有N个布尔变量,x1,..,xN.我想表达一个约束条件,即N中的N个应该是真的.我怎么能在Z3Py中做到这一点？有没有内置的支持？我检查了在线文档,但Z3Py文档没有提及任何API.

对于N个中的一个约束,我知道我可以单独表达至少一个是真的(断言Or(x1,..,xN))并且最多只有一个为真(断言Not(And(xi,xj) ))所有i,j).我也知道其他方法来手动表达N-out和N-K-out-of-N约束.但是我的印象是,当解算器内置支持此约束时,它有时比手动表达它更有效.

我正在研究一个Python项目,我正在尝试以一些可怕的方式加快速度:我设置了Z3求解器,然后我分叉了这个过程,让Z3在子进程中执行求解并传递一个将模型的可挑剔表示返回到父级.

这很好用,代表了我正在尝试做的第一阶段:父进程现在不再受CPU约束.下一步是多线程父线程,以便我们可以并行解决多个Z3求解器.

我很确定在设置阶段我已经互斥了Z3的任何并发访问,并且任何时候只有一个线程应该触摸Z3.然而,尽管如此,我在libz3.so中得到随机段错误.在这一点上,重要的是要注意,它并不总是触及Z3 的相同线程 - 同一个对象(不是解算器本身,而是表达式)可能在不同的时间由不同的线程处理.

我的问题是,是否有可能多线程Z3？这里有一个简短的说明(http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html)说"从多个线程访问Z3对象是不安全的".我想我会回答我的问题,但我希望这意味着说不应该同时从多个线程访问Z3 .另一个资源(再次:在Windows上安装Z3 + Python)从莱昂纳多自己说,"Z3使用线程本地存储",我猜,这将沉没整个事业,但是a)答案是从2012年开始,所以也许是事情已经改变了,并且b)也许它使用线程本地存储来处理一些不相关的东西？

无论如何,多线程Z3是否可能(来自Python)？我不想将设置阶段推进子进程......

有等式Pell x*x - 193 * y*y = 1

在z3py:

x = BitVec('x',64)
y = BitVec('y',64)
solve(x*x - 193 * y*y == 1, x > 0, y > 0)

结果: [y = 2744248620923429728, x = 8169167793018974721]

为什么？

PS有效答案:[y = 448036604040,x = 6224323426849]

在Z3Py中,我有一个公式.如何在公式中检索变量列表？

谢谢.

我是Z3的新手,我正在查看在线python教程.

然后我想我可以检查BitVecs中的溢出行为.

我写了这段代码:

x = BitVec('x', 3)
y = Int('y')

solve(BV2Int(x) == y, Not(BV2Int(x + 1) == (y + 1)))

我期待[y = 7,x = 7](即当值相等但后继不是因为x + 1将为0而y + 1将为8)

但Z3回答[y = 0,x = 0].

我究竟做错了什么？

在之前的文章中,使用Z3Py在线解决了涉及运算放大器的一些问题.但是现在Z3Py在线无法使用我试图在线使用Z3 SMT-LIB来解决这些问题.

例1:

在以下电路中找到R的值

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

(declare-const R Real)
(declare-const V1 Real)
(declare-const V2 Real)
(declare-const Vo Real)
(declare-const I1 Real)
(declare-const I2 Real)
(declare-const g Real)
(assert (= (/ V1 (+ R -50)) I1))
(assert (= (/ V2 (+ R  10)) I2))
(assert (= (* (* R (+ I1 I2)) -1) g))
(assert (= Vo g))
(assert (= Vo -2))
(assert (= V1 1))
(assert (= V2 0.5))
(assert (> R 0))
(assert (> R 50))
(check-sat)
(get-model) …

我正在使用Z3解决八皇后难题。我知道在这个问题上每个女王可以用一个整数表示。但是，当我用两个整数表示皇后时，如下所示：

from z3 import *

X = [[Int("x_%s_%s" % (i+1, j+1)) for j in range(8)] for i in range(8) ]

cells_c = [Or(X[i][j] == 0, X[i][j] == 1) for i in range(8) for j in range(8) ]

rows_c = [Sum(X[i]) == 1 for i in range(8)]

cols_c = [Sum([X[i][j] for i in range(8)]) == 1 for j in range(8) ]

diagonals_c = [Implies(And(X[i][j] == 1, X[k][h] == 1), abs(k - i) != abs(j - h))
           for i in range(8) for …

我无法让任何 z3py 示例正常工作。我能够使用 github 上的自述文件中的说明成功安装它。我成功更新了 python 路径以指向适当的目录。此外，我能够成功导入 z3，但每次声明变量时都会出现错误。编译器无法识别 Int、Ints、Real 和 RealVal。

我举了一个例子来说明。

代码：

from z3 import *
x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)

错误：回溯（最近一次调用）：文件“test.py”，第 3 行，在 x = Int('x') 中 NameError: 名称 'Int' 未定义

我真的很感激任何帮助。太感谢了。