Home Docs Download Mail FAQ Awards Status MSR

Z3An Efficient SMT Solver

OCaml API (Index)

Module Z3: Sections

Z3

Module Z3


module Z3: sig  end

type symbol
type literals
type theory
type theory_data
type config
type context
type sort
type func_decl
type ast
type app
type pattern
type model
type constructor
type constructor_list
type params
type goal
type tactic
type probe
type stats
type solver
type ast_vector
type ast_map
type apply_result
type func_interp
type func_entry
type fixedpoint

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 =
| PARAMETER_INT
| PARAMETER_DOUBLE
| PARAMETER_RATIONAL
| PARAMETER_SYMBOL
| PARAMETER_SORT
| PARAMETER_AST
| PARAMETER_FUNC_DECL
type parameter_kind = enum_3

type enum_4 =
| UNINTERPRETED_SORT
| BOOL_SORT
| INT_SORT
| REAL_SORT
| BV_SORT
| ARRAY_SORT
| DATATYPE_SORT
| RELATION_SORT
| FINITE_DOMAIN_SORT
| UNKNOWN_SORT
type sort_kind = enum_4

type enum_5 =
| NUMERAL_AST
| APP_AST
| VAR_AST
| QUANTIFIER_AST
| SORT_AST
| FUNC_DECL_AST
| UNKNOWN_AST
type ast_kind = enum_5

type enum_6 =
| OP_TRUE
| OP_FALSE
| OP_EQ
| OP_DISTINCT
| OP_ITE
| OP_AND
| OP_OR
| OP_IFF
| OP_XOR
| OP_NOT
| OP_IMPLIES
| OP_OEQ
| OP_ANUM
| OP_AGNUM
| 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_TO_REAL
| OP_TO_INT
| OP_IS_INT
| OP_POWER
| OP_STORE
| OP_SELECT
| OP_CONST_ARRAY
| OP_ARRAY_MAP
| OP_ARRAY_DEFAULT
| OP_SET_UNION
| OP_SET_INTERSECT
| OP_SET_DIFFERENCE
| OP_SET_COMPLEMENT
| OP_SET_SUBSET
| OP_AS_ARRAY
| OP_BNUM
| 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_EXT_ROTATE_LEFT
| OP_EXT_ROTATE_RIGHT
| OP_INT2BV
| OP_BV2INT
| OP_CARRY
| OP_XOR3
| OP_PR_UNDEF
| OP_PR_TRUE
| OP_PR_ASSERTED
| OP_PR_GOAL
| OP_PR_MODUS_PONENS
| OP_PR_REFLEXIVITY
| OP_PR_SYMMETRY
| OP_PR_TRANSITIVITY
| OP_PR_TRANSITIVITY_STAR
| OP_PR_MONOTONICITY
| OP_PR_QUANT_INTRO
| OP_PR_DISTRIBUTIVITY
| OP_PR_AND_ELIM
| OP_PR_NOT_OR_ELIM
| OP_PR_REWRITE
| OP_PR_REWRITE_STAR
| OP_PR_PULL_QUANT
| OP_PR_PULL_QUANT_STAR
| OP_PR_PUSH_QUANT
| OP_PR_ELIM_UNUSED_VARS
| OP_PR_DER
| OP_PR_QUANT_INST
| OP_PR_HYPOTHESIS
| OP_PR_LEMMA
| OP_PR_UNIT_RESOLUTION
| OP_PR_IFF_TRUE
| OP_PR_IFF_FALSE
| OP_PR_COMMUTATIVITY
| OP_PR_DEF_AXIOM
| OP_PR_DEF_INTRO
| OP_PR_APPLY_DEF
| OP_PR_IFF_OEQ
| OP_PR_NNF_POS
| OP_PR_NNF_NEG
| OP_PR_NNF_STAR
| OP_PR_CNF_STAR
| OP_PR_SKOLEMIZE
| OP_PR_MODUS_PONENS_OEQ
| OP_PR_TH_LEMMA
| OP_RA_STORE
| OP_RA_EMPTY
| OP_RA_IS_EMPTY
| OP_RA_JOIN
| OP_RA_UNION
| OP_RA_WIDEN
| OP_RA_PROJECT
| OP_RA_FILTER
| OP_RA_NEGATION_FILTER
| OP_RA_RENAME
| OP_RA_COMPLEMENT
| OP_RA_SELECT
| OP_RA_CLONE
| OP_FD_LT
| OP_LABEL
| OP_LABEL_LIT
| OP_UNINTERPRETED
type decl_kind = enum_6

type enum_7 =
| NO_FAILURE
| UNKNOWN
| TIMEOUT
| MEMOUT_WATERMARK
| CANCELED
| NUM_CONFLICTS
| THEORY
| QUANTIFIERS
type search_failure = enum_7

type enum_8 =
| PRINT_SMTLIB_FULL
| PRINT_LOW_LEVEL
| PRINT_SMTLIB_COMPLIANT
| PRINT_SMTLIB2_COMPLIANT
type ast_print_mode = enum_8

type enum_9 =
| OK
| SORT_ERROR
| IOB
| INVALID_ARG
| PARSER_ERROR
| NO_PARSER
| INVALID_PATTERN
| MEMOUT_FAIL
| FILE_ACCESS_ERROR
| INTERNAL_FATAL
| INVALID_USAGE
| DEC_REF_ERROR
| EXCEPTION
type error_code = enum_9

type enum_10 =
| GOAL_PRECISE
| GOAL_UNDER
| GOAL_OVER
| GOAL_UNDER_OVER
type goal_prec = enum_10


Types

Most of the types in the API are abstract.




lbool Lifted Boolean type: false, undefined, true.


symbol In Z3, a symbol can be represented using integers and strings (See Z3.get_symbol_kind).




parameter_kind The different kinds of parameters that can be associated with function symbols.


sort_kind The different kinds of Z3 types (See Z3.get_sort_kind).


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




decl_kind The different kinds of interpreted function kinds.

Example: T1: (R a b) T2: (R c b) T3: (R c d) trans* T1 T2 T3: (R a d) R must be a symmetric and transitive relation.

Assuming that this proof object is a proof for (R s t), then a proof checker must check if it is possible to prove (R s t) using the antecedents, symmetry and transitivity. That is, if there is a path from s to t, if we view every antecedent (R a b) as an edge between a and b.

T1: (~ p q) quant-intro T1: (~ (forall (x) p) (forall (x) q))

(= (f a (g c d)) (g (f a c) (f a d)))

If f and g are associative, this proof also justifies the following equality:

(= (f (g a b) (g c d)) (g (f a c) (f a d) (f b c) (f b d)))

where each f and g can have arbitrary number of arguments.

This proof object has no antecedents. Remark. This rule is used by the CNF conversion pass and instantiated by f = or, and g = and.

T1: (and l_1 ... l_n) and-elim T1: l_i T1: (not (or l_1 ... l_n)) not-or-elim T1: (not l_i)

This proof object has no antecedents. The conclusion of a rewrite rule is either an equality (= t s), an equivalence (iff t s), or equi-satisfiability (~ t s). Remark: if f is bool, then = is iff.

Examples: (= (+ x 0) x) (= (+ x 1 2) (+ 3 x)) (iff (or x false) x)

(iff (forall (x_1 ... x_m) (and p_1x_1 ... x_m ... p_nx_1 ... x_m)) (and (forall (x_1 ... x_m) p_1x_1 ... x_m) ... (forall (x_1 ... x_m) p_nx_1 ... x_m))) This proof object has no antecedents.

It is used to justify the elimination of unused variables. This proof object has no antecedents.

This proof object has no antecedents.

Several variables can be eliminated simultaneously.

T1: false lemma T1: (or (not l_1) ... (not l_n)) This proof object has one antecedent: a hypothetical proof for false. It converts the proof in a proof for (or (not l_1) ... (not l_n)), when T1 contains the hypotheses: l_1, ..., l_n.

comm: (= (f a b) (f b a))

f is a commutative operator.

This proof object has no antecedents. Remark: if f is bool, then = is iff.

(or (not (and p q)) p) (or (not (and p q)) q) (or (not (and p q r)) p) (or (not (and p q r)) q) (or (not (and p q r)) r) ... (or (and p q) (not p) (not q)) (or (not (or p q)) p q) (or (or p q) (not p)) (or (or p q) (not q)) (or (not (iff p q)) (not p) q) (or (not (iff p q)) p (not q)) (or (iff p q) (not p) (not q)) (or (iff p q) p q) (or (not (ite a b c)) (not a) b) (or (not (ite a b c)) a c) (or (ite a b c) (not a) (not b)) (or (ite a b c) a (not c)) (or (not (not a)) (not a)) (or (not a) a) This proof object has no antecedents. Note: all axioms are propositional tautologies. Note also that 'and' and 'or' can take multiple arguments. You can recover the propositional tautologies by unfolding the Boolean connectives in the axioms a small bounded number of steps (=3).

When e is of Boolean type: def-intro: (and (or n (not e)) (or (not n) e))

or: def-intro: (or (not n) e) when e only occurs positively.

When e is of the form (ite cond th el): def-intro: (and (or (not cond) (= n th)) (or cond (= n el)))

Otherwise: def-intro: (= n e)

This proof object is only used if the parameter PROOF_MODE is 1.

This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.

sk: (~ (not (forall x (p x y))) (not (p (sk y) y))) sk: (~ (exists x (p x y)) (p (sk y) y))

This proof object has no antecedents.

The theory lemma function comes with one or more parameters. The first parameter indicates the name of the theory. For the theory of arithmetic, additional parameters provide hints for checking the theory lemma. The hints for arithmetic are:

target = filter_by_negation(pos, neg, columns)

where columns are pairs c1, d1, .., cN, dN of columns from pos and neg, such that target are elements in x in pos, such that there is no y in neg that agrees with x on the columns c1, d1, .., cN, dN.




search_failure The different kinds of search failure types.




ast_print_mode Z3 pretty printing modes (See Z3.set_ast_print_mode).




error_code Z3 error codes




goal_prec A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving and transforming Goals. Some of these transformations apply under/over approximations.





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 wishes 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 context using the given configuration.

After a context is created, the configuration cannot be changed, although some parameters can be changed using Z3.update_param_value. All main interaction with Z3 happens in the context of a context.


