Search code examples
z3z3py

How to use substitute method in Z3 to replace a variable to True its not working and it replaces with ζ1 and also simplify method doesn't work?

This is the following code . I also tried to convert it into Bool and BoolRef but here also it didn't work:-

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
Solution

  • Stack-overflow works the best if you post code that people can run on their own; without seeing other parts of what you are doing it's impossible for other people to figure out what else might cause issues in your code.

    Having said that, here's how you'd substitute True for a variable:

    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)

    When I run this, I get:

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

    which shows the effect of the substitution and the further simplification of the expression. Note the use of the term BoolVal(True) to get access to the constant value True as a boolean expression.