Search code examples
z3smtsatcvc4

How to declare forall quantifiers in SMTLIB / Z3 / CVC4?

I'm stuck on how to how to create a statement in SMTLIB2 that asserts something like

forall x < 100, f(x) = 100

This property would be check a function that adds 1 to all numbers less than 100 recursively:

(define-fun-rec incUntil100 ((x Int)) Int  
    (ite 
        (= x 100) 
        100
        (incUntil100 (+ x 1))
    )
)

I read through the Z3 tutorial on quantifiers and patterns, but that didn't seem to get me much anywhere.

Solution

  • In SMTLib, you'd write that property as follows:

    (assert (forall ((x Int)) (=> (< x 100) (= (incUntil100 x) 100))))
(check-sat)

    But if you try this, you'll see that z3 will loop forever and CVC4 will tell you unknown as the answer. While you can define and assert these sorts of functions in SMTLib, solver support for actual proofs is rather weak, as they do not do induction out-of-the box.

    If proving properties of recursive functions is your goal, SMT-solvers are not a good choice; instead look into theorem provers such as Isabelle, HOL, Coq, Lean, ACL2, etc.; which are built for that very purpose.