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

Z3 An Efficient SMT Solver

C API


Types

Most of the types in the C API are opaque pointers.

  • Z3_config: a configuration object used to initialize logical contexts.
  • Z3_context: logical context. This is the main Z3 data-structure.
  • Z3_symbol: a Lisp-link symbol. It is used to name types, constants, and functions. A symbol can be created using string or integers.
  • Z3_ast: abstract syntax tree node. That is, the data-structure used in Z3 to represent terms, formulas and types.
  • Z3_type_ast: a kind of AST used to represent types.
  • Z3_const_ast: a kind of AST used to represent constant and function declarations.
  • Z3_numeral_ast: a kind of AST used to represent numerals.
  • Z3_pattern_ast: a kind of AST used to represent pattern and multi-patterns used to guide quantifier instantiation.
  • Z3_model: a model for the constraints asserted into the logical context.
  • Z3_value: a value assigned to a constant in a model (Z3_model).


enum  Z3_lbool { Z3_L_FALSE = -1, Z3_L_UNDEF, Z3_L_TRUE }
 Lifted Boolean type: false, undefined, true. More...
enum  Z3_symbol_kind { Z3_INT_SYMBOL, Z3_STRING_SYMBOL }
 In Z3, a symbol can be represented using integers and strings (See Z3_get_symbol_kind). More...
enum  Z3_type_kind {
  Z3_UNINTERPRETED_TYPE, Z3_BOOL_TYPE, Z3_INT_TYPE, Z3_REAL_TYPE,
  Z3_BV_TYPE, Z3_ARRAY_TYPE, Z3_TUPLE_TYPE, Z3_UNKNOWN_TYPE = 1000
}
 The different kinds of Z3 types (See Z3_get_type_kind). More...
enum  Z3_ast_kind {
  Z3_NUMERAL_AST, Z3_CONST_DECL_AST, Z3_CONST_AST, Z3_TYPE_AST,
  Z3_VAR_AST, Z3_PATTERN_AST, Z3_QUANTIFIER_AST, Z3_UNKNOWN_AST = 1000
}
 The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types. More...
enum  Z3_decl_kind {
  Z3_OP_TRUE = 0x100, Z3_OP_FALSE, Z3_OP_EQ, Z3_OP_DISTINCT,
  Z3_OP_ITE, Z3_OP_AND, Z3_OP_OR, Z3_OP_IFF,
  Z3_OP_XOR, Z3_OP_NOT, Z3_OP_IMPLIES, Z3_OP_LE = 0x200,
  Z3_OP_GE, Z3_OP_LT, Z3_OP_GT, Z3_OP_ADD,
  Z3_OP_SUB, Z3_OP_UMINUS, Z3_OP_MUL, Z3_OP_DIV,
  Z3_OP_IDIV, Z3_OP_REM, Z3_OP_MOD, Z3_OP_STORE = 0x300,
  Z3_OP_SELECT, Z3_OP_CONST_ARRAY, Z3_OP_ARRAY_DEFAULT, Z3_OP_STORE_ITE,
  Z3_OP_SET_UNION, Z3_OP_SET_INTERSECT, Z3_OP_SET_DIFFERENCE, Z3_OP_SET_COMPLEMENT,
  Z3_OP_SET_SUBSET, Z3_OP_BIT1 = 0x400, Z3_OP_BIT0, Z3_OP_BNEG,
  Z3_OP_BADD, Z3_OP_BSUB, Z3_OP_BMUL, Z3_OP_BSDIV,
  Z3_OP_BUDIV, Z3_OP_BSREM, Z3_OP_BUREM, Z3_OP_BSMOD,
  Z3_OP_BSDIV0, Z3_OP_BUDIV0, Z3_OP_BSREM0, Z3_OP_BUREM0,
  Z3_OP_BSMOD0, Z3_OP_ULEQ, Z3_OP_SLEQ, Z3_OP_UGEQ,
  Z3_OP_SGEQ, Z3_OP_ULT, Z3_OP_SLT, Z3_OP_UGT,
  Z3_OP_SGT, Z3_OP_BAND, Z3_OP_BOR, Z3_OP_BNOT,
  Z3_OP_BXOR, Z3_OP_BNAND, Z3_OP_BNOR, Z3_OP_BXNOR,
  Z3_OP_CONCAT, Z3_OP_SIGN_EXT, Z3_OP_ZERO_EXT, Z3_OP_EXTRACT,
  Z3_OP_REPEAT, Z3_OP_BREDOR, Z3_OP_BREDAND, Z3_OP_BCOMP,
  Z3_OP_BSHL, Z3_OP_BLSHR, Z3_OP_BASHR, Z3_OP_ROTATE_LEFT,
  Z3_OP_ROTATE_RIGHT, Z3_OP_INT2BV, Z3_OP_BV2INT, Z3_OP_UNINTERPRETED
}
 The different kinds of interpreted function kinds. More...
