OCaml API (Index)

module Z3: sig  end

Summary: Create a configuration.

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

set_param_value cfg "MODEL" "true"

• Remarks: Consider using Z3.mk_context_x instead of using explicit configuration objects. The function Z3.mk_context_x receives an array of string pairs. This array represents the configuration options.

• See also: Z3.set_param_value
• See also: Z3.del_config

Summary: Delete the given configuration object.

• See also: Z3.mk_config

Summary: Set a configuration parameter.

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

       z3.exe -ini?
       

• See also: Z3.mk_config

Summary: Create a logical context using the given configuration.

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

• Remarks: Consider using Z3.mk_context_x instead of using explicit configuration objects. The function Z3.mk_context_x receives an array of string pairs. This array represents the configuration options.

• See also: Z3.del_context

Summary: Delete the given logical context.

• See also: Z3.mk_config

Summary: Enable trace messages to a file

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

• See also: Z3.trace_off

Summary: Enable trace messages to a standard error.

• See also: Z3.trace_off

Summary: Enable trace messages to a standard output.

• See also: Z3.trace_off

Summary: Disable trace messages.

• See also: Z3.trace_to_file
• See also: Z3.trace_to_stdout
• See also: Z3.trace_to_stderr

Summary: Create a Z3 symbol using an integer.

Symbols are used to name several term and type constructors.

• See also: Z3.mk_string_symbol

Summary: Create a Z3 symbol using a C string.

Symbols are used to name several term and type constructors.

• See also: Z3.mk_int_symbol

Summary: compare sorts.

Summary: Create a free (uninterpreted) type using the given name (symbol).

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

Summary: Create the Boolean type.

This type is used to create propositional variables and predicates.

Summary: Create an integer type.

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

• See also: Z3.mk_bv_sort

Summary: Create a real type.

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

Summary: Create a bit-vector type of the given size.

This type can also be seen as a machine integer.

• Remarks: The size of the bitvector type must be greater than zero.

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.

• See also: Z3.mk_select
• See also: Z3.mk_store

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.

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.

Summary: Create a list sort

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

Summary: Create a constructor.

sort reference is 0, then the value in sort_refs should be an index referring to one of the recursive datatypes that is declared.

Summary: Query constructor for declared funcions.

Summary: Reclaim memory allocated to constructor.

Summary: Create recursive datatype. Return the datatype sort.

Summary: Create list of constructors.

Summary: reclaim memory allocated for constructor list.

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

Summary: Create mutually recursive datatypes.

Summary: Create injective function declaration

Summary: compare terms.

Summary: Declare a constant or function.

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

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

• See also: Z3.mk_app

Summary: Create a constant or function application.

• See also: Z3.mk_func_decl

Summary: Declare and create a constant.

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

• See also: Z3.mk_func_decl
• See also: Z3.mk_app

Summary: Create a labeled formula.

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

Summary: Declare a fresh constant or function.

Z3 will generate an unique name for this function declaration.

• See also: Z3.mk_func_decl

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) [||].

• See also: Z3.mk_func_decl
• See also: Z3.mk_app

Summary: Create an AST node representing true.

Summary: Create an AST node representing false.

Summary: [ mk_eq c l r ] Create an AST node representing l = r .

The nodes l and r must have the same type.

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

All arguments must have the same sort.

• Remarks: The number of arguments of a distinct construct must be greater than one.

Summary: [ mk_not c a ] Create an AST node representing not(a) .

The node a must have Boolean sort.

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.

Summary: [ mk_iff c t1 t2 ] Create an AST node representing t1 iff t2 .

The nodes t1 and t2 must have Boolean sort.

Summary: [ mk_implies c t1 t2 ] Create an AST node representing t1 implies t2 .

The nodes t1 and t2 must have Boolean sort.

Summary: [ mk_xor c t1 t2 ] Create an AST node representing t1 xor t2 .

The nodes t1 and t2 must have Boolean sort.

Summary: [ mk_and c [| t_1; ...; t_n |] ] Create the conjunction: t_1 and ... and t_n.

All arguments must have Boolean sort.

