CODEWITHSUNDEEP
z3py
trshmanx
trshmanx

Reputation: 680

Can we evaluate z3py expressions from a string?

I could not find anything on the subject in the docs. I tried like : s.add("Or(a==1, a==2, a==3), Or(b==1, b==2, b==3), Or(c==1, c==2, c==3)"), but that is not working. Is it possible?

In sympy we can do this with sympify or parse_expr

Edit:

I see I can use just pythons eval. It also has parse_smt2_string(), but no reference how SMT2 works.

Upvotes: 0

Views: 174

Answers (1)

alias
alias

Reputation: 30525

eval is the way to go. There's no support in z3py in any way to parse what's essentially a Python program. Note that for that to work, you should somehow have the variables a/b and c in the environment, either by explicit declaration or by eval'ing their declarations from a string like "a, b, c = Ints('a b c')"

Regarding your comment "No reference how SMT2 works:" SMTLib is the standard format accepted by all SMT-solvers, including z3. See here: http://smtlib.cs.uiowa.edu/

Upvotes: 1

Related Questions