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

【问题标题】：Z3 How to check whether a model satisfies a new assertion/constraintZ3 如何检查模型是否满足新的断言/约束
【发布时间】：2021-05-11 01:50:02
【问题描述】：

我正在使用 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)

【问题讨论】：

标签： z3 z3py

【解决方案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

【讨论】：