• Remarks: The number of arguments must be greater than zero.

Summary: [ mk_or c [| t_1; ...; t_n |] ] Create the disjunction: t_1 or ... or t_n.

All arguments must have Boolean sort.

• Remarks: The number of arguments must be greater than zero.

Summary: [ mk_add c [| t_1; ...; t_n |] ] Create the term: t_1 + ... + t_n.

All arguments must have int or real sort.

• Remarks: The number of arguments must be greater than zero.

Summary: [ mk_mul c [| t_1; ...; t_n |] ] Create the term: t_1 * ... * t_n.

All arguments must have int or real sort.

• Remarks: Z3 has limited support for non-linear arithmetic.
• Remarks: The number of arguments must be greater than zero.

Summary: [ mk_sub c [| t_1; ...; t_n |] ] Create the term: t_1 - ... - t_n.

All arguments must have int or real sort.

• Remarks: The number of arguments must be greater than zero.

Summary: [ mk_unary_minus c arg ] Create the term: - arg.

The argument must have int or real type.

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.

Summary: [ mk_mod c t_1 t_2 ] Create the term: t_1 mod t_2.

The arguments must have int type.

Summary: [ mk_rem c t_1 t_2 ] Create the term: t_1 rem t_2.

The arguments must have int type.

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.

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.

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.

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.

Summary: [ mk_int2real c t1 ] Coerce an integer to a real.

There is no converse operation exposed, but 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.

Summary: [ mk_bvneg c t1 ] Bitwise negation.

The node t1 must have a bit-vector sort.

Summary: [ mk_bvand c t1 t2 ] Bitwise and.

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

Summary: [ mk_bvor c t1 t2 ] Bitwise or.

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

Summary: [ mk_bvxor c t1 t2 ] Bitwise exclusive-or.

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

Summary: [ mk_bvnand c t1 t2 ] Bitwise nand.

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

Summary: [ mk_bvnor c t1 t2 ] Bitwise nor.

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

Summary: [ mk_bvxnor c t1 t2 ] Bitwise xnor.

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

Summary: [ mk_bvneg c t1 ] Standard two's complement unary minus.

The node t1 must have bit-vector sort.

Summary: [ mk_bvadd c t1 t2 ] Standard two's complement addition.

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

Summary: [ mk_bvsub c t1 t2 ] Standard two's complement subtraction.

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

Summary: [ mk_bvmul c t1 t2 ] Standard two's complement multiplication.

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

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.

Summary: [ mk_bvsdiv c t1 t2 ] Two's complement signed division.

It is defined in the following way:

• The floor of t1/t2 if t2 is different from zero, and t1*t2 >= 0 .

• The ceiling of t1/t2 if t2 is different from zero, and t1*t2 < 0 .

If t2 is zero, then the result is undefined.

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

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.

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.

• See also: Z3.mk_bvsmod

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.

• See also: Z3.mk_bvsrem

Summary: [ mk_bvult c t1 t2 ] Unsigned less than.

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

Summary: [ mk_bvslt c t1 t2 ] Two's complement signed less than.

It abbreviates:

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

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

Summary: [ mk_bvule c t1 t2 ] Unsigned less than or equal to.

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

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.

Summary: [ mk_bvuge c t1 t2 ] Unsigned greater than or equal to.

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

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.

Summary: [ mk_bvugt c t1 t2 ] Unsigned greater than.

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

Summary: [ mk_bvsgt c t1 t2 ] Two's complement signed greater than.

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

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

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.

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.

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.

Summary: [ mk_bvshl c t1 t2 ] Shift left.

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

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

Summary: [ mk_bvlshr c t1 t2 ] Logical shift right.

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

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

Summary: [ mk_bvashr c t1 t2 ] Arithmetic shift right.

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

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

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

Summary: [ mk_select c a i ] Array 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.

• See also: Z3.mk_array_sort
• See also: Z3.mk_store

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 .

• See also: Z3.mk_array_sort
• See also: Z3.mk_select

Summary: Create the constant array.

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 .

• See also: Z3.mk_array_sort
• See also: Z3.mk_store
• See also: Z3.mk_select

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.

