时间戳

首页 > 解决方案 > 如何在 Z3 中使用替代方法将变量替换为 True 它不起作用，它替换为 ζ1 并且简化方法不起作用？

z3 - 如何在 Z3 中使用替代方法将变量替换为 True 它不起作用，它替换为 ζ1 并且简化方法不起作用？

问题描述

这是下面的代码。我也尝试将其转换为 Bool 和 BoolRef 但在这里它也不起作用：-

print(A)
substitute(A, (Var[0], Bool(True) )) # where Var[0] = x_0_2

Output:-
And(And(And(And(x_0_3, Not(x_0_2)), Not(x_0_1)), Not(x_0_0)),
And(And(And(x_1_3 == x_0_0, x_1_2 == x_0_3),
        x_1_1 == x_0_2),
    x_1_0 == x_0_1))
    x_0_3 ∧ ¬ζ1 ∧ ¬x_0_1 ∧ ¬x_0_0 ∧ x_1_3 = x_0_0 ∧ x_1_2 = x_0_3 ∧ x_1_1 = ζ1 ∧ x_1_0 = x_0_1

标签： z3z3py

解决方案

如果您发布人们可以自己运行的代码，则 Stack-overflow 效果最好；没有看到你正在做的其他部分，其他人不可能弄清楚还有什么可能导致你的代码出现问题。

话虽如此，以下是您如何替换True变量：

from z3 import *

x, y = Bools('x y')
expr = And(x, Or(y, And(x, y)))
print expr
expr2 = substitute(expr, (x, BoolVal(True)))
print expr2
print simplify(expr2)

当我运行它时，我得到：

And(x, Or(y, And(x, y)))
And(True, Or(y, And(True, y)))
y

这显示了替换的效果和表达式的进一步简化。请注意使用该术语BoolVal(True)来访问True作为布尔表达式的常量值。

推荐阅读