Z3 如何检查模型是否满足新的断言/约束

Question

我正在使用 z3py 进行编码。请参阅以下示例。

from z3 import *

x = Int('x')
y = Int('y')

s = Solver()

s.add(x+y>3)

if s.check()==sat:
    m = s.model()
    # how to check whether model m satisfies x+y<5 ?
    print(m)

Answer 1

您可以评估模型中的表达式:

from z3 import *

x = Int('x')
y = Int('y')

s = Solver()

s.add(x+y>3)

if s.check()==sat:
    m = s.model()
    print(m)
    print(m.evaluate(x+y<5))

这打印:

[x = 4, y = 0]
True