Summary: Create a numeral of a given sort.

• See also: Z3.mk_int
• See also: Z3.mk_unsigned_int

Summary: Create a real from a fraction.

• Precondition: den != 0

• See also: Z3.mk_numeral
• See also: Z3.mk_int
• See also: Z3.mk_unsigned_int

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.

• See also: Z3.mk_numeral

Summary: Create a numeral of a given sort.

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

• See also: Z3.mk_numeral

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.

• See also: Z3.mk_forall
• See also: Z3.mk_exists

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.

• See also: Z3.mk_forall
• See also: Z3.mk_exists

Summary: Create a forall formula.

mk_forall c w p t n b creates a forall formula, where w is the weight, p is an array of patterns, t is an array with the 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.

• See also: Z3.mk_pattern
• See also: Z3.mk_bound
• See also: Z3.mk_exists

Summary: Create an exists formula. Similar to Z3.mk_forall.

• See also: Z3.mk_pattern
• See also: Z3.mk_bound
• See also: Z3.mk_forall

Summary: Create a quantifier - universal or existential, with pattern hints.

• See also: Z3.mk_pattern
• See also: Z3.mk_bound
• See also: Z3.mk_forall
• See also: Z3.mk_exists

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

the quantifier during instantiation. By default, pass the weight 0.

• See also: Z3.mk_pattern
• See also: Z3.mk_exists_const

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.

the quantifier during instantiation. By default, pass the weight 0.

• See also: Z3.mk_pattern
• See also: Z3.mk_forall_const

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.

Summary: [ get_symbol_int c s ] Return the symbol int value.

• Precondition: get_symbol_kind s == INT_SYMBOL

• See also: Z3.mk_int_symbol

Summary: [ get_symbol_string c s ] Return the symbol name.

• Precondition: get_symbol_string s == STRING_SYMBOL

• See also: Z3.mk_string_symbol

Summary: Return the kind of the given AST.

Summary: Return numeral value, as a string of a numeric constant term

• Precondition: get_ast_kind c a == NUMERAL_AST

Summary: Return numeral value, as a pair of 64 bit numbers if the representation fits.

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

• Precondition: get_ast_kind a == NUMERAL_AST

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.

• Precondition: get_ast_kind c v == NUMERAL_AST

• See also: Z3.get_numeral_string

Summary: [ get_numeral_uint c v ] Similar to Z3.get_numeral_string, but only succeeds if the value can fit in a machine unsigned int int. Return TRUE if the call succeeded.

• Precondition: get_ast_kind c v == NUMERAL_AST

• See also: Z3.get_numeral_string

Summary: Return L_TRUE if a is true, L_FALSE if it is false, and L_UNDEF otherwise.

Summary: Return the declaration of a constant or function application.

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.

Summary: [ get_app_arg c a i ] Return the i-th argument of the given application.

• Precondition: i < get_num_args c a

Summary: Return index of de-Brujin bound variable.

• Precondition: get_ast_kind a == VAR_AST

Summary: Determine if quantifier is universal.

• Precondition: get_ast_kind a == QUANTIFIER_AST

Summary: Obtain weight of quantifier.

• Precondition: get_ast_kind a == QUANTIFIER_AST

Summary: Return number of patterns used in quantifier.

• Precondition: get_ast_kind a == QUANTIFIER_AST

Summary: Return i'th pattern.

• Precondition: get_ast_kind a == QUANTIFIER_AST

Summary: Return symbol of the i'th bound variable.

• Precondition: get_ast_kind a == QUANTIFIER_AST

Summary: Return sort of the i'th bound variable.

• Precondition: get_ast_kind a == QUANTIFIER_AST

Summary: Return body of quantifier.

• Precondition: get_ast_kind a == QUANTIFIER_AST

Summary: Return number of bound variables of quantifier.

• Precondition: get_ast_kind a == QUANTIFIER_AST

Summary: Return the constant declaration name as a symbol.

Summary: Return the number of parameters associated with a declaration.

Summary: Return the parameter type associated with a declaration.

