Z3 with string expressions
string, z3
Solution
I see the following options:
1) you can implement your own parser, and invoke the Z3 API functions. Pro: you can use your "favorite" language for writing formulas. Con: it is "busy" work.
2) you can use the API `Z3_parse_smtlib2_string`. Con: your formulas must be in SMT 2.0 format. For example, you would have to write `(and (= x y) (not (= x y)))` instead of `(x == y) && !(x == z)`.
3) You can use the Z3 Python API, and parse strings using the `eval` function in Python. Here is an example:
from z3 import *
# Creating x, y
x = Int('x')
y = Int('y')
# Creating the formula using Python
f = And(x == y, Not(x == y))
print f
# Using eval to parse the string.
s = "And(x == y, Not(x == y))"
f2 = eval(s)
print f2
BTW, this script does not work at rise4fun http://rise4fun.com/z3py because the function `eval` is not allowed there, but you can use the script above in your local Z3 installation.
Problem
I'm trying to use Z3 to determine if an expression is satisfiable. I could easily do this by defining the context then the int_const variables and the formula. To evaluate an expression programmatically you would have to write everything in code. Let's say the logical expression is given in the form of a string, what then? For example, "x == y && !x == z" would be expressed in the C API as: ``` context c; expr x = c.int_const("x") //Same for other variables ... formula = (x == y) && (!x == z); solver s(c); s.add(formula); //s.check() ...etc etc ``` Okay, I can write the code for this particular formula, but how could I do that programmatically given a string. I'm open to anything you can think of. Thank you :)