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

Question

使用以下代码：

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))

我得到以下错误：

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

当只使用z3.Solver()而没有给出新的z3.Context作为参数时，代码就可以工作了。

请有人回答以下问题：

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

Answer 1

SolverFor() 解决方案：

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

例如，如果您键入：

s = SolverFor("LIA")

然后变量s将包含一个基于线性整数算法的求解器，或者如果您键入

s = SolverFor("LRA")

然后变量s将包含一个基于线性实算法的求解器。

请注意，到目前为止(但是我已经有一段时间没有使用z3了，那么更新的版本可能已经修复了这个问题)，如果您指定了一个不存在/不受支持的逻辑，例如键入SolverFor("abc")，那么就不会产生错误，并且逻辑将像往常一样自动地被猜测。

由于上面的问题，测试您希望实际使用的逻辑的唯一方法是比较与自动选择的逻辑相关的性能，或者尝试解决一些您指定的逻辑不支持的事情(例如，在指定只接受整数变量的LIA时使用实变量)，以查看是否生成了错误。如果是的话，那么求解者实际上是在尝试使用这种逻辑。