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.
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_numeral_double⚠	Return numeral as a double.
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_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_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_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_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