14

I'm trying to define a theory of sets (union, intersection etc.) for Z3 using the SMTLIB interface. Unfortunately, my current definition hangs z3 for a trivial query, so I guess I'm missing some simple option/flags.

here's the permalink: http://rise4fun.com/Z3/JomY

(declare-sort Set)
(declare-fun emp () Set)
(declare-fun add (Set Int) Set)
(declare-fun cup (Set Set) Set)
(declare-fun cap (Set Set) Set)
(declare-fun dif (Set Set) Set)
(declare-fun sub (Set Set) Bool)
(declare-fun mem (Int Set) Bool)
(assert (forall ((x Int)) (not (mem x emp))))
(assert (forall ((x Int) (s1 Set) (s2 Set)) 
            (= (mem x (cup s1 s2)) (or (mem x s1) (mem x s2)))))
(assert (forall ((x Int) (s1 Set) (s2 Set)) 
            (= (mem x (cap s1 s2)) (and (mem x s1) (mem x s2)))))
(assert (forall ((x Int) (s1 Set) (s2 Set)) 
            (= (mem x (dif s1 s2)) (and (mem x s1) (not (mem x s2))))))
(assert (forall ((x Int) (s Set) (y Int)) 
            (= (mem x (add s y)) (or (mem x s) (= x y)))))

(declare-fun z3v8 () Bool)
(assert (not z3v8))
(check-sat)

Any hint as to what I'm missing?

Also, from what I can tell there is no standard SMT-LIB2 encoding of the set operations e.g. Z3.mk_set_{add,del,empty,...} (which is why I'm trying to get that functionality via quantifiers.) Is that correct? Or is there another route?

Thanks!

Ranjit.

Ranjit Jhala
  • 1,242
  • 8
  • 18

1 Answers1

14

Your formula is satisfiable, and Z3 is not capable to produce a model for this kind of formula. Note that, it will have to generate an interpretation for the uninterpreted sort Set. There are a couple of alternatives you may consider.

1- Disable the model-based quantifier instantiation (MBQI) module. BTW, all Boogie-based tools (VCC, Dafny, Coral, etc) do that. To disable the MBQI module, we have to use

(set-option :auto-config false)
(set-option :mbqi false)

Remark: in the work-in-progress branch, the option :mbqi has been renamed to :smt.mbqi.

Cons: when the MBQI module is disable, Z3 will usually return unknown for satisfiable formulas that contain quantifier.

2- Encode sets of T as Arrays from T to Boolean. Z3 supports extended array theory. The extended theory has two new operators: ((_ const T) a) constant arrays, ((_ map f) a b) map operator. This paper describes the extended array theory, and how to encode set operations such as union and intersection using it. The rise4fun website has examples. This is a good alternative if these are the only quantifiers in your problem because the problem is now in a decidable fragment. On the other hand, if you have additional quantified formulas that contain sets, then this will probably perform poorly. The problem is that the model built by the array theory is unaware of the existence of the additional quantifiers.

For example of how to encode the above operators using const and map see: http://rise4fun.com/Z3/DWYC

3- Represent sets of T as functions from T to Bool. This approach usually works well if we don't have sets of sets, or uninterpreted functions that take sets as arguments. the Z3 online tutorial has an example (Quantifiers section).

Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53