FOL definitional theory in Z3

Question

I want to put a first-order theory into Z3, an SMT solver developed by Microsoft. This theory contains two objects obj1 and obj2, a function move that takes an object and returns an action, and a one-placed predicate occurs that takes an action as argument. The theory contains the formula occurs(move(obj1)), and I want to make sure that this is the only way in which the occurs predicate is true. I do this by giving a definition of occurs:

forall (A) (occurs(A) <-> (A = move(obj1)))

This means that occurs(move(obj1)) can be inferred from the theory, but occurs(move(obj2)) cannot. To prove this, I have translated this into Z3 as follows:

(declare-datatypes () (( Obj obj1 obj2 )))
(declare-sort Action 0)

(declare-fun occurs (Action) Bool)
(declare-fun move (Obj) Action)

(assert (forall ((A Action)) (
    = (occurs A) (= A (move obj1))
)))

(check-sat)
(get-value ((occurs (move obj1))))
(get-value ((occurs (move obj2))))

The problem is that this gives the following output:

sat
(((occurs (move obj1)) true))
(((occurs (move obj2)) true))

Which I do not understand, because the definition of occurs provides all the necessary and sufficient condition for the predicate to be true, so I would think that occurs(move(obj2)) cannot be true in any model. What am I doing wrong?

Update Thanks to de Moura I have been able to find a solution for my problem. What I need to do is to provide unique names axioms for the actions, which in my case is the move function. I need to state that move will never return the same element of sort Action when it has two different arguments. This could be done in several ways, but I found this the most concise version:

(assert (forall ((o1 Obj) (o2 Obj)) 
    (=> (not (= o1 o2)) (not (= (move o1) (move o2))))))

Leonardo de Moura Leonardo de Moura · Accepted Answer · 2012-10-29T21:58:13

You are assuming constraints that you did not assert. For example, nothing prevents move to be the constant function. The model produced by Z3 is correct. You can obtain the model by adding the command (get-model) after (check-sat). The command (declare-sort Action 0) is declaring a unintepreted sort. In the model produced by Z3, the interpretation of sort Action contains only one element, and occurs and move are constant functions. This is a model because all assertions in your script are satisfied by it.

FOL definitional theory in Z3

1 Answers