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:
- TIP allows polymorphism and type variables in function definitions. SMT-LIB only allows polymorphism in datatype definitions.
- TIP allows higher-order functions, while SMT-LIB does not.
- TIP allows partial functions. SMT-LIB does not.
- For convenience, TIP has a special command
provefor stating a goal to prove. This allows us to state several subgoals to be proved as separate proof attempts, in one file.
- TIP uses a different syntax for annotations than SMT-LIB.
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)))) (define-fun-rec plus ((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.
- To convert a problem to standard SMT-LIB format, run
- To replace
matchexpressions with selector functions (e.g.
tip --remove-match. You can combine this with conversion to SMT-LIB format with
- To convert a problem to Why3 format, run
TIP also supports polymorphism. Here is an example showing the right identity of append over polymorphic lists:
(declare-datatype list (par (a) ((nil) (cons (head a) (tail (list a)))))) (define-fun-rec append (par (a) (((xs (list a)) (ys (list a))) (list a))) (match xs ((nil (_ nil a)) ((cons x zs) (cons x (append zs ys)))))) (prove (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).
- To eliminate polymorphism from a problem, run
This is an example property about mapping functions over lists:
(declare-datatype list (par (a) ((nil) (cons (head a) (tail (list a)))))) (define-fun-rec map (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)))))) (prove (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
c, there is a type
(=> a b c), which is different from its curried version
(=> a (=> b c):
- To construct a value of type
(=> a b c), write
lambda ((x a) (y b)) .... To apply it, write
(@ f x y).
- To construct a value of type
(=> a (=> b c)), write `
lambda ((x a)) (lambda ((y b)) ...). To apply it, write
(@ (@ f x) y).
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.
- To eliminate lambdas from a problem, run
This document does not yet cover partial functions or annotations.