val interrupt : context -> unit
Summary: Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers, simplifiers and tactics.
val mk_context_rc : config -> context
Summary: Create a context using the given configuration. This function is similar to Z3.mk_context. However, in the context returned by this function, the user is responsible for managing ast reference counters. Managing reference counters is a burden and error-prone, but allows the user to use the memory more efficiently. The user must invoke Z3.inc_ref for any ast returned by Z3, and Z3.dec_ref whenever the ast is not needed anymore. This idiom is similar to the one used in BDD (binary decision diagrams) packages such as CUDD.

Remark: sort, func_decl, app, pattern are ast's.

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 inc_ref : context -> ast -> unit
Summary: Increment the reference counter of the given AST. The context c should have been created using Z3.mk_context_rc. This function is a NOOP if c was created using Z3.mk_context.
val dec_ref : context -> ast -> unit
Summary: Decrement the reference counter of the given AST. The context c should have been created using Z3.mk_context_rc. This function is a NOOP if c was created using Z3.mk_context.
val update_param_value : context -> string -> string -> unit
Summary: Update a mutable configuration parameter.

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

       z3.exe -ini?
       

Only a few configuration parameters are mutable once the context is created. The error handler is invoked when trying to modify an immutable parameter.


val get_param_value : context -> string -> string option
Summary: Get a configuration parameter.

Returns None if the parameter value does not exist.




Parameters


val mk_params : context -> params
Summary: Create a Z3 (empty) parameter set. Starting at Z3 4.0, parameter sets are used to configure many components such as: simplifiers, tactics, solvers, etc.
val params_inc_ref : context -> params -> unit
Summary: Increment the reference counter of the given parameter set.
val params_dec_ref : context -> params -> unit
Summary: Decrement the reference counter of the given parameter set.
val params_set_bool : context -> params -> symbol -> bool -> unit
Summary: Add a Boolean parameter k with value v to the parameter set p.
val params_set_uint : context -> params -> symbol -> int -> unit
Summary: Add a unsigned int parameter k with value v to the parameter set p.
val params_set_double : context -> params -> symbol -> float -> unit
Summary: Add a double parameter k with value v to the parameter set p.
val params_set_symbol : context -> params -> symbol -> symbol -> unit
Summary: Add a symbol parameter k with value v to the parameter set p.
val params_to_string : context -> params -> string
Summary: Convert a parameter set into a string. This function is mainly used for printing the contents of a parameter set.


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.

NB. Not all integers can be passed to this function. The legal range of unsigned int integers is 0 to 2^30-1.


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.




Sorts


val mk_uninterpreted_sort : context -> symbol -> sort
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_sort : context -> sort
Summary: Create the Boolean type.

This type is used to create propositional variables and predicates.

val mk_int_sort : context -> sort
Summary: Create the 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_sort creates a bit-vector type.


val mk_real_sort : context -> sort
Summary: Create the real type.

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

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

This type can also be seen as a machine integer.


val mk_finite_domain_sort : context -> symbol -> int64 -> sort
Summary: Create a named finite domain sort.

To create constants that belong to the finite domain, use the APIs for creating numerals and pass a numeric constant together with the sort returned by this call.


val mk_array_sort : context -> sort -> sort -> sort
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_sort : context ->
symbol ->
symbol array ->
sort array -> sort * func_decl * func_decl array
Summary: Create a tuple type.

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

val mk_enumeration_sort : context ->
symbol ->
symbol array -> sort * func_decl array * func_decl array
Summary: Create a enumeration sort.

mk_enumeration_sort c enums creates an enumeration sort with enumeration names enums, it also returns n predicates, where n is the number of enums corresponding to testing whether an element is one of the enumerants.

val mk_list_sort : context ->
symbol ->
sort ->
sort * func_decl * func_decl * func_decl * func_decl *
func_decl * func_decl
Summary: Create a list sort

mk_list_sort c name elem_sort creates a list sort of name, over elements of sort elem_sort.

val mk_constructor : context ->
symbol ->
symbol -> symbol array -> sort array -> int array -> constructor
Summary: Create a constructor.
val del_constructor : context -> constructor -> unit
Summary: Reclaim memory allocated to constructor.
val mk_datatype : context ->
symbol -> constructor array -> sort * constructor array
Summary: Create datatype, such as lists, trees, records, enumerations or unions of records. The datatype may be recursive. Return the datatype sort.
val mk_constructor_list : context -> constructor array -> constructor_list
Summary: Create list of constructors.
val del_constructor_list : context -> constructor_list -> unit
Summary: Reclaim memory allocated for constructor list.

Each constructor inside the constructor list must be independently reclaimed using Z3.del_constructor.

val mk_datatypes : context ->
symbol array ->
constructor_list array -> sort array * constructor_list array
Summary: Create mutually recursive datatypes.


Constants and Applications


val mk_func_decl : context -> symbol -> sort array -> sort -> func_decl
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.

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


val mk_const : context -> symbol -> sort -> 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_fresh_func_decl : context -> string -> sort array -> sort -> func_decl
Summary: Declare a fresh constant or function.

Z3 will generate an unique name for this function declaration.


val mk_fresh_const : context -> string -> sort -> 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) [||].




Propositional Logic and Equality


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.

The distinct construct is used for declaring the arguments pairwise distinct. That is, Forall 0 <= i < j < num_args. not argsi = argsj .

All arguments must have the same sort.


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

The node a must have Boolean sort.

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 sort, t2 and t3 must have the same sort. The sort of the new node is equal to the sort 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 sort.

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 sort.

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 sort.

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 sort.


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 sort.




Arithmetic: Integers and Reals


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 sort.


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 sort.


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 sort.


val mk_unary_minus : context -> ast -> ast
Summary: [ mk_unary_minus c arg ] Create the term: - arg.

The arguments must have int or real type.

val mk_div : context -> ast -> ast -> ast
Summary: [ mk_div c t_1 t_2 ] Create the term: t_1 div t_2.

The arguments must either both have int type or both have real type. If the arguments have int type, then the result type is an int type, otherwise the the result type is real.

val mk_mod : context -> ast -> ast -> ast
Summary: [ mk_mod c t_1 t_2 ] Create the term: t_1 mod t_2.

The arguments must have int type.

val mk_rem : context -> ast -> ast -> ast
Summary: [ mk_rem c t_1 t_2 ] Create the term: t_1 rem t_2.

The arguments must have int type.

val mk_power : context -> ast -> ast -> ast
The 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 sort, 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 sort, 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 sort, 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 sort, and must be int or real.

val mk_int2real : context -> ast -> ast
Summary: [ mk_int2real c t1 ] Coerce an integer to a real.

There is also a converse operation exposed. It follows the semantics prescribed by the SMT-LIB standard.

You can take the floor of a real by creating an auxiliary integer constant k and and asserting mk_int2real(k) <= t1 < mk_int2real(k)+1 .

The node t1 must have sort integer.


val mk_real2int : context -> ast -> ast
Summary: [ mk_real2int c t1 ] Coerce a real to an integer.

The semantics of this function follows the SMT-LIB standard for the function to_int


val mk_is_int : context -> ast -> ast
Summary: [ mk_is_int c t1 ] Check if a real number is an integer.




Bit-vectors


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

The node t1 must have a bit-vector sort.

val mk_bvredand : context -> ast -> ast
Summary: [ mk_bvredand c t1 ] Take conjunction of bits in vector, return vector of length 1.

The node t1 must have a bit-vector sort.

val mk_bvredor : context -> ast -> ast
Summary: [ mk_bvredor c t1 ] Take disjunction of bits in vector, return vector of length 1.

The node t1 must have a bit-vector sort.

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 sort.

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 sort.

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 sort.

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 sort.

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 sort.

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 sort.

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

The node t1 must have bit-vector sort.

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 sort.

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 sort.

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 sort.

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 sort.

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 sort.

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 sort.

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 sort.


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 sort.


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 sort.

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|] t1) bit1)
               (= (extract[|m-1|:|m-1|] t2) bit0))
          (and (= (extract[|m-1|:|m-1|] t1) (extract[|m-1|:|m-1|] t2))
               (bvult t1 t2)))
       

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

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 sort.

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 sort.

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 sort.

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 sort.

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 sort.

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 sort.

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 sorts

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 sort.

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 sort.

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 sort.

val mk_repeat : context -> int -> ast -> ast
Summary: [ mk_repeat c i t1 ] Repeat the given bit-vector up length i .

The node t1 must have a bit-vector sort.

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.

NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.

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

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.

NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.

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

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.

NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.

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

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 sort.

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 sort.

val mk_ext_rotate_left : context -> ast -> ast -> ast
Summary: [ mk_ext_rotate_left c t1 t2 ] Rotate bits of t1 to the left t2 times.

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

val mk_ext_rotate_right : context -> ast -> ast -> ast
Summary: [ mk_ext_rotate_right c t1 t2 ] Rotate bits of t1 to the right t2 times.

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

val mk_int2bv : context -> int -> ast -> ast
Summary: [ mk_int2bv c n t1 ] Create an n bit bit-vector from the integer argument t1.

NB. This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function.

The node t1 must have integer sort.

val mk_bv2int : context -> ast -> bool -> ast
Summary: [ mk_bv2int c t1 is_signed ] Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 is treated as unsigned int. So the result is non-negative and in the range 0..2^N-1 , where N are the number of bits in t1. If is_signed is true, t1 is treated as a signed bit-vector.

NB. This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function.

The node t1 must have a bit-vector sort.

val mk_bvadd_no_overflow : context -> ast -> ast -> bool -> ast
Summary: [ mk_bvadd_no_overflow c t1 t2 is_signed ] Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.

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

val mk_bvadd_no_underflow : context -> ast -> ast -> ast
Summary: [ mk_bvadd_no_underflow c t1 t2 ] Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.

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

val mk_bvsub_no_overflow : context -> ast -> ast -> ast
Summary: [ mk_bvsub_no_overflow c t1 t2 ] Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.

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

val mk_bvsub_no_underflow : context -> ast -> ast -> bool -> ast
Summary: [ mk_bvsub_no_underflow c t1 t2 is_signed ] Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.

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

val mk_bvsdiv_no_overflow : context -> ast -> ast -> ast
Summary: [ mk_bvsdiv_no_overflow c t1 t2 ] Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.

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

val mk_bvneg_no_overflow : context -> ast -> ast
Summary: [ mk_bvneg_no_overflow c t1 ] Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector.

The node t1 must have bit-vector sort.

val mk_bvmul_no_overflow : context -> ast -> ast -> bool -> ast
Summary: [ mk_bvmul_no_overflow c t1 t2 is_signed ] Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.

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

val mk_bvmul_no_underflow : context -> ast -> ast -> ast
Summary: [ mk_bvmul_no_underflow c t1 t2 ] Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflow.

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



