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

Z3An Efficient SMT Solver

OCaml API (Index)

Module Z3: Sections

type config
type context
type ast
type type_ast
type const_decl_ast
type const_ast
type numeral_ast
type pattern_ast
type symbol
type value
type parameter
type model
type labels

type enum_1 =
| L_FALSE
| L_UNDEF
| L_TRUE
type lbool = enum_1

type enum_2 =
| INT_SYMBOL
| STRING_SYMBOL
type symbol_kind = enum_2

type enum_3 =
| UNINTERPRETED_TYPE
| BOOL_TYPE
| INT_TYPE
| REAL_TYPE
| BV_TYPE
| ARRAY_TYPE
| TUPLE_TYPE
| UNKNOWN_TYPE
type type_kind = enum_3

type enum_4 =
| NUMERAL_AST
| CONST_DECL_AST
| CONST_AST
| TYPE_AST
| VAR_AST
| PATTERN_AST
| QUANTIFIER_AST
| UNKNOWN_AST
type ast_kind = enum_4

type enum_5 =
| OP_TRUE
| OP_FALSE
| OP_EQ
| OP_DISTINCT
| OP_ITE
| OP_AND
| OP_OR
| OP_IFF
| OP_XOR
| OP_NOT
| OP_IMPLIES
| OP_LE
| OP_GE
| OP_LT
| OP_GT
| OP_ADD
| OP_SUB
| OP_UMINUS
| OP_MUL
| OP_DIV
| OP_IDIV
| OP_REM
| OP_MOD
| OP_STORE
| OP_SELECT
| OP_CONST_ARRAY
| OP_ARRAY_DEFAULT
| OP_STORE_ITE
| OP_SET_UNION
| OP_SET_INTERSECT
| OP_SET_DIFFERENCE
| OP_SET_COMPLEMENT
| OP_SET_SUBSET
| OP_BIT1
| OP_BIT0
| OP_BNEG
| OP_BADD
| OP_BSUB
| OP_BMUL
| OP_BSDIV
| OP_BUDIV
| OP_BSREM
| OP_BUREM
| OP_BSMOD
| OP_BSDIV0
| OP_BUDIV0
| OP_BSREM0
| OP_BUREM0
| OP_BSMOD0
| OP_ULEQ
| OP_SLEQ
| OP_UGEQ
| OP_SGEQ
| OP_ULT
| OP_SLT
| OP_UGT
| OP_SGT
| OP_BAND
| OP_BOR
| OP_BNOT
| OP_BXOR
| OP_BNAND
| OP_BNOR
| OP_BXNOR
| OP_CONCAT
| OP_SIGN_EXT
| OP_ZERO_EXT
| OP_EXTRACT
| OP_REPEAT
| OP_BREDOR
| OP_BREDAND
| OP_BCOMP
| OP_BSHL
| OP_BLSHR
| OP_BASHR
| OP_ROTATE_LEFT
| OP_ROTATE_RIGHT
| OP_INT2BV
| OP_BV2INT
| OP_UNINTERPRETED
type decl_kind = enum_5

type enum_6 =
| BOOL_VALUE
| NUMERAL_VALUE
| ARRAY_VALUE
| TUPLE_VALUE
| UNKNOWN_VALUE
type value_kind = enum_6


Create configuration


val mk_config : unit -> config
Summary: Create a configuration.

Configurations are created in order to assign parameters prior to creating contexts for Z3 interaction. For example, if the users whishes to use model generation, then call:

set_param_value cfg "MODEL" "true"


val del_config : config -> unit
Summary: Delete the given configuration object.


val set_param_value : config -> string -> string -> unit
Summary: Set a configuration parameter.

The list of all configuration parameters can be obtained using the Z3 executable: 

       z3.exe -ini?




Create context


val mk_context : config -> context
Summary: Create a logical context using the given configuration.

After a context is created, the configuration cannot be changed. All main interaction with Z3 happens in the context of a context.


val del_context : context -> unit
Summary: Delete the given logical context.


val trace_to_file : context -> string -> bool
Summary: Enable trace messages to a file

When trace messages are enabled, Z3 will record the operations performed on a context in the given file file. Return TRUE if the file was opened successfully, and FALSE otherwise.


