[][src]Crate z3_sys

Enums

AstKind

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

AstPrintMode

Z3 pretty printing modes (See Z3_set_ast_print_mode).

DeclKind

The different kinds of interpreted function kinds.

ErrorCode

Z3 error codes (See Z3_get_error_code).

GoalPrec

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.

ParamKind

The different kinds of parameters that can be associated with parameter sets. (see Z3_mk_params).

ParameterKind

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

SortKind

The different kinds of Z3 types (See Z3_get_sort_kind).

SymbolKind

The different kinds of symbol. In Z3, a symbol can be represented using integers and strings. See Z3_get_symbol_kind.

Constants

Z3_TRUE
Z3_FALSE
Z3_L_FALSE
Z3_L_UNDEF
Z3_L_TRUE

Functions

Z3_global_param_set

Set a global (or module) parameter. This setting is shared by all Z3 contexts.

Z3_global_param_reset_all

Restore the value of all global (and module) parameters. This command will not affect already created objects (such as tactics and solvers).

Z3_global_param_get

Get a global (or module) parameter.

Z3_mk_config

Create a configuration object for the Z3 context object.

Z3_del_config

Delete the given configuration object.

Z3_set_param_value

Set a configuration parameter.

Z3_mk_context

Create a context using the given configuration.

Z3_mk_context_rc

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 Z3_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 Z3_ast returned by Z3, and Z3_dec_ref whenever the Z3_ast is not needed anymore. This idiom is similar to the one used in BDD (binary decision diagrams) packages such as CUDD.

Z3_del_context

Delete the given logical context.

Z3_inc_ref

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.

Z3_dec_ref

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.

Z3_update_param_value

Set a value of a context parameter.

Z3_interrupt

Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers, simplifiers and tactics.

Z3_mk_params

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.

Z3_params_inc_ref

Increment the reference counter of the given parameter set.

Z3_params_dec_ref

Decrement the reference counter of the given parameter set.

Z3_params_set_bool

Add a Boolean parameter k with value v to the parameter set p.

Z3_params_set_uint

Add a unsigned parameter k with value v to the parameter set p.

Z3_params_set_double

Add a double parameter k with value v to the parameter set p.

Z3_params_set_symbol

Add a symbol parameter k with value v to the parameter set p.

Z3_params_to_string

Convert a parameter set into a string. This function is mainly used for printing the contents of a parameter set.

Z3_params_validate

Validate the parameter set p against the parameter description set d.

Z3_param_descrs_inc_ref

Increment the reference counter of the given parameter description set.

Z3_param_descrs_dec_ref

Decrement the reference counter of the given parameter description set.

Z3_param_descrs_get_kind

Return the kind associated with the given parameter name n.

Z3_param_descrs_size

Return the number of parameters in the given parameter description set.

Z3_param_descrs_get_name

Return the number of parameters in the given parameter description set.

Z3_param_descrs_get_documentation

Retrieve documentation string corresponding to parameter name s.

Z3_param_descrs_to_string

Convert a parameter description set into a string. This function is mainly used for printing the contents of a parameter description set.

Z3_mk_int_symbol

Create a Z3 symbol using an integer.

Z3_mk_string_symbol

Create a Z3 symbol using a C string.

Z3_mk_uninterpreted_sort

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

Z3_mk_bool_sort

Create the Boolean type.

Z3_mk_int_sort

Create the integer type.

Z3_mk_real_sort

Create the real type.

Z3_mk_bv_sort

Create a bit-vector type of the given size.

Z3_mk_finite_domain_sort

Create a named finite domain sort.

Z3_mk_array_sort

Create an array type.

Z3_mk_array_sort_n

Create an array type with N arguments

Z3_mk_tuple_sort

Create a tuple type.

Z3_mk_enumeration_sort

Create a enumeration sort.

Z3_mk_list_sort

Create a list sort

Z3_mk_constructor

Create a constructor.

Z3_del_constructor

Reclaim memory allocated to constructor.

Z3_mk_datatype

Create datatype, such as lists, trees, records, enumerations or unions of records. The datatype may be recursive. Return the datatype sort.

Z3_mk_constructor_list

Create list of constructors.

Z3_del_constructor_list

Reclaim memory allocated for constructor list.

Z3_mk_datatypes

Create mutually recursive datatypes.

Z3_query_constructor

Query constructor for declared functions.

Z3_mk_func_decl

Declare a constant or function.

Z3_mk_app

Create a constant or function application.

Z3_mk_const

Declare and create a constant.

Z3_mk_fresh_func_decl

Declare a fresh constant or function.

Z3_mk_fresh_const

Declare and create a fresh constant.

Z3_mk_rec_func_decl

Declare a recursive function

Z3_add_rec_def

Define the body of a recursive function.

Z3_mk_true

Create an AST node representing true.

Z3_mk_false

Create an AST node representing false.

Z3_mk_eq

Create an AST node representing l = r.

Z3_mk_distinct

Create an AST node representing distinct(args[0], ..., args[num_args-1]).

Z3_mk_not

Create an AST node representing not(a).

Z3_mk_ite

Create an AST node representing an if-then-else: ite(t1, t2, t3).

Z3_mk_iff

Create an AST node representing t1 iff t2.

Z3_mk_implies

Create an AST node representing t1 implies t2.

Z3_mk_xor

Create an AST node representing t1 xor t2.

Z3_mk_and

Create an AST node representing args[0] and ... and args[num_args-1].

Z3_mk_or

Create an AST node representing args[0] or ... or args[num_args-1].

Z3_mk_add

Create an AST node representing args[0] + ... + args[num_args-1].

Z3_mk_mul

Create an AST node representing args[0] * ... * args[num_args-1].

Z3_mk_sub

Create an AST node representing args[0] - ... - args[num_args - 1].

Z3_mk_unary_minus

Create an AST node representing - arg.

Z3_mk_div

Create an AST node representing arg1 div arg2.

Z3_mk_mod

Create an AST node representing arg1 mod arg2.

Z3_mk_rem

Create an AST node representing arg1 rem arg2.

Z3_mk_power

Create an AST node representing arg1 ^ arg2.

Z3_mk_lt

Create less than.

Z3_mk_le

Create less than or equal to.

Z3_mk_gt

Create greater than.

Z3_mk_ge

Create greater than or equal to.

Z3_mk_is_int

Check if a real number is an integer.

Z3_mk_bvnot

Bitwise negation.

Z3_mk_bvredand

Take conjunction of bits in vector, return vector of length 1.

Z3_mk_bvredor

Take disjunction of bits in vector, return vector of length 1.

Z3_mk_bvand

Bitwise and.

Z3_mk_bvor

Bitwise or.

Z3_mk_bvxor

Bitwise exclusive-or.

Z3_mk_bvnand

Bitwise nand.

Z3_mk_bvnor

Bitwise nor.

Z3_mk_bvxnor

Bitwise xnor.

Z3_mk_bvneg

Standard two's complement unary minus.

