如何使用z3將新值賦給文字

Question

有一組這樣的4個公式x - y < 2x - y > 2 x> 3 y < 4。當第一個公式被刪除時，可以找到x=4 y=-1的模型。如何使用z3（api）在第一個公式上用4和-1替換x和y？非常感謝你。

Answer 1

您可以使用Z3_substitute API。這裏是一個使用Z3 Python的例子。我使用Python，因爲它是更方便，we can test it online using rise4fun。我們可以使用Z3 C/C++，.Net或Java API編寫相同的示例。

x, y = Ints('x y') 

s = Solver() 
s.add(x - y > 2, x > 3, y < 4) 
print s.check() 
m = s.model() 
print m 
# We can retrieve the value assigned to x by using m[x]. 
# The api has a function called substitute that replaces (and simplifies) 
# an expression using a substitution. 
# The substitution is a sequence of pairs of the form (f, t). 
# That is, Z3 will replace f with the term t. 

F1 = x - y < 2 

# Let us use substitute to replace x with 10 
print substitute(F1, (x, IntVal(10))) 

# Now, let us replace x and y with values assigned by the model m. 
print substitute(F1, (x, m[x]), (y, m[y]))