CODEWITHSUNDEEP
setz3smt
Kun
Kun

Reputation: 101

How to prove two relations equal in Z3 using HORN logic

I'm using Horn Logic in Z3 to model check CSP (Process Algebra), because Horn Logic is good at dealing with recursive definitions. But, I was stuck in some trick problems. For example, I have the following code:

(declare-rel A (Int))
(declare-rel B (Int))

(rule (A 1))
(rule (A 2))

(rule (B 1))
(rule (B 2))

Then, how can I prove A and B are equal. This is similar to proving the equivalence of two sets in Z3 using Horn Logic.

Please, anyone can give me a clue? Many thanks.

Upvotes: 1

Views: 197

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

There is an engine that supports stratified negation. It works for finite domains only. Using stratified negation you can check equivalence. For example:

(declare-rel A ((_ BitVec 8)))
(declare-rel B ((_ BitVec 8)))
(declare-rel q ())

(rule (A #x01))
(rule (A #x02))

(rule (B #x01))
(rule (B #x02))

(declare-var x (_ BitVec 8))

(rule (=> (and (A x) (not (B x))) q))
(rule (=> (and (B x) (not (A x))) q))

(query q)

Upvotes: 0

Related Questions