标签: z3py

我正在尝试将 z3py 集成到我的应用程序中。有涉及小实数的断言，例如

solver.add(x <= 1e-6)

然后我收到以下错误：

File "~/src/solver/z3.py", line 2001, in __le__
  a, b = _coerce_exprs(self, other)
File "~/src/solver/z3.py", line 846, in _coerce_exprs
  b = s.cast(b)
File "~/src/solver/z3.py", line 1742, in cast
  return RealVal(val, self.ctx)
File "~/src/solver/z3.py", line 2526, in RealVal
  return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx)
File "~/src/solver/z3core.py", line 1774, in Z3_mk_numeral
  raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err))
src.solver.z3types.Z3Exception: 'parser error'

虽然断言

solver.add(x <= 1e-4)

似乎没问题。

因此，我猜测 z3 中存在某种精度限制。如果是这样，是否可以选择让第一个断言通过？

谢谢。

如何使用 Z3 的 Python API 执行量词消除？虽然我检查了教程和 API，但无法做到。

我有一个公式，它有一个存在量词，我希望 Z3 给我一个新公式，这样这个量词就被消除了。我基本上想做与此相同的事情：

如何使用 Z3 隐藏变量

但使用 Python 接口。我的公式也是线性算术。

谢谢！

添加：在进行量词消除后，我将用另一个“添加”无量词公式。因此，如果我使用 Tactic，是否可以将子目标（即策略的输出）转换为线性算术表达式？

我正在使用Z3的python api来做一些增量求解.我迭代地将约束推送到求解器,同时使用solver.push()命令检查每个步骤的不可满足性.我想了解Z3是否会使用先前约束的学习引理或者在使用新添加的约束求解时先前获得的满意解.我从不使用solver.pop()命令.在哪里可以获得有关如何使用先前迭代中完成的工作的更多详细信息？

任何人都可以告诉我如何通过Z3py实现最小化整数问题,如下所示？我如何定义所有声明？这里所有变量都是int sort.

Z3中是否有专门的求解器可以解决这类问题？如果有,那么我该如何设置该求解器的配置？

谢谢

z3 的 C API 具有 Z3_mk_bvadd_no_overflow 等函数，但这些函数似乎无法从 Python API 中获得。在我开始破解这个问题之前，我只想验证一下情况是否如此，并请求将这些添加到正式版本中。

我正在尝试将类似的内容添加到 z3.py 中，但到目前为止尚未设法获得正确的详细信息。关于我哪里出错的建议将不胜感激。我正在 contrib 分支工作。

def Bvadd_no_overflow(a, b, si, ctx=None):
    """Create a Z3 bvadd_no_overflow expression.

    """
    ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
    # argh can't hard-code the 32
    s = BitVecSort(32,ctx)
    a = s.cast(a)
    b = s.cast(b)
    # this function requires a bool as the last argument but is it a python bool, a
    # z3 bool, or what?
    return BitVecRef(Z3_mk_bvadd_no_overflow(ctx.ref(), a.as_ast(), b.as_ast(), 1), ctx) 

下面的Python代码段说明了Z3的存储性能行为。在不push()调用的情况下，z3会在0.1秒内检查公式。有了push()（并且没有额外的断言），z3需要0.8s。即使在交换s.append(f)和之后也会发生类似的结果s.push()。

import time
import z3
f = z3.parse_smt2_file("smt-lib/QF_BV/RWS/Example_1.txt.smt2")
s = z3.Solver()
s.append(f)
t1 = time.time()
s.check()  # 0.10693597793579102 seconds
print(time.time() - t1)

s = z3.Solver()
t1 = time.time()
s.append(f)
s.push()
s.check()  # 0.830916166305542 seconds
print(time.time() - t1)

知道为什么会出现这种减速吗？而且，如何解决？

我正在使用z3-4.3.2.bb56885147e4-x64-osx-10.9.2。

我是 z3py 和 SMT 的新手，我还没有找到关于 z3py 的好的教程。

这是我的问题设置：

给定输入整数数组 I=[1,2,3,4,5]，输出整数数组 O=[1,2,4,5]。

我想推断运算符Delete的k，它删除数组中位置k处的元素，其中

Delete(I,O) = \xc2\xa0(ForAll 0<=x<k, O[x] = I[x] ) and (ForAll k<=x<length(I)-1, O[x] = I[x+1]) is true\n

我应该使用 Array 或 IntVector，还是其他任何东西来表示输入/输出数组？

编辑：

我的代码如下：

from z3 import *\n\nk=Int('k')\ns=Solver()\n\nx = Int('x')\ny = Int('y')\n\ns.add(k >= 0)\ns.add(k < 4)    \ns.add(x >= 0)\ns.add(x < k)\ns.add(y >= k)\ns.add(y < 4)\n\nI = Array('I',IntSort(),IntSort())\nO = Array('O',IntSort(),IntSort())\nStore(I, 0, 1)\nStore(I, 1, 2)\nStore(I, 2, 3)\nStore(I, 3, 4)\nStore(I, 4, 5)\n\nStore(O, 0, 1)\nStore(O, 1, …

我正在尝试使用Python中的Z3 Thoerem Prover解决一个方程式。但是我得到的解决方案是错误的。

from z3 import *    
solv = Solver()
x = Int("x")
y = Int("y")
z = Int("z")
s = Solver()
s.add(x/(y+z)+y/(x+z)+z/(x+y)==10, x>0, y>0, z>0)
s.add()
print(s.check())
print(s.model())

我得到这个解决方案：

[z = 60, y = 5, x = 1]

但是，当您将这些值填写到给定的方程式中时，结果为：10.09735182849937。但是我想找到的是一个精确的解决方案。我究竟做错了什么？

谢谢你的帮助 ：）

我正在尝试使用 z3py 作为优化求解器来最大化从一张纸上切下的长方体的体积。python API 提供了 Optimize() 对象，但使用它似乎不可靠，给我的解决方案显然不准确。

我尝试使用h = opt.maximisefollow byopt.upper(h)以及简单地检查模型，以及在将长方体添加到模型之前v = w*b*l和之后定义长方体的体积，以及将目标设置为w*b*l而不是v。他们都没有给我任何类似好的解决方案。

from z3 import *
l = Real("l")
w = Real("w")
b = Real("b")
v = Real("v")
opt = Optimize()
width = 63.6
height = 51

opt.add(b+l <= width)
opt.add(w+b+w+l+w <= height)
opt.add(w > 0)
opt.add(b > 0)
opt.add(l > 0)
opt.add(v == w*b*l)
opt.maximize(w * b * l)
# h = opt.maximize(v)


print(opt.check())
# print(opt.upper(h))
print(opt.model())

输出： …

有没有办法对 a 中的元素进行索引BitVec？我想要这样的事情：

s = Solver()
x = BitVec('x', 8)
s.add(Not(And(x[0], x[2])))

或者屏蔽是隔离位的唯一方法：

s.add(x & 5 != 5)