Arrays


val mk_select : context -> ast -> ast -> ast
Summary: [ mk_select c a i ] Array read. The argument a is the array and i is the index of the array that gets read.

The node a must have an array sort domain -> range , and i must have the sort domain. The sort 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 sort domain -> range , i must have sort domain, v must have sort range. The sort of the result is domain -> range . The semantics of this function is given by the theory of arrays described in the SMT-LIB standard. See http: The result of this function is an array that is equal to a (with respect to select) on all indices except for i, where it maps to v (and the select of a with respect to i may be a different value).


val mk_const_array : context -> sort -> ast -> ast
Summary: Create the constant array.

The resulting term is an array, such that a select on an arbitrary index produces the value v.

val mk_map : context -> func_decl -> int -> ast -> ast
Summary: [ mk_map f n args ] map f on the the argument arrays.

The n nodes args must be of array sorts domain_i -> range_i . The function declaration f must have type range_1 .. range_n -> range . v must have sort range. The sort of the result is domain_i -> range .


val mk_array_default : context -> ast -> ast
Summary: Access the array default value. Produces the default range value, for arrays that can be represented as finite maps with a default range value.


Sets


val mk_set_sort : context -> sort -> sort
Summary: Create Set type.
val mk_empty_set : context -> sort -> ast
Summary: Create the empty set.
val mk_full_set : context -> sort -> ast
Summary: Create the full set.
val mk_set_add : context -> ast -> ast -> ast
Summary: Add an element to a set.

The first argument must be a set, the second an element.

val mk_set_del : context -> ast -> ast -> ast
Summary: Remove an element to a set.

The first argument must be a set, the second an element.

val mk_set_union : context -> ast array -> ast
Summary: Take the union of a list of sets.
val mk_set_intersect : context -> ast array -> ast
Summary: Take the intersection of a list of sets.
val mk_set_difference : context -> ast -> ast -> ast
Summary: Take the set difference between two sets.
val mk_set_complement : context -> ast -> ast
Summary: Take the complement of a set.
val mk_set_member : context -> ast -> ast -> ast
Summary: Check for set membership.

The first argument should be an element type of the set.

val mk_set_subset : context -> ast -> ast -> ast
Summary: Check for subsetness of sets.


Numerals


val mk_numeral : context -> string -> sort -> ast
Summary: Create a numeral of a given sort.
val mk_real : context -> int -> int -> ast
Summary: Create a real from a fraction.
val mk_int : context -> int -> sort -> ast
Summary: Create a numeral of a given sort.

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_int64 : context -> int64 -> sort -> ast
Summary: Create a numeral of a given sort.

This function can be use to create numerals that fit in a machine long long 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
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 -> sort -> 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 array -> sort array -> symbol array -> ast -> ast
Summary: Create a forall formula. It takes an expression body that contains bound variables of the same sorts as the sorts listed in the array sorts. The bound variables are de-Bruijn indices created using Z3.mk_bound. The array decl_names contains the names that the quantified formula uses for the bound variables. Z3 applies the convention that the last element in the decl_names and sorts array refers to the variable with index 0, the second to last element of decl_names and sorts refers to the variable with index 1, etc.

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 sorts 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 array -> sort array -> symbol array -> ast -> ast
Summary: Create an exists formula. Similar to Z3.mk_forall.


val mk_quantifier : context ->
bool ->
int ->
pattern array -> sort array -> symbol array -> ast -> ast
Summary: Create a quantifier - universal or existential, with pattern hints. See the documentation for Z3.mk_forall for an explanation of the parameters.
val mk_quantifier_ex : context ->
bool ->
int ->
symbol ->
symbol ->
pattern array ->
ast array -> sort array -> symbol array -> ast -> ast
Summary: Create a quantifier - universal or existential, with pattern hints, no patterns, and attributes
val mk_forall_const : context -> int -> app array -> pattern array -> ast -> ast
Summary: Create a universal quantifier using a list of constants that will form the set of bound variables.
val mk_exists_const : context -> int -> app array -> pattern array -> ast -> ast
Summary: Similar to Z3.mk_forall_const.

Summary: Create an existential quantifier using a list of constants that will form the set of bound variables.

val mk_quantifier_const : context ->
bool -> int -> app array -> pattern array -> ast -> ast
Summary: Create a universal or existential quantifier using a list of constants that will form the set of bound variables.
val mk_quantifier_const_ex : context ->
bool ->
int ->
symbol ->
symbol ->
app array -> pattern array -> ast array -> ast -> ast
Summary: Create a universal or existential quantifier using a list of constants that will form the set of bound variables.


Accessors




Symbols


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.




Sorts


val sort_to_ast : context -> sort -> ast
Summary: Convert a sort into ast.
val is_eq_sort : context -> sort -> sort -> bool
Summary: compare sorts.
val get_sort_id : context -> sort -> int
Summary: Return a unique identifier for s.
val get_sort_name : context -> sort -> symbol
Summary: Return the sort name as a symbol.
val get_sort_kind : context -> sort -> sort_kind
Summary: Return the sort kind (e.g., array, tuple, int, bool, etc).




Bitvectors


val get_bv_sort_size : context -> sort -> int
Summary: [ get_bv_sort_size c t ] Return the size of the given bit-vector sort.




Finite Domains


val get_finite_domain_sort_size : context -> sort -> int64 option
Summary: Return the size of the sort in r. Return None if the call failed. That is, get_sort_kind(s) == FINITE_DOMAIN_SORT


Arrays


val get_array_sort_domain : context -> sort -> sort
Summary: [ get_array_sort_domain c t ] Return the domain of the given array sort.


val get_array_sort_range : context -> sort -> sort
Summary: [ get_array_sort_range c t ] Return the range of the given array sort.




Datatypes


val get_tuple_sort_mk_decl : context -> sort -> func_decl
Summary: [ get_tuple_sort_mk_decl c t ] Return the constructor declaration of the given tuple sort.


val get_tuple_sort_num_fields : context -> sort -> int
Summary: [ get_tuple_sort_num_fields c t ] Return the number of fields of the given tuple sort.


val get_tuple_sort_field_decl : context -> sort -> int -> func_decl
Summary: [ get_tuple_sort_field_decl c t i ] Return the i-th field declaration (i.e., projection function declaration) of the given tuple sort.


val get_datatype_sort_num_constructors : context -> sort -> int
Summary: Return number of constructors for datatype.


val get_datatype_sort_constructor : context -> sort -> int -> func_decl
Summary: Return idx'th constructor.


val get_datatype_sort_recognizer : context -> sort -> int -> func_decl
Summary: Return idx'th recognizer.


val get_datatype_sort_constructor_accessor : context -> sort -> int -> int -> func_decl
Summary: Return idx_a'th accessor for the idx_c'th constructor.


val query_constructor : context ->
constructor -> int -> func_decl * func_decl * func_decl array
Summary: Query constructor for declared functions.


Relations


val get_relation_arity : context -> sort -> int
Summary: Return arity of relation.


val get_relation_column : context -> sort -> int -> sort
Summary: Return sort at i'th column of relation sort.




Function Declarations


val func_decl_to_ast : context -> func_decl -> ast
Summary: Convert a func_decl into ast.
val is_eq_func_decl : context -> func_decl -> func_decl -> bool
Summary: compare terms.
val get_func_decl_id : context -> func_decl -> int
Summary: Return a unique identifier for f.
val get_decl_name : context -> func_decl -> symbol
Summary: Return the constant declaration name as a symbol.
val get_decl_kind : context -> func_decl -> decl_kind
Summary: Return declaration kind corresponding to declaration.
val get_domain_size : context -> func_decl -> int
Summary: Return the number of parameters of the given declaration.


val get_arity : context -> func_decl -> int
Summary: Alias for get_domain_size.


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


val get_range : context -> func_decl -> sort
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 sort of the constant.

val get_decl_num_parameters : context -> func_decl -> int
Summary: Return the number of parameters associated with a declaration.
val get_decl_parameter_kind : context -> func_decl -> int -> parameter_kind
Summary: Return the parameter type associated with a declaration.
val get_decl_int_parameter : context -> func_decl -> int -> int
Summary: Return the integer value associated with an integer parameter.


val get_decl_double_parameter : context -> func_decl -> int -> float
Summary: Return the double value associated with an double parameter.


val get_decl_symbol_parameter : context -> func_decl -> int -> symbol
Summary: Return the double value associated with an double parameter.


val get_decl_sort_parameter : context -> func_decl -> int -> sort
Summary: Return the sort value associated with a sort parameter.


val get_decl_ast_parameter : context -> func_decl -> int -> ast
Summary: Return the expresson value associated with an expression parameter.


val get_decl_func_decl_parameter : context -> func_decl -> int -> func_decl
Summary: Return the expresson value associated with an expression parameter.


val get_decl_rational_parameter : context -> func_decl -> int -> string
Summary: Return the rational value, as a string, associated with a rational parameter.




Applications