val trace_to_stderr : context -> unit
Summary: Enable trace messages to a standard error.


val trace_to_stdout : context -> unit
Summary: Enable trace messages to a standard output.


val trace_off : context -> unit
Summary: Disable trace messages.




Theories


val enable_arithmetic : context -> unit
Summary: Enable arithmetic theory in the given logical context.
val enable_bv : context -> unit
Summary: Enable bit-vector theory in the given logical context.
val enable_arrays : context -> unit
Summary: Enable array theory in the given logical context.
val enable_tuples : context -> unit
Summary: Enable tuple theory in the given logical context.


Symbols


val mk_int_symbol : context -> int -> symbol
Summary: Create a Z3 symbol using an integer.

Symbols are used to name several term and type constructors.


val mk_string_symbol : context -> string -> symbol
Summary: Create a Z3 symbol using a C string.

Symbols are used to name several term and type constructors.




Types


val mk_uninterpreted_type : context -> symbol -> type_ast
Summary: Create a free (uninterpreted) type using the given name (symbol).

Two free types are considered the same iff the have the same name.

val mk_bool_type : context -> type_ast
Summary: Create the Boolean type.

This type is used to create propositional variables and predicates.

val mk_int_type : context -> type_ast
Summary: Create an integer type.

This type is not the int type found in programming languages. A machine integer can be represented using bit-vectors. The function Z3.mk_bv_type creates a bit-vector type.


val mk_real_type : context -> type_ast
Summary: Create a real type.

This type is not a floating point number. Z3 does not have support for floating point numbers yet.

val mk_bv_type : context -> int -> type_ast
Summary: Create a bit-vector type of the given size.

This type can also be seen as a machine integer.


val mk_array_type : context -> type_ast -> type_ast -> type_ast
Summary: Create an array type.

We usually represent the array type as: domain -> range . Arrays are usually used to model the heap/memory in software verification.


val mk_tuple_type : context ->
symbol ->
symbol array ->
type_ast array ->
type_ast * const_decl_ast * const_decl_ast array
Summary: Create a tuple type.

mk_tuple_type c name field_names field_types creates a tuple with a constructor named name, a n fields, where n is the size of the arrays field_names and field_types.



Constants and Applications


val mk_func_decl : context ->
symbol -> type_ast array -> type_ast -> const_decl_ast
Summary: Declare a constant or function.

mk_func_decl c n d r creates a function with name n, domain d, and range r. The arity of the function is the size of the array d.

After declaring a constant or function, the function Z3.mk_app can be used to create a constant or function application.


val mk_app : context -> const_decl_ast -> ast array -> ast
Summary: Create a constant or function application.


val mk_const : context -> symbol -> type_ast -> ast
Summary: Declare and create a constant.

mk_const c s t is a shorthand for mk_app c (mk_func_decl c s [||] t) [||]


val mk_label : context -> symbol -> bool -> ast -> ast
Summary: Create a labeled formula.

A label behaves as an identity function, so the truth value of the labeled formula is unchanged. Labels are used for identifying useful sub-formulas when generating counter-examples.

val mk_fresh_func_decl : context -> string -> type_ast array -> type_ast -> const_decl_ast
Summary: Declare a fresh constant or function.

Z3 will generate an unique name for this function declaration.


val mk_fresh_const : context -> string -> type_ast -> ast
Summary: Declare and create a fresh constant.

mk_fresh_const c p t is a shorthand for mk_app c (mk_fresh_func_decl c p [||] t) [||].


val mk_true : context -> ast
Summary: Create an AST node representing true.
val mk_false : context -> ast
Summary: Create an AST node representing false.
val mk_eq : context -> ast -> ast -> ast
Summary: [ mk_eq c l r ] Create an AST node representing l = r .

The nodes l and r must have the same type.

val mk_distinct : context -> ast array -> ast
Summary: [ mk_distinct c [| t_1; ...; t_n |] ] Create an AST node represeting a distinct construct. It is used for declaring the arguments t_i pairwise distinct.

All arguments must have the same type.


val mk_not : context -> ast -> ast
Summary: [ mk_not c a ] Create an AST node representing not(a) .

The node a must have Boolean type.