Z3_mk_bvadd

Standard two's complement addition.

Z3_mk_bvsub

Standard two's complement subtraction.

Z3_mk_bvmul

Standard two's complement multiplication.

Z3_mk_bvudiv

Unsigned division.

Z3_mk_bvsdiv

Two's complement signed division.

Z3_mk_bvurem

Unsigned remainder.

Z3_mk_bvsrem

Two's complement signed remainder (sign follows dividend).

Z3_mk_bvsmod

Two's complement signed remainder (sign follows divisor).

Z3_mk_bvult

Unsigned less than.

Z3_mk_bvslt

Two's complement signed less than.

Z3_mk_bvule

Unsigned less than or equal to.

Z3_mk_bvsle

Two's complement signed less than or equal to.

Z3_mk_bvuge

Unsigned greater than or equal to.

Z3_mk_bvsge

Two's complement signed greater than or equal to.

Z3_mk_bvugt

Unsigned greater than.

Z3_mk_bvsgt

Two's complement signed greater than.

Z3_mk_concat

Concatenate the given bit-vectors.

Z3_mk_extract

Extract the bits high down to low from a bit-vector of size m to yield a new bit-vector of size n, where n = high - low + 1.

Z3_mk_sign_ext

Sign-extend of the given bit-vector to the (signed) equivalent bit-vector of size m+i, where m is the size of the given bit-vector.

Z3_mk_zero_ext

Extend the given bit-vector with zeros to the (unsigned) equivalent bit-vector of size m+i, where m is the size of the given bit-vector.

Z3_mk_repeat

Repeat the given bit-vector up length i.

Z3_mk_bvshl

Shift left.

Z3_mk_bvlshr

Logical shift right.

Z3_mk_bvashr

Arithmetic shift right.

Z3_mk_rotate_left

Rotate bits of t1 to the left i times.

Z3_mk_rotate_right

Rotate bits of t1 to the right i times.

Z3_mk_ext_rotate_left

Rotate bits of t1 to the left t2 times.

Z3_mk_ext_rotate_right

Rotate bits of t1 to the right t2 times.

Z3_mk_bvadd_no_overflow

Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.

Z3_mk_bvadd_no_underflow

Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.

Z3_mk_bvsub_no_overflow

Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.

Z3_mk_bvsub_no_underflow

Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.

Z3_mk_bvsdiv_no_overflow

Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.

Z3_mk_bvneg_no_overflow

Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector.

Z3_mk_bvmul_no_overflow

Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.

Z3_mk_bvmul_no_underflow

Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflow.

Z3_mk_select

Array read. The argument a is the array and i is the index of the array that gets read.

Z3_mk_select_n

n-ary Array read. The argument a is the array and idxs are the indices of the array that gets read.

Z3_mk_store

Array update.

Z3_mk_store_n

n-ary Array update.

Z3_mk_const_array

Create the constant array.

Z3_mk_map

Map f on the argument arrays.

Z3_mk_array_default

Access the array default value. Produces the default range value, for arrays that can be represented as finite maps with a default range value.

Z3_mk_as_array

Create array with the same interpretation as a function. The array satisfies the property (f x) = (select (_ as-array f) x) for every argument x.

Z3_mk_set_sort

Create Set type.

Z3_mk_empty_set

Create the empty set.

Z3_mk_full_set

Create the full set.

Z3_mk_set_add

Add an element to a set.

Z3_mk_set_del

Remove an element to a set.

Z3_mk_set_union

Take the union of a list of sets.

Z3_mk_set_intersect

Take the intersection of a list of sets.

Z3_mk_set_difference

Take the set difference between two sets.

Z3_mk_set_complement

Take the complement of a set.

Z3_mk_set_member

Check for set membership.

Z3_mk_set_subset

Check for subsetness of sets.

Z3_mk_array_ext

Create array extensionality index given two arrays with the same sort. The meaning is given by the axiom: (=> (= (select A (array-ext A B)) (select B (array-ext A B))) (= A B))

Z3_mk_numeral

Create a numeral of a given sort.

Z3_mk_real

Create a real from a fraction.

Z3_mk_int

Create a numeral of an int, bit-vector, or finite-domain sort.

Z3_mk_unsigned_int

Create a numeral of a int, bit-vector, or finite-domain sort.

Z3_mk_bv_numeral

create a bit-vector numeral from a vector of Booleans.

Z3_mk_seq_sort

Create a sequence sort out of the sort for the elements.

Z3_is_seq_sort

Check if s is a sequence sort.

Z3_mk_re_sort

Create a regular expression sort out of a sequence sort.

Z3_is_re_sort

Check if s is a regular expression sort.

Z3_mk_string_sort

Create a sort for 8 bit strings.

Z3_is_string_sort

Check if s is a string sort.

Z3_mk_string

Create a string constant out of the string that is passed in

Z3_is_string

Determine if s is a string constant.

Z3_get_string

Retrieve the string constant stored in s.

Z3_mk_seq_empty

Create an empty sequence of the sequence sort seq.

Z3_mk_seq_unit

Create a unit sequence of a.

Z3_mk_seq_concat

Concatenate sequences.

Z3_mk_seq_prefix

Check if prefix is a prefix of s.

Z3_mk_seq_suffix

Check if suffix is a suffix of s.

Z3_mk_seq_contains

Check if container contains containee.

Z3_mk_seq_extract

Extract subsequence starting at offset of length.

Z3_mk_seq_replace

Replace the first occurrence of src with dst in s.

Z3_mk_seq_at

Retrieve from s the unit sequence positioned at position index.

Z3_mk_seq_length

Return the length of the sequence s.

Z3_mk_seq_index

Return index of first occurrence of substr in s starting from offset offset. If s does not contain substr, then the value is -1, if offset is the length of s, then the value is -1 as well. The function is under-specified if offset is negative or larger than the length of s.

Z3_mk_str_to_int

Convert string to integer.

Z3_mk_int_to_str

Integer to string conversion.

Z3_mk_seq_to_re

Create a regular expression that accepts the sequence seq.

Z3_mk_seq_in_re

Check if seq is in the language generated by the regular expression re.

Z3_mk_re_plus

Create the regular language re+.

Z3_mk_re_star

Create the regular language re*.

Z3_mk_re_option

Create the regular language [re].

Z3_mk_re_union

Create the union of the regular languages.

Z3_mk_re_concat

Create the concatenation of the regular languages.

Z3_mk_re_range

Create the range regular expression over two sequences of length 1.

Z3_mk_re_loop

Create a regular expression loop. The supplied regular expression r is repeated between lo and hi times. The lo should be below hi with one execution: when supplying the value hi as 0, the meaning is to repeat the argument r at least lo number of times, and with an unbounded upper bound.

Z3_mk_re_intersect

Create the intersection of the regular languages.

Z3_mk_re_complement

Create the complement of the regular language re.

Z3_mk_re_empty

Create an empty regular expression of sort re.

Z3_mk_re_full

Create an universal regular expression of sort re.

