Is there an equivalent to define-const in the Z3 Python API? I am trying to rewrite the example below (similar to this example) in Python:
(define-const a String "hello")
(define-const b String "world")
(simplify (= a b))
(check-sat)
(get-model)
whose output is
false
sat
(
(define-fun b () String
"world")
(define-fun a () String
"hello")
)
I tried replacing define-const with a constant declaration followed by an assertion, but the result was not quite the same:
from z3 import *
a = String('a')
b = String('b')
s = Solver()
s.add(a == 'hello')
s.add(b == 'world')
print(simplify(a == b))
print(s.check())
print(s.model())
output:
a == b
sat
[a = "hello", b = "world"]
I also tried using StringVal() but the result was also not the same:
from z3 import *
a = StringVal('hello')
b = StringVal('world')
s = Solver()
s.add(a == 'hello')
s.add(b == 'world')
print(simplify(a == b))
print(s.check())
print(s.model())
output:
False
sat
[]
I have tried searching documentation and elsewhere but was unsuccessful.
This is a bit of a strange thing to do, since define-const is simply a macro. If you're using the Python API, you'd simply use a StringVal. But then, those variables don't show up in the solver, because there's no connection between the Python level object, and what gets asserted in the solver. This is what you are seeing in the last example you tried.
And this is perfectly fine: In SMTLib, constants live together with all the other variables; but in z3py you get two different worlds. A better question to ask is, perhaps, what exactly are you trying to achieve? Trying to simulate SMTLib exactly by the Python interface isn't an explicit goal. In particular, the Python interface allows for easier programming and access to z3 internals that are not available in the SMTLib world. Don't try to equate them!
Having said all this, the most "faithful" way to simulate the SMTLib you have in z3py would be:
from z3 import *
a = StringVal("hello")
b = StringVal("world")
print(simplify(a == b))
s = Solver()
print(s.check())
m = s.model()
print("a =", m.evaluate(a))
print("b =", m.evaluate(b))
This prints:
False
sat
a = "hello"
b = "world"
This matches the output you're expecting, but then again it's not really the best use of the API. Instead of trying to simulate SMTLib exactly, "what problem are you trying to solve" is a better goal to focus on.