val mk_ite : context -> ast -> ast -> ast -> ast
Summary: [ mk_ite c t1 t2 t2 ] Create an AST node representing an if-then-else: ite(t1, t2, t3) .

The node t1 must have Boolean type, t2 and t3 must have the same type. The type of the new node is equal to the type of t2 and t3.

val mk_iff : context -> ast -> ast -> ast
Summary: [ mk_iff c t1 t2 ] Create an AST node representing t1 iff t2 .

The nodes t1 and t2 must have Boolean type.

val mk_implies : context -> ast -> ast -> ast
Summary: [ mk_implies c t1 t2 ] Create an AST node representing t1 implies t2 .

The nodes t1 and t2 must have Boolean type.

val mk_xor : context -> ast -> ast -> ast
Summary: [ mk_xor c t1 t2 ] Create an AST node representing t1 xor t2 .

The nodes t1 and t2 must have Boolean type.

val mk_and : context -> ast array -> ast
Summary: [ mk_and c [| t_1; ...; t_n |] ] Create the conjunction: t_1 and ... and t_n.

All arguments must have Boolean type.


val mk_or : context -> ast array -> ast
Summary: [ mk_or c [| t_1; ...; t_n |] ] Create the disjunction: t_1 or ... or t_n.

All arguments must have Boolean type.


val mk_add : context -> ast array -> ast
Summary: [ mk_add c [| t_1; ...; t_n |] ] Create the term: t_1 + ... + t_n.

All arguments must have int or real type.


val mk_mul : context -> ast array -> ast
Summary: [ mk_mul c [| t_1; ...; t_n |] ] Create the term: t_1 * ... * t_n.

All arguments must have int or real type.


val mk_sub : context -> ast array -> ast
Summary: [ mk_sub c [| t_1; ...; t_n |] ] Create the term: t_1 - ... - t_n.

All arguments must have int or real type.


val mk_lt : context -> ast -> ast -> ast
Summary: [ mk_lt c t1 t2 ] Create less than.

The nodes t1 and t2 must have the same type, and must be int or real.

val mk_le : context -> ast -> ast -> ast
Summary: [ mk_le c t1 t2 ] Create less than or equal to.

The nodes t1 and t2 must have the same type, and must be int or real.

val mk_gt : context -> ast -> ast -> ast
Summary: [ mk_gt c t1 t2 ] Create greater than.

The nodes t1 and t2 must have the same type, and must be int or real.

val mk_ge : context -> ast -> ast -> ast
Summary: [ mk_ge c t1 t2 ] Create greater than or equal to.

The nodes t1 and t2 must have the same type, and must be int or real.

val mk_bvnot : context -> ast -> ast
Summary: [ mk_bvneg c t1 ] Bitwise negation.

The node t1 must have a bit-vector type.

val mk_bvand : context -> ast -> ast -> ast
Summary: [ mk_bvand c t1 t2 ] Bitwise and.

The nodes t1 and t2 must have the same bit-vector type.

val mk_bvor : context -> ast -> ast -> ast
Summary: [ mk_bvor c t1 t2 ] Bitwise or.

The nodes t1 and t2 must have the same bit-vector type.

val mk_bvxor : context -> ast -> ast -> ast
Summary: [ mk_bvxor c t1 t2 ] Bitwise exclusive-or.

The nodes t1 and t2 must have the same bit-vector type.

val mk_bvnand : context -> ast -> ast -> ast
Summary: [ mk_bvnand c t1 t2 ] Bitwise nand.

The nodes t1 and t2 must have the same bit-vector type.

val mk_bvnor : context -> ast -> ast -> ast
Summary: [ mk_bvnor c t1 t2 ] Bitwise nor.

The nodes t1 and t2 must have the same bit-vector type.

val mk_bvxnor : context -> ast -> ast -> ast
Summary: [ mk_bvxnor c t1 t2 ] Bitwise xnor.

The nodes t1 and t2 must have the same bit-vector type.

val mk_bvneg : context -> ast -> ast
Summary: [ mk_bvneg c t1 ] Standard two's complement unary minus.

The node t1 must have bit-vector type.

val mk_bvadd : context -> ast -> ast -> ast
Summary: [ mk_bvadd c t1 t2 ] Standard two's complement addition.

