CODEWITHSUNDEEP
z3
Shambo
Shambo

Reputation: 946

Defining Set in z3

To create a Sets of 3 elements (1,2,3) in Z3, I am using the follows code: 

(define-sort Set () ( Array Int Bool ) )
(declare-const s Set ) 
( assert  ( and ( = ( select s 1 ) true )  ( = ( select s 2 ) true ) 
           ( = ( select s 3 ) true )  ) )

The Model I am getting is as follows : 

(model 
  (define-fun s () (Array Int Bool)
    (_ as-array k!0))
  (define-fun k!0 ((x!1 Int)) Bool
    (ite (= x!1 2) true
    (ite (= x!1 3) true
    (ite (= x!1 1) true
      true))))
)

But instead how can I get a model of the form : 

(model    (define-fun s () (Array Int Bool)
    (_ as-array k!0))   (define-fun k!0 ((x!1 Int)) Bool
    (ite (= x!1 2) true
    (ite (= x!1 3) true
    (ite (= x!1 1) true
      false)))) )

So that elements other than the set members are not included in the set.

Upvotes: 1

Views: 2056

Answers (1)

Philippe
Philippe

Reputation: 9762

You can achieve this by starting from the empty set, i.e. the array that is defined to be false everywhere.

Here is an example:

(declare-const s1 (Array Int Bool))

(assert (= s1
  (store
    (store
      (store 
        ((as const (Array Int Bool)) false)
        1 true)
      2 true)
    3 true)
))

(check-sat)
(get-model)

Upvotes: 3

Related Questions