Distinct Sets in Z3

Question

I have the following program:

;;; Sets
(declare-fun lock_0 (Int) Bool)
(declare-fun lock_1 (Int) Bool)
(declare-fun lock_2 (Int) Bool)
(declare-fun lock_3 (Int) Bool)

;;; verify if sets lock_0 and lock_1 haven't elements in common
(assert (exists ((x Int)) (=> (lock_0 x) (not (lock_1 x)))))

;;; verify if sets lock_2 and lock_3 haven't elements in common
(assert (exists ((x Int)) (=> (lock_2 x) (not (lock_3 x)))))

;;; Sets only contain 1 for Lock_0 and lock_1 or 2 for lock_2 or lock_3
(assert (forall ((x Int)) (= (lock_0 x) (= x 2))))
(assert (forall ((x Int)) (= (lock_1 x) (= x 2))))
(assert (forall ((x Int)) (= (lock_2 x)  (= x 1))))
(assert (forall ((x Int)) (= (lock_3 x)  (= x 1))))

;;; set [l1]
(declare-fun SL1 (Int) Bool) 
;;; set only contain 1
(assert (forall ((x Int)) (= (SL1 x) (= x 1))))
;;; SL1 subset lock_2
(assert (forall ((x Int)) (=> (SL1 x) (lock_2 x))))

;; sat
(check-sat)
( get-value (( lock_0 1 )))
( get-value (( lock_0 2 )))
( get-value (( lock_1 1 )))
( get-value (( lock_1 2 )))
( get-value (( lock_2 1 )))
( get-value (( lock_2 2 )))
( get-value (( lock_3 1 )))
( get-value (( lock_3 2 )))
( get-value (( SL1 1 )))
( get-value (( SL1 2 )))

Result:

sat
((( lock_0 1 ) false))
((( lock_0 2 ) true))
((( lock_1 1 ) false))
((( lock_1 2 ) true))
((( lock_2 1 ) true))
((( lock_2 2 ) false))
((( lock_3 1 ) true))
((( lock_3 2 ) false))
((( SL1 1 ) true))
((( SL1 2 ) false))

I need to generate lock_0 and lock_1 the following sets:

[] - Empty set
[2]

And to generate lock_2 and lock_3 the following sets:

[] - Empty set
[1]

But the sets lock_0 and lock_1 can not have elements in common.

But in the end I get:

( get-value (( lock_0 2 ))) true
( get-value (( lock_1 2 ))) true

the result is true for everyone and should be false in one case, for example:

( get-value (( lock_0 2 ))) false
( get-value (( lock_1 2 ))) true

For the sets can not contain equal elements.

Same problem to lock_2 and lock_3.

If I add:

;;; Set [l2]
(declare-fun SL2 (Int) Bool)

;;; set only contain 2
(assert (forall ((x Int)) (= (SL2 x) (= x 2))))
;;; SL2 is subset lock_0
(assert (forall ((x Int)) (=> (SL2 x) (lock_0 x))))

;; unsat
(check-sat)

I hope that the result is unsat, but as the sets (lock_0 and lock_1 or lock_2 and lock_3) are equal I'll get sat.

For example: If I obtain lock_0 = [] and lock_1 = [2] and lock_2 = [1] and lock_3 = [], the program was correct.

How can I solve this problem?

START EDIT

To adding this piece of code: (assert (forall ((x Int)) (or (not (lock_0 x)) (not (lock_1 x)))))

the result is unsat. And it should be sat.

So how can I generate for the same set, the empty set or the set {2}? Or it is not possible to do?

If this is not possible, then we can make the element 0 is the empty set? But for that I can only have the following sets:

[0] - empty set 
[2]

So I do: (assert (forall ((x Int)) (= (lock_1 x) (or (= x 0) (= x 2)))))

But if I want the sets lock_0 and lock_1 may also have 3 as an element should get:

[0] - empty set
[2]
[3]
[2,3] - may not include zero, since only the zero should be used as the singleton set [0]

