Skip to content

Language

Jump to bottom
AdrienChampion edited this page Oct 20, 2018 · 11 revisions

Hoice currently supports a subset of the SMT-LIB 2.6 Horn clause format used by the SV-COMP.

The basic sorts supported are Bool, Int, Real and Array. Note that internally, reasoning about Arrays is in a very early stage. Should you use Arrays, expect a lot of unknown. Hoice also supports datatypes.

Hoice supports define-funs and let-bindings.

The following describes a legal SMT-LIB 2.6 Horn clause script for hoice.

The script optionally opens with a (set-logic HORN) command. The rest of the script is composed of predicate declarations, assertions, check-sats and get-models in any order.

Predicate Declarations

Predicate declarations use the declare-fun command and have the following shape:

(declare-fun <ident> ( <sort>* ) Bool)

Note in particular that you cannot declare functions with a non-Bool codomain.

Assertions

All assertions must be of the following Horn clause form

(assert
  ( forall ( <vars> ) (=> <body> <head>) )
)

or

(assert
  (not ( exists ( <vars> ) <body> ) )
)

The body of the clause must be equivalent (potentially after simplification) to a conjunction of

  • atoms, i.e. expressions that do not mention predicates introduced by predicate declarations, and
  • predicate applications, i.e. expressions of the form (<ident> <expr>*) where the <expr>* are atoms.

Assuming (declare-fun pred ( Int ) Bool) was issued previously and the n_* are among <vars>, example of legal bodies include

  • (and (> n_0 3) (= n_1 7) (pred (+ n_0 n_1 42)) )
  • (not (or (> n_0 3) (= n_1 7) (not (pred (+ n_0 n_1 42))) ) )

The head of the clause is either an atom or a predicate application as defined above.

Check-sat

The standard SMT-LIB (check-sat) command, which can produce

  • sat, meaning some definitions for the predicate declared that respect all the clauses asserted exist (Allows the (get-model) command.)
  • unsat, meaning such definitions do not exist
  • unknown, meaning hoice gave up. (This currently should only happen if your script uses arrays.)

Get-model

The standard SMT-LIB (get-model) command, only legal directly after a (check-sat) to which hoice answered sat. Its output is

(model
  <def>*
)

where each <def> is

(define-fun <ident> ( (<var> <sort>) ) Bool <expr>)

uniquely defining predicate <ident> declared by the script, and has the same signature as the script's declaration. <expr> is an arbitrary expression: in particular it can contain existential/universal quantifiers and use predicates defined earlier in the model.

Examples

Take a look at our benchmarks for a better feel of the format.

Clone this wiki locally