TIP Format

This document contains the TIP format, which is an extension of SMT-LIB for expressing inductive problems. The grammar of the format can also be viewed as BNF.

Scope of the benchmark suite

The benchmark suite focuses exclusively on problems that need induction over datatypes. Also, although we support higher-order functions and quantification over functions, problems that need a lot of higher-order reasoning (e.g. synthesis of functions) are probably better suited for THF.

Differences between TIP and SMT-LIB 2.6

Our ambition is to keep TIP as close to SMT-LIB as possible. However, there are still a few incompatibilities:

The TIP tools can convert TIP files not compatible with SMT-LIB 2.6 to valid SMT-LIB syntax (use the command tip --smtlib myTIPfile.smt2). This includes monomorphisation to remove type variables, removal of lambdas, completion of partial functions, removal of annotations and a translation pass which remove the prove statement and replaces them with valid SMT-LIB syntax using push/pop.

Datatypes, match-expressions and recursion

This example specifies the commutativity of plus over natural numbers:

(declare-datatype Nat ((Zero) (Succ (pred Nat))))
  ((x Nat) (y Nat)) Nat
  (match x
    (((Succ n) (Succ (plus n y)))
     (_ y))))
(prove (forall ((n Nat) (m Nat)) (= (plus n m) (plus m n))))

The syntax should be familiar to users of SMT-LIB. Natural numbers are defined with declare-datatype, and the function is declared using define-fun-rec. Both are part of the SMT-LIB v2.6 standard. We define plus rather than axiomatising it because, if the problem is from a functional program, we want to be explicit about which axioms are function definitions.

TIP has a prove construct which declares the goal, akin to conjecture in TPTP, or goal in Why3. It is not part of SMT-LIB. If the problem uses prove only once, then (prove p) means the same as (assert (not p)). If prove is used several times, it indicates that there are several goals which must all be proved.


TIP also supports polymorphism. Here is an example showing the right identity of append over polymorphic lists:

  list (par (a) ((nil) (cons (head a) (tail (list a))))))
  (par (a) (((xs (list a)) (ys (list a))) (list a)))
  (match xs
    ((nil (_ nil a))
     ((cons x zs) (cons x (append zs ys))))))
  (par (a) (forall ((xs (list a))) (= (append xs (_ nil a)) xs))))

We allow polymorphic datatypes, declarations and assertions using the syntactic form (par (A) ...) to quantify over the type variable A. Only rank-1 polymorphism is supported. Note that TIP allows both polymorphic datatypes and polymorphic functions, unlike SMT-LIB 2.6, which only allows it in datatype definitions.

An underscore is used to instantiate a polymorphic function at a given type. In general, if f is a polymorphic function symbol having n type arguments, then (_ f t1 ... tn) applies f to the type arguments t1 ... tn. Explicit type arguments must be given whenever a function’s type cannot be inferred by looking at the types of its arguments. In the example above, this occurs with (_ nil a).

Higher-order functions

This is an example property about mapping functions over lists:

  list (par (a) ((nil) (cons (head a) (tail (list a))))))
  (par (a b) (((f (=> a b)) (xs (list a))) (list b)))
  (match xs
    ((nil (_ nil b))
     ((cons y ys) (cons (@ f y) (map f ys))))))
  (par (a b c)
    (forall ((f (=> b c)) (g (=> a b)) (xs (list a)))
      (= (map (lambda ((x a)) (@ f (@ g x))) xs) (map f (map g xs))))))

Lambdas are introduced much like lets in SMT-LIB, with an identifier list with explicit types. They are applied using ‘@’. Note that the function spaces are a family of types, with different arities. Thus, for some types a, b and c, there is a type (=> a b c), which is different from its curried version (=> a (=> b c):

That is, if you want to partially apply a function, you must either write a lambda, or define it in a curried fashion in the problem.


This document does not yet cover partial functions or annotations.