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 设置逻辑，而不是使用 Solver() 函数构造函数创建求解器，您可以使用 SolverFor(logic) 函数，其中 logic 是您想要的逻辑使用。

例如，如果您键入：

s = SolverFor("LIA")

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

s = SolverFor("LRA")

那么变量 s 将包含一个基于线性实数算术的求解器。

请注意，到目前为止（但我有一段时间没有使用 z3，然后更新的版本可能已经解决了这个问题）如果您指定 non-existing/unsupported 逻辑，例如输入 SolverFor("abc") ，那么就不会产生错误，并且会像往常一样自动猜测逻辑。

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

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

z3py: How do I set the used logic in z3py?

z3

z3py