val app_to_ast : context -> app -> ast
Summary: Convert a app into ast.
val get_app_decl : context -> app -> func_decl
Summary: Return the declaration of a constant or function application.
val get_app_num_args : context -> app -> int
Summary: [ get_app_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_app_arg : context -> app -> int -> ast
Summary: [ get_app_arg c a i ] Return the i-th argument of the given application.




Terms


val is_eq_ast : context -> ast -> ast -> bool
Summary: compare terms.
val get_ast_id : context -> ast -> int
Summary: Return a unique identifier for t. Implicitly used by Pervasives.compare for values of type ast, app, sort, func_decl, and pattern.
val get_ast_hash : context -> ast -> int
Summary: Return a hash code for the given AST. Implicitly used by Hashtbl.hash for values of type ast, app, sort, func_decl, and pattern.
val get_sort : context -> ast -> sort
Summary: Return the sort of an AST node.

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

val is_well_sorted : context -> ast -> bool
Summary: Return true if the given expression t is well sorted.
val get_bool_value : context -> ast -> lbool
Summary: Return L_TRUE if a is true, L_FALSE if it is false, and L_UNDEF otherwise.
val get_ast_kind : context -> ast -> ast_kind
Summary: Return the kind of the given AST.
val is_app : context -> ast -> bool
val is_numeral_ast : context -> ast -> bool
val is_algebraic_number : context -> ast -> bool
Summary: Return true if the give AST is a real algebraic number.
val to_app : context -> ast -> app
Summary: Convert an ast into an APP_AST.


val to_func_decl : context -> ast -> func_decl
Summary: Convert an AST into a FUNC_DECL_AST. This is just type casting.




Numerals


val get_numeral_string : context -> ast -> string
Summary: Return numeral value, as a string of a numeric constant term


val get_numeral_decimal_string : context -> ast -> int -> string
Summary: Return numeral as a string in decimal notation. The result has at most precision decimal places.


val get_numerator : context -> ast -> ast
Summary: Return the numerator (as a numeral AST) of a numeral AST of sort Real.


val get_denominator : context -> ast -> ast
Summary: Return the denominator (as a numeral AST) of a numeral AST of sort Real.


val get_numeral_small : context -> ast -> bool * int64 * int64
Summary: Return numeral value, as a pair of 64 bit numbers if the representation fits.
val get_numeral_int : context -> ast -> bool * int
Summary: [ get_numeral_int c v ] Similar to Z3.get_numeral_string, but only succeeds if the value can fit in a machine int. Return TRUE if the call succeeded.


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


val get_numeral_rational_int64 : context -> ast -> bool * int64 * int64
Summary: [ get_numeral_rational_int64 c x y ] Similar to Z3.get_numeral_string, but only succeeds if the value can fit as a reational number as machine long long int. Return TRUE if the call succeeded.


val get_algebraic_number_lower : context -> ast -> int -> ast
Summary: Return a lower bound for the given real algebraic number. The interval isolating the number is smaller than 1/10^precision. The result is a numeral AST of sort Real.


val get_algebraic_number_upper : context -> ast -> int -> ast
Summary: Return a upper bound for the given real algebraic number. The interval isolating the number is smaller than 1/10^precision. The result is a numeral AST of sort Real.




Patterns


val pattern_to_ast : context -> pattern -> ast
Summary: Convert a pattern into ast.
val get_pattern_num_terms : context -> pattern -> int
Summary: Return number of terms in pattern.
val get_pattern : context -> pattern -> int -> ast
Summary: Return i'th ast in pattern.


Quantifiers


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
Summary: Return i'th pattern.


val get_quantifier_num_no_patterns : context -> ast -> int
Summary: Return number of no_patterns used in quantifier.


val get_quantifier_no_pattern_ast : context -> ast -> int -> ast
Summary: Return i'th no_pattern.


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


val get_quantifier_bound_sort : context -> ast -> int -> sort
Summary: Return sort 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.




Simplification


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

Provides an interface to the AST simplifier used by Z3.

val simplify_ex : context -> ast -> params -> ast
Summary: Interface to simplifier.

Provides an interface to the AST simplifier used by Z3. This procedure is similar to Z3.simplify, but the behavior of the simplifier can be configured using the given parameter set.

val simplify_get_help : context -> string
Summary: Return a string describing all available parameters.


Modifiers


val update_term : context -> ast -> ast array -> ast
Summary: Update the arguments of term a using the arguments args. The number of arguments num_args should coincide with the number of arguments to a. If a is a quantifier, then num_args has to be 1.
val substitute : context -> ast -> ast array -> ast array -> ast
Summary: Substitute every occurrence of fromi in a with toi , for i smaller than num_exprs. The result is the new AST. The arrays from and to must have size num_exprs. For every i smaller than num_exprs, we must have that sort of fromi must be equal to sort of toi .
val substitute_vars : context -> ast -> ast array -> ast
Summary: Substitute the free variables in a with the expressions in to. For every i smaller than num_exprs, the variable with de-Bruijn index i is replaced with term toi .
val translate : context -> ast -> context -> ast
Summary: Translate/Copy the AST a from context source to context target. AST a must have been created using context source.


Models


val model_inc_ref : context -> model -> unit
Summary: Increment the reference counter of the given model.
val model_dec_ref : context -> model -> unit
Summary: Decrement the reference counter of the given model.
val model_get_const_interp : context -> model -> func_decl -> ast
Summary: Return the interpretation (i.e., assignment) of constant a in the model m. Return None, if the model does not assign an interpretation for a. That should be interpreted as: the value of a does not matter.


val model_get_func_interp : context -> model -> func_decl -> func_interp
Summary: Return the interpretation of the function f in the model m. Return None, if the model does not assign an interpretation for f. That should be interpreted as: the f does not matter.


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


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


val model_get_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 model_get_func_decl : context -> model -> int -> func_decl
Summary: [ model_get_func_decl c m i ] Return the declaration of the i-th function in the given model.


val model_eval : context -> model -> ast -> bool -> ast option
Summary: [ eval c m t ] Evaluate the AST node t in the given model.

Return None if the term was not successfully evaluated.

If model_completion is TRUE, then Z3 will assign an interpretation for any constant or function that does not have an interpretation in m. These constants and functions were essentially don't cares.

The evaluation may fail for the following reasons:


val model_get_num_sorts : context -> model -> int
Summary: Return the number of uninterpreted sorts that m assigs an interpretation to.

Z3 also provides an intepretation for uninterpreted sorts used in a formua. The interpretation for a sort s is a finite set of distinct values. We say this finite set is the "universe" of s.


val model_get_sort : context -> model -> int -> sort
Summary: Return a uninterpreted sort that m assigns an interpretation.


val model_get_sort_universe : context -> model -> sort -> ast_vector
Summary: Return the finite set of distinct values that represent the interpretation for sort s.


val is_as_array : context -> ast -> bool
Summary: The (_ as-array f) AST node is a construct for assigning interpretations for arrays in Z3. It is the array such that forall indices i we have that (select (_ as-array f) i) is equal to (f i) . This procedure returns TRUE if the a is an as-array AST node.

Z3 current solvers have minimal support for as_array nodes.


val get_as_array_func_decl : context -> ast -> func_decl
Summary: Return the function declaration f associated with a (_ as_array f) node.


val func_interp_inc_ref : context -> func_interp -> unit
Summary: Increment the reference counter of the given func_interp object.
val func_interp_dec_ref : context -> func_interp -> unit
Summary: Decrement the reference counter of the given func_interp object.
val func_interp_get_num_entries : context -> func_interp -> int
Summary: Return the number of entries in the given function interpretation.

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. This procedure return the number of element in the finite map of f.

val func_interp_get_entry : context -> func_interp -> int -> func_entry
Summary: Return a "point" of the given function intepretation. It represents the value of f in a particular point.


val func_interp_get_else : context -> func_interp -> ast
Summary: Return the 'else' value of the given function interpretation.

A function interpretation is represented as a finite map and an 'else' value. This procedure returns the 'else' value.

val func_interp_get_arity : context -> func_interp -> int
Summary: Return the arity (number of arguments) of the given function interpretation.
val func_entry_inc_ref : context -> func_entry -> unit
Summary: Increment the reference counter of the given func_entry object.
val func_entry_dec_ref : context -> func_entry -> unit
Summary: Decrement the reference counter of the given func_entry object.
val func_entry_get_value : context -> func_entry -> ast
Summary: Return the value of this point.

A func_entry object represents an element in the finite map used to encode a function interpretation.


val func_entry_get_num_args : context -> func_entry -> int
Summary: Return the number of arguments in a func_entry object.


val func_entry_get_arg : context -> func_entry -> int -> ast
Summary: Return an argument of a func_entry object.




Interaction logging.


val open_log : string -> bool
Summary: Log interaction to a file.
val append_log : string -> unit
Summary: Append user-defined string to interaction log.

The interaction log is opened using open_log. It contains the formulas that are checked using Z3. You can use this command to append comments, for instance.

val close_log : unit -> unit
Summary: Close interaction log.
val toggle_warning_messages : bool -> unit
Summary: Enable/disable printing warning messages to the console.

Warnings are printed after passing true, warning messages are suppressed after calling this method with false.



String conversion


val set_ast_print_mode : context -> ast_print_mode -> unit
Summary: Select mode for the format used for pretty-printing AST nodes.

The default mode for pretty printing AST nodes is to produce SMT-LIB style output where common subexpressions are printed at each occurrence. The mode is called PRINT_SMTLIB_FULL. To print shared common subexpressions only once, use the PRINT_LOW_LEVEL mode. To print in way that conforms to SMT-LIB standards and uses let expressions to share common sub-expressions use PRINT_SMTLIB_COMPLIANT.


val ast_to_string : context -> ast -> string
Summary: Convert the given AST node into a string.


val pattern_to_string : context -> pattern -> string
val sort_to_string : context -> sort -> string
val func_decl_to_string : context -> func_decl -> string
val model_to_string : context -> model -> string
Summary: Convert the given model into a string.
val benchmark_to_smtlib_string : context ->
string -> string -> string -> string -> ast array -> ast -> string
Summary: Convert the given benchmark into SMT-LIB formatted string.


Parser interface


val parse_smtlib_string : context ->
string ->
symbol array ->
sort array -> symbol array -> func_decl array -> unit
Summary: [ parse_smtlib_string c str sort_names sorts decl_names decls ] Parse the given string using the SMT-LIB parser.

The symbol table of the parser can be initialized using the given sorts and declarations. The symbols in the arrays sort_names and decl_names don't need to match the names of the sorts and declarations in the arrays sorts and decls. This is an useful feature since we can use arbitrary names to reference sorts and declarations defined using the C API.

The formulas, assumptions and declarations defined in str can be extracted using the functions: Z3.get_smtlib_num_formulas, Z3.get_smtlib_formula, Z3.get_smtlib_num_assumptions, Z3.get_smtlib_assumption, Z3.get_smtlib_num_decls, and Z3.get_smtlib_decl.

val parse_smtlib_file : context ->
string ->
symbol array ->
sort array -> symbol array -> func_decl array -> unit
Summary: Similar to Z3.parse_smtlib_string, but reads the benchmark from a file.
val get_smtlib_num_formulas : context -> int
Summary: Return the number of SMTLIB formulas parsed by the last call to Z3.parse_smtlib_string or Z3.parse_smtlib_file.
val get_smtlib_formula : context -> int -> ast
Summary: [ get_smtlib_formula c i ] Return the i-th formula parsed by the last call to Z3.parse_smtlib_string or Z3.parse_smtlib_file.


val get_smtlib_num_assumptions : context -> int
Summary: Return the number of SMTLIB assumptions parsed by Z3.parse_smtlib_string or Z3.parse_smtlib_file.
val get_smtlib_assumption : context -> int -> ast
Summary: [ get_smtlib_assumption c i ] Return the i-th assumption parsed by the last call to Z3.parse_smtlib_string or Z3.parse_smtlib_file.


val get_smtlib_num_decls : context -> int
Summary: Return the number of declarations parsed by Z3.parse_smtlib_string or Z3.parse_smtlib_file.
val get_smtlib_decl : context -> int -> func_decl
Summary: [ get_smtlib_decl c i ] Return the i-th declaration parsed by the last call to Z3.parse_smtlib_string or Z3.parse_smtlib_file.


val get_smtlib_num_sorts : context -> int
Summary: Return the number of sorts parsed by Z3.parse_smtlib_string or Z3.parse_smtlib_file.
val get_smtlib_sort : context -> int -> sort
Summary: [ get_smtlib_sort c i ] Return the i-th sort parsed by the last call to Z3.parse_smtlib_string or Z3.parse_smtlib_file.


val get_smtlib_error : context -> string
Summary: [ get_smtlib_error c ] Retrieve that last error message information generated from parsing.
val parse_z3_string : context -> string -> ast
Summary: [ parse_z3_string c str ] Parse the given string using the Z3 native parser.

Return the conjunction of asserts made in the input.

val parse_z3_file : context -> string -> ast
Summary: Similar to Z3.parse_z3_string, but reads the benchmark from a file.
val parse_smtlib2_string : context ->
string ->
symbol array ->
sort array -> symbol array -> func_decl array -> ast
Summary: [ parse_smtlib2_string c str ] Parse the given string using the SMT-LIB2 parser.

It returns a formula comprising of the conjunction of assertions in the scope (up to push/pop) at the end of the string.

val parse_smtlib2_file : context ->
string ->
symbol array ->
sort array -> symbol array -> func_decl array -> ast
Summary: Similar to Z3.parse_smtlib2_string, but reads the benchmark from a file.


Miscellaneous


val get_version : unit -> int * int * int * int
Summary: Return Z3 version number information.
val reset_memory : unit -> unit
Summary: Reset all allocated resources.

Use this facility on out-of memory errors. It allows discharging the previous state and resuming afresh. Any pointers previously returned by the API become invalid.



External Theory Plugins


val mk_theory : context -> string -> theory
Summary: Create a new user defined theory. The new theory will be identified by the name th_name. A theory must be created before asserting any assertion to the given context.
val theory_mk_sort : context -> theory -> symbol -> sort
Summary: Create an interpreted theory sort.
val theory_mk_value : context -> theory -> symbol -> sort -> ast
Summary: Create an interpreted theory constant value. Values are assumed to be different from each other.
val theory_mk_constant : context -> theory -> symbol -> sort -> ast
Summary: Create an interpreted constant for the given theory.
val theory_mk_func_decl : context ->
theory -> symbol -> sort array -> sort -> func_decl
Summary: Create an interpreted function declaration for the given theory.
val theory_get_context : theory -> context
Summary: Return the context where the given theory is installed.
val set_delete_callback : theory -> (unit -> unit) -> unit
Summary: Set a callback that is invoked when theory t is deleted. This callback should be used to delete external data-structures associated with the given theory.


val set_reduce_app_callback : theory -> (func_decl -> ast array -> ast option) -> unit
Summary: Set a callback for simplifying operators of the given theory. The callback f is invoked by Z3's simplifier.
val set_reduce_eq_callback : theory -> (ast -> ast -> ast option) -> unit
Summary: Set a callback for simplifying the atom s_1 = s_2 , when the sort of s_1 and s_2 is an interpreted sort of the given theory. The callback f is invoked by Z3's simplifier.
val set_reduce_distinct_callback : theory -> (ast array -> ast option) -> unit
Summary: Set a callback for simplifying the atom distinct(s_1, ..., s_n) , when the sort of s_1, ..., s_n is an interpreted sort of the given theory. The callback f is invoked by Z3's simplifier.
val set_new_app_callback : theory -> (ast -> unit) -> unit
Summary: Set a callback that is invoked when a theory application is finally added into the logical context. Note that, not every application contained in an asserted expression is actually added into the logical context because it may be simplified during a preprocessing step.


val set_new_elem_callback : theory -> (ast -> unit) -> unit
Summary: Set a callback that is invoked when an expression of sort s, where s is an interpreted sort of the theory \c t, is finally added into the logical context. Note that, not every expression contained in an asserted expression is actually added into the logical context because it may be simplified during a preprocessing step.


val set_init_search_callback : theory -> (unit -> unit) -> unit
Summary: Set a callback that is invoked when Z3 starts searching for a satisfying assignment.
val set_push_callback : theory -> (unit -> unit) -> unit
Summary: Set a callback that is invoked when Z3 creates a case-split (aka backtracking point).

When a case-split is created we say the search level is increased.

val set_pop_callback : theory -> (unit -> unit) -> unit
Summary: Set a callback that is invoked when Z3 backtracks a case-split.

When a case-split is backtracked we say the search level is decreased.

val set_restart_callback : theory -> (unit -> unit) -> unit
Summary: Set a callback that is invoked when Z3 restarts the search for a satisfying assignment.
val set_reset_callback : theory -> (unit -> unit) -> unit
Summary: Set a callback that is invoked when the logical context is reset by the user. This callback is useful for reseting any data-structure maintained by the user theory solver.
val set_final_check_callback : theory -> (unit -> bool) -> unit
Summary: Set a callback that is invoked before Z3 starts building a model. A theory may use this callback to perform expensive operations.

If the theory returns false, Z3 will assume that theory is giving up, and it will assume that it was not possible to decide if the asserted constraints are satisfiable or not.

val set_new_eq_callback : theory -> (ast -> ast -> unit) -> unit
Summary: Set a callback that is invoked when an equality s_1 = s_2 is found by the logical context.
val set_new_diseq_callback : theory -> (ast -> ast -> unit) -> unit
Summary: Set a callback that is invoked when a disequality s_1 != s_2 is found by the logical context.
val set_new_assignment_callback : theory -> (ast -> bool -> unit) -> unit
Summary: Set a callback that is invoked when a theory predicate is assigned to true/false by Z3.
val set_new_relevant_callback : theory -> (ast -> unit) -> unit
Summary: Set a callback that is invoked when an expression is marked as relevant during the search. This callback is only invoked when relevancy propagation is enabled.
val theory_assert_axiom : theory -> ast -> unit
Summary: Assert a theory axiom/lemmas during the search.

An axiom added at search level n will remain in the logical context until level n is backtracked.

The callbacks for push (Z3.set_push_callback) and pop (Z3.set_pop_callback) can be used to track when the search level is increased (i.e., new case-split) and decreased (i.e., case-split is backtracked).

Z3 tracks the theory axioms asserted. So, multiple assertions of the same axiom are ignored.

val theory_assume_eq : theory -> ast -> ast -> unit
Summary: Inform to the logical context that lhs and rhs have the same interpretation in the model being built by theory t. If lhs = rhs is inconsistent with other theories, then the logical context will backtrack.

For more information, see the paper "Model-Based Theory Combination" in the Z3 website.

val theory_enable_axiom_simplification : theory -> bool -> unit
Summary: Enable/disable the simplification of theory axioms asserted using Z3.theory_assert_axiom. By default, the simplification of theory specific operators is disabled. That is, the reduce theory callbacks are not invoked for theory axioms. The default behavior is useful when asserting axioms stating properties of theory operators.
val theory_get_eqc_root : theory -> ast -> ast
Summary: Return the root of the equivalence class containing n.
val theory_get_eqc_next : theory -> ast -> ast
Summary: Return the next element in the equivalence class containing n.

The elements in an equivalence class are organized in a circular list. You can traverse the list by calling this function multiple times using the result from the previous call. This is illustrated in the code snippet below.

           ast curr = n;
           do
             curr = theory_get_eqc_next(theory, curr);
           while (curr != n);
       

val theory_get_num_parents : theory -> ast -> int
Summary: Return the number of parents of n that are operators of the given theory.
val theory_get_parent : theory -> ast -> int -> ast
Summary: Return the i-th parent of n. See Z3.theory_get_num_parents.
val theory_is_value : theory -> ast -> bool
Summary: Return TRUE if n is an interpreted theory value.
val theory_is_decl : theory -> func_decl -> bool
Summary: Return TRUE if d is an interpreted theory declaration.
val theory_get_num_elems : theory -> int
Summary: Return the number of expressions of the given theory in the logical context. These are the expressions notified using the callback Z3.set_new_elem_callback.
val theory_get_elem : theory -> int -> ast
Summary: Return the i-th elem of the given theory in the logical context.


val theory_get_num_apps : theory -> int
Summary: Return the number of theory applications in the logical context. These are the expressions notified using the callback Z3.set_new_app_callback.
val theory_get_app : theory -> int -> ast
Summary: Return the i-th application of the given theory in the logical context.




Fixedpoint facilities


val mk_fixedpoint : context -> fixedpoint
Summary: Create a new fixedpoint context.
val fixedpoint_inc_ref : context -> fixedpoint -> unit
Summary: Increment the reference counter of the given fixedpoint context
val fixedpoint_dec_ref : context -> fixedpoint -> unit
Summary: Decrement the reference counter of the given fixedpoint context.
val fixedpoint_add_rule : context -> fixedpoint -> ast -> symbol -> unit
Summary: Add a universal Horn clause as a named rule. The horn_rule should be of the form:

           horn_rule ::= (forall (bound-vars) horn_rule)
                      |  (=> atoms horn_rule)
                      |  atom
       

val fixedpoint_assert : context -> fixedpoint -> ast -> unit
Summary: Assert a constraint to the fixedpoint context.

The constraints are used as background axioms when the fixedpoint engine uses the PDR mode. They are ignored for standard Datalog mode.

val fixedpoint_query : context -> fixedpoint -> ast -> lbool
Summary: Pose a query against the asserted rules.

           query ::= (exists (bound-vars) query)
                 |  literals 
        

query returns


val fixedpoint_query_relations : context -> fixedpoint -> func_decl array -> lbool
Summary: Pose multiple queries against the asserted rules.

The queries are encoded as relations (function declarations).

query returns


val fixedpoint_get_answer : context -> fixedpoint -> ast
Summary: Retrieve a formula that encodes satisfying answers to the query.

When used in Datalog mode, the returned answer is a disjunction of conjuncts. Each conjunct encodes values of the bound variables of the query that are satisfied. In PDR mode, the returned answer is a single conjunction.

The previous call to fixedpoint_query must have returned L_TRUE.

val fixedpoint_get_reason_unknown : context -> fixedpoint -> string
Summary: Retrieve a string that describes the last status returned by Z3.fixedpoint_query.

Use this method when Z3.fixedpoint_query returns L_UNDEF.

val fixedpoint_get_statistics : context -> fixedpoint -> stats
Summary: Retrieve statistics information from the last call to Z3.fixedpoint_query.
val fixedpoint_register_relation : context -> fixedpoint -> func_decl -> unit
Summary: Register relation as Fixedpoint defined. Fixedpoint defined relations have least-fixedpoint semantics. For example, the relation is empty if it does not occur in a head or a fact.
val fixedpoint_set_predicate_representation : context -> fixedpoint -> func_decl -> symbol array -> unit
Summary: Configure the predicate representation.

It sets the predicate to use a set of domains given by the list of symbols. The domains given by the list of symbols must belong to a set of built-in domains.

val fixedpoint_simplify_rules : context ->
fixedpoint -> ast array -> func_decl array -> ast_vector
Summary: Simplify rules into a set of new rules that are returned. The simplification routines apply inlining, quantifier elimination, and other algebraic simplifications.
val fixedpoint_to_string : context -> fixedpoint -> ast array -> string
Summary: Print the current rules and background axioms as a string.


AST vectors


val mk_ast_vector : context -> ast_vector
Summary: Return an empty AST vector.
val ast_vector_inc_ref : context -> ast_vector -> unit
Summary: Increment the reference counter of the given AST vector.
val ast_vector_dec_ref : context -> ast_vector -> unit
Summary: Decrement the reference counter of the given AST vector.
val ast_vector_size : context -> ast_vector -> int
Summary: Return the size of the given AST vector.
val ast_vector_get : context -> ast_vector -> int -> ast
Summary: Return the AST at position i in the AST vector v.


val ast_vector_set : context -> ast_vector -> int -> ast -> unit
Summary: Update position i of the AST vector v with the AST a.


val ast_vector_resize : context -> ast_vector -> int -> unit
Summary: Resize the AST vector v.
val ast_vector_push : context -> ast_vector -> ast -> unit
Summary: Add the AST a in the end of the AST vector v. The size of v is increased by one.
val ast_vector_translate : context -> ast_vector -> context -> ast_vector
Summary: Translate the AST vector v from context s into an AST vector in context t.
val ast_vector_to_string : context -> ast_vector -> string
Summary: Convert AST vector into a string.


AST maps


val mk_ast_map : context -> ast_map
Summary: Return an empty mapping from AST to AST
val ast_map_inc_ref : context -> ast_map -> unit
Summary: Increment the reference counter of the given AST map.
val ast_map_dec_ref : context -> ast_map -> unit
Summary: Decrement the reference counter of the given AST map.
val ast_map_contains : context -> ast_map -> ast -> bool
Summary: Return true if the map m contains the AST key k.
val ast_map_find : context -> ast_map -> ast -> ast
Summary: Return the value associated with the key k.

The procedure invokes the error handler if k is not in the map.

val ast_map_insert : context -> ast_map -> ast -> ast -> unit
Summary: Store/Replace a new key, value pair in the given map.
val ast_map_erase : context -> ast_map -> ast -> unit
Summary: Erase a key from the map.
val ast_map_reset : context -> ast_map -> unit
Summary: Remove all keys from the given map.
val ast_map_size : context -> ast_map -> int
Summary: Return the size of the given map.
val ast_map_keys : context -> ast_map -> ast_vector
Summary: Return the keys stored in the given map.
val ast_map_to_string : context -> ast_map -> string
Summary: Convert the given map into a string.


Goals


val mk_goal : context -> bool -> bool -> bool -> goal
Summary: Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers.

If models == true, then model generation is enabled for the new goal.

If unsat_cores == true, then unsat core generation is enabled for the new goal.

If proofs == true, then proof generation is enabled for the new goal. Remark, the Z3 context c must have been created with proof generation support.

val goal_inc_ref : context -> goal -> unit
Summary: Increment the reference counter of the given goal.
val goal_dec_ref : context -> goal -> unit
Summary: Decrement the reference counter of the given goal.
val goal_precision : context -> goal -> goal_prec
Summary: Return the "precision" of the given goal. Goals can be transformed using over and under approximations. A under approximation is applied when the objective is to find a model for a given goal. An over approximation is applied when the objective is to find a proof for a given goal.
val goal_assert : context -> goal -> ast -> unit
Summary: Add a new formula a to the given goal.
val goal_inconsistent : context -> goal -> bool
Summary: Return true if the given goal contains the formula false.
val goal_depth : context -> goal -> int
Summary: Return the depth of the given goal. It tracks how many transformations were applied to it.
val goal_reset : context -> goal -> unit
Summary: Erase all formulas from the given goal.
val goal_size : context -> goal -> int
Summary: Return the number of formulas in the given goal.
val goal_formula : context -> goal -> int -> ast
Summary: Return a formula from the given goal.


val goal_num_exprs : context -> goal -> int
Summary: Return the number of formulas, subformulas and terms in the given goal.
val goal_is_decided_sat : context -> goal -> bool
Summary: Return true if the goal is empty, and it is precise or the product of a under approximation.
val goal_is_decided_unsat : context -> goal -> bool
Summary: Return true if the goal contains false, and it is precise or the product of an over approximation.
val goal_translate : context -> goal -> context -> goal
Summary: Copy a goal g from the context source to a the context target.
val goal_to_string : context -> goal -> string
Summary: Convert a goal into a string.


Tactics and Probes


val mk_tactic : context -> string -> tactic
Summary: Return a tactic associated with the given name. The complete list of tactics may be obtained using the procedures Z3.get_num_tactics and Z3.get_tactic_name. It may also be obtained using the command (help-tactics) in the SMT 2.0 front-end.

Tactics are the basic building block for creating custom solvers for specific problem domains.

val tactic_inc_ref : context -> tactic -> unit
Summary: Increment the reference counter of the given tactic.
val tactic_dec_ref : context -> tactic -> unit
Summary: Decrement the reference counter of the given tactic.
val mk_probe : context -> string -> probe
Summary: Return a probe associated with the given name. The complete list of probes may be obtained using the procedures Z3.get_num_probes and Z3.get_probe_name. It may also be obtained using the command (help-tactics) in the SMT 2.0 front-end.

Probes are used to inspect a goal (aka problem) and collect information that may be used to decide which solver and/or preprocessing step will be used.

val probe_inc_ref : context -> probe -> unit
Summary: Increment the reference counter of the given probe.
val probe_dec_ref : context -> probe -> unit
Summary: Decrement the reference counter of the given probe.
val tactic_and_then : context -> tactic -> tactic -> tactic
Summary: Return a tactic that applies t1 to a given goal and t2 to every subgoal produced by t1.
val tactic_or_else : context -> tactic -> tactic -> tactic
Summary: Return a tactic that first applies t1 to a given goal, if it fails then returns the result of t2 applied to the given goal.
val tactic_par_or : context -> tactic array -> tactic
Summary: Return a tactic that applies the given tactics in parallel.
val tactic_par_and_then : context -> tactic -> tactic -> tactic
Summary: Return a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1. The subgoals are processed in parallel.
val tactic_try_for : context -> tactic -> int -> tactic
Summary: Return a tactic that applies t to a given goal for ms milliseconds. If t does not terminate in ms milliseconds, then it fails.
val tactic_when : context -> probe -> tactic -> tactic
Summary: Return a tactic that applies t to a given goal is the probe p evaluates to true. If p evaluates to false, then the new tactic behaves like the skip tactic.
val tactic_cond : context -> probe -> tactic -> tactic -> tactic
Summary: Return a tactic that applies t1 to a given goal if the probe p evaluates to true, and t2 if p evaluates to false.
val tactic_repeat : context -> tactic -> int -> tactic
Summary: Return a tactic that keeps applying t until the goal is not modified anymore or the maximum number of iterations max is reached.
val tactic_skip : context -> tactic
Summary: Return a tactic that just return the given goal.
val tactic_fail : context -> tactic
Summary: Return a tactic that always fails.
val tactic_fail_if : context -> probe -> tactic
Summary: Return a tactic that fails if the probe p evaluates to false.
val tactic_fail_if_not_decided : context -> tactic
Summary: Return a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains false).
val tactic_using_params : context -> tactic -> params -> tactic
Summary: Return a tactic that applies t using the given set of parameters.
val probe_const : context -> float -> probe
Summary: Return a probe that always evaluates to val.
val probe_lt : context -> probe -> probe -> probe
Summary: Return a probe that evaluates to "true" when the value returned by p1 is less than the value returned by p2.