Summary: Return the integer value associated with an integer parameter.

• Precondition: get_decl_parameter_kind c d idx == PARAMETER_INT

Summary: Return the double value associated with an double parameter.

• Precondition: get_decl_parameter_kind c d idx == PARAMETER_DOUBLE

Summary: Return the double value associated with an double parameter.

• Precondition: get_decl_parameter_kind c d idx == PARAMETER_SYMBOL

Summary: Return the sort value associated with a sort parameter.

• Precondition: get_decl_parameter_kind c d idx == PARAMETER_SORT

Summary: Return the expresson value associated with an expression parameter.

• Precondition: get_decl_parameter_kind c d idx == PARAMETER_AST

Summary: Return the expresson value associated with an expression parameter.

• Precondition: get_decl_parameter_kind c d idx == PARAMETER_FUNC_DECL

Summary: Return the rational value, as a string, associated with a rational parameter.

• Precondition: get_decl_parameter_kind c d idx == PARAMETER_RATIONAL

Summary: Return the sort name as a symbol.

Summary: Return the sort of an AST node.

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

Summary: Return the number of parameters of the given declaration.

• See also: Z3.get_domain_size

Summary: [ get_domain c d i ] Return the sort of the i-th parameter of the given function declaration.

• Precondition: i < get_domain_size d

• See also: Z3.get_domain_size

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.

Summary: Return the sort kind (e.g., array, tuple, int, bool, etc).

• See also: Z3.sort_kind

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

• Precondition: get_sort_kind c t == BV_SORT

• See also: Z3.mk_bv_sort
• See also: Z3.get_sort_kind

Summary: [ get_array_sort_domain c t ] Return the domain of the given array sort.

• Precondition: get_sort_kind c t == ARRAY_SORT

• See also: Z3.mk_array_sort
• See also: Z3.get_sort_kind

Summary: [ get_array_sort_range c t ] Return the range of the given array sort.

• Precondition: get_sort_kind c t == ARRAY_SORT

• See also: Z3.mk_array_sort
• See also: Z3.get_sort_kind

Summary: [ get_tuple_sort_mk_decl c t ] Return the constructor declaration of the given tuple sort.

• Precondition: get_sort_kind c t == DATATYPE_SORT

• See also: Z3.mk_tuple_sort
• See also: Z3.get_sort_kind

Summary: Return declaration kind corresponding to declaration.

Summary: [ get_tuple_sort_num_fields c t ] Return the number of fields of the given tuple sort.

• Precondition: get_sort_kind c t == DATATYPE_SORT

• Remarks: Consider using the function Z3.get_tuple_sort, which returns a tuple: tuple constructor, and an array of the tuple sort fields.

• See also: Z3.mk_tuple_sort
• See also: Z3.get_sort_kind

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.

• Remarks: Consider using the function Z3.get_tuple_sort, which returns a tuple: tuple constructor, and an array of the tuple sort fields.

• Precondition: get_sort_kind t == DATATYPE_SORT
• Precondition: i < get_tuple_sort_num_fields c t

• See also: Z3.mk_tuple_sort
• See also: Z3.get_sort_kind

Summary: Return number of constructors for datatype.

• Precondition: get_sort_kind t == DATATYPE_SORT

• See also: Z3.get_datatype_sort_constructor
• See also: Z3.get_datatype_sort_recognizer
• See also: Z3.get_datatype_sort_constructor_accessor

Summary: Return idx'th constructor.

• Precondition: get_sort_kind t == DATATYPE_SORT
• Precondition: idx < get_datatype_sort_num_constructors c t

• See also: Z3.get_datatype_sort_num_constructors
• See also: Z3.get_datatype_sort_recognizer
• See also: Z3.get_datatype_sort_constructor_accessor

Summary: Return idx'th recognizer.

• Precondition: get_sort_kind t == DATATYPE_SORT
• Precondition: idx < get_datatype_sort_num_constructors c t

• See also: Z3.get_datatype_sort_num_constructors
• See also: Z3.get_datatype_sort_constructor
• See also: Z3.get_datatype_sort_constructor_accessor

