z3py：如何在z3py中设置使用的逻辑？

使用下面的代码：z3py：如何在z3py中设置使用的逻辑？

import z3 

solver = z3.Solver(ctx=z3.Context()) 
#solver = z3.Solver() 

Direction = z3.Datatype('Direction') 
Direction.declare('up') 
Direction.declare('down') 
Direction = Direction.create() 

Cell = z3.Datatype('Cell') 
Cell.declare('cons', ('front', Direction), ('back', z3.IntSort())) 
Cell = Cell.create() 

mycell = z3.Const("mycell", Cell) 

solver.add(Cell.cons(Direction.up, 10) == Cell.cons(Direction.up, 10))

我得到以下错误：当只有使用z3.Solver()没有给出一个新的z3.Context作为参数的代码工作

Traceback (most recent call last): 
    File "thedt2opttest.py", line 17, in <module> 
    solver.add(Cell.cons(Direction.up, 10) == Cell.cons(Direction.up, 10)) 
    File "/home/john/tools/z3-master/build/python/z3/z3.py", line 6052, in add 
    self.assert_exprs(*args) 
    File "/home/john/tools/z3-master/build/python/z3/z3.py", line 6040, in assert_exprs 
    arg = s.cast(arg) 
    File "/home/john/tools/z3-master/build/python/z3/z3.py", line 1304, in cast 
    _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value") 
    File "/home/john/tools/z3-master/build/python/z3/z3.py", line 90, in _z3_assert 
    raise Z3Exception(msg) 
z3types.Z3Exception: Value cannot be converted into a Z3 Boolean value

。

可有人请回答下列问题：

是这里有什么区别？
如何在z3py中设置逻辑？
我应该使用哪种逻辑与数据类型？

来源

2017-04-27 John Smith

解决方案：SolverFor()

要设置与Z3Py逻辑，而不是使用Solver()函数构造函数创建解算器，你可以使用SolverFor(logic)函数，其中logic是你想用逻辑。

例如，如果键入：

s = SolverFor("LIA")

那么变量s将包含基于线性整数运算在求解器，或如果键入

s = SolverFor("LRA")

则变量s将包含基于线性实数算术的求解器。

如果你指定一个不存在/不支持的逻辑，例如输入SolverFor("abc")，那么请注意，到目前为止（但我还没有使用z3一段时间，然后更新后的版本可能已经修复了这个问题）被生成并且逻辑会像往常一样自动被猜测。

由于上述问题，测试您想要的逻辑是否真正被使用的唯一方法是将性能与自动选择的逻辑进行比较，或尝试解决某些逻辑不支持的问题您指定（例如，当您指定只接受整数varaibales的LIA时使用实变量）以查看是否生成错误。如果是的话，那么求解器实际上就是试图使用那个逻辑。

来源

2017-05-12 08:57:55

z3py：如何在z3py中设置使用的逻辑？

回答

相关问题