Z3_mk_pattern

Create a pattern for quantifier instantiation.

Z3_mk_bound

Create a bound variable.

Z3_mk_forall

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.

Z3_mk_exists

Create an exists formula. Similar to Z3_mk_forall.

Z3_mk_quantifier

Create a quantifier - universal or existential, with pattern hints. See the documentation for Z3_mk_forall for an explanation of the parameters.

Z3_mk_quantifier_ex

Create a quantifier - universal or existential, with pattern hints, no patterns, and attributes

Z3_mk_forall_const

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

Z3_mk_exists_const

Similar to Z3_mk_forall_const.

Z3_mk_quantifier_const

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

Z3_mk_quantifier_const_ex

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

Z3_mk_lambda

Create a lambda expression.

Z3_mk_lambda_const

Create a lambda expression using a list of constants that form the set of bound variables

Z3_get_symbol_kind

Return SymbolKind::Int if the symbol was constructed using Z3_mk_int_symbol, and SymbolKind::String if the symbol was constructed using Z3_mk_string_symbol.

Z3_get_symbol_int

Return the symbol int value.

Z3_get_symbol_string

Return the symbol name.

Z3_get_sort_name

Return the sort name as a symbol.

Z3_get_sort_id

Return a unique identifier for s.

Z3_sort_to_ast

Convert a Z3_sort into Z3_ast. This is just type casting.

Z3_is_eq_sort

compare sorts.

Z3_get_sort_kind

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

Z3_get_bv_sort_size

Return the size of the given bit-vector sort.

Z3_get_finite_domain_sort_size

Store the size of the sort in r. Return false if the call failed. That is, Z3_get_sort_kind(s) == SortKind::FiniteDomain

Z3_get_array_sort_domain

Return the domain of the given array sort.

Z3_get_array_sort_range

Return the range of the given array sort.

Z3_get_tuple_sort_mk_decl

Return the constructor declaration of the given tuple sort.

Z3_get_tuple_sort_num_fields

Return the number of fields of the given tuple sort.

Z3_get_tuple_sort_field_decl

Return the i-th field declaration (i.e., projection function declaration) of the given tuple sort.

Z3_get_datatype_sort_num_constructors

Return number of constructors for datatype.

Z3_get_datatype_sort_constructor

Return idx'th constructor.

Z3_get_datatype_sort_recognizer

Return idx'th recognizer.

Z3_get_datatype_sort_constructor_accessor

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

Z3_datatype_update_field

Update record field with a value.

Z3_get_relation_arity

Return arity of relation.

Z3_get_relation_column

Return sort at i'th column of relation sort.

Z3_mk_atmost

Pseudo-Boolean relations.

Z3_mk_atleast

Pseudo-Boolean relations.

Z3_mk_pble

Pseudo-Boolean relations.

Z3_mk_pbge

Pseudo-Boolean relations.

Z3_mk_pbeq

Pseudo-Boolean relations.

Z3_func_decl_to_ast

Convert a Z3_func_decl into Z3_ast. This is just type casting.

Z3_is_eq_func_decl

Compare terms.

Z3_get_func_decl_id

Return a unique identifier for f.

Z3_get_decl_name

Return the constant declaration name as a symbol.

Z3_get_decl_kind

Return declaration kind corresponding to declaration.

Z3_get_domain_size

Return the number of parameters of the given declaration.

Z3_get_arity

Alias for Z3_get_domain_size.

Z3_get_domain

Return the sort of the i-th parameter of the given function declaration.

Z3_get_range

Return the range of the given declaration.

Z3_get_decl_num_parameters

Return the number of parameters associated with a declaration.

Z3_get_decl_parameter_kind

Return the parameter type associated with a declaration.

Z3_get_decl_int_parameter

Return the integer value associated with an integer parameter.

Z3_get_decl_double_parameter

Return the double value associated with an double parameter.

Z3_get_decl_symbol_parameter

Return the double value associated with an double parameter.

Z3_get_decl_sort_parameter

Return the sort value associated with a sort parameter.

Z3_get_decl_ast_parameter

Return the expression value associated with an expression parameter.

Z3_get_decl_func_decl_parameter

Return the expression value associated with an expression parameter.

Z3_get_decl_rational_parameter

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

Z3_app_to_ast

Convert a Z3_app into Z3_ast. This is just type casting.

Z3_get_app_decl

Return the declaration of a constant or function application.

Z3_get_app_num_args

Return the number of argument of an application. If t is an constant, then the number of arguments is 0.

Z3_get_app_arg

Return the i-th argument of the given application.

Z3_is_eq_ast

Compare terms.

Z3_get_ast_id

Return a unique identifier for t.

Z3_get_ast_hash

Return a hash code for the given AST.

Z3_get_sort

Return the sort of an AST node.

Z3_is_well_sorted

Return true if the given expression t is well sorted.

Z3_get_bool_value

Return Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF otherwise.

Z3_get_ast_kind

Return the kind of the given AST.

Z3_is_app
Z3_is_numeral_ast
Z3_is_algebraic_number

Return true if the given AST is a real algebraic number.

Z3_to_app

Convert an ast into an Z3_App. This is just type casting.

Z3_to_func_decl

Convert an AST into a Z3_func_decl. This is just type casting.

Z3_get_numeral_string

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

Z3_get_numeral_decimal_string

Return numeral as a string in decimal notation. The result has at most precision decimal places.

Z3_get_numerator

Return the numerator (as a numeral AST) of a numeral AST of sort Real.

Z3_get_denominator

Return the denominator (as a numeral AST) of a numeral AST of sort Real.

Z3_get_numeral_small

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

Z3_get_numeral_int

Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int. Return true if the call succeeded.

Z3_get_numeral_uint

Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine unsigned int. Return true if the call succeeded.

Z3_get_algebraic_number_lower

Return a lower bound for the given real algebraic number.

Z3_get_algebraic_number_upper

Return an upper bound for the given real algebraic number.

Z3_pattern_to_ast

Convert a Z3_pattern into Z3_ast. This is just type casting.

Z3_get_pattern_num_terms

Return number of terms in pattern.

Z3_get_pattern

Return i'th ast in pattern.

Z3_get_index_value

Return index of de-Bruijn bound variable.

Z3_is_quantifier_forall

Determine if quantifier is universal.

Z3_is_quantifier_exists

Determine if ast is an existential quantifier.

Z3_is_lambda

Determine if ast is a lambda expression.

Z3_get_quantifier_weight

Obtain weight of quantifier.

Z3_get_quantifier_num_patterns

Return number of patterns used in quantifier.

Z3_get_quantifier_pattern_ast

Return i'th pattern.

Z3_get_quantifier_num_no_patterns

Return number of no_patterns used in quantifier.

Z3_get_quantifier_no_pattern_ast

Return i'th no_pattern.

Z3_get_quantifier_num_bound

Return number of bound variables of quantifier.

Z3_get_quantifier_bound_name

Return symbol of the i'th bound variable.

