Home • Docs • Download • Mail • FAQ • Awards • Status • MSR

Z3 An Efficient SMT Solver

Z3 native input format

Our native, and very low-level, input format for Z3 follows some of the conventions found in the DIMACS format for SAT problems and by the Spear input format.

We should emphasize that the low-level format is intended for making it easy to exchange machine generated benchmarks with Z3. The format is extensible, as the grammar allows for selecting solvers and adding semantic attachments with constructors. The SMT-LIB and Simplify text formats are easier to write and read for a human consumer.

Every line consists of a command that gets interpreted as a declaration of a node in anbstract syntax tree, or as a control instruction to Z3, such as to augment the current context with constraints or check for satisfiability.

    command := 
      | ast
      | control 
      |  ; commented line

White spaces are implicit in the production rules. The legal white-spaces have the ASCII representations

     ' ' | \ t | \ r

Comment lines start with ;. All characters up to the newline \ n are ignored.

We use id for identifiers in general. Identifiers associated with certain semantic categories, such as ast nodes, or types are prefixed by the category and suffixed by id. For example, we have:

   ast-id        - identifier for ast nodes

   type-id       - identifier for type nodes

   parameter-id  - identifier for ast

   name-id       - identifier for a function/type name

   decl-id       - identifier for declaration node

   context-id    - identifier for Boolean context