val probe_gt : context -> probe -> probe -> probe
Summary: Return a probe that evaluates to "true" when the value returned by p1 is greater than the value returned by p2.


val probe_le : context -> probe -> probe -> probe
Summary: Return a probe that evaluates to "true" when the value returned by p1 is less than or equal to the value returned by p2.


val probe_ge : context -> probe -> probe -> probe
Summary: Return a probe that evaluates to "true" when the value returned by p1 is greater than or equal to the value returned by p2.


val probe_eq : context -> probe -> probe -> probe
Summary: Return a probe that evaluates to "true" when the value returned by p1 is equal to the value returned by p2.


val probe_and : context -> probe -> probe -> probe
Summary: Return a probe that evaluates to "true" when p1 and p2 evaluates to true.


val probe_or : context -> probe -> probe -> probe
Summary: Return a probe that evaluates to "true" when p1 or p2 evaluates to true.


val probe_not : context -> probe -> probe
Summary: Return a probe that evaluates to "true" when p does not evaluate to true.


val get_num_tactics : context -> int
Summary: Return the number of builtin tactics available in Z3.
val get_tactic_name : context -> int -> string
Summary: Return the name of the idx tactic.


val get_num_probes : context -> int
Summary: Return the number of builtin probes available in Z3.
val get_probe_name : context -> int -> string
Summary: Return the name of the i probe.


