评价一个Z3表达

Question

我在Z3py，比方说一个约束，

z3.Real('x')<=3 

是否有评估约束简单，内置的方式，为“真”或潜在的模型“假”？例如，使用z3.Real('x')->2评估约束条件应该给出“true”。

Answer 1

您可以评估Solver.check返回sat时可以提取的模型下的表达式（使用Solver.model（）检索模型），也可以将自己的模型表示为替换（当模型仅提及常量），然后使用“替代”方法将模型中的值替换为表达式，然后使用“简化”来评估结果表达式。