Identifiers can be any sequence of non-whitespace and non-newline characters whose first character is not one of the decimal digits. Identifiers enclosed in quotes ''...'' are treated specially: the quotes are stripped. Thus, the identifier consisting of zero characters is written ''''. The identifier ''null'' is allowed for skolem-id and quant-id.

Control commands

To load a theory solver for integer linear arithmetic, include a line of the form Solver LIA. To load the mixed integer/real solver include instead a line of the form Solver LRA

Use Push and Pop to push/pop contexts (constraints that are asserted under a Push are removed after a Pop). To reset the state entirely, use Reset.

To assert a constraint use Assert ast-id, where the ast-id is an identifier declared for a boolean typed term.

To check for satisfiability of all asserted constraints use Check.

  control :=
     | Solver solver        - load specified theory solver 
     | Assert ast-id        - assert constraint 
     | Check                - check for satisfiability of asserts
     | Push                 - push a context
     | Pop                  - pop a context
     | Version major minor build-number revision - specify Z3 version

  solver :=
     | LRA                  - mixed integer/real arithmetic 
     | LIA                  - integer arithmetic

Abstract syntax trees

Every node in the abstract syntax trees understood by Z3 is declared by using a syntax category identifier, followed by a (unique) identifier that names the node. The node identifier is followed by a description of the node.

In overview abstract syntax tree nodes are declared using the commands:

  ast :=
     | Type id type 
     | Dec id declaration
     | Const id constant             
     | Fun id function               
     | App id built-in               
     | Num id numeral                
     | Qua id quantifier                     
     | Var id bound-variable             
     | Ctx id local-context          
     | Lab id label-term         
     | Pat id pattern

Types

Types are created from a name and optional parameters. A number of names are reserved for built-in theories. These names are: 
    int  real  bool  bv  array
When the name of a type is one of these, the type is automatically associated with the respective theory. The bv type takes one numeric parameter (the bit-width of the bit-vector), and array takes n+1 parameters (the n types for the domain of the array and the last parameter for the range of the array.

 type := name '[' parameter* ']'

 parameter := number | ast-id | symbol
A parameter can either be an integer, an identifier used for another defined term or type, or a symbol. Symbols are given as strings. The parser first attempts to identify a parameter as a previously defined term or type, and if there is no such previously defined term/type, then it treats the string as a symbol.

Function and constant declarations

In Z3, functions are constants that take more than zero arguments, thus, everything is treated as a constant.

Constant declarations comprise of a name, followed by a non-empty list of types, all but the first types are the domain of the function (there are no domain types for 0-ary constants), the last type is the range. A constant declaration is followed by optional theory specific information.

The codes used in the theory specific information is described under Z3 theories

The theory specific information indicates whether the constant is associative/commutative/injective; a list of parameters may also be used to indicate auxiliary information for the constant declarations.

 declaration := name-id type-id* [const-info]

 const-info := BUILTIN theory kind-num (:assoc | :comm | :inj | parameter)*

 theory := 
    | basic -  built-in types and operations 
    | arith -  arithmetical 
    | bv    -  bit-vectors 
    | array -  arrays 
    | tuple -  tuples

Terms

Terms are built from constants, function applications, labeling, context formation, quantification and bound variables.

A constant consists of a declarations, functions consist of a declaration followed by a non-empty list of term identifiers. All constants and function applications can be constructed using the Fun construct. However, two shortcuts are available.

  constant  := name-id type-id

  function  := decl-id ast-id*

  built-in  := name-id [ [ parameter* ] ] ast-id*

Labeled terms consist of a polarity (LBLPOS for positive context, LBLNEG for negative contexts), a name, and a term identifier.

  label-term  :=  (LBLPOS | LBLNEG) label-name ast-id

Local contexts consist of an identifier for the underlying term, followed by a predicate summarizing the context in which the term is interpreted.

  local-context :=  ast-id context-id

A quantifier consists of 

  quantifier  :=  
      (FORALL | EXISTS) 
      weight-num  
      skolem-id
      quant-id 
      decls-num
      (name-id type-id)*
      pattern-num
      pattern-id*
      ast-id

A bound variable consists of a de-Brujin index for the bound variable together with the type of the bound variable. While the type can be computed by matching the index of the de-Brujin index with the associated quantifier,

Patterns comprise of a list of terms.

  bound-variable  :=  index-num type-id

  numeral   :=  rational type-id

  rational  :=  number [/number]

  number    :=  [0-9]+

  pattern   :=  id ast-id*

Examples

Integer Arithmetic

Suppose we wish to check whether 
	z0 >= 0 && z1 >= 0 && z2 >= 1 && z1 >= z2 && z2 >= z0
is satisfiable for 
z0, z1, z2
integers. With the low-level input format, we may specify this by:

   Type INT  int
   Type BOOL bool
   Const z0  z0 INT
   Const z1  z1 INT
   Const z2  z2 INT
   Num   0   0 INT
   Num   1   1 INT
   App c0 >= z0 0
   Assert c0
   App c1 >= z1 0
   Assert c1
   App c2 >= z2 1
   Assert c2
   App c3 >= z1 z2
   Assert c3
   App c4 >= z2 z0
   Assert c4
   Check

Notice that the identifiers may be arbitrary strings, including numerals. So for instance, we used 1 to represent integer 1.

Bit-vectors

We can check whether 32-bit addition is commutative. Z3 reports unsat in for the first check. The second satisfiable check illustrates the use of parameters (extract takes two integer parameters for the range of bits extracted from the bit-vectors).

   Type bool bool 
   Type bv32 bv [ 32 ]
   Type bv64 bv [ 64 ]
   Num 0 0 bv32
   Num 1 1 bv32
   Const x0 x0 bv32
   Const x1 x1 bv32
   Const x2 x2 bv64
   App a bvadd x0 x1
   App b bvadd x1 x0
   App eq = a b
   App constraint1 not eq
   Push
   Assert constraint1
   Check
   Pop
   App c extract [ 31 0 ] x2
   App eq2 = a c
   App constraint2 not eq2
   Push
   Assert constraint2
   Check
   Pop

We added the declarations of bit-vector constants 0 and 1. Like integers, these are also numerals, but with bit-vector type.

Arrays

The low-level version of: { store(f1,i1,v1) = store(f2,i2,v2) && i1 != i3 && i2 != i3 && select(f1,i3) != select(f2,i3) } is:

  Type Index Index
  Type Elem Elem
  Type Array array [ Index Elem ]
  Type bool bool
  Const i1 i1 Index
  Const i2 i2 Index
  Const i3 i3 Index
  Const v1 v1 Elem
  Const v2 v2 Elem
  Const f1 f1 Array
  Const f2 f2 Array
  App n1 store f1 i1 v1
  App n2 store f2 i2 v2
  App n3 = n1 n2
  App n4 = i1 i3
  App n5 not n4
  App n6 = i2 i3
  App n7 not n6 
  App n8 select f1 i3
  App n9 select f2 i3
  App n10 = n8 n9
  App n11 not n10
  Assert n3
  Assert n5
  Assert n7
  Assert n11
  Check

Tuples

To check projection over tuples 
  (= x (first (mk_tuple x y)))

we write: 

  Type int int
  Type pair tuple [ mk_tuple first int second int ]
  Dec first first pair int BUILTIN tuple 1 first 
  Dec mk_tuple mk_tuple int int pair BUILTIN tuple 0 pair 
  Const x x int
  Const y y int
  Const p p pair
  App n1 mk_tuple x y
  App n2 first n1
  App n3 = n2 x
  App n4 not n3
  Assert n4
  Check

Notice that the constructor and projection operators have to be re-declared.

Quantifier

A quantifier expression is built using the identifier Qua. For instance, the quantified formula: 
  (forall (?x int) { ((type ?x)) } (implies (= (type ?x) 0) (= ?x 0)))

can be built using the following sequence:

  Ty int int
  Dec type type int int
  Num 0  0 int
  Var b0 0 int
  Fun e0 type b0
  Pat pattern e0
  App e1 = e0 0
  App e2 = b0 0
  App body implies e1 e2
  Qua q FORALL 2 "null" "null" 1 ?x int 1 pattern body
  Assert q
Last modified Wed Sep 3 08:54:17 2008