Z3_get_quantifier_bound_sort

Return sort of the i'th bound variable.

Z3_get_quantifier_body

Return body of quantifier.

Z3_simplify

Interface to simplifier.

Z3_simplify_ex

Interface to simplifier.

Z3_simplify_get_help

Return a string describing all available parameters.

Z3_simplify_get_param_descrs

Return the parameter description set for the simplify procedure.

Z3_update_term

Update the arguments of term a using the arguments args.

Z3_substitute

Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs.

Z3_substitute_vars

Substitute the free variables in a with the expressions in to.

Z3_translate

Translate/Copy the AST a from context source to context target.

Z3_mk_model

Create a fresh model object. It has reference count 0.

Z3_model_inc_ref

Increment the reference counter of the given model.

Z3_model_dec_ref

Decrement the reference counter of the given model.

Z3_model_eval

Evaluate the AST node t in the given model. Return true if succeeded, and store the result in v.

Z3_model_get_const_interp

Return the interpretation (i.e., assignment) of constant a in the model m.

Z3_model_has_interp

Test if there exists an interpretation (i.e., assignment) for a in the model m.

Z3_model_get_func_interp

Return the interpretation of the function f in the model m.

Z3_model_get_num_consts

Return the number of constants assigned by the given model.

Z3_model_get_const_decl

Return the i-th constant in the given model.

Z3_model_get_num_funcs

Return the number of function interpretations in the given model.

Z3_model_get_func_decl

Return the declaration of the i-th function in the given model.

Z3_model_get_num_sorts

Return the number of uninterpreted sorts that m assigns an interpretation to.

Z3_model_get_sort

Return an uninterpreted sort that m assigns an interpretation.

Z3_model_get_sort_universe

Return the finite set of distinct values that represent the interpretation for sort s.

Z3_model_translate

Translate model from context c to context dst.

Z3_is_as_array

The (_ as-array f) AST node is a construct for assigning interpretations for arrays in Z3.

Z3_get_as_array_func_decl

Return the function declaration f associated with a (_ as_array f) node.

Z3_add_func_interp

Create a fresh func_interp object, add it to a model for a specified function. It has reference count 0.

Z3_add_const_interp

Add a constant interpretation.

Z3_func_interp_inc_ref

Increment the reference counter of the given Z3_func_interp object.

Z3_func_interp_dec_ref

Decrement the reference counter of the given Z3_func_interp object.

Z3_func_interp_get_num_entries

Return the number of entries in the given function interpretation.

Z3_func_interp_get_entry

Return a "point" of the given function interpretation. It represents the value of f in a particular point.

Z3_func_interp_get_else

Return the 'else' value of the given function interpretation.

Z3_func_interp_set_else

Return the 'else' value of the given function interpretation.

Z3_func_interp_get_arity

Return the arity (number of arguments) of the given function interpretation.

Z3_func_interp_add_entry

add a function entry to a function interpretation.

Z3_func_entry_inc_ref

Increment the reference counter of the given Z3_func_entry object.

Z3_func_entry_dec_ref

Decrement the reference counter of the given Z3_func_entry object.

Z3_func_entry_get_value

Return the value of this point.

Z3_func_entry_get_num_args

Return the number of arguments in a Z3_func_entry object.

Z3_func_entry_get_arg

Return an argument of a Z3_func_entry object.

Z3_open_log

Log interaction to a file.

Z3_append_log

Append user-defined string to interaction log.

Z3_close_log

Close interaction log.

Z3_toggle_warning_messages

Enable/disable printing warning messages to the console.

Z3_set_ast_print_mode

Select mode for the format used for pretty-printing AST nodes.

Z3_ast_to_string

Convert the given AST node into a string.

Z3_pattern_to_string
Z3_sort_to_string
Z3_func_decl_to_string
Z3_model_to_string

Convert the given model into a string.

Z3_benchmark_to_smtlib_string

Convert the given benchmark into SMT-LIB formatted string.

Z3_get_parser_error

Retrieve that last error message information generated from parsing.

Z3_get_error_code

Return the error code for the last API call.

Z3_set_error_handler

Register a Z3 error handler.

Z3_set_error

Set an error.

Z3_get_error_msg

Return a string describing the given error code.

Z3_get_version

Return Z3 version number information.

Z3_get_full_version

Return a string that fully describes the version of Z3 in use.

Z3_enable_trace

Enable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise

Z3_disable_trace

Disable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise

Z3_reset_memory

Reset all allocated resources.

Z3_finalize_memory

Destroy all allocated resources.

Z3_mk_goal

Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers.

Z3_goal_inc_ref

Increment the reference counter of the given goal.

Z3_goal_dec_ref

Decrement the reference counter of the given goal.

Z3_goal_precision

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.

Z3_goal_assert

Add a new formula a to the given goal. The formula is split according to the following procedure that is applied until a fixed-point: Conjunctions are split into separate formulas. Negations are distributed over disjunctions, resulting in separate formulas. If the goal is false, adding new formulas is a no-op. If the formula a is true, then nothing is added. If the formula a is false, then the entire goal is replaced by the formula false.

Z3_goal_inconsistent

Return true if the given goal contains the formula false.

Z3_goal_depth

Return the depth of the given goal. It tracks how many transformations were applied to it.

Z3_goal_reset

Erase all formulas from the given goal.

Z3_goal_size

Return the number of formulas in the given goal.

Z3_goal_formula

Return a formula from the given goal.

Z3_goal_num_exprs

Return the number of formulas, subformulas and terms in the given goal.

Z3_goal_is_decided_sat

Return true if the goal is empty, and it is precise or the product of a under approximation.

Z3_goal_is_decided_unsat

Return true if the goal contains false, and it is precise or the product of an over approximation.

Z3_goal_translate

Copy a goal g from the context source to the context target.

Z3_goal_convert_model

Convert a model of the formulas of a goal to a model of an original goal. The model may be null, in which case the returned model is valid if the goal was established satisfiable.

Z3_goal_to_string

Convert a goal into a string.

Z3_goal_to_dimacs_string

Convert a goal into a DIMACS formatted string. The goal must be in CNF. You can convert a goal to CNF by applying the tseitin-cnf tactic. Bit-vectors are not automatically converted to Booleans either, so the if caller intends to preserve satisfiability, it should apply bit-blasting tactics. Quantifiers and theory atoms will not be encoded.

Z3_mk_tactic

Return a tactic associated with the given name.

Z3_tactic_inc_ref

Increment the reference counter of the given tactic.

Z3_tactic_dec_ref

Decrement the reference counter of the given tactic.

Z3_mk_probe

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-tactic) in the SMT 2.0 front-end.

Z3_probe_inc_ref

Increment the reference counter of the given probe.

Z3_probe_dec_ref

Decrement the reference counter of the given probe.

Z3_tactic_and_then

Return a tactic that applies t1 to a given goal and t2 to every subgoal produced by t1.

Z3_tactic_or_else

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.

