2

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.

Alex Coleman
  • 607
  • 1
  • 4
  • 11

1 Answers1

2

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.

alias
  • 28,120
  • 2
  • 23
  • 40
  • 1
    I can write proofs in Coq, but I was hoping to automate this process. Is there no good way of automating quantified SMT formulae? – Alex Coleman Apr 14 '21 at 22:41
  • 1
    Currently, patterns are the only mechanism to get any reasonable output from quantified proofs. There are some examples here https://rise4fun.com/z3/tutorialcontent/guide#h28 but it's rather tricky to make it do anything fancy; especially in the presence of recursive functions like you have. Also keep in mind that z3 and cvc4 will have different levels of support, so consistency isn't guaranteed either. – alias Apr 14 '21 at 23:43