CODEWITHSUNDEEP
z3z3py
John Smith
John Smith

Reputation: 781

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

Using the following code:

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

I get the following error:

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

When only using z3.Solver() without giving a new z3.Context as Parameter the code is working.

Can someone please answer the following questions:

Upvotes: 1

Views: 1688

Answers (1)

GeekInDisguise
GeekInDisguise

Reputation: 1567

Solution: SolverFor()

To set a logic with Z3Py, instead of creating a solver using the Solver() function constructor, you can use the SolverFor(logic) function, where logic is the logic you would like to use.

For example, if you type:

s = SolverFor("LIA")

then the variable s would contain a solver based on Linear Integer Arithmetics, or if you type

s = SolverFor("LRA")

then the variable s would contain a solver based on Linear Real Arithmetics.

Beware that, so far (but I haven't used z3 for a while, then the updated versions may have fixed this) if you specify a non-existing/unsupported logic, for example typing SolverFor("abc"), then no error would be generated and the logic would be guessed automatically as usual.

Because of the issue above, the only ways to test whether the logic you want is actually being used would be to compare the performances with respect to an automatically chosen logic, or to try solving something which is not supported by the logic you specified (for example, using real variables when you specified LIA which only accepts integer varaibales) to see if an error is generated. If yes, then the solver is actually trying to use that logic.

Upvotes: 3

Related Questions