Z3_tactic_par_or

Return a tactic that applies the given tactics in parallel.

Z3_tactic_par_and_then

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.

Z3_tactic_try_for

Return a tactic that applies t to a given goal for ms milliseconds. If t does not terminate in ms milliseconds, then it fails.

Z3_tactic_when

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.

Z3_tactic_cond

Return a tactic that applies t1 to a given goal if the probe p evaluates to true, and t2 if p evaluates to false.

Z3_tactic_repeat

Return a tactic that keeps applying t until the goal is not modified anymore or the maximum number of iterations max is reached.

Z3_tactic_skip

Return a tactic that just return the given goal.

Z3_tactic_fail

Return a tactic that always fails.

Z3_tactic_fail_if

Return a tactic that fails if the probe p evaluates to false.

Z3_tactic_fail_if_not_decided

Return a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains false).

Z3_tactic_using_params

Return a tactic that applies t using the given set of parameters.

Z3_probe_const

Return a probe that always evaluates to val.

Z3_probe_lt

Return a probe that evaluates to "true" when the value returned by p1 is less than the value returned by p2.

Z3_probe_gt

Return a probe that evaluates to "true" when the value returned by p1 is greater than the value returned by p2.

Z3_probe_le

Return a probe that evaluates to "true" when the value returned by p1 is less than or equal to the value returned by p2.

Z3_probe_ge

Return a probe that evaluates to "true" when the value returned by p1 is greater than or equal to the value returned by p2.

Z3_probe_eq

Return a probe that evaluates to "true" when the value returned by p1 is equal to the value returned by p2.

Z3_probe_and

Return a probe that evaluates to "true" when p1 and p2 evaluates to true.

Z3_probe_or

Return a probe that evaluates to "true" when p1 or p2 evaluates to true.

Z3_probe_not

Return a probe that evaluates to "true" when p does not evaluate to true.

Z3_get_num_tactics

Return the number of builtin tactics available in Z3.

Z3_get_tactic_name

Return the name of the idx tactic.

Z3_get_num_probes

Return the number of builtin probes available in Z3.

Z3_get_probe_name

Return the name of the i probe.

Z3_tactic_get_help

Return a string containing a description of parameters accepted by the given tactic.

Z3_tactic_get_param_descrs

Return the parameter description set for the given tactic object.

Z3_tactic_get_descr

Return a string containing a description of the tactic with the given name.

Z3_probe_get_descr

Return a string containing a description of the probe with the given name.

Z3_probe_apply

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.

Z3_tactic_apply

Apply tactic t to the goal g.

Z3_tactic_apply_ex

Apply tactic t to the goal g using the parameter set p.

Z3_apply_result_inc_ref

Increment the reference counter of the given Z3_apply_result object.

Z3_apply_result_dec_ref

Decrement the reference counter of the given Z3_apply_result object.

Z3_apply_result_to_string

Convert the Z3_apply_result object returned by Z3_tactic_apply into a string.

Z3_apply_result_get_num_subgoals

Return the number of subgoals in the Z3_apply_result object returned by Z3_tactic_apply.

Z3_apply_result_get_subgoal

Return one of the subgoals in the Z3_apply_result object returned by Z3_tactic_apply.

Z3_apply_result_convert_model

Convert a model for the subgoal Z3_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 Z3_tactic_apply(c, t, g).

Z3_mk_solver

Create a new solver. This solver is a "combined solver" (see combined_solver module) that internally uses a non-incremental (solver1) and an incremental solver (solver2). This combined solver changes its behaviour based on how it is used and how its parameters are set.

Z3_mk_simple_solver

Create a new incremental solver.

Z3_mk_solver_for_logic

Create a new solver customized for the given logic. It behaves like Z3_mk_solver if the logic is unknown or unsupported.

Z3_mk_solver_from_tactic

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.

Z3_solver_translate

Copy a solver s from the context source to the context target.

Z3_solver_import_model_converter

Ad-hoc method for importing model conversion from solver.

Z3_solver_get_help

Return a string describing all solver available parameters.

Z3_solver_get_param_descrs

Return the parameter description set for the given solver object.

Z3_solver_set_params

Set the given solver using the given parameters.

Z3_solver_inc_ref

Increment the reference counter of the given solver.

Z3_solver_dec_ref

Decrement the reference counter of the given solver.

Z3_solver_push

Create a backtracking point.

Z3_solver_pop

Backtrack n backtracking points.

Z3_solver_reset

Remove all assertions from the solver.

Z3_solver_get_num_scopes

Return the number of backtracking points.

Z3_solver_assert

Assert a constraint into the solver.

Z3_solver_assert_and_track

Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant p.

Z3_solver_from_file

load solver assertions from a file.

Z3_solver_from_string

load solver assertions from a string.

Z3_solver_get_assertions

Return the set of asserted formulas on the solver.

Z3_solver_get_units

Return the set of units modulo model conversion.

Z3_solver_get_non_units

Return the set of non units in the solver state.

Z3_solver_check

Check whether the assertions in a given solver are consistent or not.

Z3_solver_check_assumptions

Check whether the assertions in the given solver and optional assumptions are consistent or not.

Z3_get_implied_equalities

Retrieve congruence class representatives for terms.

Z3_solver_get_consequences

retrieve consequences from solver that determine values of the supplied function symbols.

Z3_solver_cube

Extract a next cube for a solver. The last cube is the constant true or false. The number of (non-constant) cubes is by default 1. For the sat solver cubing is controlled using parameters sat.lookahead.cube.cutoff and sat.lookahead.cube.fraction.

Z3_solver_get_model

Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions

Z3_solver_get_proof

Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions

Z3_solver_get_unsat_core

Retrieve the unsat core for the last Z3_solver_check_assumptions The unsat core is a subset of the assumptions a.

Z3_solver_get_reason_unknown

Return a brief justification for an "unknown" result (i.e., Z3_L_UNDEF) for the commands Z3_solver_check and Z3_solver_check_assumptions

Z3_solver_get_statistics

Return statistics for the given solver.

Z3_solver_to_string

Convert a solver into a string.

Z3_stats_to_string

Convert a statistics into a string.

Z3_stats_inc_ref

Increment the reference counter of the given statistics object.

Z3_stats_dec_ref

Decrement the reference counter of the given statistics object.

Z3_stats_size

Return the number of statistical data in s.

Z3_stats_get_key

Return the key (a string) for a particular statistical data.

Z3_stats_is_uint

Return true if the given statistical data is a unsigned integer.

Z3_stats_is_double

Return true if the given statistical data is a double.

Z3_stats_get_uint_value

Return the unsigned value of the given statistical data.

Z3_stats_get_double_value

Return the double value of the given statistical data.

Z3_get_estimated_alloc_size

Return the estimated allocated memory in bytes.

Z3_mk_ast_vector

Return an empty AST vector.

Z3_ast_vector_inc_ref

Increment the reference counter of the given AST vector.

Z3_ast_vector_dec_ref

