Recursive Functions

As of v1.7, hoice supports mutually recursive functions. They are defined as specified in the SMT-LIB 2.6 standard, using the define-funs-rec command.

Hoice has a special treatment for recursive functions (and their invariants, see below). User-defined functions are used internally to formulate candidates for the predicates. This is especially useful when dealing with datatypes to raise hoice's expressiveness. For instance by defining a function computing the depth of a tree.

Users can also specify invariants for their functions. Doing so can prove very rewarding: when hoice interacts with the underlying SMT solver, function invariants usually cut a lot of the search space for the solver and tend to improve performance drastically.

For instance, the following defines a length function over lists and asserts the fact that it is always positive.

(define-funs-rec
  (
    (len ( (l (Lst Int)) ) Int)
  )
  (
    (ite
      (= l nil)
      0
      (+ 1 (len (tail l)))
    )
  )
)
(assert (forall ( (l (Lst Int)) )
  (>= (len l) 0)
))

Note that the invariant is asserted. Hoice will not check that it holds, users are responsible for making sure that it is the case. For instance by proving it with hoice:

(declare-fun len ((List Int) Int) Bool)

(assert (forall ( (l (List Int)) )
    (=> (= l nil) (len l 0))
))
(assert (forall ( (hd Int) (tl (List Int)) (lngth Int) )
    (=>
        (len tl lngth)
        (len (insert hd tl) (+ lngth 1))
    )
))
(assert (forall ((l (List Int)) (lngth Int))
    (=>
        (len l lngth)
        (>= lngth 0)
    )
))

(check-sat)
; sat