The nodes t1 and t2 must have the same bit-vector type.

val mk_bvsub : context -> ast -> ast -> ast
Summary: [ mk_bvsub c t1 t2 ] Standard two's complement subtraction.

The nodes t1 and t2 must have the same bit-vector type.

val mk_bvmul : context -> ast -> ast -> ast
Summary: [ mk_bvmul c t1 t2 ] Standard two's complement multiplication.

The nodes t1 and t2 must have the same bit-vector type.

val mk_bvudiv : context -> ast -> ast -> ast
Summary: [ mk_bvudiv c t1 t2 ] Unsigned division.

It is defined as the floor of t1/t2 if t2 is different from zero. If t2 is zero, then the result is undefined.

The nodes t1 and t2 must have the same bit-vector type.

val mk_bvsdiv : context -> ast -> ast -> ast
Summary: [ mk_bvsdiv c t1 t2 ] Two's complement signed division.

It is defined in the following way:

If t2 is zero, then the result is undefined.

The nodes t1 and t2 must have the same bit-vector type.

val mk_bvurem : context -> ast -> ast -> ast
Summary: [ mk_bvurem c t1 t2 ] Unsigned remainder.

It is defined as t1 - (t1 /u t2) * t2 , where /u represents unsigned int division.

If t2 is zero, then the result is undefined.

The nodes t1 and t2 must have the same bit-vector type.

val mk_bvsrem : context -> ast -> ast -> ast
Summary: [ mk_bvsrem c t1 t2 ] Two's complement signed remainder (sign follows dividend).

It is defined as t1 - (t1 /s t2) * t2 , where /s represents signed division. The most significant bit (sign) of the result is equal to the most significant bit of t1.

If t2 is zero, then the result is undefined.

The nodes t1 and t2 must have the same bit-vector type.


val mk_bvsmod : context -> ast -> ast -> ast
Summary: [ mk_bvsmod c t1 t2 ] Two's complement signed remainder (sign follows divisor).

If t2 is zero, then the result is undefined.

The nodes t1 and t2 must have the same bit-vector type.


val mk_bvult : context -> ast -> ast -> ast
Summary: [ mk_bvult c t1 t2 ] Unsigned less than.

The nodes t1 and t2 must have the same bit-vector type.

val mk_bvslt : context -> ast -> ast -> ast
Summary: [ mk_bvslt c t1 t2 ] Two's complement signed less than.

It abbreviates: 

      (or (and (= (extract[|m-1|:|m-1|] s) bit1)
               (= (extract[|m-1|:|m-1|] t) bit0))
          (and (= (extract[|m-1|:|m-1|] s) (extract[|m-1|:|m-1|] t))
               (bvult s t)))

The nodes t1 and t2 must have the same bit-vector type.

val mk_bvule : context -> ast -> ast -> ast
Summary: [ mk_bvule c t1 t2 ] Unsigned less than or equal to.

The nodes t1 and t2 must have the same bit-vector type.

val mk_bvsle : context -> ast -> ast -> ast
Summary: [ mk_bvsle c t1 t2 ] Two's complement signed less than or equal to.

The nodes t1 and t2 must have the same bit-vector type.

val mk_bvuge : context -> ast -> ast -> ast
Summary: [ mk_bvuge c t1 t2 ] Unsigned greater than or equal to.

The nodes t1 and t2 must have the same bit-vector type.

val mk_bvsge : context -> ast -> ast -> ast
Summary: [ mk_bvsge c t1 t2 ] Two's complement signed greater than or equal to.

The nodes t1 and t2 must have the same bit-vector type.

val mk_bvugt : context -> ast -> ast -> ast
Summary: [ mk_bvugt c t1 t2 ] Unsigned greater than.

The nodes t1 and t2 must have the same bit-vector type.

val mk_bvsgt : context -> ast -> ast -> ast
Summary: [ mk_bvsgt c t1 t2 ] Two's complement signed greater than.

The nodes t1 and t2 must have the same bit-vector type.

val mk_concat : context -> ast -> ast -> ast
Summary: [ mk_concat c t1 t2 ] Concatenate the given bit-vectors.