val tactic_get_help : context -> tactic -> string
Summary: Return a string containing a description of parameters accepted by the given tactic.
val tactic_get_descr : context -> string -> string
Summary: Return a string containing a description of the tactic with the given name.
val probe_get_descr : context -> string -> string
Summary: Return a string containing a description of the probe with the given name.
val probe_apply : context -> probe -> goal -> float
Summary: Execute the probe over the goal. The probe always produce a double value. "Boolean" probes return 0.0 for false, and a value different from 0.0 for true.
val tactic_apply : context -> tactic -> goal -> apply_result
Summary: Apply tactic t to the goal g.
val tactic_apply_ex : context -> tactic -> goal -> params -> apply_result
Summary: Apply tactic t to the goal g using the parameter set p.
val apply_result_inc_ref : context -> apply_result -> unit
Summary: Increment the reference counter of the given apply_result object.
val apply_result_dec_ref : context -> apply_result -> unit
Summary: Decrement the reference counter of the given apply_result object.
val apply_result_to_string : context -> apply_result -> string
Summary: Convert the apply_result object returned by Z3.tactic_apply into a string.
val apply_result_get_num_subgoals : context -> apply_result -> int
Summary: Return the number of subgoals in the apply_result object returned by Z3.tactic_apply.
val apply_result_get_subgoal : context -> apply_result -> int -> goal
Summary: Return one of the subgoals in the apply_result object returned by Z3.tactic_apply.