enum  Z3_value_kind {
  Z3_BOOL_VALUE, Z3_NUMERAL_VALUE, Z3_ARRAY_VALUE, Z3_TUPLE_VALUE,
  Z3_UNKNOWN_VALUE = 1000
}
 The different kinds of Z3 values (See Z3_get_value_kind). More...
enum  Z3_error_code {
  Z3_OK, Z3_TYPE_ERROR, Z3_IOB, Z3_INVALID_ARG,
  Z3_PARSER_ERROR, Z3_NO_PARSER, Z3_INVALID_PATTERN
}
 Z3 error codes (See Z3_get_error_code). More...
typedef int Z3_bool
 Z3 Boolean type. It is just an alias for int.
typedef const char * Z3_string
 Z3 string type. It is just an alias for const char *.
typedef void Z3_error_handler (Z3_error_code e)
 Z3 custom error handler (See Z3_set_error_handler).
#define Z3_TRUE   1
 True value. It is just an alias for 1.
#define Z3_FALSE   0
 False value. It is just an alias for 0.

Create configuration

Z3_config Z3_API Z3_mk_config ()
 Create a configuration.
void Z3_API Z3_del_config (__in Z3_config c)
 Delete the given configuration object.
void Z3_API Z3_set_param_value (__in Z3_config c, __in_z Z3_string param_id, __in_z Z3_string param_value)
 Set a configuration parameter.

Create context

Z3_context Z3_API Z3_mk_context (__in Z3_config c)
 Create a logical context using the given configuration.
void Z3_API Z3_del_context (__in Z3_context c)
 Delete the given logical context.
Z3_bool Z3_API Z3_trace_to_file (__in Z3_context c, __in_z Z3_string trace_file)
 Enable trace messages to a file.
void Z3_API Z3_trace_to_stderr (__in Z3_context c)
 Enable trace messages to a standard error.
void Z3_API Z3_trace_to_stdout (__in Z3_context c)
 Enable trace messages to a standard output.
void Z3_API Z3_trace_off (__in Z3_context c)
 Disable trace messages.

Theories

void Z3_API Z3_enable_arithmetic (__in Z3_context c)
 Enable arithmetic theory in the given logical context.
void Z3_API Z3_enable_bv (__in Z3_context c)
 Enable bit-vector theory in the given logical context.
void Z3_API Z3_enable_arrays (__in Z3_context c)
 Enable array theory in the given logical context.
void Z3_API Z3_enable_tuples (__in Z3_context c)
 Enable tuple theory in the given logical context.

Symbols

Z3_symbol Z3_API Z3_mk_int_symbol (__in Z3_context c, __in int i)
 Create a Z3 symbol using an integer.
Z3_symbol Z3_API Z3_mk_string_symbol (__in Z3_context c, __in_z Z3_string s)
 Create a Z3 symbol using a C string.

Types

Z3_type_ast Z3_API Z3_mk_uninterpreted_type (__in Z3_context c, __in Z3_symbol s)
 Create a free (uninterpreted) type using the given name (symbol).
Z3_type_ast Z3_API Z3_mk_bool_type (__in Z3_context c)
 Create the Boolean type.
Z3_type_ast Z3_API Z3_mk_int_type (__in Z3_context c)
 Create an integer type.
Z3_type_ast Z3_API Z3_mk_real_type (__in Z3_context c)
 Create a real type.
Z3_type_ast Z3_API Z3_mk_bv_type (__in Z3_context c, __in unsigned sz)
 Create a bit-vector type of the given size.
Z3_type_ast Z3_API Z3_mk_array_type (__in Z3_context c, __in Z3_type_ast domain, __in Z3_type_ast range)
 Create an array type.
Z3_type_ast Z3_API Z3_mk_tuple_type (__in Z3_context c, __in Z3_symbol mk_tuple_name, __in unsigned num_fields, __in_ecount(num_fields) Z3_symbol const field_names[], __in_ecount(num_fields) Z3_type_ast const field_types[], __out Z3_const_decl_ast *mk_tuple_decl, __out_ecount(num_fields) Z3_const_decl_ast proj_decl[])
 Create a tuple type.

Constants and Applications

Z3_const_decl_ast Z3_API Z3_mk_func_decl (__in Z3_context c, __in Z3_symbol s, __in unsigned domain_size, __in_ecount(domain_size) Z3_type_ast const domain[], __in Z3_type_ast range)
 Declare a constant or function.
