Datatypes

As of v1.7, hoice supports mutually recursive datatypes.

Declaring Datatypes

Datatypes are declared using the declare-datatypes command. Please refer to the SMT-LIB 2.6 standard for syntax-related details.

(declare-datatypes ( (List 1) ) (
  (par (T) (
    (nil)
    (insert (head T) (tail (List T)))
  ) )
) )

In fact, hoice already has a built-in List datatype, which is defined as the datatype in the example above. Hoice allows users to re-define it though, so it can be overwritten to anything.

Declaring a datatype as above yields the nullary constructor symbol nil and the binary constructor symbol insert. The latter takes a symbol of sort T and a list of Ts. For each variant of the datatype, a unary tester symbol is created: here, is-nil and is-insert. Formula (is-<variant> <datatype>) constrains <datatype> to be a specific variant <variant>.

Note also that insert's two arguments are named. They are the fields of the insert variant.

For instance, (is-insert (insert <hd> <tl>)) is always true whatever <hd> and <tl> are. Conversely (is-insert nil) and (is-nil (insert <hd> <tl>)) are always false.

Declaring datatypes also give access to projection unary symbols.

Projectors

Projectors allow to project a datatype to its fields. For instance,

(=  (head (insert 3 <tl>))  3)

is a tautology.

Projectors are a bit dangerous because their semantics might differ from what one would expect. They are total functions. For instance, (head nil) is not a problem, although it is not specified and could be anything. Hence,

(declare-const l (List Int))
(assert (and
    (is-nil l)
    (= 7 (head l))
))
(check-sat)
; sat

is satisfiable.

To avoid problems, to access fields we recommend to first test that the datatype is indeed the right variant. For instance,

(define-fun head_or_neg ( (l (List Int)) )
    (ite (is_insert l)
        (head l)
        (- 1)
)   )

Function Reconstruction

This feature can be disabled with --fun_preds off.

Horn clause problems over datatypes are difficult. One of the main difficulties is that the solver, hoice here, lacks ways to express complex properties about user-defined algebraic datatypes. The depth of a tree, the reverse of a list...

One way to address this problem is to give hoice recursive functions. Another, internal and automatic way is to check the predicates and see if some of them could be reconstructed as functions. This is what hoice does under the hood whenever it sees datatypes. For instance, in a Horn clause problem with the following clauses

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

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

hoice will see that len is really a recursive function and define len as the recursive function

(define-funs-rec
    ( (len_fun ( (l (Lst Int)) ) Int) )
    ( (ite (is-nil l)
        0
        (+ 1 (len (tail l)))
) ) )
(define-fun len ( (l (Lst Int)) (n Int) ) Bool
    (= (len_fun l) n)
)

This means that when it prints the model, hoice will give the additional recursive functions so that the predicate definitions make sense. Make sure your model parser can handle recursive functions if you use this feature.