model - 如何使用 z3 为文字分配新值

Question

有一组 4 个公式，这些x - y < 2 x - y > 2x > 3 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]))