Decrement the reference counter of the given AST vector.

Z3_ast_vector_size

Return the size of the given AST vector.

Z3_ast_vector_get

Return the AST at position i in the AST vector v.

Z3_ast_vector_set

Update position i of the AST vector v with the AST a.

Z3_ast_vector_resize

Resize the AST vector v.

Z3_ast_vector_push

Add the AST a in the end of the AST vector v. The size of v is increased by one.

Z3_ast_vector_translate

Translate the AST vector v from context s into an AST vector in context t.

Z3_ast_vector_to_string

Convert AST vector into a string.

Z3_mk_ast_map

Return an empty mapping from AST to AST

Z3_ast_map_inc_ref

Increment the reference counter of the given AST map.

Z3_ast_map_dec_ref

Decrement the reference counter of the given AST map.

Z3_ast_map_contains

Return true if the map m contains the AST key k.

Z3_ast_map_find

Return the value associated with the key k.

Z3_ast_map_insert

Store/Replace a new key, value pair in the given map.

Z3_ast_map_erase

Erase a key from the map.

Z3_ast_map_reset

Remove all keys from the given map.

Z3_ast_map_size

Return the size of the given map.

Z3_ast_map_keys

Return the keys stored in the given map.

Z3_ast_map_to_string

Convert the given map into a string.

Z3_algebraic_is_value

Return true if a can be used as value in the Z3 real algebraic number package.

Z3_algebraic_is_pos

Return true if a is positive, and false otherwise.

Z3_algebraic_is_neg

Return true if a is negative, and false otherwise.

Z3_algebraic_is_zero

Return true if a is zero, and false otherwise.

Z3_algebraic_sign

Return 1 if a is positive, 0 if a is zero, and -1 if a is negative.

Z3_algebraic_add

Return the value a + b.

Z3_algebraic_sub

Return the value a - b.

Z3_algebraic_mul

Return the value a * b.

Z3_algebraic_div

Return the value a / b.

Z3_algebraic_root

Return the a^(1/k)

Z3_algebraic_power

Return the a^k

Z3_algebraic_lt

Return true if a < b, and false otherwise.

Z3_algebraic_gt

Return true if a > b, and false otherwise.

Z3_algebraic_le

Return true if a <= b, and false otherwise.

Z3_algebraic_ge

Return true if a >= b, and false otherwise.

Z3_algebraic_eq

Return true if a == b, and false otherwise.

Z3_algebraic_neq

Return true if a != b, and false otherwise.

Z3_algebraic_roots

Given a multivariate polynomial p(x_0, ..., x_{n-1}, x_n), returns the roots of the univariate polynomial p(a[0], ..., a[n-1], x_n).

Z3_algebraic_eval

Given a multivariate polynomial p(x_0, ..., x_{n-1}), return the sign of p(a[0], ..., a[n-1]).

Z3_polynomial_subresultants

Return the nonzero subresultants of p and q with respect to the "variable" x.

Z3_rcf_del

Delete a RCF numeral created using the RCF API.

Z3_rcf_mk_rational

Return a RCF rational using the given string.

Z3_rcf_mk_small_int

Return a RCF small integer.

Z3_rcf_mk_pi

Return Pi

Z3_rcf_mk_e

