[−][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 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 |
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 if-then-else: |
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 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 |
Z3_mk_sign_ext⚠ | Sign-extend of the given bit-vector to the (signed) equivalent bit-vector of
size |
Z3_mk_zero_ext⚠ | Extend the given bit-vector with zeros to the (unsigned) equivalent
bit-vector of size |
Z3_mk_repeat⚠ | Repeat the given bit-vector 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 bit-wise addition
of |
Z3_mk_bvadd_no_underflow⚠ | Create a predicate that checks that the bit-wise signed addition
of |
Z3_mk_bvsub_no_overflow⚠ | Create a predicate that checks that the bit-wise signed subtraction
of |
Z3_mk_bvsub_no_underflow⚠ | Create a predicate that checks that the bit-wise subtraction
of |
Z3_mk_bvsdiv_no_overflow⚠ | Create a predicate that checks that the bit-wise signed division
of |
Z3_mk_bvneg_no_overflow⚠ | Check that bit-wise negation does not overflow when
|
Z3_mk_bvmul_no_overflow⚠ | Create a predicate that checks that the bit-wise multiplication
of |
Z3_mk_bvmul_no_underflow⚠ | Create a predicate that checks that the bit-wise signed multiplication
of |
Z3_mk_select⚠ | Array read.
The argument |
Z3_mk_select_n⚠ | n-ary Array read.
The argument |
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 |
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 bit-vector 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 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_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 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_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 i-th 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 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 |
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 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 |
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 user-defined string to interaction log. |
Z3_close_log⚠ | Close interaction log. |
Z3_toggle_warning_messages⚠ | Enable/disable printing warning messages to the console. |
Z3_set_ast_print_mode⚠ | Select mode for the format used for pretty-printing AST nodes. |
Z3_ast_to_string⚠ | Convert the given AST node into a string. |
Z3_pattern_to_string⚠ | |
Z3_sort_to_string⚠ | |
Z3_func_decl_to_string⚠ | |
Z3_model_to_string⚠ | Convert the given model into a string. |
Z3_benchmark_to_smtlib_string⚠ | Convert the given benchmark into SMT-LIB formatted string. |
Z3_get_parser_error⚠ | Retrieve that last error message information generated from parsing. |
Z3_get_error_code⚠ | Return the error code for the last API call. |
Z3_set_error_handler⚠ | Register a Z3 error handler. |
Z3_set_error⚠ | Set an error. |
Z3_get_error_msg⚠ | Return a string describing the given error code. |
Z3_get_version⚠ | Return Z3 version number information. |
Z3_get_full_version⚠ | Return a string that fully describes the version of Z3 in use. |
Z3_enable_trace⚠ | Enable tracing messages tagged as |
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 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_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 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_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⚠ | 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 |
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 least-fixedpoint semantics. For example, the relation is empty if it does not occur in a head or a fact. |
Z3_fixedpoint_set_predicate_representation⚠ | Configure the predicate representation. |
Z3_fixedpoint_get_rules⚠ | Retrieve set of rules from fixedpoint context. |
Z3_fixedpoint_get_assertions⚠ | Retrieve set of background assertions from fixedpoint context. |
Z3_fixedpoint_set_params⚠ | Set parameters on fixedpoint context. |
Z3_fixedpoint_get_help⚠ | Return a string describing all fixedpoint available parameters. |
Z3_fixedpoint_get_param_descrs⚠ | Return the parameter description set for the given fixedpoint object. |
Z3_fixedpoint_to_string⚠ | Print the current rules and background axioms as a string. |
Z3_fixedpoint_from_string⚠ | Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the string. |
Z3_fixedpoint_from_file⚠ | Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the file. |
Z3_fixedpoint_push⚠ | Create a backtracking point. |
Z3_fixedpoint_pop⚠ | Backtrack one backtracking point. |
Z3_fixedpoint_init⚠ | Initialize the context with a user-defined state. |
Z3_fixedpoint_set_reduce_assign_callback⚠ | Register a callback to destructive updates. |
Z3_fixedpoint_set_reduce_app_callback⚠ | Register a callback for building terms based on the relational operators. |
Z3_fixedpoint_add_callback⚠ | Set export callback for lemmas. |
Z3_fixedpoint_add_constraint⚠ | |
Z3_mk_optimize⚠ | Create a new optimize context. |
Z3_optimize_inc_ref⚠ | Increment the reference counter of the given optimize context |
Z3_optimize_dec_ref⚠ | Decrement the reference counter of the given optimize context. |
Z3_optimize_assert⚠ | Assert hard constraint to the optimization context. |
Z3_optimize_assert_soft⚠ | Assert soft constraint to the optimization context. |
Z3_optimize_maximize⚠ | Add a maximization constraint. |
Z3_optimize_minimize⚠ | Add a minimization constraint. |
Z3_optimize_push⚠ | Create a backtracking point. |
Z3_optimize_pop⚠ | Backtrack one level. |
Z3_optimize_check⚠ | Check consistency and produce optimal values. |
Z3_optimize_get_reason_unknown⚠ | Retrieve a string that describes the last status returned by |
Z3_optimize_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 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_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 |
Z3_mk_fpa_inf⚠ | Create a floating-point infinity of sort |
Z3_mk_fpa_zero⚠ | Create a floating-point zero of sort |
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 |
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 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 |
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_rational_int64⚠ | Similar to |
Z3_get_numeral_uint64⚠ | Similar to |
Z3_mk_bv2int⚠ | Create an integer from the bit-vector argument |
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 |
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 |
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_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 user-defined domains. |
Z3_fixedpoint_reduce_app_callback_fptr | |
Z3_fixedpoint_new_lemma_eh | |
Z3_fixedpoint_predecessor_eh | |
Z3_fixedpoint_unfold_eh |