Add binary operator to z3-CodePudding

I'm trying to parse and translate a string to its equivalent z3 form.

import z3

expr = 'x   y = 10'

p = my_parse_expr_to_z3(expr)  # results in: ([x, ' ', y], '==', [10]) 
p = my_flatten(p)              # after flatten: [x, ' ', y, '==', 10]

Type-checking of parsed string:

for e in p:    
    print(type(e), e)   

# -->
      <class 'z3.z3.ArithRef'>   x
      <class 'str'>                  
      <class 'z3.z3.ArithRef'>   y
      <class 'str'>              ==
      <class 'int'>              10

When I now try:

s = z3.Solver()
s.add(*p)

I get:

Traceback (most recent call last):
  File "<input>", line 1, in <module>
  File "...\venv\lib\site-packages\z3\z3.py", line 6938, in add
    self.assert_exprs(*args)
  File "..\venv\lib\site-packages\z3\z3.py", line 6926, in assert_exprs
    arg = s.cast(arg)
  File "..\venv\lib\site-packages\z3\z3.py", line 1505, in cast
    _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
  File "..\venv\lib\site-packages\z3\z3.py", line 112, in _z3_assert
    raise Z3Exception(msg)
z3.z3types.Z3Exception: Value cannot be converted into a Z3 Boolean value

The equal and plus signs occurs to be of the false type/usage? How can I translate that correctly?

CodePudding user response：

Where's the definition of parse_expr_to_z3 coming from? It's definitely not something that comes with z3 itself, so you must be getting it from some other third-party, or perhaps you wrote it yourself. Without knowing how it's defined, it's impossible for anyone on stack-overflow to give you any guidance.

In any case, as you suspected its results are not something you can feed back to z3. It fails precisely because what you can add to the solver must be constraints, i.e., expressions of type Bool in z3. Clearly, none of those constituents have that type.

So, long story short, this parse_expr_to_z3 doesn't seem to be designed to do what you intended. Contact its developer for further details on what the intended use case is.

If you're trying to load assertions from a string to z3, then you can do that using the so called SMTLib format. Something like:

from z3 import *

expr = """
(declare-const x Int)
(declare-const y Int)
(assert (= (  x y) 10))
"""

p = parse_smt2_string(expr)

s = Solver()
s.add(p)
print(s.check())
print(s.model())

This prints:

sat
[y = 0, x = 10]

You can find more about SMTLib syntax in https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf

Note that trying to do this using any other syntax (like your proposed 'x y = 10') is going to require knowledge of the variables in the string (x and y in this case, but can of course be arbitrary), and what sort of symbols ( and = in your case, but again can be any number of different symbols) and their precise meanings. Without knowing your exact needs, it's hard to opine, but using anything other than the existing support for SMTLib syntax itself will require a non-insignificant amount of work.