val apply_result_convert_model : context -> apply_result -> int -> model -> model
Summary: Convert a model for the subgoal apply_result_get_subgoal(c, r, i) into a model for the original goal g. Where g is the goal used to create r using tactic_apply(c, t, g).


Solvers


val mk_solver : context -> solver
Summary: Create a new (incremental) solver. This solver also uses a set of builtin tactics for handling the first check-sat command, and check-sat commands that take more than a given number of milliseconds to be solved.
val mk_simple_solver : context -> solver
Summary: Create a new (incremental) solver.
val mk_solver_for_logic : context -> symbol -> solver
Summary: Create a new solver customized for the given logic. It behaves like Z3.mk_solver if the logic is unknown or unsupported.
val mk_solver_from_tactic : context -> tactic -> solver
Summary: Create a new solver that is implemented using the given tactic. The solver supports the commands Z3.solver_push and Z3.solver_pop, but it will always solve each Z3.solver_check from scratch.
val solver_get_help : context -> solver -> string
Summary: Return a string describing all solver available parameters.
val solver_set_params : context -> solver -> params -> unit
Summary: Set the given solver using the given parameters.
val solver_inc_ref : context -> solver -> unit
Summary: Increment the reference counter of the given solver.
val solver_dec_ref : context -> solver -> unit
Summary: Decrement the reference counter of the given solver.
val solver_push : context -> solver -> unit
Summary: Create a backtracking point.

The solver contains a stack of assertions.


val solver_pop : context -> solver -> int -> unit
Summary: Backtrack n backtracking points.


val solver_reset : context -> solver -> unit
Summary: Remove all assertions from the solver.
val solver_get_num_scopes : context -> solver -> int
Summary: Return the number of backtracking points.


val solver_assert : context -> solver -> ast -> unit
Summary: Assert a constraint into the solver.

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

val solver_get_assertions : context -> solver -> ast_vector
Summary: Return the set of asserted formulas as a goal object.
val solver_check : context -> solver -> lbool
Summary: Check whether the assertions in a given solver are consistent or not.

The function Z3.solver_get_model retrieves a model if the assertions are not unsatisfiable (i.e., the result is not \c L_FALSE) and model construction is enabled.

The function Z3.solver_get_proof retrieves a proof if proof generation was enabled when the context was created, and the assertions are unsatisfiable (i.e., the result is L_FALSE).

val solver_check_assumptions : context -> solver -> ast array -> lbool
Summary: Check whether the assertions in the given solver and optional assumptions are consistent or not.

The function Z3.solver_get_unsat_core retrieves the subset of the assumptions used in the unsatisfiability proof produced by Z3.


val solver_get_model : context -> solver -> model
Summary: Retrieve the model for the last Z3.solver_check or Z3.solver_check_assumptions

The error handler is invoked if a model is not available because the commands above were not invoked for the given solver, or if the result was L_FALSE.

val solver_get_proof : context -> solver -> ast
Summary: Retrieve the proof for the last Z3.solver_check or Z3.solver_check_assumptions

The error handler is invoked if proof generation is not enabled, or if the commands above were not invoked for the given solver, or if the result was different from L_FALSE.

val solver_get_unsat_core : context -> solver -> ast_vector
Summary: Retrieve the unsat core for the last Z3.solver_check_assumptions The unsat core is a subset of the assumptions a.
val solver_get_reason_unknown : context -> solver -> string
Summary: Return a brief justification for an "unknown" result (i.e., L_UNDEF) for the commands Z3.solver_check and Z3.solver_check_assumptions
val solver_get_statistics : context -> solver -> stats
Summary: Return statistics for the given solver.
val solver_to_string : context -> solver -> string
Summary: Convert a solver into a string.


Statistics


val stats_to_string : context -> stats -> string
Summary: Convert a statistics into a string.
val stats_inc_ref : context -> stats -> unit
Summary: Increment the reference counter of the given statistics object.
val stats_dec_ref : context -> stats -> unit
Summary: Decrement the reference counter of the given statistics object.
val stats_size : context -> stats -> int
Summary: Return the number of statistical data in s.
val stats_get_key : context -> stats -> int -> string
Summary: Return the key (a string) for a particular statistical data.


val stats_is_uint : context -> stats -> int -> bool
Summary: Return TRUE if the given statistical data is a unsigned int integer.


val stats_is_double : context -> stats -> int -> bool
Summary: Return TRUE if the given statistical data is a double.


val stats_get_uint_value : context -> stats -> int -> int
Summary: Return the unsigned int value of the given statistical data.


val stats_get_double_value : context -> stats -> int -> float
Summary: Return the double value of the given statistical data.




Deprecated Injective functions API


val mk_injective_function : context -> symbol -> sort array -> sort -> func_decl
Deprecated. This method just asserts a (universally quantified) formula that asserts that the new function is injective. It is compatible with the old interface for solving: Z3.assert_cnstr, Z3.check_assumptions, etc.
Summary: Create injective function declaration


Deprecated Constraints API


val set_logic : context -> string -> bool
Deprecated. Subsumed by Z3.mk_solver_for_logic
Summary: Set the SMTLIB logic to be used in the given logical context. It is incorrect to invoke this function after invoking Z3.check, Z3.check_and_get_model, Z3.check_assumptions and Z3.push. Return TRUE if the logic was changed successfully, and FALSE otherwise.
val push : context -> unit
Deprecated. Subsumed by Z3.solver_push
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
Deprecated. Subsumed by Z3.solver_pop
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 get_num_scopes : context -> int
Deprecated. Subsumed by Z3.solver_get_num_scopes.
Summary: Retrieve the current scope level.

It retrieves the number of scopes that have been pushed, but not yet popped.


val persist_ast : context -> ast -> int -> unit
Deprecated. This function has no effect.
val assert_cnstr : context -> ast -> unit
Deprecated. Subsumed by Z3.solver_assert
Summary: Assert a constraint 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
Deprecated. Subsumed by Z3.solver_check
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 valid model is returned. Otherwise, it is unsafe to use the returned model.


val check : context -> lbool
Deprecated. Subsumed by Z3.solver_check
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 check_assumptions : context ->
ast array ->
int -> ast array -> lbool * model * ast * int * ast array
Deprecated. Subsumed by Z3.solver_check_assumptions
Summary: Check whether the given logical context and optional assumptions 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 valid model is returned. Otherwise, it is unsafe to use the returned model.

val get_implied_equalities : context -> ast array -> lbool * int array
Deprecated. Subsumed by solver API
Summary: Retrieve congruence class representatives for terms.

The function can be used for relying on Z3 to identify equal terms under the current set of assumptions. The array of terms and array of class identifiers should have the same length. The class identifiers are numerals that are assigned to the same value for their corresponding terms if the current context forces the terms to be equal. You cannot deduce that terms corresponding to different numerals must be all different, (especially when using non-convex theories). All implied equalities are returned by this call. This means that two terms map to the same class identifier if and only if the current context implies that they are equal.

A side-effect of the function is a satisfiability check. The function return L_FALSE if the current assertions are not satisfiable.


val del_model : context -> model -> unit
Deprecated. Subsumed by solver API
Summary: Delete a model object.




Deprecated Search control API


val soft_check_cancel : context -> unit
Deprecated. Use Z3.interrupt instead.
Summary: Cancel an ongoing check.

Notifies the current check to abort and return. This method should be called from a different thread than the one performing the check.

val get_search_failure : context -> search_failure
Deprecated. Subsumed by Z3.solver_get_reason_unknown
Summary: Retrieve reason for search failure.

If a call to Z3.check or Z3.check_and_get_model returns L_UNDEF, use this facility to determine the more detailed cause of search failure.



Deprecated Labels API


val mk_label : context -> symbol -> bool -> ast -> ast
Deprecated. Labels are only supported by the old Solver API. This feature is not essential (it can be simulated using auxiliary Boolean variables). It is only available for backward compatibility.
Summary: Create a labeled formula.
val get_relevant_labels : context -> literals
Deprecated. This procedure is based on the old Solver API.
Summary: Retrieve the set of labels that were relevant in the context of the current satisfied context.


val get_relevant_literals : context -> literals
Deprecated. This procedure is based on the old Solver API.
Summary: Retrieve the set of literals that satisfy the current context.


val get_guessed_literals : context -> literals
Deprecated. This procedure is based on the old Solver API.
Summary: Retrieve the set of literals that whose assignment were guess, but not propagated during the search.


val del_literals : context -> literals -> unit
Deprecated. This procedure is based on the old Solver API.
Summary: Delete a labels context.


val get_num_literals : context -> literals -> int
Deprecated. This procedure is based on the old Solver API.
Summary: Retrieve the number of label symbols that were returned.


val get_label_symbol : context -> literals -> int -> symbol
Deprecated. This procedure is based on the old Solver API.
Summary: Retrieve label symbol at idx.
val get_literal : context -> literals -> int -> ast
Deprecated. This procedure is based on the old Solver API.
Summary: Retrieve literal expression at idx.
val disable_literal : context -> literals -> int -> unit
Deprecated. This procedure is based on the old Solver API.
Summary: Disable label.

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


val block_literals : context -> literals -> unit
Deprecated. This procedure is based on the old Solver API.
Summary: Block subsequent checks using the remaining enabled labels.


Deprecated Model API


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


val get_model_constant : context -> model -> int -> func_decl
Deprecated. use Z3.model_get_const_decl
Summary: [ get_model_constant c m i ] Return the i-th constant in the given model.


val get_model_num_funcs : context -> model -> int
Deprecated. use Z3.model_get_num_funcs
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 get_model_func_decl : context -> model -> int -> func_decl
Deprecated. use Z3.model_get_func_decl
Summary: [ get_model_func_decl c m i ] Return the declaration of the i-th function in the given model.


