在 Z3 中评估分配的变量和子句？答案

【问题标题】：Evaluating assigned variables and clauses in Z3?在 Z3 中评估分配的变量和子句？
【发布时间】：2022-08-08 10:49:45
【问题描述】：

我是 z3 的新手，所以这可能真的很容易。

我有一些变量和子句：

d = {
    \"p0\":  Bool(\"p0\"),
    \"p1\":  Bool(\"p1\"),
    \"p2\":  Bool(\"p2\"),
    \"p3\":  Bool(\"p3\")
}

d[\'p4\'] = And([d[\"p0\"], Or([d[\"p1\"],d[\"p2\"]])])
d[\'p5\'] = d[\'p4\']
d[\'p6\'] = And([d[\"p3\"], d[\'p5\']])
d[\'p7\'] = And([d[\'p2\'],d[\'p3\']])

我可以获得满意的模型

s = Solver()
s.add(d[\'p6\'])
s.check()
sol = s.model()
sol ---> [p3 = True, p1 = True, p0 = True, p2 = False]

什么是实现函数f(sol,d) 的最佳和最有效的方法，该函数返回一个eval_dict，这样

eval_dict = f(sol,d)
eval_dict --->  {
    \'p0\': True,
    \'p1\': True,
    \'p2\': False,
    \'p3\': True,
    \'p4\': True,
    \'p5\': True,
    \'p6\': True,
    \'p7\': False
}

标签： python z3 smt z3py

【解决方案1】：

以下功能应该做：

def modelDict(sol, d):
    return {k: sol.evaluate(v, model_completion=True) for k, v in d.items()}

与您的程序一起使用时，它会打印：

>>> print(modelDict(sol, d))
{'p0': True, 'p1': True, 'p2': False, 'p3': True, 'p4': True, 'p5': True, 'p6': True, 'p7': False}

【讨论】：