Summary: Return idx_a'th accessor for the idx_c'th constructor.

• Precondition: get_sort_kind t == DATATYPE_SORT
• Precondition: idx_c < get_datatype_sort_num_constructors c t
• Precondition: idx_a < get_domain_size c get_datatype_sort_constructor c idx_c

• See also: Z3.get_datatype_sort_num_constructors
• See also: Z3.get_datatype_sort_constructor
• See also: Z3.get_datatype_sort_recognizer

Summary: Return number of terms in pattern.

Summary: Return i'th ast in pattern.

Summary: Interface to simplifier.

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

Summary: Convert a APP_AST into an AST. This is just type casting.

Summary: Convert an AST into a APP_AST. This is just type casting.

• Warning: This conversion is only safe if Z3.get_ast_kind returns app.

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.

• See also: Z3.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.

• See also: Z3.push

Summary: Persist AST through num_scopes pops.

Normally, references to terms are no longer valid when popping scopes beyond the level where the terms are created. If you want to reference a term below the scope where it was created, use this method to specify how many pops the term should survive. The num_scopes should be at most equal to the number of calls to push subtracted with the calls to pop.

Summary: Assert a constraing into the logical context.

After one assertion, the logical context may become inconsistent.

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

• See also: Z3.check
• See also: Z3.check_and_get_model

Summary: Check whether the given logical context is consistent or not.

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

• Remarks: Model construction must be enabled using configuration parameters (See, Z3.mk_config).

• See also: Z3.check
• See also: Z3.del_model

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.

• See also: Z3.check_and_get_model

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), a non-0 model argument is passed in, and model construction is enabled (see Z3.mk_config), then a model is stored in m. Otherwise, m is left unchanged. The caller is responsible for deleting the model using the function Z3.del_model.

• Remarks: If the model argument is non-0, then model construction must be enabled using configuration parameters (See, Z3.mk_config).

The unsatisfiable core is a subset of the assumptions, so the array has the same size as the assumptions. The core array is not populated if core_size is set to 0.

• See also: Z3.check
• See also: Z3.del_model

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). Since Z3 does not rely on exhaustive equality propagation, it is the case that that not all implied equalities are returned by this call. Only implied equalities that follow from simple constraint and equality propagation is discovered.

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

• See also: Z3.check_and_get_model
• See also: Z3.check

Summary: Delete a model object.

• See also: Z3.check_and_get_model

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.

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.

Summary: Retrieve the set of labels that were relevant in the context of the current satisfied context.

• See also: Z3.del_literals
• See also: Z3.get_num_literals
• See also: Z3.get_label_symbol
• See also: Z3.get_literal

Summary: Retrieve the set of literals that satisfy the current context.

• See also: Z3.del_literals
• See also: Z3.get_num_literals
• See also: Z3.get_label_symbol
• See also: Z3.get_literal

Summary: Retrieve the set of literals that whose assignment were guess, but not propagated during the search.

• See also: Z3.del_literals
• See also: Z3.get_num_literals
• See also: Z3.get_label_symbol
• See also: Z3.get_literal

Summary: Delete a labels context.

• See also: Z3.get_relevant_labels

Summary: Retrieve the number of label symbols that were returned.

• See also: Z3.get_relevant_labels

Summary: Retrieve label symbol at idx.

Summary: Retrieve literal expression at idx.

Summary: Disable label.

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

• See also: Z3.block_literals

Summary: Block subsequent checks using the remaining enabled labels.

Summary: Return the number of constants assigned by the given model.

• Remarks: Consider using Z3.get_model_constants.

• See also: Z3.get_model_constant

Summary: [ get_model_constant c m i ] Return the i-th constant in the given model.

• Remarks: Consider using Z3.get_model_constants.

• Precondition: i < get_model_num_constants c m

• See also: Z3.eval

Summary: Return the value of the given constant or function in the given model.

Summary: [ is_array_value c v ] Determine whether the term encodes an array value. Return the number of entries mapping to non-default values of the array.

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.

• Precondition: TRUE == is_array_value c v &num_entries

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.

