0
$\begingroup$
(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

$\endgroup$
1
  • 3
    $\begingroup$ Hurray, we have our first Z3 question. $\endgroup$ Mar 22, 2023 at 14:18

1 Answer 1

3
$\begingroup$

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*.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.