val eval_func_decl : context -> model -> func_decl -> bool * ast
Deprecated. Consider using Z3.model_eval or Z3.model_get_func_interp
Summary: Return the value of the given constant or function in the given model.
val is_array_value : context -> model -> ast -> bool * int
Deprecated. Use Z3.is_as_array
Summary: [ is_array_value c v ] Determine whether the term encodes an array value. A term encodes an array value if it is a nested sequence of applications of store on top of a constant array. The indices to the stores have to be values (for example, integer constants) so that equality between the indices can be evaluated. Array values are useful for representing interpretations for arrays.

Return the number of entries mapping to non-default values of the array.

val get_array_value : context ->
model ->
ast ->
ast array -> ast array -> ast array * ast array * ast
Deprecated. Use func_interp objects and Z3.get_as_array_func_decl
Summary: [ get_array_value c v ] An array values is represented as a dictionary plus a default (else) value. This function returns the array graph.


val get_model_func_else : context -> model -> int -> ast
Deprecated. Use func_interp objects
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
Deprecated. Use func_interp objects
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
Deprecated. Use func_interp objects
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 : context -> model -> int -> int -> int -> ast
Deprecated. Use func_interp objects
Summary: [ get_model_func_entry_arg c m i j k ] Return the k-th argument 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_value : context -> model -> int -> int -> ast
Deprecated. Use func_interp objects
Summary: [ get_model_func_entry_value c m i j ] Return the return value 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 eval : context -> model -> ast -> bool * ast
Deprecated. Use Z3.model_eval
Summary: [ eval c m t ] Evaluate the AST node t in the given model.

Return a pair: Boolean and value. The Boolean is true if the term was successfully evaluated.

The evaluation may fail for the following reasons:


val eval_decl : context -> model -> func_decl -> ast array -> bool * ast
Deprecated. Consider using Z3.model_eval and Z3.substitute_vars
Summary: Evaluate declaration given values.

Provides direct way to evaluate declarations without going over terms.



Deprecated String conversion API


val context_to_string : context -> string
Deprecated. This method is obsolete. It just displays the internal representation of the global solver available for backward compatibility reasons.
Summary: Convert the given logical context into a string.

This function is mainly used for debugging purposes. It displays the internal structure of a logical context.

val statistics_to_string : context -> string
Deprecated. This method is based on the old solver API. Use Z3.stats_to_string when using the new solver API.
Summary: Return runtime statistics as a string.

This function is mainly used for debugging purposes. It displays statistics of the search activity.

val get_context_assignment : context -> ast
Deprecated. This method is based on the old solver API.
Summary: Extract satisfying assignment from context as a conjunction.

This function can be used for debugging purposes. It returns a conjunction of formulas that are assigned to true in the current context. This conjunction will contain not only the assertions that are set to true under the current assignment, but will also include additional literals if there has been a call to Z3.check or Z3.check_and_get_model.



ML Extensions


val mk_context_x : (string * string) array -> context
[ mk_context_x configs ] is a shorthand for the context with configurations in configs.
val get_app_args : context -> app -> ast array
[ get_app_args c a ] is the array of arguments of an application. If t is a constant, then the array is empty.


val get_domains : context -> func_decl -> sort array
[ get_app_args c d ] is the array of parameters of d.


val get_array_sort : context -> sort -> sort * sort
[ get_array_sort c t ] is the domain and the range of t.


val get_tuple_sort : context -> sort -> func_decl * func_decl array
[ get_tuple_sort c ty ] is the pair (mk_decl, fields) where mk_decl is the constructor declaration of ty, and fields is the array of fields in ty.



type datatype_constructor_refined = {
   constructor : func_decl;
   recognizer : func_decl;
   accessors : func_decl array;
}
[ datatype_constructor_refined ] is the refinement of a datatype constructor.

It contains the constructor declaration, recognizer, and list of accessor functions.


[ get_datatype_sort c ty ] is the array of triples (constructor, recognizer, fields) where constructor is the constructor declaration of ty, recognizer is the recognizer for the constructor, and fields is the array of fields in ty.



val get_datatype_sort : context -> sort -> datatype_constructor_refined array
val get_model_constants : context -> model -> func_decl array
[ get_model_constants c m ] is the array of constants in the model m.


val get_model_func_entry : context -> model -> int -> int -> ast array * ast
[ get_model_func_entry c m i j ] is the j'th entry in the i'th function in the model m.


val get_model_func_entries : context -> model -> int -> (ast array * ast) array
[ get_model_func_entries c m i ] is the array of entries in the i'th function in the model m.


val get_model_funcs : context ->
model -> (symbol * (ast array * ast) array * ast) array
[ get_model_funcs c m ] is the array of functions in the model m. Each function is represented by the triple (decl, entries, else), where decl is the declaration name for the function, entries is the array of entries in the function, and else is the default (else) value for the function.


val get_smtlib_formulas : context -> ast array
[ get_smtlib_formulas c ] is the array of formulas created by a preceding call to Z3.parse_smtlib_string or Z3.parse_smtlib_file.

Recommend use Z3.parse_smtlib_string_x or Z3.parse_smtlib_file_x for functional style interface to the SMT-LIB parser.


val get_smtlib_assumptions : context -> ast array
[ get_smtlib_assumptions c ] is the array of assumptions created by a preceding call to Z3.parse_smtlib_string or Z3.parse_smtlib_file.

Recommend use Z3.parse_smtlib_string_x or Z3.parse_smtlib_file_x for functional style interface to the SMT-LIB parser.


val get_smtlib_decls : context -> func_decl array
[ get_smtlib_decls c ] is the array of declarations created by a preceding call to Z3.parse_smtlib_string or Z3.parse_smtlib_file.

Recommend use Z3.parse_smtlib_string_x or Z3.parse_smtlib_file_x for functional style interface to the SMT-LIB parser.


val get_smtlib_parse_results : context -> ast array * ast array * func_decl array
[ get_smtlib_parse_results c ] is the triple (get_smtlib_formulas c, get_smtlib_assumptions c, get_smtlib_decls c).

Recommend use Z3.parse_smtlib_string_x or Z3.parse_smtlib_file_x for functional style interface to the SMT-LIB parser.


val parse_smtlib_string_formula : context ->
string ->
symbol array ->
sort array -> symbol array -> func_decl array -> ast
[ parse_smtlib_string_formula c ... ] calls (parse_smtlib_string c ...) and returns the single formula produced.

Recommended for functional style interface to the SMT-LIB parser.


val parse_smtlib_file_formula : context ->
string ->
symbol array ->
sort array -> symbol array -> func_decl array -> ast
[ parse_smtlib_file_formula c ... ] calls (parse_smtlib_file c ...) and returns the single formula produced.

Recommended for functional style interface to the SMT-LIB parser.


val parse_smtlib_string_x : context ->
string ->
symbol array ->
sort array ->
symbol array ->
func_decl array -> ast array * ast array * func_decl array
[ parse_smtlib_string_x c ... ] is (parse_smtlib_string c ...; get_smtlib_parse_results c)

Recommended for functional style interface to the SMT-LIB parser.


val parse_smtlib_file_x : context ->
string ->
symbol array ->
sort array ->
symbol array ->
func_decl array -> ast array * ast array * func_decl array
[ parse_smtlib_file_x c ... ] is (parse_smtlib_file c ...; get_smtlib_parse_results c)

Recommended for functional style interface to the SMT-LIB parser.



type symbol_refined =
| Symbol_int of int
| Symbol_string of string
| Symbol_unknown
[ symbol_refined ] is the refinement of a Z3.symbol .


val symbol_refine : context -> symbol -> symbol_refined
[ symbol_refine c s ] is the refined symbol of s.



[ sort_refined ] is the refinement of a Z3.sort .




type sort_refined =
| Sort_uninterpreted of symbol
| Sort_bool
| Sort_int
| Sort_real
| Sort_bv of int
| Sort_array of (sort * sort)
| Sort_datatype of datatype_constructor_refined array
| Sort_relation
| Sort_finite_domain
| Sort_unknown of symbol
val sort_refine : context -> sort -> sort_refined
[ sort_refine c t ] is the refined sort of t.



type binder_type =
| Forall
| Exists
[ binder_type ] is a universal or existential quantifier.



type numeral_refined =
| Numeral_small of (int64 * int64)
| Numeral_large of string
[ numeral_refined ] is the refinement of a numeral .

Numerals whose fractional representation can be fit with 64 bit integers are treated as small.


type term_refined =
| Term_app of (decl_kind * func_decl * ast array)
| Term_quantifier of (binder_type * int * ast array array * (symbol * sort) array
* ast)
| Term_numeral of (numeral_refined * sort)
| Term_var of (int * sort)
[ term_refined ] is the refinement of a Z3.ast .


val term_refine : context -> ast -> term_refined
[ term_refine c a ] is the refined term of a.


val mk_theory : context -> string -> theory
[ mk_theory c name ] create a custom theory.
val set_delete_callback : theory -> (unit -> unit) -> unit
[ set_delete_callback th cb ] set callback when theory gets deleted.
val set_reduce_app_callback : theory -> (func_decl -> ast array -> ast option) -> unit
[ set_reduce_app_callback th cb ] set callback for simplifying theory terms.
val set_reduce_eq_callback : theory -> (ast -> ast -> ast option) -> unit
[ set_reduce_eq_callback th cb ] set callback for simplifying equalities over theory terms.
val set_reduce_distinct_callback : theory -> (ast array -> ast option) -> unit
[ set_reduce_distinct_callback th cb ] set callback for simplifying disequalities over theory terms.
val set_new_app_callback : theory -> (ast -> unit) -> unit
[ set_new_app_callback th cb ] set callback for registering new application.
val set_new_elem_callback : theory -> (ast -> unit) -> unit
[ set_new_elem_callback th cb ] set callback for registering new element.


val set_init_search_callback : theory -> (unit -> unit) -> unit
[ set_init_search_callback th cb ] set callback when Z3 starts searching for a satisfying assignment.
val set_push_callback : theory -> (unit -> unit) -> unit
[ set_push_callback th cb ] set callback for a logical context push.
val set_pop_callback : theory -> (unit -> unit) -> unit
[ set_pop_callback th cb ] set callback for a logical context pop.
val set_restart_callback : theory -> (unit -> unit) -> unit
[ set_restart_callback th cb ] set callback for search restart.
val set_reset_callback : theory -> (unit -> unit) -> unit
val set_final_check_callback : theory -> (unit -> bool) -> unit
val set_new_eq_callback : theory -> (ast -> ast -> unit) -> unit
val set_new_diseq_callback : theory -> (ast -> ast -> unit) -> unit
val set_new_assignment_callback : theory -> (ast -> bool -> unit) -> unit
val set_new_relevant_callback : theory -> (ast -> unit) -> unit