• Remarks: Consider using Z3.get_model_funcs.

• See also: Z3.get_model_func_decl
• See also: Z3.get_model_func_else
• See also: Z3.get_model_func_num_entries
• See also: Z3.get_model_func_entry_num_args
• See also: Z3.get_model_func_entry_arg

Summary: [ get_model_func_decl c m i ] Return the declaration of the i-th function in the given model.

• Remarks: Consider using Z3.get_model_funcs.

• Precondition: i < get_model_num_funcs c m

• See also: Z3.get_model_num_funcs

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.

• Remarks: Consider using Z3.get_model_funcs.

• Precondition: i < get_model_num_funcs c m

• See also: Z3.get_model_num_funcs
• See also: Z3.get_model_func_num_entries
• See also: Z3.get_model_func_entry_num_args
• See also: Z3.get_model_func_entry_arg

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.

• Remarks: Consider using Z3.get_model_funcs.

• Precondition: i < get_model_num_funcs c m

• See also: Z3.get_model_num_funcs
• See also: Z3.get_model_func_else
• See also: Z3.get_model_func_entry_num_args
• See also: Z3.get_model_func_entry_arg

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.

• Remarks: Consider using Z3.get_model_funcs.

• Precondition: i < get_model_num_funcs c m
• Precondition: j < get_model_func_num_entries c m i

• See also: Z3.get_model_num_funcs
• See also: Z3.get_model_func_num_entries
• See also: Z3.get_model_func_entry_arg

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.

• Remarks: Consider using Z3.get_model_funcs.

• Precondition: i < get_model_num_funcs c m
• Precondition: j < get_model_func_num_entries c m i
• Precondition: k < get_model_func_entry_num_args c m i j

• See also: Z3.get_model_num_funcs
• See also: Z3.get_model_func_num_entries
• See also: Z3.get_model_func_entry_num_args

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.

• Remarks: Consider using Z3.get_model_funcs.

• Precondition: i < get_model_num_funcs c m
• Precondition: j < get_model_func_num_entries c m i

• See also: Z3.get_model_num_funcs
• See also: Z3.get_model_func_num_entries

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:

• t contains a quantifier or bound variable.

• the model m is partial, that is, it doesn't have a complete interpretation for free functions. That is, the option PARTIAL_MODELS=true was used.

• the evaluator doesn't have support for some interpreted operator.

• t is type incorrect.

• The result of an intepreted operator in t is undefined (e.g. division by zero).

Summary: Evaluate declaration given values.

Provides direct way to evaluate declarations without going over terms.

Summary: Log interaction to a file.

Summary: Close interaction log.

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.

• See also: Z3.ast_to_string
• See also: Z3.pattern_to_string
• See also: Z3.func_decl_to_string

Summary: Convert the given AST node into a string.

• See also: Z3.pattern_to_string
• See also: Z3.sort_to_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.

Summary: Convert the given benchmark into SMT-LIB formatted string.

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.

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.

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.

Summary: Similar to Z3.parse_smtlib_string, but reads the benchmark from a file.

Summary: Return the number of SMTLIB formulas parsed by the last call to Z3.parse_smtlib_string or Z3.parse_smtlib_file.

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.

• Precondition: i < get_smtlib_num_formulas c

Summary: Return the number of SMTLIB assumptions parsed by Z3.parse_smtlib_string or Z3.parse_smtlib_file.

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.

• Precondition: i < get_smtlib_num_assumptions c

Summary: Return the number of declarations parsed by Z3.parse_smtlib_string or Z3.parse_smtlib_file.

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.

• Precondition: i < get_smtlib_num_decls c

Summary: Return the number of sorts parsed by Z3.parse_smtlib_string or Z3.parse_smtlib_file.

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.

• Precondition: i < get_smtlib_num_sorts c

Summary: [ get_smtlib_error c ] Retrieve that last error message information generated from parsing.

Summary: [ parse_z3_string c str ] Parse the given string using the Z3 native parser.

Return the conjunction of asserts made in the input.

Summary: Similar to Z3.parse_z3_string, but reads the benchmark from a file.

