model - z3 を使用してリテラルに新しい値を割り当てる方法

Question

これらx - y < 2 x - y > 2x > 3のように 4 つの式の集合があります。y < 4最初の式を消去すると、 のモデルx=4 y=-1が見つかります。z3(api) を使用して最初の数式で x と y を 4 と -1 に置き換えるにはどうすればよいですか? どうもありがとうございました。

Answer 1

Z3_substituteAPIを使用できます。Z3 Python を使用した例を次に示します。Python を使用しているのは、より便利で、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]))