Return e (Euler's constant)

Z3_rcf_mk_infinitesimal

Return a new infinitesimal that is smaller than all elements in the Z3 field.

Z3_rcf_mk_roots

Store in roots the roots of the polynomial a[n-1]*x^{n-1} + ... + a[0]. The output vector roots must have size n. It returns the number of roots of the polynomial.

Z3_rcf_add

Return the value a + b.

Z3_rcf_sub

Return the value a - b.

Z3_rcf_mul

Return the value a * b.

Z3_rcf_div

Return the value a / b.

Z3_rcf_neg

Return the value -a.

Z3_rcf_inv

Return the value 1/a.

Z3_rcf_power

Return the value a^k.

Z3_rcf_lt

Return true if a < b.

Z3_rcf_gt

Return true if a > b.

Z3_rcf_le

Return true if a <= b.

Z3_rcf_ge

Return true if a >= b.

Z3_rcf_eq

Return true if a == b.

Z3_rcf_neq

Return true if a != b.

Z3_rcf_num_to_string

Convert the RCF numeral into a string.

Z3_rcf_num_to_decimal_string

Convert the RCF numeral into a string in decimal notation.

Z3_rcf_get_numerator_denominator

Extract the "numerator" and "denominator" of the given RCF numeral.

Z3_mk_fixedpoint

Create a new fixedpoint context.

Z3_fixedpoint_inc_ref

Increment the reference counter of the given fixedpoint context

Z3_fixedpoint_dec_ref

Decrement the reference counter of the given fixedpoint context.

Z3_fixedpoint_add_rule

Add a universal Horn clause as a named rule. The horn_rule should be of the form:

Z3_fixedpoint_add_fact

Add a Database fact.

Z3_fixedpoint_assert

Assert a constraint to the fixedpoint context.

Z3_fixedpoint_query

Pose a query against the asserted rules.

Z3_fixedpoint_query_relations

Pose multiple queries against the asserted rules.

Z3_fixedpoint_get_answer

Retrieve a formula that encodes satisfying answers to the query.

Z3_fixedpoint_get_reason_unknown

Retrieve a string that describes the last status returned by Z3_fixedpoint_query.

Z3_fixedpoint_update_rule

Update a named rule. A rule with the same name must have been previously created.

Z3_fixedpoint_get_num_levels

Query the PDR engine for the maximal levels properties are known about predicate.

Z3_fixedpoint_get_cover_delta

Retrieve the current cover of pred up to level unfoldings. Return just the delta that is known at level. To obtain the full set of properties of pred one should query at level+1 , level+2 etc, and include level=-1.

Z3_fixedpoint_add_cover

Add property about the predicate pred. Add a property of predicate pred at level. It gets pushed forward when possible.

Z3_fixedpoint_get_statistics

Retrieve statistics information from the last call to Z3_fixedpoint_query.

Z3_fixedpoint_register_relation

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.

Z3_fixedpoint_set_predicate_representation

Configure the predicate representation.

Z3_fixedpoint_get_rules

Retrieve set of rules from fixedpoint context.

Z3_fixedpoint_get_assertions

Retrieve set of background assertions from fixedpoint context.

Z3_fixedpoint_set_params

Set parameters on fixedpoint context.

Z3_fixedpoint_get_help

Return a string describing all fixedpoint available parameters.

Z3_fixedpoint_get_param_descrs

Return the parameter description set for the given fixedpoint object.

Z3_fixedpoint_to_string

Print the current rules and background axioms as a string.

Z3_fixedpoint_from_string

Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the string.

Z3_fixedpoint_from_file

Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the file.

Z3_fixedpoint_push

Create a backtracking point.

Z3_fixedpoint_pop

Backtrack one backtracking point.

Z3_fixedpoint_init

Initialize the context with a user-defined state.

Z3_fixedpoint_set_reduce_assign_callback

Register a callback to destructive updates.

Z3_fixedpoint_set_reduce_app_callback

Register a callback for building terms based on the relational operators.

Z3_fixedpoint_add_callback

Set export callback for lemmas.

Z3_fixedpoint_add_constraint
Z3_mk_optimize

Create a new optimize context.

Z3_optimize_inc_ref

Increment the reference counter of the given optimize context

Z3_optimize_dec_ref

Decrement the reference counter of the given optimize context.

Z3_optimize_assert

Assert hard constraint to the optimization context.

Z3_optimize_assert_soft

Assert soft constraint to the optimization context.

Z3_optimize_maximize

Add a maximization constraint.

Z3_optimize_minimize

Add a minimization constraint.

Z3_optimize_push

Create a backtracking point.

Z3_optimize_pop

Backtrack one level.

Z3_optimize_check

Check consistency and produce optimal values.

Z3_optimize_get_reason_unknown

Retrieve a string that describes the last status returned by Z3_optimize_check.

Z3_optimize_get_model

Retrieve the model for the last Z3_optimize_check

Z3_optimize_get_unsat_core

Retrieve the unsat core for the last Z3_optimize_check.

Z3_optimize_set_params

Set parameters on optimization context.

Z3_optimize_get_param_descrs

Return the parameter description set for the given optimize object.

Z3_optimize_get_lower

Retrieve lower bound value or approximation for the i'th optimization objective.

Z3_optimize_get_upper

Retrieve upper bound value or approximation for the i'th optimization objective.

Z3_optimize_get_lower_as_vector

Retrieve lower bound value or approximation for the i'th optimization objective. The returned vector is of length 3. It always contains numerals. The three numerals are coefficients a, b, c and encode the result of Z3_optimize_get_lower a * infinity + b + c * epsilon.

Z3_optimize_get_upper_as_vector

Retrieve upper bound value or approximation for the i'th optimization objective.

Z3_optimize_to_string

Print the current context as a string.

Z3_optimize_from_string

Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context.

Z3_optimize_from_file

Parse an SMT-LIB2 file with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context.

Z3_optimize_get_help

Return a string containing a description of parameters accepted by optimize.

Z3_optimize_get_statistics

Retrieve statistics information from the last call to Z3_optimize_check

Z3_optimize_get_assertions

Return the set of asserted formulas on the optimization context.

Z3_optimize_get_objectives

Return objectives on the optimization context. If the objective function is a max-sat objective it is returned as a Pseudo-Boolean (minimization) sum of the form (+ (if f1 w1 0) (if f2 w2 0) ...) If the objective function is entered as a maximization objective, then return the corresponding minimization objective. In this way the resulting objective function is always returned as a minimization objective.

Z3_mk_fpa_rounding_mode_sort

Create the RoundingMode sort.

Z3_mk_fpa_round_nearest_ties_to_even

Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.

Z3_mk_fpa_rne

Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.

Z3_mk_fpa_round_nearest_ties_to_away

Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.

Z3_mk_fpa_rna

Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.

Z3_mk_fpa_round_toward_positive

Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.

Z3_mk_fpa_rtp

Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.

Z3_mk_fpa_round_toward_negative

Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.

Z3_mk_fpa_rtn

Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.

Z3_mk_fpa_round_toward_zero

Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.

Z3_mk_fpa_rtz

Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.

Z3_mk_fpa_sort

Create a FloatingPoint sort.

Z3_mk_fpa_sort_half

Create the half-precision (16-bit) FloatingPoint sort.

Z3_mk_fpa_sort_single

Create the single-precision (32-bit) FloatingPoint sort.

Z3_mk_fpa_sort_double

Create the double-precision (64-bit) FloatingPoint sort.

Z3_mk_fpa_sort_quadruple

Create the quadruple-precision (128-bit) FloatingPoint sort.

Z3_mk_fpa_nan

Create a floating-point NaN of sort s.

Z3_mk_fpa_inf

Create a floating-point infinity of sort s.

Z3_mk_fpa_zero

Create a floating-point zero of sort s.

Z3_mk_fpa_fp

Create an expression of FloatingPoint sort from three bit-vector expressions.

Z3_mk_fpa_numeral_float

Create a numeral of FloatingPoint sort from a float.

Z3_mk_fpa_numeral_double

Create a numeral of FloatingPoint sort from a double.

Z3_mk_fpa_numeral_int

Create a numeral of FloatingPoint sort from a signed integer.

Z3_mk_fpa_numeral_int_uint

Create a numeral of FloatingPoint sort from a sign bit and two integers.

Z3_mk_fpa_abs

Floating-point absolute value

Z3_mk_fpa_neg

Floating-point negation

Z3_mk_fpa_add

Floating-point addition

Z3_mk_fpa_sub

Floating-point subtraction

Z3_mk_fpa_mul

Floating-point multiplication

Z3_mk_fpa_div

Floating-point division

Z3_mk_fpa_fma

Floating-point fused multiply-add.

Z3_mk_fpa_sqrt

Floating-point square root

Z3_mk_fpa_rem

Floating-point remainder

Z3_mk_fpa_round_to_integral

Floating-point roundToIntegral. Rounds a floating-point number to the closest integer, again represented as a floating-point number.

Z3_mk_fpa_min

Minimum of floating-point numbers.

Z3_mk_fpa_max

Maximum of floating-point numbers.

Z3_mk_fpa_leq

Floating-point less than or equal.

Z3_mk_fpa_lt

Floating-point less than.

Z3_mk_fpa_geq

Floating-point greater than or equal.

Z3_mk_fpa_gt

Floating-point greater than.

Z3_mk_fpa_eq

Floating-point equality.

Z3_mk_fpa_is_normal

Predicate indicating whether t is a normal floating-point number.

Z3_mk_fpa_is_subnormal

Predicate indicating whether t is a subnormal floating-point number.

Z3_mk_fpa_is_zero

Predicate indicating whether t is a floating-point number with zero value, i.e., +zero or -zero.

Z3_mk_fpa_is_infinite

Predicate indicating whether t is a floating-point number representing +oo or -oo.

Z3_mk_fpa_is_nan

Predicate indicating whether t is a NaN.

Z3_mk_fpa_is_negative

Predicate indicating whether t is a negative floating-point number.

Z3_mk_fpa_is_positive

Predicate indicating whether t is a positive floating-point number.

Z3_mk_fpa_to_fp_bv

Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.

Z3_mk_fpa_to_fp_float

Conversion of a FloatingPoint term into another term of different FloatingPoint sort.

Z3_mk_fpa_to_fp_real

Conversion of a term of real sort into a term of FloatingPoint sort.

Z3_mk_fpa_to_fp_signed

Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.

Z3_mk_fpa_to_fp_unsigned

Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort.

Z3_mk_fpa_to_ubv

Conversion of a floating-point term into an unsigned bit-vector.

Z3_mk_fpa_to_sbv

Conversion of a floating-point term into a signed bit-vector.

Z3_mk_fpa_to_real

Conversion of a floating-point term into a real-numbered term.

Z3_fpa_get_ebits

Retrieves the number of bits reserved for the exponent in a FloatingPoint sort.

Z3_fpa_get_sbits

Retrieves the number of bits reserved for the significand in a FloatingPoint sort.

Z3_fpa_is_numeral_nan

Checks whether a given floating-point numeral is a NaN.

Z3_fpa_is_numeral_inf

Checks whether a given floating-point numeral is a +oo or -oo.

Z3_fpa_is_numeral_zero

Checks whether a given floating-point numeral is +zero or -zero.

Z3_fpa_is_numeral_normal

Checks whether a given floating-point numeral is normal.

Z3_fpa_is_numeral_subnormal

Checks whether a given floating-point numeral is subnormal.

Z3_fpa_is_numeral_positive

Checks whether a given floating-point numeral is positive.

Z3_fpa_is_numeral_negative

Checks whether a given floating-point numeral is negative.

Z3_fpa_get_numeral_sign_bv

Retrieves the sign of a floating-point literal as a bit-vector expression.

Z3_fpa_get_numeral_significand_bv

Retrieves the significand of a floating-point literal as a bit-vector expression.

Z3_fpa_get_numeral_sign

Retrieves the sign of a floating-point literal.

Z3_fpa_get_numeral_significand_string

Return the significand value of a floating-point numeral as a string.

Z3_fpa_get_numeral_exponent_string

Return the exponent value of a floating-point numeral as a string.

Z3_fpa_get_numeral_exponent_bv

Retrieves the exponent of a floating-point literal as a bit-vector expression.

Z3_mk_fpa_to_ieee_bv

Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.

Z3_mk_fpa_to_fp_int_real

Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort.

Z3_fixedpoint_query_from_lvl

Pose a query against the asserted rules at the given level.

Z3_fixedpoint_get_ground_sat_answer

Retrieve a bottom-up (from query) sequence of ground facts

Z3_fixedpoint_get_rules_along_trace

Obtain the list of rules along the counterexample trace.

Z3_fixedpoint_get_rule_names_along_trace

Obtain the list of rules along the counterexample trace.

Z3_fixedpoint_add_invariant

Add an assumed invariant of predicate pred.

Z3_fixedpoint_get_reachable

Retrieve reachable states of a predicate.

Z3_qe_model_project

Project variables given a model

Z3_qe_model_project_skolem

Project variables given a model

Z3_model_extrapolate

Extrapolates a model of a formula

Z3_qe_lite

Best-effort quantifier elimination

Z3_eval_smtlib2_string

Parse and evaluate and SMT-LIB2 command sequence. The state from a previous call is saved so the next evaluation builds on top of the previous call.

Z3_fpa_get_numeral_exponent_int64

Return the exponent value of a floating-point numeral as a signed 64-bit integer

Z3_fpa_get_numeral_significand_uint64

Return the significand value of a floating-point numeral as a uint64.

Z3_get_numeral_int64

Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int64_t int. Return true if the call succeeded.

Z3_get_numeral_rational_int64

Similar to Z3_get_numeral_string, but only succeeds if the value can fit as a rational number as machine int64_t int. Return true if the call succeeded.

Z3_get_numeral_uint64

Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine uint64_t int. Return true if the call succeeded.

Z3_mk_bv2int

Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 is treated as unsigned. 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.

Z3_mk_fpa_numeral_int64_uint64

Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.

Z3_mk_fpa_sort_16

Create the half-precision (16-bit) FloatingPoint sort.

Z3_mk_fpa_sort_32

Create the single-precision (32-bit) FloatingPoint sort.

Z3_mk_fpa_sort_64

Create the double-precision (64-bit) FloatingPoint sort.

Z3_mk_fpa_sort_128

Create the quadruple-precision (128-bit) FloatingPoint sort.

Z3_mk_int2real

Coerce an integer to a real.

Z3_mk_int2bv

Create an n bit bit-vector from the integer argument t1.

Z3_mk_int64

Create a numeral of a int, bit-vector, or finite-domain sort.

Z3_mk_real2int

Coerce a real to an integer.

Z3_mk_unsigned_int64

Create a numeral of a int, bit-vector, or finite-domain sort.

Z3_parse_smtlib2_string

Parse the given string using the SMT-LIB2 parser.

Z3_parse_smtlib2_file

Similar to Z3_parse_smtlib2_string, but reads the benchmark from a file.

Type Definitions

Z3_symbol

Lisp-like symbol used to name types, constants, and functions. A symbol can be created using string or integers.

Z3_literals
Z3_config

Configuration object used to initialize logical contexts.

Z3_context

Manager of all other Z3 objects, global configuration options, etc.

Z3_sort

Kind of AST used to represent types.

Z3_func_decl

Kind of AST used to represent function symbols.

Z3_ast

Abstract Syntax Tree node. That is, the data structure used in Z3 to represent terms, formulas, and types.

Z3_app

Kind of AST used to represent function applications.

Z3_pattern

Kind of AST used to represent pattern and multi-patterns used to guide quantifier instantiation.

Z3_model

Model for the constraints inserted into the logical context.

Z3_constructor

Type constructor for a (recursive) datatype.

Z3_constructor_list

List of constructors for a (recursive) datatype.

Z3_params

Parameter set used to configure many components such as: simplifiers, tactics, solvers, etc.

Z3_param_descrs

Provides a collection of parameter names, their types, default values and documentation strings. Solvers, tactics, and other objects accept different collection of parameters.

Z3_goal

Set of formulas that can be solved and/or transformed using tactics and solvers.

Z3_tactic

Basic building block for creating custom solvers for specific problem domains.

Z3_probe

Function/predicate used to inspect a goal and collect information that may be used to decide which solver and/or preprocessing step will be used.

Z3_stats

Statistical data for a solver.

Z3_solver

(Incremental) solver, possibly specialized by a particular tactic or logic.

Z3_ast_vector

Vector of Z3_ast objects.

Z3_ast_map

Mapping from Z3_ast to Z3_ast objects.

Z3_apply_result

Collection of subgoals resulting from applying of a tactic to a goal.

Z3_func_interp

Interpretation of a function in a model.

Z3_func_entry

Representation of the value of a Z3_func_interp at a particular point.

Z3_fixedpoint

Context for the recursive predicate solver.

Z3_optimize

Context for solving optimization queries.

Z3_rcf_num
Z3_bool

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

Z3_string

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

Z3_string_ptr
Z3_lbool

Lifted Boolean type: false, undefined, true.

Z3_error_handler

Z3 custom error handler (See Z3_set_error_handler).

Z3_fixedpoint_reduce_assign_callback_fptr

The following utilities allows adding user-defined domains.

Z3_fixedpoint_reduce_app_callback_fptr
Z3_fixedpoint_new_lemma_eh
Z3_fixedpoint_predecessor_eh
Z3_fixedpoint_unfold_eh