Summary: Return Z3 version number information.

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.

[ mk_context_x configs ] is a shorthand for the context with configurations in configs.

[ get_app_args c a ] is the array of arguments of an application. If t is a constant, then the array is empty.

• See also: Z3.get_app_num_args
• See also: Z3.get_app_arg

[ get_app_args c d ] is the array of parameters of d.

• See also: Z3.get_domain_size
• See also: Z3.get_domain

[ get_array_sort c t ] is the domain and the range of t.

• See also: Z3.get_array_sort_domain
• See also: Z3.get_array_sort_range

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

• See also: Z3.get_tuple_sort_mk_decl
• See also: Z3.get_tuple_sort_num_fields
• See also: Z3.get_tuple_sort_field_decl

[ datatype_constructor_refined ] is the refinement of a datatype constructor.

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

val get_model_constants : context -> model -> func_decl array

[ get_model_constants c m ] is the array of constants in the model m.

• See also: Z3.get_model_num_constants
• See also: Z3.get_model_constant

[ get_model_func_entry c m i j ] is the j'th entry in the i'th function in the model m.

• See also: Z3.get_model_func_entry_num_args
• See also: Z3.get_model_func_entry_arg
• See also: Z3.get_model_func_entry_value

[ get_model_func_entries c m i ] is the array of entries in the i'th function in the model m.

• See also: Z3.get_model_func_num_entries
• See also: Z3.get_model_func_entry

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

• See also: Z3.get_model_num_funcs
• See also: Z3.get_model_func_decl
• See also: Z3.get_model_func_entries
• See also: Z3.get_model_func_else

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

• See also: Z3.parse_smtlib_string_x
• See also: Z3.parse_smtlib_file_x
• See also: Z3.parse_smtlib_string
• See also: Z3.parse_smtlib_file
• See also: Z3.get_smtlib_num_formulas
• See also: Z3.get_smtlib_formula

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

• See also: Z3.parse_smtlib_string_x
• See also: Z3.parse_smtlib_file_x
• See also: Z3.parse_smtlib_string
• See also: Z3.parse_smtlib_file
• See also: Z3.get_smtlib_num_assumptions
• See also: Z3.get_smtlib_assumption

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

• See also: Z3.parse_smtlib_string_x
• See also: Z3.parse_smtlib_file_x
• See also: Z3.parse_smtlib_string
• See also: Z3.parse_smtlib_file
• See also: Z3.get_smtlib_num_decls
• See also: Z3.get_smtlib_decl

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

• See also: Z3.parse_smtlib_string_x
• See also: Z3.parse_smtlib_file_x
• See also: Z3.parse_smtlib_string
• See also: Z3.parse_smtlib_file
• See also: Z3.get_smtlib_formulas
• See also: Z3.get_smtlib_assumptions
• See also: Z3.get_smtlib_decls

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

• See also: Z3.parse_smtlib_file_formula
• See also: Z3.parse_smtlib_string_x

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

• See also: Z3.parse_smtlib_file_formula
• See also: Z3.parse_smtlib_file_x

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

• See also: Z3.parse_smtlib_file_x
• See also: Z3.parse_smtlib_string
• See also: Z3.get_smtlib_parse_results

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

• See also: Z3.parse_smtlib_string_x
• See also: Z3.parse_smtlib_file
• See also: Z3.get_smtlib_parse_results

[ symbol_refined ] is the refinement of a Z3.symbol .

• See also: Z3.symbol_refine
• See also: Z3.get_symbol_kind

[ symbol_refine c s ] is the refined symbol of s.

• See also: Z3.symbol_refined
• See also: Z3.get_symbol_kind

[ sort_refine c t ] is the refined sort of t.

• See also: Z3.sort_refined
• See also: Z3.get_sort_kind

[ binder_type ] is a universal or existential quantifier.

• See also: Z3.term_refined

[ numeral_refined ] is the refinement of a numeral .

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

[ term_refined ] is the refinement of a Z3.ast .

• See also: Z3.term_refine

[ term_refine c a ] is the refined term of a.

• See also: Z3.term_refined