CHC-COMP Benchmark Format

(Revision: April 7, 2020)

Comments on this document can be submitted through Gitter or emailed directly to the organizers.

The format used for the CHC-COMP benchmarks is based on the SMT-LIB language version 2.6. Specifically, the format is a syntactic fragment of SMT-LIB format with the restrictions outlined in the rest of this document.

benchmark   ::=
   set_info*                                            (1)
   logic
   set_info*
   fun_decl+
   (assert chc_assert)*
   (assert chc_query)
   (check-sat)
   (exit)?                                              (2)

logic       ::= (set-logic HORN)
fun_decl    ::= (declare-fun symbol ( sort* ) Bool)

chc_assert  ::=   ;; a well-formed first-order sentence of the form
  | (forall ( var_decl+ ) (=> chc_tail chc_head))
  | (forall ( var_decl+ ) chc_head)                     (3)
  | u_predicate

var_decl    ::=
  | (symbol sort)

chc_head    ::=
  | u_pred_atom, where all argument variables in the atom are DISTINCT

chc_tail    ::=
  | u_pred_atom
  | i_formula
  | (and u_pred_atom+ i_formula*)

u_pred_atom   ::=                                       (4)
  | u_predicate          ;; nullary predicate
  | (u_predicate var*)   ;; predicate with arguments

chc_query   ::=  ;; a well-formed first-order sentence of the form
  | (forall ( var_decl+ ) (=> chc_tail false))

u_predicate ::=
  | uninterpreted predicate (i.e., Boolean function)

i_formula   ::=
  | an SMT-LIB formula over variables, and interpreted functions and predicates

An example of an input in the CHC-COMP format is shown below:

(set-logic HORN)
(set-info :status sat)

(declare-fun Inv (Int) Bool)

;; fact
(assert (forall ((x Int)) (=> (= x 0) (Inv x))))
;; chc
(assert (forall ((x Int) (y Int))
                (=> (and (Inv x) (<= x 10) (= y (+ x 1)))
                   (Inv y))))
;; query
(assert (forall ((x Int)) (=> (and (Inv x) (> x 15)) false)))

(check-sat)