Why doesn't the `div` predicate work here?

Question

(declare-fun pdiv (Int Int Int) Bool)
(assert (forall ((x Int) (y Int) (z Int)) (=> (= z (div x y)) (pdiv z x y))))

When I check sat, I've got unknown by Z3

Answer 1

It is very common for Z3 to return unknown instead of sat when using quantifiers. Indeed, constraint systems which use forall's (particularly with Ints) quickly reach into undecidable territory.

There are two options. First, if you want to extract a model out of your satisfiable constraints, you can in this instance define pdiv instead of declaring it:

(define-fun pdiv ((z Int) (x Int) (y Int)) Bool 
    (= z (div x y))
)
(declare-const z Int)
(declare-const x Int)
(assert (= x 3))
(declare-const y Int)
(assert (= y 3))
(assert (pdiv z x y))
(check-sat)
(get-model)
; sat -- z = 1

define-fun is just a macro expansion, so the semantics here are a little different from your example -- if you intended pdiv to be strictly weaker than z = div x y, you will need to encode this differently.

The other option is to keep the quantified version, but instead of checking sat, you negate the formula and check for unsat:

(declare-fun pdiv (Int Int Int) Bool)
(assert (forall ((x Int) (y Int) (z Int)) (=> (= z (div x y)) (pdiv z x y))))

(declare-const mygoal Bool)
(assert (= mygoal (pdiv 2 6 3)))
(assert (not mygoal))
(check-sat)
; unsat

This second option is used pervasively in program verification, where quantifiers are used all over the place to encode axioms about the programs at hand. For example, this is what happens in F*.