CODEWITHSUNDEEP
z3matchingassociativitycommutativity
simon1505475
simon1505475

Reputation: 675

Does Z3 have a feature for facilitating the matching of subformulas in chains of associative / commutative operators?

Let's say I have a user-defined commutative and associative operator op. The code below is invalid because I'm using op with more than two arguments. Let's suppose for a moment that it is valid and that it means "the way op is applied is irrelevant".

(declare-sort T 0)
(declare-fun op (T T) T)
(declare-fun P (T) Bool)
(declare-const a T)
(declare-const b T)
(declare-const c T)
(declare-const d T)
(declare-const k T)
; associativity
(assert (forall ((x T) (y T)) (z T)) 
                (= (op x (op y z)) 
                   (op (op x y) z))))
; commutativity
(assert (forall ((x T) (y T))) 
                (= (op x y) 
                   (op y x))))
; assumption 1
(assert (forall ((x T) (y T)) (= (op x y) k)))
; assumption 2
(assert (P (op a c k)))
; conjecture
(assert (not (P (op a b c d))))

What would be the best way to ensure that assumption 1 be instantiated with x, y := b, d and that assumption 2 become applicable to prove the conjecture?

One solution that I am considering is to generate all possible binary trees that would correspond to (op a b c d). That is pretty expensive however: there are 5 different binary trees with 4 leaves and 24 different permutations of the leaves for a total 120 different binary trees. I can also hold back and hope that z3 uses associativity and commutativity on its own and trigger the right instantiation of assumption 1.

The problem becomes even more hairy if we consider that chains like (op a b c) can appear inside a universal quantification. We could probably use patterns (op a (op b c)), (op b (op a c)), etc to maximize the chances of the quantification being instantiated but the pattern has to emerge somewhere and z3 probably doesn't have the guidance to make it appear on its own.

Is there anything better I could do?

Thanks! Simon

Upvotes: 1

Views: 131

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

Z3 does not have any special support for matching modulo A, C, AC, ACI. For the particular example you give it turns out that assumption 1 is much more important, but that is just an artifact of this particular example.

Upvotes: 1

Related Questions