[−][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 
DeclKind  The different kinds of interpreted function kinds. 
ErrorCode  Z3 error codes (See 
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 
ParameterKind  The different kinds of parameters that can be associated with function symbols. 
SortKind  The different kinds of Z3 types (See 
SymbolKind  The different kinds of symbol.
In Z3, a symbol can be represented using integers and
strings. See 
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_del_context^{⚠}  Delete the given logical context. 
Z3_inc_ref^{⚠}  Increment the reference counter of the given AST.
The context 
Z3_dec_ref^{⚠}  Decrement the reference counter of the given AST.
The 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 
Z3_params_set_uint^{⚠}  Add a unsigned parameter 
Z3_params_set_double^{⚠}  Add a double parameter 
Z3_params_set_symbol^{⚠}  Add a symbol parameter 
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 
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 
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 
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 bitvector 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 
Z3_mk_false^{⚠}  Create an AST node representing 
Z3_mk_eq^{⚠}  Create an AST node representing 
Z3_mk_distinct^{⚠}  Create an AST node representing 
Z3_mk_not^{⚠}  Create an AST node representing 
Z3_mk_ite^{⚠}  Create an AST node representing an ifthenelse: 
Z3_mk_iff^{⚠}  Create an AST node representing 
Z3_mk_implies^{⚠}  Create an AST node representing 
Z3_mk_xor^{⚠}  Create an AST node representing 
Z3_mk_and^{⚠}  Create an AST node representing 
Z3_mk_or^{⚠}  Create an AST node representing 
Z3_mk_add^{⚠}  Create an AST node representing 
Z3_mk_mul^{⚠}  Create an AST node representing 
Z3_mk_sub^{⚠}  Create an AST node representing 
Z3_mk_unary_minus^{⚠}  Create an AST node representing 
Z3_mk_div^{⚠}  Create an AST node representing 
Z3_mk_mod^{⚠}  Create an AST node representing 
Z3_mk_rem^{⚠}  Create an AST node representing 
Z3_mk_power^{⚠}  Create an AST node representing 
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 exclusiveor. 
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 bitvectors. 
Z3_mk_extract^{⚠}  Extract the bits 
Z3_mk_sign_ext^{⚠}  Signextend of the given bitvector to the (signed) equivalent bitvector of
size 
Z3_mk_zero_ext^{⚠}  Extend the given bitvector with zeros to the (unsigned) equivalent
bitvector of size 
Z3_mk_repeat^{⚠}  Repeat the given bitvector up length 
Z3_mk_bvshl^{⚠}  Shift left. 
Z3_mk_bvlshr^{⚠}  Logical shift right. 
Z3_mk_bvashr^{⚠}  Arithmetic shift right. 
Z3_mk_rotate_left^{⚠}  Rotate bits of 
Z3_mk_rotate_right^{⚠}  Rotate bits of 
Z3_mk_ext_rotate_left^{⚠}  Rotate bits of 
Z3_mk_ext_rotate_right^{⚠}  Rotate bits of 
Z3_mk_bvadd_no_overflow^{⚠}  Create a predicate that checks that the bitwise addition
of 
Z3_mk_bvadd_no_underflow^{⚠}  Create a predicate that checks that the bitwise signed addition
of 
Z3_mk_bvsub_no_overflow^{⚠}  Create a predicate that checks that the bitwise signed subtraction
of 
Z3_mk_bvsub_no_underflow^{⚠}  Create a predicate that checks that the bitwise subtraction
of 
Z3_mk_bvsdiv_no_overflow^{⚠}  Create a predicate that checks that the bitwise signed division
of 
Z3_mk_bvneg_no_overflow^{⚠}  Check that bitwise negation does not overflow when

Z3_mk_bvmul_no_overflow^{⚠}  Create a predicate that checks that the bitwise multiplication
of 
Z3_mk_bvmul_no_underflow^{⚠}  Create a predicate that checks that the bitwise signed multiplication
of 
Z3_mk_select^{⚠}  Array read.
The argument 
Z3_mk_select_n^{⚠}  nary Array read.
The argument 
Z3_mk_store^{⚠}  Array update. 
Z3_mk_store_n^{⚠}  nary 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 (_ asarray 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 (arrayext A B)) (select B (arrayext 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, bitvector, or finitedomain sort. 
Z3_mk_unsigned_int^{⚠}  Create a numeral of a int, bitvector, or finitedomain sort. 
Z3_mk_bv_numeral^{⚠}  create a bitvector 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 
Z3_mk_re_sort^{⚠}  Create a regular expression sort out of a sequence sort. 
Z3_is_re_sort^{⚠}  Check if 
Z3_mk_string_sort^{⚠}  Create a sort for 8 bit strings. 
Z3_is_string_sort^{⚠}  Check if 
Z3_mk_string^{⚠}  Create a string constant out of the string that is passed in 
Z3_is_string^{⚠}  Determine if 
Z3_get_string^{⚠}  Retrieve the string constant stored in 
Z3_mk_seq_empty^{⚠}  Create an empty sequence of the sequence sort 
Z3_mk_seq_unit^{⚠}  Create a unit sequence of 
Z3_mk_seq_concat^{⚠}  Concatenate sequences. 
Z3_mk_seq_prefix^{⚠}  Check if 
Z3_mk_seq_suffix^{⚠}  Check if 
Z3_mk_seq_contains^{⚠}  Check if 
Z3_mk_seq_extract^{⚠}  Extract subsequence starting at 
Z3_mk_seq_replace^{⚠}  Replace the first occurrence of 
Z3_mk_seq_at^{⚠}  Retrieve from 
Z3_mk_seq_length^{⚠}  Return the length of the sequence 
Z3_mk_seq_index^{⚠}  Return index of first occurrence of 
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 
Z3_mk_seq_in_re^{⚠}  Check if 
Z3_mk_re_plus^{⚠}  Create the regular language 
Z3_mk_re_star^{⚠}  Create the regular language 
Z3_mk_re_option^{⚠}  Create the regular language 
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 
Z3_mk_re_intersect^{⚠}  Create the intersection of the regular languages. 
Z3_mk_re_complement^{⚠}  Create the complement of the regular language 
Z3_mk_re_empty^{⚠}  Create an empty regular expression of sort 
Z3_mk_re_full^{⚠}  Create an universal regular expression of sort 
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 
Z3_mk_exists^{⚠}  Create an exists formula. Similar to 
Z3_mk_quantifier^{⚠}  Create a quantifier  universal or existential, with pattern hints.
See the documentation for 
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_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 
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 
Z3_sort_to_ast^{⚠}  Convert a 
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 bitvector sort. 
Z3_get_finite_domain_sort_size^{⚠}  Store the size of the sort in 
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 ith 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^{⚠}  PseudoBoolean relations. 
Z3_mk_atleast^{⚠}  PseudoBoolean relations. 
Z3_mk_pble^{⚠}  PseudoBoolean relations. 
Z3_mk_pbge^{⚠}  PseudoBoolean relations. 
Z3_mk_pbeq^{⚠}  PseudoBoolean relations. 
Z3_func_decl_to_ast^{⚠}  Convert a 
Z3_is_eq_func_decl^{⚠}  Compare terms. 
Z3_get_func_decl_id^{⚠}  Return a unique identifier for 
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^{⚠}  Return the sort of the ith 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_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 
Z3_get_app_arg^{⚠}  Return the ith argument of the given application. 
Z3_is_eq_ast^{⚠}  Compare terms. 
Z3_get_ast_id^{⚠}  Return a unique identifier for 
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 
Z3_get_bool_value^{⚠}  Return 
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 
Z3_to_func_decl^{⚠}  Convert an AST into a 
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 
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_uint^{⚠}  Similar to 
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_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 deBruijn 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 
Z3_substitute^{⚠}  Substitute every occurrence of 
Z3_substitute_vars^{⚠}  Substitute the free variables in 
Z3_translate^{⚠}  Translate/Copy the AST 
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 
Z3_model_get_const_interp^{⚠}  Return the interpretation (i.e., assignment) of constant 
Z3_model_has_interp^{⚠}  Test if there exists an interpretation (i.e., assignment) for 
Z3_model_get_func_interp^{⚠}  Return the interpretation of the function 
Z3_model_get_num_consts^{⚠}  Return the number of constants assigned by the given model. 
Z3_model_get_const_decl^{⚠}  Return the ith 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 ith function in the given model. 
Z3_model_get_num_sorts^{⚠}  Return the number of uninterpreted sorts that 
Z3_model_get_sort^{⚠}  Return an uninterpreted sort that 
Z3_model_get_sort_universe^{⚠}  Return the finite set of distinct values that represent the interpretation for sort 
Z3_model_translate^{⚠}  Translate model from context 
Z3_is_as_array^{⚠}  The 
Z3_get_as_array_func_decl^{⚠}  Return the function declaration 
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_dec_ref^{⚠}  Decrement the reference counter of the given 
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 
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_dec_ref^{⚠}  Decrement the reference counter of the given 
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_get_arg^{⚠}  Return an argument of a 
Z3_open_log^{⚠}  Log interaction to a file. 
Z3_append_log^{⚠}  Append userdefined 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 prettyprinting 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 SMTLIB 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 
Z3_disable_trace^{⚠}  Disable tracing messages tagged as 
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 
Z3_goal_inconsistent^{⚠}  Return true if the given goal contains the formula 
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 
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 tseitincnf tactic. Bitvectors are not automatically converted to Booleans either, so the if caller intends to preserve satisfiability, it should apply bitblasting 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_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 
Z3_tactic_or_else^{⚠}  Return a tactic that first applies 
Z3_tactic_par_or^{⚠}  Return a tactic that applies the given tactics in parallel. 
Z3_tactic_par_and_then^{⚠}  Return a tactic that applies 
Z3_tactic_try_for^{⚠}  Return a tactic that applies 
Z3_tactic_when^{⚠}  Return a tactic that applies 
Z3_tactic_cond^{⚠}  Return a tactic that applies 
Z3_tactic_repeat^{⚠}  Return a tactic that keeps applying 
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 
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 
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 
Z3_probe_gt^{⚠}  Return a probe that evaluates to "true" when the value returned by 
Z3_probe_le^{⚠}  Return a probe that evaluates to "true" when the value returned by 
Z3_probe_ge^{⚠}  Return a probe that evaluates to "true" when the value returned by 
Z3_probe_eq^{⚠}  Return a probe that evaluates to "true" when the value returned by 
Z3_probe_and^{⚠}  Return a probe that evaluates to "true" when 
Z3_probe_or^{⚠}  Return a probe that evaluates to "true" when 
Z3_probe_not^{⚠}  Return a probe that evaluates to "true" when 
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 
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 
Z3_tactic_apply_ex^{⚠}  Apply tactic 
Z3_apply_result_inc_ref^{⚠}  Increment the reference counter of the given 
Z3_apply_result_dec_ref^{⚠}  Decrement the reference counter of the given 
Z3_apply_result_to_string^{⚠}  Convert the 
Z3_apply_result_get_num_subgoals^{⚠}  Return the number of subgoals in the 
Z3_apply_result_get_subgoal^{⚠}  Return one of the subgoals in the 
Z3_apply_result_convert_model^{⚠}  Convert a model for the subgoal 
Z3_mk_solver^{⚠}  Create a new solver. This solver is a "combined solver" (see combined_solver module) that internally uses a nonincremental (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_from_tactic^{⚠}  Create a new solver that is implemented using the given tactic.
The solver supports the commands 
Z3_solver_translate^{⚠}  Copy a solver 
Z3_solver_import_model_converter^{⚠}  Adhoc 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 
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 
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 
Z3_solver_get_model^{⚠}  Retrieve the model for the last 
Z3_solver_get_proof^{⚠}  Retrieve the proof for the last 
Z3_solver_get_unsat_core^{⚠}  Retrieve the unsat core for the last 
Z3_solver_get_reason_unknown^{⚠}  Return a brief justification for an "unknown" result (i.e., 
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 
Z3_stats_get_key^{⚠}  Return the key (a string) for a particular statistical data. 
Z3_stats_is_uint^{⚠}  Return 
Z3_stats_is_double^{⚠}  Return 
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 
Z3_ast_vector_set^{⚠}  Update position 
Z3_ast_vector_resize^{⚠}  Resize the AST vector 
Z3_ast_vector_push^{⚠}  Add the AST 
Z3_ast_vector_translate^{⚠}  Translate the AST vector 
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 
Z3_ast_map_find^{⚠}  Return the value associated with the key 
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 
Z3_algebraic_is_pos^{⚠}  Return 
Z3_algebraic_is_neg^{⚠}  Return 
Z3_algebraic_is_zero^{⚠}  Return 
Z3_algebraic_sign^{⚠}  Return 1 if 
Z3_algebraic_add^{⚠}  Return the value 
Z3_algebraic_sub^{⚠}  Return the value 
Z3_algebraic_mul^{⚠}  Return the value 
Z3_algebraic_div^{⚠}  Return the value 
Z3_algebraic_root^{⚠}  Return the 
Z3_algebraic_power^{⚠}  Return the 
Z3_algebraic_lt^{⚠}  Return 
Z3_algebraic_gt^{⚠}  Return 
Z3_algebraic_le^{⚠}  Return 
Z3_algebraic_ge^{⚠}  Return 
Z3_algebraic_eq^{⚠}  Return 
Z3_algebraic_neq^{⚠}  Return 
Z3_algebraic_roots^{⚠}  Given a multivariate polynomial 
Z3_algebraic_eval^{⚠}  Given a multivariate polynomial 
Z3_polynomial_subresultants^{⚠}  Return the nonzero subresultants of 
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 
Z3_rcf_add^{⚠}  Return the value 
Z3_rcf_sub^{⚠}  Return the value 
Z3_rcf_mul^{⚠}  Return the value 
Z3_rcf_div^{⚠}  Return the value 
Z3_rcf_neg^{⚠}  Return the value 
Z3_rcf_inv^{⚠}  Return the value 
Z3_rcf_power^{⚠}  Return the value 
Z3_rcf_lt^{⚠}  Return 
Z3_rcf_gt^{⚠}  Return 
Z3_rcf_le^{⚠}  Return 
Z3_rcf_ge^{⚠}  Return 
Z3_rcf_eq^{⚠}  Return 
Z3_rcf_neq^{⚠}  Return 
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 
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_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 
Z3_fixedpoint_add_cover^{⚠}  Add property about the predicate 
Z3_fixedpoint_get_statistics^{⚠}  Retrieve statistics information from the last call to 
Z3_fixedpoint_register_relation^{⚠}  Register relation as Fixedpoint defined. Fixedpoint defined relations have leastfixedpoint 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 SMTLIB2 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 SMTLIB2 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 userdefined 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_get_model^{⚠}  Retrieve the model for the last 
Z3_optimize_get_unsat_core^{⚠}  Retrieve the unsat core for the last 
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_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 SMTLIB2 string with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context. 
Z3_optimize_from_file^{⚠}  Parse an SMTLIB2 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_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 maxsat objective it is returned as a PseudoBoolean (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 halfprecision (16bit) FloatingPoint sort. 
Z3_mk_fpa_sort_single^{⚠}  Create the singleprecision (32bit) FloatingPoint sort. 
Z3_mk_fpa_sort_double^{⚠}  Create the doubleprecision (64bit) FloatingPoint sort. 
Z3_mk_fpa_sort_quadruple^{⚠}  Create the quadrupleprecision (128bit) FloatingPoint sort. 
Z3_mk_fpa_nan^{⚠}  Create a floatingpoint NaN of sort 
Z3_mk_fpa_inf^{⚠}  Create a floatingpoint infinity of sort 
Z3_mk_fpa_zero^{⚠}  Create a floatingpoint zero of sort 
Z3_mk_fpa_fp^{⚠}  Create an expression of FloatingPoint sort from three bitvector 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^{⚠}  Floatingpoint absolute value 
Z3_mk_fpa_neg^{⚠}  Floatingpoint negation 
Z3_mk_fpa_add^{⚠}  Floatingpoint addition 
Z3_mk_fpa_sub^{⚠}  Floatingpoint subtraction 
Z3_mk_fpa_mul^{⚠}  Floatingpoint multiplication 
Z3_mk_fpa_div^{⚠}  Floatingpoint division 
Z3_mk_fpa_fma^{⚠}  Floatingpoint fused multiplyadd. 
Z3_mk_fpa_sqrt^{⚠}  Floatingpoint square root 
Z3_mk_fpa_rem^{⚠}  Floatingpoint remainder 
Z3_mk_fpa_round_to_integral^{⚠}  Floatingpoint roundToIntegral. Rounds a floatingpoint number to the closest integer, again represented as a floatingpoint number. 
Z3_mk_fpa_min^{⚠}  Minimum of floatingpoint numbers. 
Z3_mk_fpa_max^{⚠}  Maximum of floatingpoint numbers. 
Z3_mk_fpa_leq^{⚠}  Floatingpoint less than or equal. 
Z3_mk_fpa_lt^{⚠}  Floatingpoint less than. 
Z3_mk_fpa_geq^{⚠}  Floatingpoint greater than or equal. 
Z3_mk_fpa_gt^{⚠}  Floatingpoint greater than. 
Z3_mk_fpa_eq^{⚠}  Floatingpoint equality. 
Z3_mk_fpa_is_normal^{⚠}  Predicate indicating whether 
Z3_mk_fpa_is_subnormal^{⚠}  Predicate indicating whether 
Z3_mk_fpa_is_zero^{⚠}  Predicate indicating whether 
Z3_mk_fpa_is_infinite^{⚠}  Predicate indicating whether 
Z3_mk_fpa_is_nan^{⚠}  Predicate indicating whether 
Z3_mk_fpa_is_negative^{⚠}  Predicate indicating whether 
Z3_mk_fpa_is_positive^{⚠}  Predicate indicating whether 
Z3_mk_fpa_to_fp_bv^{⚠}  Conversion of a single IEEE 7542008 bitvector into a floatingpoint 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 bitvector term into a term of FloatingPoint sort. 
Z3_mk_fpa_to_fp_unsigned^{⚠}  Conversion of a 2's complement unsigned bitvector term into a term of FloatingPoint sort. 
Z3_mk_fpa_to_ubv^{⚠}  Conversion of a floatingpoint term into an unsigned bitvector. 
Z3_mk_fpa_to_sbv^{⚠}  Conversion of a floatingpoint term into a signed bitvector. 
Z3_mk_fpa_to_real^{⚠}  Conversion of a floatingpoint term into a realnumbered 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 floatingpoint numeral is a NaN. 
Z3_fpa_is_numeral_inf^{⚠}  Checks whether a given floatingpoint numeral is a +oo or oo. 
Z3_fpa_is_numeral_zero^{⚠}  Checks whether a given floatingpoint numeral is +zero or zero. 
Z3_fpa_is_numeral_normal^{⚠}  Checks whether a given floatingpoint numeral is normal. 
Z3_fpa_is_numeral_subnormal^{⚠}  Checks whether a given floatingpoint numeral is subnormal. 
Z3_fpa_is_numeral_positive^{⚠}  Checks whether a given floatingpoint numeral is positive. 
Z3_fpa_is_numeral_negative^{⚠}  Checks whether a given floatingpoint numeral is negative. 
Z3_fpa_get_numeral_sign_bv^{⚠}  Retrieves the sign of a floatingpoint literal as a bitvector expression. 
Z3_fpa_get_numeral_significand_bv^{⚠}  Retrieves the significand of a floatingpoint literal as a bitvector expression. 
Z3_fpa_get_numeral_sign^{⚠}  Retrieves the sign of a floatingpoint literal. 
Z3_fpa_get_numeral_significand_string^{⚠}  Return the significand value of a floatingpoint numeral as a string. 
Z3_fpa_get_numeral_exponent_string^{⚠}  Return the exponent value of a floatingpoint numeral as a string. 
Z3_fpa_get_numeral_exponent_bv^{⚠}  Retrieves the exponent of a floatingpoint literal as a bitvector expression. 
Z3_mk_fpa_to_ieee_bv^{⚠}  Conversion of a floatingpoint term into a bitvector term in IEEE 7542008 format. 
Z3_mk_fpa_to_fp_int_real^{⚠}  Conversion of a realsorted significand and an integersorted 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 bottomup (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 
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^{⚠}  Besteffort quantifier elimination 
Z3_eval_smtlib2_string^{⚠}  Parse and evaluate and SMTLIB2 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 floatingpoint numeral as a signed 64bit integer 
Z3_fpa_get_numeral_significand_uint64^{⚠}  Return the significand value of a floatingpoint numeral as a uint64. 
Z3_get_numeral_int64^{⚠}  Similar to 
Z3_get_numeral_rational_int64^{⚠}  Similar to 
Z3_get_numeral_uint64^{⚠}  Similar to 
Z3_mk_bv2int^{⚠}  Create an integer from the bitvector argument 
Z3_mk_fpa_numeral_int64_uint64^{⚠}  Create a numeral of FloatingPoint sort from a sign bit and two 64bit integers. 
Z3_mk_fpa_sort_16^{⚠}  Create the halfprecision (16bit) FloatingPoint sort. 
Z3_mk_fpa_sort_32^{⚠}  Create the singleprecision (32bit) FloatingPoint sort. 
Z3_mk_fpa_sort_64^{⚠}  Create the doubleprecision (64bit) FloatingPoint sort. 
Z3_mk_fpa_sort_128^{⚠}  Create the quadrupleprecision (128bit) FloatingPoint sort. 
Z3_mk_int2real^{⚠}  Coerce an integer to a real. 
Z3_mk_int2bv^{⚠}  Create an 
Z3_mk_int64^{⚠}  Create a numeral of a int, bitvector, or finitedomain sort. 
Z3_mk_real2int^{⚠}  Coerce a real to an integer. 
Z3_mk_unsigned_int64^{⚠}  Create a numeral of a int, bitvector, or finitedomain sort. 
Z3_parse_smtlib2_string^{⚠}  Parse the given string using the SMTLIB2 parser. 
Z3_parse_smtlib2_file^{⚠}  Similar to 
Type Definitions
Z3_symbol  Lisplike 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 multipatterns 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_map  
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_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 
Z3_string_ptr  
Z3_lbool  Lifted Boolean type: 
Z3_error_handler  Z3 custom error handler (See 
Z3_fixedpoint_reduce_assign_callback_fptr  The following utilities allows adding userdefined domains. 
Z3_fixedpoint_reduce_app_callback_fptr  
Z3_fixedpoint_new_lemma_eh  
Z3_fixedpoint_predecessor_eh  
Z3_fixedpoint_unfold_eh 