So I do: (assert (forall ((x Int)) (= (lock_1 x) (or (= x 0) (and (!= x 0) (or (= x 2) (= x 3)))))))

Is that right?

Another question: if I want to create a function that takes a set as I do that? For a set is a function. For example:

(define-fun example ((s1 Set) (s2 Set) (x Int)) Int
  (if (and (s1 x) (not (s2 x)))
      (* x x)
      0))

But I do not know what to get instead of Set (Set s1), can help me please.

END EDIT

Answer 1

I see some problems in your encoding.

First, the command

;;; verify if sets lock_0 and lock_1 haven't elements in common
(assert (exists ((x Int)) (=> (lock_0 x) (not (lock_1 x)))))

is asserting that there is an element x such that x is not in lock_0 or x is not in lock_1. This assertion is almost vacuous. It is just preventing both "sets" from simultaneously containing all integers. Your comments suggests that you are actually trying to assert

(assert (forall ((x Int)) (or (not (lock_0 x)) (not (lock_1 x)))))

That is, the intersection of both sets is empty.

Second, you say you expect/need lock_0 and lock_2 to be the empty set, but you asserted

(assert (forall ((x Int)) (= (lock_0 x) (= x 2))))
(assert (forall ((x Int)) (= (lock_2 x)  (= x 1))))

These two assertions are essentially saying that lock_0 is the singleton set {2}, and lock_2 is the singleton set {1}.

BTW, if we replace

(assert (exists ((x Int)) (=> (lock_0 x) (not (lock_1 x)))))

with

(assert (forall ((x Int)) (or (not (lock_0 x)) (not (lock_1 x))))), (1)

the problem becomes trivially unsatisfiable after we assert

(assert (forall ((x Int)) (= (lock_0 x) (= x 2)))) (2)

(assert (forall ((x Int)) (= (lock_1 x) (= x 2)))) (3)

Since, (1) is saying that lock_0 and lock_1 do not have elements in common, and (2) and (3) are saying they are the singleton set {2}.

EDIT (for extra questions)

If we want to say that lock_0 is the empty set, we can just say that it is always false

(assert (forall ((x Int)) (not (lock_0 x))))

The command

(assert (forall ((x Int)) (= (lock_1 x) (or (= x 0) (= x 2)))))

is asserting that lock_1 is the set {0, 2}. If we want to say that lock_1 is the empty set or the set {2}, we should assert:

(assert (or (forall ((x Int)) (not (lock_1 x))) 
            (forall ((x Int)) (= (lock_1 x) (= x 2)))))

To say that lock_1 may contain only the values 2 and 3, we should assert:

(assert (forall ((x Int)) (=> (lock_1 x) (or (= x 2) (= x 3)))))

Note that, I'm using implication (=>) instead of equality. In this case, we have that lock_1 may be one of the following sets: {} (empty set), {2}, {3}, or {2, 3}.

The command define-fun does not take functions as arguments. The command define-fun is just defining a macro. It does not add any extra power to Z3.

If you want a more powerful language to interact with Z3, you should consider Z3Py, the Python front-end for Z3. Here is an example using Z3Py (it is also available online here).

# Declare a function from Int to Bool
lock_1 = Function('lock_1', IntSort(), BoolSort())
x = Int('x')

s = Solver()
# Assert that lock_1 is the empty set
s.add(ForAll(x, Not(lock_1(x))))
print(s.check())

# Declare a function that returns x*x if x is in s1 but not in s2
# Remark: example is a Python function that builds a Z3 expression.
def example(s1, s2, x):
    # Remark: the function If creates a Z3 if expression.
    return If(And(s1(x), Not(s2(x))), x*x, 0)

lock_2 = Function('lock_2', IntSort(), BoolSort())

s = Solver()
a = Int('a')
s.add(a == example(lock_1, lock_2, 3))
s.add(lock_1(3))
s.add(Not(lock_2(3)))
print(s)
print(s.check())
m = s.model()
print(m[a])

END EDIT