CODEWITHSUNDEEP
z3
user2203454
user2203454

Reputation: 13

Simplifying non-boolean expressions in Z3 assuming a set of axioms

Is there a way to simplify non-boolean expressions in Z3 assuming a set of axioms?

For example, I would like to assert that "a==b", and then simplify the expression "If(a == b, 1, 2)" to get "1".

In particular, I'm interested in working with array theory:

I = BitVecSort(32)
A = Array('A', I, I)
a = BitVec('a',32)
b = BitVec('b',32)
c = BitVec('c',32)
...
A2 = Store(A, a, 1) 
A3 = Store(A2, b, 2) 
A4 = Store(A3, c, 3)

simplify_assuming(A4[a], Distinct(a, b, c))

This should return "1", since the Select expression can be simplified to "1" assuming all the indexes are distinct, according to the array theory rules.

I've tried to use the "ctx-solver-simplify" tactic, but it seems to only work for boolean expressions. Is there some other way to simplify non-boolean expressions, or somehow tell the array rewriter that the indexes are distinct?

Thanks.

Upvotes: 1

Views: 909

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

As Nikolaj described in the comment above, ctx-solver-simplify will not walk under non-Boolean expressions. Another option is to use the tactic solve-eqs that will use asserted equalities to rewrite the rest of the formula. For example, given the equality a == b, Z3 will replace every occurrence of b with a (or vice-versa). After that, if(a == b, 1, 2) will be rewritten to 1.

However, solve-eqs will not use disequalities such as Distinct(a, b, c). Another option is to use the tactic propagate-values. It replaces every occurrence of an assertion P with true. Similarly, if we have an assertion not P, it will replace every other occurrence of P with false. This tactic is essentially performing unit Boolean propagation. Moreover, it is meant to be fast, and will not apply any form of theory reasoning. Example, if we have Distinct(a, b, c), it will not replace a == b with false. So, this approach may be too fragile for your purposes. Here is a script that uses it. It is also available online here. In this script, I wrap the expression A4[a] using a fresh predicate P because a Z3 Goal is a set of Boolean formulas. I use blast_distinct to convert the Distinct into a sequence of disequalities, and expand_select_store to expand a term of the form store(A, i, v)[j] into an if-then-else of the form if(i == j, v, A[j]). Note that, the result contains P(1) that indicates that P(A4[a]) was simplified to 1.

I = BitVecSort(32)
A = Array('A', I, I)
a = BitVec('a',32)
b = BitVec('b',32)
c = BitVec('c',32)
A2 = Store(A, a, 1) 
A3 = Store(A2, b, 2) 
A4 = Store(A3, c, 3)

P = Function('P', I, BoolSort())
G = Goal()
G.add(P(A4[a]))
G.add(Distinct(c, b, a))

T = Then(With("simplify", blast_distinct=True, expand_select_store=True), "propagate-values")
print(T(G))

Upvotes: 1

Related Questions