Z3_ast Z3_API Z3_mk_app (__in Z3_context c, __in Z3_const_decl_ast d, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
 Create a constant or function application.
Z3_ast Z3_API Z3_mk_const (__in Z3_context c, __in Z3_symbol s, __in Z3_type_ast ty)
 Declare and create a constant.
Z3_ast Z3_API Z3_mk_label (__in Z3_context c, __in Z3_symbol s, Z3_bool is_pos, Z3_ast f)
 Create a labeled formula.
Z3_const_decl_ast Z3_API Z3_mk_fresh_func_decl (__in Z3_context c, __in_z Z3_string prefix, __in unsigned domain_size, __in_ecount(domain_size) Z3_type_ast const domain[], __in Z3_type_ast range)
 Declare a fresh constant or function.
Z3_ast Z3_API Z3_mk_fresh_const (__in Z3_context c, __in_z Z3_string prefix, __in Z3_type_ast ty)
 Declare and create a fresh constant.
Z3_ast Z3_API Z3_mk_true (__in Z3_context c)
 Create an AST node representing true.
Z3_ast Z3_API Z3_mk_false (__in Z3_context c)
 Create an AST node representing false.
Z3_ast Z3_API Z3_mk_eq (__in Z3_context c, __in Z3_ast l, __in Z3_ast r)
 Create an AST node representing l = r.
Z3_ast Z3_API Z3_mk_distinct (__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
 Create an AST node representing distinct(args[0], ..., args[num_args-1]).
Z3_ast Z3_API Z3_mk_not (__in Z3_context c, __in Z3_ast a)
 Create an AST node representing not(a).
Z3_ast Z3_API Z3_mk_ite (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2, __in Z3_ast t3)
 Create an AST node representing an if-then-else: ite(t1, t2, t3).
Z3_ast Z3_API Z3_mk_iff (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Create an AST node representing t1 iff t2.
Z3_ast Z3_API Z3_mk_implies (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Create an AST node representing t1 implies t2.
Z3_ast Z3_API Z3_mk_xor (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Create an AST node representing t1 xor t2.
Z3_ast Z3_API Z3_mk_and (__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
 Create an AST node representing args[0] and ... and args[num_args-1].
Z3_ast Z3_API Z3_mk_or (__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
 Create an AST node representing args[0] or ... or args[num_args-1].
Z3_ast Z3_API Z3_mk_add (__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
 Create an AST node representing args[0] + ... + args[num_args-1].
Z3_ast Z3_API Z3_mk_mul (__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
 Create an AST node representing args[0] * ... * args[num_args-1].
Z3_ast Z3_API Z3_mk_sub (__in Z3_context c, __in unsigned num_args, __in_ecount(num_args) Z3_ast const args[])
 Create an AST node representing args[0] - ... - args[num_args - 1].
Z3_ast Z3_API Z3_mk_lt (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Create less than.
Z3_ast Z3_API Z3_mk_le (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Create less than or equal to.
Z3_ast Z3_API Z3_mk_gt (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Create greater than.
Z3_ast Z3_API Z3_mk_ge (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Create greater than or equal to.
Z3_ast Z3_API Z3_mk_bvnot (__in Z3_context c, __in Z3_ast t1)
 Bitwise negation.
Z3_ast Z3_API Z3_mk_bvand (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Bitwise and.
Z3_ast Z3_API Z3_mk_bvor (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Bitwise or.
Z3_ast Z3_API Z3_mk_bvxor (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Bitwise exclusive-or.
Z3_ast Z3_API Z3_mk_bvnand (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Bitwise nand.
Z3_ast Z3_API Z3_mk_bvnor (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Bitwise nor.
Z3_ast Z3_API Z3_mk_bvxnor (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Bitwise xnor.
Z3_ast Z3_API Z3_mk_bvneg (__in Z3_context c, __in Z3_ast t1)
 Standard two's complement unary minus.
Z3_ast Z3_API Z3_mk_bvadd (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Standard two's complement addition.
Z3_ast Z3_API Z3_mk_bvsub (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Standard two's complement subtraction.
Z3_ast Z3_API Z3_mk_bvmul (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Standard two's complement multiplication.
Z3_ast Z3_API Z3_mk_bvudiv (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Unsigned division.
Z3_ast Z3_API Z3_mk_bvsdiv (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Two's complement signed division.
Z3_ast Z3_API Z3_mk_bvurem (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Unsigned remainder.
Z3_ast Z3_API Z3_mk_bvsrem (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Two's complement signed remainder (sign follows dividend).
Z3_ast Z3_API Z3_mk_bvsmod (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Two's complement signed remainder (sign follows divisor).
Z3_ast Z3_API Z3_mk_bvult (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Unsigned less than.
Z3_ast Z3_API Z3_mk_bvslt (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Two's complement signed less than.
Z3_ast Z3_API Z3_mk_bvule (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Unsigned less than or equal to.
Z3_ast Z3_API Z3_mk_bvsle (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Two's complement signed less than or equal to.
Z3_ast Z3_API Z3_mk_bvuge (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Unsigned greater than or equal to.
Z3_ast Z3_API Z3_mk_bvsge (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Two's complement signed greater than or equal to.
Z3_ast Z3_API Z3_mk_bvugt (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Unsigned greater than.
Z3_ast Z3_API Z3_mk_bvsgt (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Two's complement signed greater than.
Z3_ast Z3_API Z3_mk_concat (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Concatenate the given bit-vectors.
Z3_ast Z3_API Z3_mk_extract (__in Z3_context c, __in unsigned high, __in unsigned low, __in Z3_ast t1)
 Extract the bits high down to low from a bitvector of size m to yield a new bitvector of size n, where n = high - low + 1.
Z3_ast Z3_API Z3_mk_sign_ext (__in Z3_context c, __in unsigned i, __in Z3_ast t1)
 Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector.
Z3_ast Z3_API Z3_mk_zero_ext (__in Z3_context c, __in unsigned i, __in Z3_ast t1)
 Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i, where m is the size of the given bit-vector.
Z3_ast Z3_API Z3_mk_bvshl (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Shift left.
Z3_ast Z3_API Z3_mk_bvlshr (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Logical shift right.
Z3_ast Z3_API Z3_mk_bvashr (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Arithmetic shift right.
Z3_ast Z3_API Z3_mk_rotate_left (__in Z3_context c, __in unsigned i, __in Z3_ast t1)
 Rotate bits of t1 to the left i times.
Z3_ast Z3_API Z3_mk_rotate_right (__in Z3_context c, __in unsigned i, __in Z3_ast t1)
 Rotate bits of t1 to the right i times.
Z3_ast Z3_API Z3_mk_select (__in Z3_context c, __in Z3_ast a, __in Z3_ast i)
 Array read.
Z3_ast Z3_API Z3_mk_store (__in Z3_context c, __in Z3_ast a, __in Z3_ast i, __in Z3_ast v)
 Array update.

Numerals

Z3_ast Z3_API Z3_mk_numeral (__in Z3_context c, __in_z Z3_string numeral, __in Z3_type_ast ty)
 Create a numeral of a given type.
Z3_ast Z3_API Z3_mk_int (__in Z3_context c, __in int v, __in Z3_type_ast ty)
 Create a numeral of a given type.
Z3_ast Z3_API Z3_mk_unsigned_int (__in Z3_context c, __in unsigned v, __in Z3_type_ast ty)
 Create a numeral of a given type.
Z3_ast Z3_API Z3_mk_int64 (__in Z3_context c, __in long long v, __in Z3_type_ast ty)
 Create a numeral of a given type.
Z3_ast Z3_API Z3_mk_unsigned_int64 (__in Z3_context c, __in unsigned long long v, __in Z3_type_ast ty)
 Create a numeral of a given type.

Quantifiers

Z3_pattern_ast Z3_API Z3_mk_pattern (__in Z3_context c, __in unsigned num_patterns, __in_ecount(num_patterns) Z3_ast const terms[])
 Create a pattern for quantifier instantiation.
Z3_ast Z3_API Z3_mk_bound (__in Z3_context c, __in unsigned index, __in Z3_type_ast ty)
 Create a bound variable.
Z3_ast Z3_API Z3_mk_forall (__in Z3_context c, __in unsigned weight, __in unsigned num_patterns, __in_ecount(num_patterns) Z3_pattern_ast const patterns[], __in unsigned num_decls, __in_ecount(num_decls) Z3_type_ast const types[], __in_ecount(num_decls) Z3_symbol const decl_names[], __in Z3_ast body)
 Create a forall formula.
Z3_ast Z3_API Z3_mk_exists (__in Z3_context c, __in unsigned weight, __in unsigned num_patterns, __in_ecount(num_patterns) Z3_pattern_ast const patterns[], __in unsigned num_decls, __in_ecount(num_decls) Z3_type_ast const types[], __in_ecount(num_decls) Z3_symbol const decl_names[], __in Z3_ast body)
 Create an exists formula. Similar to Z3_mk_forall.
Z3_ast Z3_mk_quantifier (Z3_context c, Z3_bool is_forall, unsigned weight, unsigned num_patterns, Z3_pattern_ast const *patterns, unsigned num_no_patterns, Z3_ast const *no_patterns, unsigned num_decls, Z3_type_ast const *types, Z3_symbol const *decl_names, Z3_ast body)
 Create a quantifier - universal or existential, with pattern hints.

Accessors

Z3_symbol_kind Z3_API Z3_get_symbol_kind (__in Z3_context c, __in Z3_symbol s)
 Return Z3_INT_SYMBOL if the symbol was constructed using Z3_mk_int_symbol, and Z3_STRING_SYMBOL if the symbol was constructed using Z3_mk_string_symbol.
int Z3_API Z3_get_symbol_int (__in Z3_context c, __in Z3_symbol s)
 Return the symbol int value.
Z3_string Z3_API Z3_get_symbol_string (__in Z3_context c, __in Z3_symbol s)
 Return the symbol name.
Z3_bool Z3_API Z3_is_eq (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
 Return Z3_TRUE if the two given AST nodes are equal.
Z3_ast_kind Z3_API Z3_get_ast_kind (__in Z3_context c, __in Z3_ast a)
 Return the kind of the given AST.
Z3_bool Z3_API Z3_is_expr (__in Z3_context c, __in Z3_ast a)
 Return Z3_TRUE if the given AST is an expression.
Z3_const_decl_ast Z3_API Z3_get_const_ast_decl (__in Z3_context c, __in Z3_const_ast a)
 Return the declaration of a constant or function application.
unsigned Z3_API Z3_get_const_ast_num_args (__in Z3_context c, __in Z3_const_ast a)
 Return the number of argument of an application. If t is an constant, then the number of arguments is 0.
Z3_ast Z3_API Z3_get_const_ast_arg (__in Z3_context c, __in Z3_const_ast a, __in unsigned i)
 Return the i-th argument of the given application.
Z3_symbol Z3_API Z3_get_decl_name (__in Z3_context c, __in Z3_const_decl_ast d)
 Return the constant declaration name as a symbol.
Z3_symbol Z3_API Z3_get_type_name (__in Z3_context c, __in Z3_type_ast d)
 Return the type name as a symbol.
Z3_type_ast Z3_API Z3_get_type (__in Z3_context c, __in Z3_ast a)
 Return the type of an AST node.
unsigned Z3_API Z3_get_domain_size (__in Z3_context c, __in Z3_const_decl_ast d)
 Return the number of parameters of the given declaration.
Z3_type_ast Z3_API Z3_get_domain (__in Z3_context c, __in Z3_const_decl_ast d, __in unsigned i)
 Return the type of the i-th parameter of the given function declaration.
Z3_type_ast Z3_API Z3_get_range (__in Z3_context c, __in Z3_const_decl_ast d)
 Return the range of the given declaration.
Z3_type_kind Z3_API Z3_get_type_kind (__in Z3_context c, __in Z3_type_ast t)
 Return the type kind (e.g., array, tuple, int, bool, etc).
unsigned Z3_API Z3_get_bv_type_size (__in Z3_context c, __in Z3_type_ast t)
 Return the size of the given bit-vector type.
Z3_type_ast Z3_API Z3_get_array_type_domain (__in Z3_context c, __in Z3_type_ast t)
 Return the domain of the given array type.
Z3_type_ast Z3_API Z3_get_array_type_range (__in Z3_context c, __in Z3_type_ast t)
 Return the range of the given array type.
Z3_const_decl_ast Z3_API Z3_get_tuple_type_mk_decl (__in Z3_context c, __in Z3_type_ast t)
 Return the constructor declaration of the given tuple type.
unsigned Z3_API Z3_get_tuple_type_num_fields (__in Z3_context c, __in Z3_type_ast t)
 Return the number of fields of the given tuple type.
Z3_const_decl_ast Z3_API Z3_get_tuple_type_field_decl (__in Z3_context c, __in Z3_type_ast t, __in unsigned i)
 Return the i-th field declaration (i.e., projection function declaration) of the given tuple type.
Z3_decl_kind Z3_API Z3_get_decl_kind (__in Z3_context c, __in Z3_const_decl_ast d)
 Return declaration kind corresponding to declaration.
Z3_string Z3_API Z3_get_numeral_ast_value (__in Z3_context c, __in Z3_ast a)
 Return numeral value, as a string of a numeric constant term.
Z3_bool Z3_API Z3_get_numeral_ast_value_small (__in Z3_context c, __in Z3_ast a, __out long long *n, __out long long *d)
 Return numeral value, as a pair of 64 bit numbers if the representation fits.
unsigned Z3_API Z3_get_index_value (__in Z3_context c, __in Z3_ast a)
 Return index of de-Brujin bound variable.
Z3_bool Z3_API Z3_is_quantifier_forall (__in Z3_context c, __in Z3_ast a)
 Determine if quantifier is universal.
unsigned Z3_API Z3_get_quantifier_weight (__in Z3_context c, __in Z3_ast a)
 Obtain weight of quantifier.
unsigned Z3_API Z3_get_quantifier_num_patterns (__in Z3_context c, __in Z3_ast a)
 Return number of patterns used in quantifier.
Z3_pattern_ast Z3_API Z3_get_quantifier_pattern_ast (__in Z3_context c, __in Z3_ast a, unsigned i)
 Return i'th pattern.
Z3_symbol Z3_API Z3_get_quantifier_bound_name (__in Z3_context c, __in Z3_ast a, unsigned i)
 Return symbol of the i'th bound variable.
Z3_type_ast Z3_API Z3_get_quantifier_bound_type_ast (__in Z3_context c, __in Z3_ast a, unsigned i)
 Return type of the i'th bound variable.
Z3_ast Z3_API Z3_get_quantifier_body (__in Z3_context c, __in Z3_ast a)
 Return body of quantifier.
unsigned Z3_API Z3_get_quantifier_num_bound (__in Z3_context c, __in Z3_ast a)
 Return number of bound variables of quantifier.
unsigned Z3_API Z3_get_pattern_num_terms (__in Z3_context c, __in Z3_pattern_ast p)
 Return number of terms in pattern.
Z3_ast Z3_API Z3_get_pattern_ast (__in Z3_context c, __in Z3_pattern_ast p, __in unsigned idx)
 Return i'th ast in pattern.

Coercions

Z3_ast Z3_API Z3_type_ast_to_ast (__in Z3_context c, __in Z3_type_ast a)
 Convert a TYPE_AST into an AST. This is just type casting.
Z3_ast Z3_API Z3_const_ast_to_ast (__in Z3_context c, __in Z3_const_ast a)
 Convert a CONST_AST into an AST. This is just type casting.
Z3_ast Z3_API Z3_const_decl_ast_to_ast (__in Z3_context c, __in Z3_const_decl_ast a)
 Convert a CONST_DECL_AST into an AST. This is just type casting.
Z3_ast Z3_API Z3_pattern_ast_to_ast (__in Z3_context c, __in Z3_pattern_ast p)
 Convert a PATTERN_AST into an AST. This is just type casting.
Z3_const_ast Z3_API Z3_to_const_ast (__in Z3_context c, __in Z3_ast a)
 Convert an AST into a CONST_AST. This is just type casting.
Z3_numeral_ast Z3_API Z3_to_numeral_ast (__in Z3_context c, __in Z3_ast a)
 Convert an AST into a NUMERAL_AST. This is just type casting.

Constraints

void Z3_API Z3_push (__in Z3_context c)
 Create a backtracking point.
void Z3_API Z3_pop (__in Z3_context c, __in unsigned num_scopes)
 Backtrack.
void Z3_API Z3_assert_cnstr (__in Z3_context c, __in Z3_ast a)
 Assert a constraing into the logical context.
Z3_lbool Z3_API Z3_check_and_get_model (__in Z3_context c, __out Z3_model *m)
 Check whether the given logical context is consistent or not.
Z3_lbool Z3_API Z3_check (__in Z3_context c)
 Check whether the given logical context is consistent or not.
void Z3_API Z3_del_model (__in Z3_model m)
 Delete a model object.
Z3_ast Z3_API Z3_simplify (__in Z3_context c, __in Z3_ast a)
 Interface to simplifier.
Z3_labels Z3_API Z3_get_relevant_labels (__in Z3_context c)
 Retrieve the set of labels that were relevant in the context of the current satisfied context.
void Z3_API Z3_del_labels (__in Z3_context c, __in Z3_labels lbls)
 Delete a labels context.
unsigned Z3_API Z3_get_num_labels (__in Z3_context c, __in Z3_labels lbls)
 Retrieve the number of label symbols that were returned.
Z3_symbol Z3_API Z3_get_label_symbol (__in Z3_context c, __in Z3_labels lbls, __in unsigned idx)
 Retrieve label symbol at idx.
void Z3_API Z3_disable_label (__in Z3_context c, __in Z3_labels lbls, __in unsigned idx)
 Disable label.
void Z3_API Z3_block_labels (__in Z3_context c, __in Z3_labels lbls)
 Block subsequent checks using the remaining enabled labels.

Model navigation

unsigned Z3_API Z3_get_model_num_constants (__in Z3_context c, __in Z3_model m)
 Return the number of constants assigned by the given model.
Z3_const_decl_ast Z3_API Z3_get_model_constant (__in Z3_context c, __in Z3_model m, __in unsigned i)
 Return the i-th constant in the given model.
Z3_value Z3_API Z3_get_value (__in Z3_context c, __in Z3_model m, __in Z3_const_decl_ast decl)
 Return the value of the given constant or application in the given model.
Z3_type_ast Z3_API Z3_get_value_type (__in Z3_context c, __in Z3_value v)
 Return the value type.
Z3_value_kind Z3_API Z3_get_value_kind (__in Z3_context c, __in Z3_value v)
 Return the value kind (numeral, array, tuple, etc).
Z3_string Z3_API Z3_get_numeral_value_string (__in Z3_context c, __in Z3_value v)
 Return a numeral value as a string. The representation is stored in decimal notation.
Z3_bool Z3_API Z3_get_numeral_value_int (__in Z3_context c, __in Z3_value v, __out int *i)
 Similar to Z3_get_numeral_value_string, but only succeeds if the value can fit in a machine int. Return Z3_TRUE if the call succeeded.
Z3_bool Z3_API Z3_get_numeral_value_uint (__in Z3_context c, __in Z3_value v, __out unsigned *u)
 Similar to Z3_get_numeral_value_string, but only succeeds if the value can fit in a machine unsigned int. Return Z3_TRUE if the call succeeded.
Z3_bool Z3_API Z3_get_numeral_value_uint64 (__in Z3_context c, __in Z3_value v, __out unsigned long long *u)
 Similar to Z3_get_numeral_value_string, but only succeeds if the value can fit in a machine unsigned long long int. Return Z3_TRUE if the call succeeded.
Z3_bool Z3_API Z3_get_numeral_value_int64 (__in Z3_context c, __in Z3_value v, __out long long *i)
 Similar to Z3_get_numeral_value_string, but only succeeds if the value can fit in a machine long long int. Return Z3_TRUE if the call succeeded.
Z3_bool Z3_API Z3_get_bool_value_bool (__in Z3_context c, __in Z3_value v)
 Return the value of v as a Boolean value.
Z3_const_decl_ast Z3_API Z3_get_tuple_value_mk_decl (__in Z3_context c, __in Z3_value v)
 Return the constructor declaration of the given tuple value.
unsigned Z3_API Z3_get_tuple_value_num_fields (__in Z3_context c, __in Z3_value v)
 Return the number of fields of the given tuple value.
Z3_value Z3_API Z3_get_tuple_value_field (__in Z3_context c, __in Z3_value v, __in unsigned i)
 Return the i-th field of the given tuple value.
unsigned Z3_API Z3_get_array_value_size (__in Z3_context c, __in Z3_value v)
 An array values is represented as a dictionary plus a default (else) value. This function returns the size of the dictionary.
Z3_value Z3_API Z3_get_array_value_else (__in Z3_context c, __in Z3_value v)
 An array values is represented as a dictionary plus a default (else) value. This function returns the default (else) value.
Z3_value Z3_API Z3_get_array_value_entry_index (__in Z3_context c, __in Z3_value v, __in unsigned i)
 An array values is represented as a dictionary plus a default (else) value. Each dictionary entry is a pair (index, value). This function return the i-th index of the array.
Z3_value Z3_API Z3_get_array_value_entry_value (__in Z3_context c, __in Z3_value v, __in unsigned i)
 An array values is represented as a dictionary plus a default (else) value. Each dictionary entry is a pair (index, value). This function return the i-th value of the array.
unsigned Z3_API Z3_get_model_num_funcs (__in Z3_context c, __in Z3_model m)
 Return the number of function interpretations in the given model.
Z3_bool Z3_API Z3_is_model_func_internal (__in Z3_context c, __in Z3_model m, __in unsigned i)
 Return Z3_true if the i-th function in the model is internal.
Z3_const_decl_ast Z3_API Z3_get_model_func_decl (__in Z3_context c, __in Z3_model m, __in unsigned i)
 Return the declaration of the i-th function in the given model.
Z3_value Z3_API Z3_get_model_func_else (__in Z3_context c, __in Z3_model m, __in unsigned i)
 Return the 'else' value of the i-th function interpretation in the given model.
unsigned Z3_API Z3_get_model_func_num_entries (__in Z3_context c, __in Z3_model m, __in unsigned i)
 Return the number of entries of the i-th function interpretation in the given model.
unsigned Z3_API Z3_get_model_func_entry_num_args (__in Z3_context c, __in Z3_model m, __in unsigned i, __in unsigned j)
 Return the number of arguments of the j-th entry of the i-th function interpretation in the given model.
Z3_value Z3_API Z3_get_model_func_entry_arg (__in Z3_context c, __in Z3_model m, __in unsigned i, __in unsigned j, __in unsigned k)
 Return the k-th argument of the j-th entry of the i-th function interpretation in the given model.
Z3_value Z3_API Z3_get_model_func_entry_value (__in Z3_context c, __in Z3_model m, __in unsigned i, __in unsigned j)
 Return the return value of the j-th entry of the i-th function interpretation in the given model.
Z3_bool Z3_API Z3_eval (__in Z3_context c, __in Z3_model m, __in Z3_ast t, __out Z3_value *v)
 Evaluate the AST node t in the given model. Return Z3_TRUE if succeeded, and store the result in v.

Timers

void Z3_API Z3_set_soft_timeout (__in Z3_context c, __in unsigned t)
 Set a soft timeout in seconds.
void Z3_API Z3_reset_soft_timeout (__in Z3_context c)
 Disable soft timeouts.

Interaction logging.

Z3_bool Z3_API Z3_open_log (__in Z3_context c, __in_z Z3_string filename)
 Log interaction to a file.
void Z3_API Z3_close_log (__in Z3_context c)
 Close interaction log.

String conversion

Z3_string Z3_API Z3_ast_to_string (__in Z3_context c, __in Z3_ast a)
 Convert the given AST node into a string.
Z3_string Z3_API Z3_model_to_string (__in Z3_context c, __in Z3_model m)
 Convert the given model into a string.
Z3_string Z3_API Z3_value_to_string (__in Z3_context c, __in Z3_value v)
 Convert the given (model) value into a string.
Z3_string Z3_API Z3_context_to_string (__in Z3_context c)
 Convert the given logical context into a string.

Parser interface

void Z3_API Z3_parse_smtlib_string (__in Z3_context c, __in_z Z3_string str, __in unsigned num_types, __in_ecount(num_types) Z3_symbol type_names[], __in_ecount(num_types) Z3_type_ast types[], __in unsigned num_decls, __in_ecount(num_decls) Z3_symbol decl_names[], __in_ecount(num_decls) Z3_const_decl_ast decls[])
 Parse the given string using the SMT-LIB parser.
void Z3_API Z3_parse_smtlib_file (__in Z3_context c, __in_z Z3_string file_name, __in unsigned num_types, __in_ecount(num_types) Z3_symbol type_names[], __in_ecount(num_types) Z3_type_ast types[], __in unsigned num_decls, __in_ecount(num_decls) Z3_symbol decl_names[], __in_ecount(num_decls) Z3_const_decl_ast decls[])
 Similar to Z3_parse_smtlib_string, but reads the benchmark from a file.
unsigned Z3_API Z3_get_smtlib_num_formulas (__in Z3_context c)
 Return the number of SMTLIB formulas parsed by the last call to Z3_parse_smtlib_string or Z3_parse_smtlib_file.
Z3_ast Z3_API Z3_get_smtlib_formula (__in Z3_context c, __in unsigned i)
 Return the i-th formula parsed by the last call to Z3_parse_smtlib_string or Z3_parse_smtlib_file.
unsigned Z3_API Z3_get_smtlib_num_assumptions (__in Z3_context c)
 Return the number of SMTLIB assumptions parsed by Z3_parse_smtlib_string or Z3_parse_smtlib_file.
Z3_ast Z3_API Z3_get_smtlib_assumption (__in Z3_context c, __in unsigned i)
 Return the i-th assumption parsed by the last call to Z3_parse_smtlib_string or Z3_parse_smtlib_file.
unsigned Z3_API Z3_get_smtlib_num_decls (__in Z3_context c)
 Return the number of declarations parsed by Z3_parse_smtlib_string or Z3_parse_smtlib_file.
Z3_const_decl_ast Z3_API Z3_get_smtlib_decl (__in Z3_context c, __in unsigned i)
 Return the i-th declaration parsed by the last call to Z3_parse_smtlib_string or Z3_parse_smtlib_file.

Error Handling

Z3_error_code Z3_API Z3_get_error_code (__in Z3_context c)
 Return the error code for the last API call.
void Z3_API Z3_set_error_handler (__in Z3_context c, __in Z3_error_handler h)
 Register a Z3 error handler.
Z3_string Z3_API Z3_get_error_msg (__in Z3_error_code err)
 Return a string describing the given error code.

Miscellaneous

void Z3_API Z3_get_version (__out unsigned *major, __out unsigned *minor, __out unsigned *build_number, __out unsigned *revision_number)
 Return Z3 version number information.
Z3_bool Z3_API Z3_type_check (__in Z3_context c, __in Z3_ast t)
 Return Z3_TRUE if t is type correct.
unsigned Z3_API Z3_get_allocation_size ()
 Return the amount of memory allocated by Z3.

Define Documentation

#define Z3_FALSE   0

False value. It is just an alias for 0.

Definition at line 73 of file z3_api.h.

Referenced by bitvector_example1(), prove_example1(), prove_example2(), and tuple_example1().

#define Z3_TRUE   1

True value. It is just an alias for 1.

Definition at line 68 of file z3_api.h.

Referenced by array_example1(), parser_example3(), prove_example1(), prove_example2(), quantifier_example1(), tuple_example1(), and Context::TypeCheck().

Typedef Documentation

typedef int Z3_bool

Z3 Boolean type. It is just an alias for int.

Definition at line 44 of file z3_api.h.

typedef void Z3_error_handler(Z3_error_code e)

Z3 custom error handler (See Z3_set_error_handler).

Definition at line 276 of file z3_api.h.

typedef const char* Z3_string

Z3 string type. It is just an alias for const char *.

Definition at line 56 of file z3_api.h.

Enumeration Type Documentation

enum Z3_ast_kind

The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.

Enumerator:
Z3_NUMERAL_AST 
Z3_CONST_DECL_AST 
Z3_CONST_AST 
Z3_TYPE_AST 
Z3_VAR_AST 
Z3_PATTERN_AST 
Z3_QUANTIFIER_AST 
Z3_UNKNOWN_AST 

Definition at line 126 of file z3_api.h.

00127 {
00128     Z3_NUMERAL_AST,       
00129     Z3_CONST_DECL_AST,    
00130     Z3_CONST_AST,         
00131     Z3_TYPE_AST,          
00132     Z3_VAR_AST,          
00133     Z3_PATTERN_AST,       
00134     Z3_QUANTIFIER_AST,    
00135