SMT-LIB format

The SMT-LIB input format is described on the SMT-LIB web site: SMT-LIB input format.

The Native Z3 format re-uses the function names used in SMT-LIB. A table of the relevant function names is summarized in the documentation for Z3 theories.

SMT-LIB Extensions

Z3 uses a few extensions to SMT-LIB. These are described in the following.

Pattern Definitions.

Z3 uses an extension for pattern annotation. It is found in some SMT-LIB benchmarks, but is not widely documented. The annotation :pat is used to annotate quantifiers. It is a hint for Z3 (and other SMT solvers) on how to instantiate the universally quantified formula.

The grammar is

  [PATTERN_ANNOTATION] ::= :pat { [EXPR]+ }

Example:

  (forall (?ind__1 Int) (?val__1 Int)
         (implies (= (Is_BOOLEAN ?val__1) Smt.true) 
                     (= (Is_REFANY_BOOLEAN_MAP (store1 ?map__3 ?ind__1 ?val__1))  Smt.true))
         :pat {(store1 ?map__3 ?ind__1 ?val__1)}))

Z3 will instantiate this quantifier whenever it can find an instance of the pattern (store1 ?map__3 ?ind__1 ?val__1) :pat may contain more than one expression. In this case, we say it is a multi-pattern, and the quantifier will only be instantiated if Z3 can simultaneously match all of them. The concept of patterns and multi-patterns was introduced in the Simplify theorem prover. The engine used for pattern instantiation is explained in our paper on efficient E-matching.

Sort Definitions

There is a construct for defining sort names.

  :define_sorts ((IntArray  (array Int Int)))

introduces the name IntArray which can be used instead of the compound sort (array Int Int).

Then, the term (const[IntArray] 0) can be used for the array of integers where all indices map to 0.

Data-types

The :datatypes attribute lets you define recursive data-types such as lists.

  (benchmark data 
   :status unsat 
   :datatypes ((list (cons (car Int) (cdr list)) nil))
 
   :extrafuns ((a list) (b list) (c list))

   :formula (and (= a (cons 10 b)) (not (= (car a) 10)))
  )

Tuples and records are just special cases (non-recursive data-types):

  (benchmark data 
   :status unsat 
   :datatypes ((tuple (mk (first Int) (second Int))))
   :extrafuns ((a tuple) (b tuple))
   :formula  (and (= (first a) (first b))
                   (= (second a) (second b))
                   (not (= a b)))
  )

You can declare mutually recursive data-types

   :datatypes ((tree (node (children list)) (leaf (val Int)))
               (list (cons (car tree) (cdr list)) nil))

The grammar is:

  [DATATYPE_DECLS] ::= :datatypes ( [DATATYPE]+ )
  [DATATYPE] ::= ( [ID] [CONSTRUCTOR_DECL]+ )
  [CONSTRUCTOR_DECL] ::= [ID] | ( [ID] [SORT]+)

Arrays

Z3 provides a few extensions to the theory of arrays. The theoretical basis is explained in MSR-TR-121.

The extensions comprise of operations:

  (default[array_type] a) 
       Access the default element of an array.
       default takes one argument, an array 'a', and 
       returns a value in the range of the array.
       If the model for 'a' maps all but a finite 
        number of domain elements to the same value 'v', then 
       '(default[array_type] a)' will produce the value 'v'.

  (const[array_type] v) 
       Produce an array that maps everything to the value 'v'.

  (map[unary_function_symbol] a)
  (map[binary_function_symbol] a b)
  (map[ternary_function_symbol] a b c)
       Produce an array such that, respectively:

        (forall (i Index) (= (select (map[unary_f] a) i) (unary_f (select a i))))

        (forall (i Index) (= (select (map[binary_f] a b) i) (binary_f (select a i) (select b i)))

        (forall (i Index) (= (select (map[ternary_f] a b c) i) (unary_f (select a i) (select b i) (select c i))))

The following example uses default, const and map.

  (benchmark additive_bags
  :status unsat  
  :define_sorts ((IntArray  (array Int Int)))
  :extrafuns ((add_int Int Int Int) (bag IntArray))
  :assumption (forall (x Int) (y Int) (= (add_int x y) (+ x y)) :pat{ (add_int x y) })

  :formula (and (not (= (default[IntArray] bag) 0))
                (= (map[add_int] bag bag) bag))

  :formula (and (not (= (const[IntArray] 0) bag))
                (= (map[add_int] bag bag) bag))
  )