The nodes t1 and t2 must have (possibly different) bit-vector types

The result is a bit-vector of size n1+n2 , where n1 (n2) is the size of t1 (t2).

val mk_extract : context -> int -> int -> ast -> ast
Summary: [ mk_extract c high low 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 .

The node t1 must have a bit-vector type.

val mk_sign_ext : context -> int -> ast -> ast
Summary: [ mk_sign_ext c i 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.

The node t1 must have a bit-vector type.

val mk_zero_ext : context -> int -> ast -> ast
Summary: [ mk_zero_ext c i t1 ] Extend the given bit-vector with zeros to the (unsigned int) equivalent bitvector of size m+i , where m is the size of the given bit-vector.

The node t1 must have a bit-vector type.

val mk_bvshl : context -> ast -> ast -> ast
Summary: [ mk_bvshl c t1 t2 ] Shift left.

It is equivalent to multiplication by 2^x where x is the value of the third argument.

The nodes t1 and t2 must have the same bit-vector type.

val mk_bvlshr : context -> ast -> ast -> ast
Summary: [ mk_bvlshr c t1 t2 ] Logical shift right.

It is equivalent to unsigned int division by 2^x where x is the value of the third argument.

The nodes t1 and t2 must have the same bit-vector type.

val mk_bvashr : context -> ast -> ast -> ast
Summary: [ mk_bvashr c t1 t2 ] Arithmetic shift right.

It is like logical shift right except that the most significant bits of the result always copy the most significant bit of the second argument.

The nodes t1 and t2 must have the same bit-vector type.

val mk_rotate_left : context -> int -> ast -> ast
Summary: [ mk_rotate_left c i t1 ] Rotate bits of t1 to the left i times.

The node t1 must have a bit-vector type.

val mk_rotate_right : context -> int -> ast -> ast
Summary: [ mk_rotate_right c i t1 ] Rotate bits of t1 to the right i times.

The node t1 must have a bit-vector type.

val mk_select : context -> ast -> ast -> ast
Summary: [ mk_select c a i ] Array read.

The node a must have an array type domain -> range , and i must have the type domain. The type of the result is range.


val mk_store : context -> ast -> ast -> ast -> ast
Summary: [ mk_store c a i v ] Array update.

The node a must have an array type domain -> range , i must have type domain, v must have type range. The type of the result is domain -> range .




Numerals


val mk_numeral : context -> string -> type_ast -> ast
Summary: Create a numeral of a given type.


val mk_int : context -> int -> type_ast -> ast
Summary: Create a numeral of a given type.

This function can be use to create numerals that fit in a machine integer. It is slightly faster than Z3.mk_numeral since it is not necessary to parse a string.


val mk_unsigned_int : context -> int -> type_ast -> ast
Summary: Create a numeral of a given type.

This function can be use to create numerals that fit in a machine unsinged integer. It is slightly faster than Z3.mk_numeral since it is not necessary to parse a string.




Quantifiers


val mk_pattern : context -> ast array -> pattern_ast
Summary: Create a pattern for quantifier instantiation.

Z3 uses pattern matching to instantiate quantifiers. If a pattern is not provided for a quantifier, then Z3 will automatically compute a set of patterns for it. However, for optimal performance, the user should provide the patterns.

Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than one term, it is a called a multi-pattern.

In general, one can pass in a list of (multi-)patterns in the quantifier constructor.


val mk_bound : context -> int -> type_ast -> ast
Summary: Create a bound variable.

Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain the meaning of de-Bruijn indices by indicating the compilation process from non-de-Bruijn formulas to de-Bruijn format. 

 
       abs(forall (x1) phi) = forall (x1) abs1(phi, x1, 0)
       abs(forall (x1, x2) phi) = abs(forall (x1) abs(forall (x2) phi))
       abs1(x, x, n) = b_n
       abs1(y, x, n) = y
       abs1(f(t1,...,tn), x, n) = f(abs1(t1,x,n), ..., abs1(tn,x,n))
       abs1(forall (x1) phi, x, n) = forall (x1) (abs1(phi, x, n+1))

The last line is significant: the index of a bound variable is different depending on the scope in which it appears. The deeper x appears, the higher is its index.


val mk_forall : context ->
int ->
pattern_ast array ->
type_ast array -> symbol array -> ast -> ast
Summary: Create a forall formula.

mk_forall c w p t n b creates a forall formula, where w is the weight, p is an array of patterns, t is an array with the types of the bound variables, n is an array with the 'names' of the bound variables, and b is the body of the quantifier. Quantifiers are associated with weights indicating the importance of using the quantifier during instantiation.


val mk_exists : context ->
int ->
pattern_ast array ->
type_ast array -> symbol array -> ast -> ast
Summary: Create an exists formula. Similar to Z3.mk_forall.


val mk_quantifier : context ->
bool ->
int ->
int ->
pattern_ast ->
int -> ast -> int -> type_ast -> symbol -> ast -> ast
Summary: Create a quantifier - universal or existential, with pattern hints.




Accessors


val get_symbol_kind : context -> symbol -> symbol_kind
Summary: Return INT_SYMBOL if the symbol was constructed using Z3.mk_int_symbol, and STRING_SYMBOL if the symbol was constructed using Z3.mk_string_symbol.
val get_symbol_int : context -> symbol -> int
Summary: [ get_symbol_int c s ] Return the symbol int value.


val get_symbol_string : context -> symbol -> string
Summary: [ get_symbol_string c s ] Return the symbol name.


val is_eq : context -> ast -> ast -> bool
Summary: Return TRUE if the two given AST nodes are equal.
val get_ast_kind : context -> ast -> ast_kind
Summary: Return the kind of the given AST.
val is_expr : context -> ast -> bool
Summary: Return TRUE if the given AST is an expression.

An expression is a constant, application, numeral, bound variable, or quantifier.

val get_const_ast_decl : context -> const_ast -> const_decl_ast
Summary: Return the declaration of a constant or function application.
val get_const_ast_num_args : context -> const_ast -> int
Summary: [ get_const_ast_num_args c a ] Return the number of argument of an application. If t is an constant, then the number of arguments is 0.
val get_const_ast_arg : context -> const_ast -> int -> ast
Summary: [ get_const_ast_arg c a i ] Return the i-th argument of the given application.


val get_decl_name : context -> const_decl_ast -> symbol
Summary: Return the constant declaration name as a symbol.
val get_type_name : context -> type_ast -> symbol
Summary: Return the type name as a symbol.
val get_type : context -> ast -> type_ast
Summary: Return the type of an AST node.

The AST node must be a constant, application, numeral, bound variable, or quantifier.


val get_domain_size : context -> const_decl_ast -> int
Summary: Return the number of parameters of the given declaration.


val get_domain : context -> const_decl_ast -> int -> type_ast
Summary: [ get_domain c d i ] Return the type of the i-th parameter of the given function declaration.


val get_range : context -> const_decl_ast -> type_ast
Summary: [ get_range c d ] Return the range of the given declaration.

If d is a constant (i.e., has zero arguments), then this function returns the type of the constant.

val get_type_kind : context -> type_ast -> type_kind
Summary: Return the type kind (e.g., array, tuple, int, bool, etc).


val get_bv_type_size : context -> type_ast -> int
Summary: [ get_bv_type_size c t ] Return the size of the given bit-vector type.


val get_array_type_domain : context -> type_ast -> type_ast
Summary: [ get_array_type_domain c t ] Return the domain of the given array type.


val get_array_type_range : context -> type_ast -> type_ast
Summary: [ get_array_type_range c t ] Return the range of the given array type.


val get_tuple_type_mk_decl : context -> type_ast -> const_decl_ast
Summary: [ get_tuple_type_mk_decl c t ] Return the constructor declaration of the given tuple type.


val get_tuple_type_num_fields : context -> type_ast -> int
Summary: [ get_tuple_type_num_fields c t ] Return the number of fields of the given tuple type.


val get_tuple_type_field_decl : context -> type_ast -> int -> const_decl_ast
Summary: [ get_tuple_type_field_decl c t i ] Return the i-th field declaration (i.e., projection function declaration) of the given tuple type.


val get_decl_kind : context -> const_decl_ast -> decl_kind
Summary: Return declaration kind corresponding to declaration.
val get_numeral_ast_value : context -> ast -> string
Summary: Return numeral value, as a string of a numeric constant term


val get_numeral_ast_value_small : context -> ast -> bool * int64 * int64
Summary: Return numeral value, as a pair of 64 bit numbers if the representation fits.

Preturn TRUE if the numeral value fits in 64 bit numerals, FALSE otherwise.


val get_index_value : context -> ast -> int
Summary: Return index of de-Brujin bound variable.


val is_quantifier_forall : context -> ast -> bool
Summary: Determine if quantifier is universal.


val get_quantifier_weight : context -> ast -> int
Summary: Obtain weight of quantifier.


val get_quantifier_num_patterns : context -> ast -> int
Summary: Return number of patterns used in quantifier.


val get_quantifier_pattern_ast : context -> ast -> int -> pattern_ast
Summary: Return i'th pattern.


val get_quantifier_bound_name : context -> ast -> int -> symbol
Summary: Return symbol of the i'th bound variable.


val get_quantifier_bound_type_ast : context -> ast -> int -> type_ast
Summary: Return type of the i'th bound variable.


val get_quantifier_body : context -> ast -> ast
Summary: Return body of quantifier.


val get_quantifier_num_bound : context -> ast -> int
Summary: Return number of bound variables of quantifier.


val get_pattern_num_terms : context -> pattern_ast -> int
Summary: Return number of terms in pattern.
val get_pattern_ast : context -> pattern_ast -> int -> ast
Summary: Return i'th ast in pattern.


Coercions


val type_ast_to_ast : context -> type_ast -> ast
Summary: Convert a TYPE_AST into an AST. This is just type casting.
val const_ast_to_ast : context -> const_ast -> ast
Summary: Convert a CONST_AST into an AST. This is just type casting.
val const_decl_ast_to_ast : context -> const_decl_ast -> ast
Summary: Convert a CONST_DECL_AST into an AST. This is just type casting.
val pattern_ast_to_ast : context -> pattern_ast -> ast
Summary: Convert a PATTERN_AST into an AST. This is just type casting.
val to_const_ast : context -> ast -> const_ast
Summary: Convert an AST into a CONST_AST. This is just type casting.


val to_numeral_ast : context -> ast -> numeral_ast
Summary: Convert an AST into a NUMERAL_AST. This is just type casting.




Constraints


val push : context -> unit
Summary: Create a backtracking point.

The logical context can be viewed as a stack of contexts. The scope level is the number of elements on this stack. The stack of contexts is simulated using trail (undo) stacks.


val pop : context -> int -> unit
Summary: Backtrack.

Restores the context from the top of the stack, and pops it off the stack. Any changes to the logical context (by Z3.assert_cnstr or other functions) between the matching Z3.push and pop operators are flushed, and the context is completely restored to what it was right before the Z3.push.


val assert_cnstr : context -> ast -> unit
Summary: Assert a constraing into the logical context.

After one assertion, the logical context may become inconsistent.

The functions Z3.check or Z3.check_and_get_model should be used to check whether the logical context is consistent or not.


val check_and_get_model : context -> lbool * model
Summary: Check whether the given logical context is consistent or not.

If the logical context is not unsatisfiable (i.e., the return value is different from L_FALSE) and model construction is enabled (see Z3.mk_config), then a model is stored in m. Otherwise, the value 0 is stored in m. The caller is responsible for deleting the model using the function Z3.del_model.


val check : context -> lbool
Summary: Check whether the given logical context is consistent or not.

The function Z3.check_and_get_model should be used when models are needed.


val del_model : model -> unit
Summary: Delete a model object.


val simplify : context -> ast -> ast
Summary: Interface to simplifier.

Provides an interface to the AST simplifier used by Z3. It allows clients to piggyback on top of the AST simplifier for their own term manipulation.

val get_relevant_labels : context -> labels
Summary: Retrieve the set of labels that were relevant in the context of the current satisfied context.


val del_labels : context -> labels -> unit
Summary: Delete a labels context.


val get_num_labels : context -> labels -> int
Summary: Retrieve the number of label symbols that were returned.


val get_label_symbol : context -> labels -> int -> symbol
Summary: Retrieve label symbol at idx.
val disable_label : context -> labels -> int -> unit
Summary: Disable label.

The disabled label is not going to be used when blocking the subsequent search.


val block_labels : context -> labels -> unit
Summary: Block subsequent checks using the remaining enabled labels.


Model navigation


val get_model_num_constants : context -> model -> int
Summary: Return the number of constants assigned by the given model.


val get_model_constant : context -> model -> int -> const_decl_ast
Summary: [ get_model_constant c m i ] Return the i-th constant in the given model.


val get_value : context -> model -> const_decl_ast -> value
Summary: Return the value of the given constant or application in the given model.


val get_value_type : context -> value -> type_ast
Summary: Return the value type.


val get_value_kind : context -> value -> value_kind
Summary: Return the value kind (numeral, array, tuple, etc).

NUMERAL_VALUE stores the value of different types (int, real, bv, and uninterpreted).

val get_numeral_value_string : context -> value -> string
Summary: [ get_numeral_value_string c v ] Return a numeral value as a string. The representation is stored in decimal notation.


val get_numeral_value_int : context -> value -> bool * int
Summary: [ get_numeral_value_int c v ] Similar to Z3.get_numeral_value_string, but only succeeds if the value can fit in a machine int. Return TRUE if the call succeeded.


val get_numeral_value_uint : context -> value -> bool * int
Summary: [ get_numeral_value_uint c v ] Similar to Z3.get_numeral_value_string, but only succeeds if the value can fit in a machine unsigned int int. Return TRUE if the call succeeded.


val get_bool_value_bool : context -> value -> bool
Summary: [ get_bool_value_bool c v ] Return the value of v as a Boolean value.


val get_tuple_value_mk_decl : context -> value -> const_decl_ast
Summary: [ get_tuple_value_mk_decl c v ] Return the constructor declaration of the given tuple value.


val get_tuple_value_num_fields : context -> value -> int
Summary: [ get_tuple_value_num_fields c v ] Return the number of fields of the given tuple value.


val get_tuple_value_field : context -> value -> int -> value
Summary: [ get_tuple_value_field c v i ] Return the i-th field of the given tuple value.


val get_array_value_size : context -> value -> int
Summary: [ get_array_value_size c v ] An array values is represented as a dictionary plus a default (else) value. This function returns the size of the dictionary.


val get_array_value_else : context -> value -> value
Summary: [ get_array_value_else c v ] An array values is represented as a dictionary plus a default (else) value. This function returns the default (else) value.


val get_array_value_entry_index : context -> value -> int -> value
Summary: [ get_array_value_entry_index c v 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.

If v contains an entry (index, value), then

v[index] = value.


val get_array_value_entry_value : context -> value -> int -> value
Summary: [ get_array_value_entry_value c v 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.

If v contains an entry (index, value), then

v[index] = value.


val get_model_num_funcs : context -> model -> int
Summary: Return the number of function interpretations in the given model.

A function interpretation is represented as a finite map and an 'else' value. Each entry in the finite map represents the value of a function given a set of arguments.


val is_model_func_internal : context -> model -> int -> bool
Summary: [ is_model_func_internal c m i ] Return true if the i-th function in the model is \em internal.

Internal functions are created by Z3, and their interpretations are not usually useful for users.


val get_model_func_decl : context -> model -> int -> const_decl_ast
Summary: [ get_model_func_decl c m i ] Return the declaration of the i-th function in the given model.


val get_model_func_else : context -> model -> int -> value
Summary: [ get_model_func_else c m i ] Return the 'else' value of the i-th function interpretation in the given model.

A function interpretation is represented as a finite map and an 'else' value.


val get_model_func_num_entries : context -> model -> int -> int
Summary: [ get_model_func_num_entries c m i ] Return the number of entries of the i-th function interpretation in the given model.

A function interpretation is represented as a finite map and an 'else' value.


val get_model_func_entry_num_args : context -> model -> int -> int -> int
Summary: [ get_model_func_entry_num_args c m i j ] Return the number of arguments of the j-th entry of the i-th function interpretation in the given model.

A function interpretation is represented as a finite map and an 'else' value. This function returns the j-th entry of this map.

An entry represents the value of a function given a set of arguments.


val get_model_func_entry_arg : <