MathSAT API Reference
API for the MathSAT SMT solver.
More...
|
struct | msat_config |
| MathSAT configuration.
|
|
struct | msat_env |
| MathSAT environment.
|
|
struct | msat_term |
| MathSAT term.
|
|
struct | msat_decl |
| MathSAT declaration.
|
|
struct | msat_type |
| MathSAT types.
|
|
struct | msat_model |
| MathSAT model.
|
|
struct | msat_model_iterator |
| MathSAT model iterator.
|
|
struct | msat_proof_manager |
| Manager for proofs generated by MathSAT.
|
|
struct | msat_proof |
| Proof objects created by MathSAT.
|
|
struct | msat_dpll_callback |
| Callback object for using an external SAT solver as DPLL engine in MathSAT.
|
|
struct | msat_ext_dpll_interface |
| Interface that external SAT solvers must implement.
|
|
|
|
msat_config | msat_create_config (void) |
| Creates a new MathSAT configuration. More...
|
|
msat_config | msat_create_default_config (const char *logic) |
| Creates a new MathSAT configuration with the default settings for the given logic. More...
|
|
msat_config | msat_parse_config (const char *data) |
| Creates a new MathSAT configuration by parsing the given data. More...
|
|
msat_config | msat_parse_config_file (FILE *f) |
| Creates a new MathSAT configuration by parsing the given file. More...
|
|
void | msat_destroy_config (msat_config cfg) |
| Destroys a configuration. More...
|
|
msat_env | msat_create_env (msat_config cfg) |
| Creates a new MathSAT environment from the given configuration. More...
|
|
msat_env | msat_create_shared_env (msat_config cfg, msat_env sibling) |
| Creates an environment that can share terms with its sibling. More...
|
|
void | msat_destroy_env (msat_env e) |
| Destroys an environment. More...
|
|
int | msat_gc_env (msat_env env, msat_term *tokeep, size_t num_tokeep) |
| Performs garbage collection on the given environment. More...
|
|
int | msat_set_option (msat_config cfg, const char *option, const char *value) |
| Sets an option in the given configuration. More...
|
|
int | msat_set_termination_test (msat_env env, msat_termination_test func, void *user_data) |
| Installs a custom termination test in the given environment. More...
|
|
msat_type | msat_get_bool_type (msat_env env) |
| returns the type for Booleans in the given env. More...
|
|
msat_type | msat_get_rational_type (msat_env env) |
| returns the type for rationals in the given env. More...
|
|
msat_type | msat_get_integer_type (msat_env env) |
| returns the type for integers in the given env. More...
|
|
msat_type | msat_get_bv_type (msat_env env, size_t width) |
| returns the type for bit-vectors of the given width. More...
|
|
msat_type | msat_get_array_type (msat_env env, msat_type itp, msat_type etp) |
| returns the type for arrays with indices of itp type and elements of etp type. More...
|
|
msat_type | msat_get_fp_type (msat_env env, size_t exp_width, size_t mant_width) |
| returns the type for floats with the given exponent and significand/mantissa width. More...
|
|
msat_type | msat_get_fp_roundingmode_type (msat_env env) |
| returns the type for float rounding modes in the given env. More...
|
|
msat_type | msat_get_simple_type (msat_env env, const char *name) |
| returns an atomic type with the given name in the given env. More...
|
|
msat_type | msat_get_function_type (msat_env env, msat_type *param_types, size_t num_params, msat_type return_type) |
| returns a function type in the given env. More...
|
|
msat_type | msat_get_enum_type (msat_env env, const char *name, size_t domain_size, const char **domain) |
| returns an enum type in the given env. More...
|
|
int | msat_is_bool_type (msat_env env, msat_type tp) |
| checks whether the given type is bool. More...
|
|
int | msat_is_rational_type (msat_env env, msat_type tp) |
| checks whether the given type is rat. More...
|
|
int | msat_is_integer_type (msat_env env, msat_type tp) |
| checks whether the given type is int. More...
|
|
int | msat_is_bv_type (msat_env env, msat_type tp, size_t *out_width) |
| checks whether the given type is a bit-vector. More...
|
|
int | msat_is_array_type (msat_env env, msat_type tp, msat_type *out_itp, msat_type *out_etp) |
| checks whether the given type is an array. More...
|
|
int | msat_is_fp_type (msat_env env, msat_type tp, size_t *out_exp_width, size_t *out_mant_width) |
| checks whether the given type is a float. More...
|
|
int | msat_is_fp_roundingmode_type (msat_env env, msat_type tp) |
| checks whether the given type is a float rounding mode type. More...
|
|
int | msat_is_enum_type (msat_env env, msat_type tp, size_t *out_domain_size, msat_decl **out_domain) |
| checks whether the given type is an enum More...
|
|
int | msat_type_equals (msat_type t1, msat_type t2) |
| checks whether two types are the same More...
|
|
char * | msat_type_repr (msat_type t) |
| Returns an internal string representation of a type. More...
|
|
size_t | msat_type_id (msat_type t) |
| Returns a numeric identifier for the input type. More...
|
|
msat_decl | msat_declare_function (msat_env e, const char *name, msat_type type) |
| Declares a new uninterpreted function/constant. More...
|
|
|
msat_term | msat_make_true (msat_env e) |
| Returns a term representing logical truth. More...
|
|
msat_term | msat_make_false (msat_env e) |
| Returns a term representing logical falsity. More...
|
|
msat_term | msat_make_iff (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the equivalence of t1 and t2. More...
|
|
msat_term | msat_make_or (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the logical OR of t1 and t2. More...
|
|
msat_term | msat_make_and (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the logical AND of t1 and t2. More...
|
|
msat_term | msat_make_not (msat_env e, msat_term t1) |
| Returns a term representing the logical negation of t1. More...
|
|
msat_term | msat_make_equal (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the equivalence of t1 and t2. More...
|
|
msat_term | msat_make_eq (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the equivalence of t1 and t2. More...
|
|
msat_term | msat_make_leq (msat_env e, msat_term t1, msat_term t2) |
| Returns an atom representing (t1 <= t2). More...
|
|
msat_term | msat_make_plus (msat_env e, msat_term t1, msat_term t2) |
| Returns an expression representing (t1 + t2). More...
|
|
msat_term | msat_make_times (msat_env e, msat_term t1, msat_term t2) |
| Returns an expression representing (t1 * t2). More...
|
|
msat_term | msat_make_divide (msat_env e, msat_term t1, msat_term t2) |
| Returns an expression representing (t1 / t2). More...
|
|
msat_term | msat_make_int_modular_congruence (msat_env e, mpz_t modulus, msat_term t1, msat_term t2) |
| Returns an expression representing (t1 = t2 mod modulus). More...
|
|
msat_term | msat_make_floor (msat_env e, msat_term t) |
| Returns an expression representing (floor t) More...
|
|
msat_term | msat_make_pi (msat_env e) |
| Returns the constant representing the pi number. More...
|
|
msat_term | msat_make_exp (msat_env e, msat_term t) |
| Returns an expression representing exp(t) More...
|
|
msat_term | msat_make_sin (msat_env e, msat_term t) |
| Returns an expression representing sin(t) More...
|
|
msat_term | msat_make_log (msat_env e, msat_term t) |
| Returns an expression representing the natural log of t. More...
|
|
msat_term | msat_make_pow (msat_env e, msat_term tb, msat_term te) |
| Returns an expression representing tb to the power of te. More...
|
|
msat_term | msat_make_asin (msat_env e, msat_term t) |
| Returns an expression representing arcsin(t) More...
|
|
msat_term | msat_make_number (msat_env e, const char *num_rep) |
| Returns an expression representing an integer or rational number. More...
|
|
msat_term | msat_make_int_number (msat_env e, int value) |
| Returns an expression representing an integer or rational number. More...
|
|
msat_term | msat_make_mpq_number (msat_env e, mpq_t value) |
| Returns an expression representing an integer or rational number. More...
|
|
msat_term | msat_make_term_ite (msat_env e, msat_term c, msat_term tt, msat_term te) |
| Returns an expression representing a term if-then-else construct. More...
|
|
msat_term | msat_make_constant (msat_env e, msat_decl var) |
| Creates a constant from a declaration. More...
|
|
msat_term | msat_make_uf (msat_env e, msat_decl func, msat_term args[]) |
| Creates an uninterpreted function application. More...
|
|
msat_term | msat_make_array_read (msat_env e, msat_term arr, msat_term idx) |
| Creates an array read operation. More...
|
|
msat_term | msat_make_array_write (msat_env e, msat_term arr, msat_term idx, msat_term elem) |
| Creates an array write operation. More...
|
|
msat_term | msat_make_array_const (msat_env e, msat_type arrtp, msat_term elem) |
| Creates a constant array. More...
|
|
msat_term | msat_make_bv_number (msat_env e, const char *num_rep, size_t width, size_t base) |
| Returns an expression representing a bit-vector number. More...
|
|
msat_term | msat_make_bv_int_number (msat_env e, int value, size_t width) |
| Returns an expression representing a bit-vector number. More...
|
|
msat_term | msat_make_bv_mpz_number (msat_env e, mpz_t value, size_t width) |
| Returns an expression representing a bit-vector number. More...
|
|
msat_term | msat_make_bv_concat (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the concatenation of t1 and t2. More...
|
|
msat_term | msat_make_bv_extract (msat_env e, size_t msb, size_t lsb, msat_term t) |
| Returns a term representing the selection of t[msb:lsb]. More...
|
|
msat_term | msat_make_bv_or (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the bit-wise OR of t1 and t2. More...
|
|
msat_term | msat_make_bv_xor (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the bit-wise XOR of t1 and t2. More...
|
|
msat_term | msat_make_bv_and (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the bit-wise AND of t1 and t2. More...
|
|
msat_term | msat_make_bv_not (msat_env e, msat_term t) |
| Returns a term representing the bit-wise negation of t. More...
|
|
msat_term | msat_make_bv_lshl (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the logical left shift of t1 by t2. More...
|
|
msat_term | msat_make_bv_lshr (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the logical right shift of t1 by t2. More...
|
|
msat_term | msat_make_bv_ashr (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the arithmetic right shift of t1 by t2. More...
|
|
msat_term | msat_make_bv_zext (msat_env e, size_t amount, msat_term t) |
| Returns a term representing the zero extension of t. More...
|
|
msat_term | msat_make_bv_sext (msat_env e, size_t amount, msat_term t) |
| Returns a term representing the sign extension of t1 by amount. More...
|
|
msat_term | msat_make_bv_plus (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the addition of t1 and t2. More...
|
|
msat_term | msat_make_bv_minus (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the subtraction of t1 by t2. More...
|
|
msat_term | msat_make_bv_neg (msat_env e, msat_term t) |
| Returns a term representing the negation of t, te two's-complement. More...
|
|
msat_term | msat_make_bv_times (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the multiplication of t1 and t2. More...
|
|
msat_term | msat_make_bv_udiv (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the unsigned division of t1 by t2. More...
|
|
msat_term | msat_make_bv_urem (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the unsigned remainder of t1 by t2. More...
|
|
msat_term | msat_make_bv_sdiv (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the signed division of t1 by t2. More...
|
|
msat_term | msat_make_bv_srem (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the signed remainder of t1 by t2. More...
|
|
msat_term | msat_make_bv_ult (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the unsigned t1 < t2. More...
|
|
msat_term | msat_make_bv_uleq (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the unsigned t1 <= t2. More...
|
|
msat_term | msat_make_bv_slt (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the signed t1 < t2. More...
|
|
msat_term | msat_make_bv_sleq (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the signed t1 <= t2. More...
|
|
msat_term | msat_make_bv_rol (msat_env e, size_t amount, msat_term t) |
| Returns a term representing the left rotation of 1 by amount bits. More...
|
|
msat_term | msat_make_bv_ror (msat_env e, size_t amount, msat_term t) |
| Returns a term representing the right rotation of 1 by amount bits. More...
|
|
msat_term | msat_make_bv_comp (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the comparison of t1 and t2, resulting in a bit-vector of size 1. More...
|
|
msat_term | msat_make_fp_roundingmode_nearest_even (msat_env e) |
| Returns a term representing the FP rounding mode ROUND_TO_NEAREST_EVEN. More...
|
|
msat_term | msat_make_fp_roundingmode_zero (msat_env e) |
| Returns a term representing the FP rounding mode ROUND_TO_ZERO. More...
|
|
msat_term | msat_make_fp_roundingmode_plus_inf (msat_env e) |
| Returns a term representing the FP rounding mode ROUND_TO_PLUS_INF. More...
|
|
msat_term | msat_make_fp_roundingmode_minus_inf (msat_env e) |
| Returns a term representing the FP rounding mode ROUND_TO_MINUS_INF. More...
|
|
msat_term | msat_make_fp_equal (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the FP equality predicate between t1 and t2. More...
|
|
msat_term | msat_make_fp_lt (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the FP < predicate between t1 and t2. More...
|
|
msat_term | msat_make_fp_leq (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the FP <= predicate between t1 and t2. More...
|
|
msat_term | msat_make_fp_neg (msat_env e, msat_term t) |
| Returns a term representing the FP negation of t. More...
|
|
msat_term | msat_make_fp_plus (msat_env e, msat_term rounding, msat_term t1, msat_term t2) |
| Returns a term representing the FP addition of t1 and t2, according to the given rounding mode. More...
|
|
msat_term | msat_make_fp_minus (msat_env e, msat_term rounding, msat_term t1, msat_term t2) |
| Returns a term representing the FP subtraction of t1 and t2, according to the given rounding mode. More...
|
|
msat_term | msat_make_fp_times (msat_env e, msat_term rounding, msat_term t1, msat_term t2) |
| Returns a term representing the FP multiplication of t1 and t2, according to the given rounding mode. More...
|
|
msat_term | msat_make_fp_div (msat_env e, msat_term rounding, msat_term t1, msat_term t2) |
| Returns a term representing the FP division of t1 and t2, according to the given rounding mode. More...
|
|
msat_term | msat_make_fp_sqrt (msat_env e, msat_term rounding, msat_term t) |
| Returns a term representing the FP square root of t, according to the given rounding mode. More...
|
|
msat_term | msat_make_fp_abs (msat_env e, msat_term t) |
| Returns a term representing the FP absolute value of t. More...
|
|
msat_term | msat_make_fp_min (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the FP min between t1 and t2. More...
|
|
msat_term | msat_make_fp_max (msat_env e, msat_term t1, msat_term t2) |
| Returns a term representing the FP max between t1 and t2. More...
|
|
msat_term | msat_make_fp_round_to_int (msat_env e, msat_term rounding, msat_term t) |
| Returns a term representing the FP round to integral of t, according to the given rounding mode. More...
|
|
msat_term | msat_make_fp_cast (msat_env e, size_t exp_w, size_t mant_w, msat_term rounding, msat_term t) |
| Returns a term representing the FP format conversion of the given input term. More...
|
|
msat_term | msat_make_fp_to_sbv (msat_env e, size_t width, msat_term rounding, msat_term t) |
| Returns a term representing the conversion of a FP term to a signed bit-vector. More...
|
|
msat_term | msat_make_fp_to_bv (msat_env e, size_t width, msat_term rounding, msat_term t) |
|
msat_term | msat_make_fp_to_ubv (msat_env e, size_t width, msat_term rounding, msat_term t) |
| Returns a term representing the conversion of a FP term to an unsigned bit-vector. More...
|
|
msat_term | msat_make_fp_from_sbv (msat_env e, size_t exp_w, size_t mant_w, msat_term rounding, msat_term t) |
| Returns a term representing the conversion of a signed bit-vector term to FP. More...
|
|
msat_term | msat_make_fp_from_ubv (msat_env e, size_t exp_w, size_t mant_w, msat_term rounding, msat_term t) |
| Returns a term representing the conversion of an unsigned bit-vector term to FP. More...
|
|
msat_term | msat_make_fp_as_ieeebv (msat_env e, msat_term t) |
| Returns a term for interpreting a FP term as a bit-vector. More...
|
|
msat_term | msat_make_fp_from_ieeebv (msat_env e, size_t exp_w, size_t mant_w, msat_term t) |
| Returns a term representing the FP number whose IEEE 754 encoding is the given bit-vector. More...
|
|
msat_term | msat_make_fp_isnan (msat_env e, msat_term t) |
| Returns the predicate for testing whether a FP term is NaN. More...
|
|
msat_term | msat_make_fp_isinf (msat_env e, msat_term t) |
| Returns the predicate for testing whether a FP term is infinity. More...
|
|
msat_term | msat_make_fp_iszero (msat_env e, msat_term t) |
| Returns the predicate for testing whether a FP term is zero. More...
|
|
msat_term | msat_make_fp_issubnormal (msat_env e, msat_term t) |
| Returns the predicate for testing whether a FP term is a subnormal. More...
|
|
msat_term | msat_make_fp_isnormal (msat_env e, msat_term t) |
| Returns the predicate for testing whether a FP term is a normal. More...
|
|
msat_term | msat_make_fp_isneg (msat_env e, msat_term t) |
| Returns the predicate for testing whether a FP term is negative. More...
|
|
msat_term | msat_make_fp_ispos (msat_env e, msat_term t) |
| Returns the predicate for testing whether a FP term is positive. More...
|
|
msat_term | msat_make_fp_plus_inf (msat_env e, size_t exp_w, size_t mant_w) |
| Returns the FP term representing +Inf of the given format. More...
|
|
msat_term | msat_make_fp_minus_inf (msat_env e, size_t exp_w, size_t mant_w) |
| Returns the FP term representing -Inf of the given format. More...
|
|
msat_term | msat_make_fp_nan (msat_env e, size_t exp_w, size_t mant_w) |
| Returns the FP term representing NaN of the given format. More...
|
|
msat_term | msat_make_fp_rat_number (msat_env e, const char *num_rep, size_t exp_w, size_t mant_w, msat_term rounding) |
| Creates an FP number from a rational number. More...
|
|
msat_term | msat_make_fp_bits_number (msat_env e, const char *bits, size_t exp_w, size_t mant_w) |
| Creates an FP number from a string of bits. More...
|
|
msat_term | msat_make_int_to_bv (msat_env e, size_t width, msat_term t) |
| Returns a term representing the conversion of an int to a bit-vector. More...
|
|
msat_term | msat_make_int_from_ubv (msat_env e, msat_term t) |
| Returns a term representing the conversion of an unsigned bit-vector to an int. More...
|
|
msat_term | msat_make_int_from_sbv (msat_env e, msat_term t) |
| Returns a term representing the conversion of a signed bit-vector to an int. More...
|
|
msat_term | msat_make_forall (msat_env e, msat_term var, msat_term body) |
| Returns a term resulting from universally quantifying the variable var in the term body. More...
|
|
msat_term | msat_make_exists (msat_env e, msat_term var, msat_term body) |
| Returns a term resulting from existentially quantifying the variable var in the term body. More...
|
|
msat_term | msat_make_variable (msat_env e, const char *name, msat_type type) |
| Returns a term representing a variable, which can be used for existential or universal quantification. More...
|
|
msat_term | msat_existentially_quantify (msat_env e, msat_term t, msat_term args[], size_t n) |
| Returns a term resulting from existentially quantifying the given constants in the given term. More...
|
|
msat_term | msat_make_term (msat_env e, msat_decl d, msat_term args[]) |
| Creates a term from a declaration and a list of arguments. More...
|
|
msat_term | msat_make_copy_from (msat_env e, msat_term t, msat_env src) |
| Creates a term in e from an equivalent term t that was created in src. More...
|
|
|
size_t | msat_term_id (msat_term t) |
| Returns a numeric identifier for t. More...
|
|
size_t | msat_term_arity (msat_term t) |
| Returns the arity of t. More...
|
|
msat_term | msat_term_get_arg (msat_term t, size_t n) |
| Returns the nth argument of t. More...
|
|
msat_type | msat_term_get_type (msat_term t) |
| Returns the type of t. More...
|
|
int | msat_term_is_true (msat_env e, msat_term t) |
| Checks whether t is the TRUE term. More...
|
|
int | msat_term_is_false (msat_env e, msat_term t) |
| Checks whether t is the FALSE term. More...
|
|
int | msat_term_is_boolean_constant (msat_env e, msat_term t) |
| Checks whether t is a boolean constant. More...
|
|
int | msat_term_is_atom (msat_env e, msat_term t) |
| Checks whether t is an atom. More...
|
|
int | msat_term_is_number (msat_env e, msat_term t) |
| Checks whether t is a number. More...
|
|
int | msat_term_is_enum_value (msat_env e, msat_term t) |
| Checks whether t is a value for an enum type. More...
|
|
int | msat_term_to_number (msat_env e, msat_term t, mpq_t out) |
| converts the given term to an mpq_t rational number More...
|
|
int | msat_term_is_and (msat_env e, msat_term t) |
| Checks whether t is an AND. More...
|
|
int | msat_term_is_or (msat_env e, msat_term t) |
| Checks whether t is an OR. More...
|
|
int | msat_term_is_not (msat_env e, msat_term t) |
| Checks whether t is a NOT. More...
|
|
int | msat_term_is_iff (msat_env e, msat_term t) |
| Checks whether t is an equivalence between boolean terms. More...
|
|
int | msat_term_is_term_ite (msat_env e, msat_term t) |
| Checks whether t is a term if-then-else. More...
|
|
int | msat_term_is_constant (msat_env e, msat_term t) |
| Checks whether t is a constant. More...
|
|
int | msat_term_is_uf (msat_env e, msat_term t) |
| Checks whether t is an uninterpreted function application. More...
|
|
int | msat_term_is_equal (msat_env e, msat_term t) |
| Checks whether t is an equality. More...
|
|
int | msat_term_is_leq (msat_env e, msat_term t) |
| Checks whether t is a (t1 <= t2) atom. More...
|
|
int | msat_term_is_plus (msat_env e, msat_term t) |
| Checks whether t is a (t1 + t2) expression. More...
|
|
int | msat_term_is_times (msat_env e, msat_term t) |
| Checks whether t is a (t1 * t2) expression. More...
|
|
int | msat_term_is_divide (msat_env e, msat_term t) |
| Checks whether t is a (t1 / t2) expression. More...
|
|
int | msat_term_is_int_modular_congruence (msat_env e, msat_term t, mpz_t out_mod) |
| Checks whether t is an integer modular congruence expression. If so, stores in out_mod the value of the modulus as a GMP bigint. More...
|
|
int | msat_term_is_floor (msat_env e, msat_term t) |
| Checks whether t is a (floor t1) expression. More...
|
|
int | msat_term_is_pi (msat_env e, msat_term t) |
| Checks whether t is a the pi constant. More...
|
|
int | msat_term_is_exp (msat_env e, msat_term t) |
| Checks whether t is a (exp t1) expression. More...
|
|
int | msat_term_is_sin (msat_env e, msat_term t) |
| Checks whether t is a (sin t1) expression. More...
|
|
int | msat_term_is_log (msat_env e, msat_term t) |
| Checks whether t is a (log t1) expression. More...
|
|
int | msat_term_is_pow (msat_env e, msat_term t) |
| Checks whether t is a (pow t1 t2) expression. More...
|
|
int | msat_term_is_asin (msat_env e, msat_term t) |
| Checks whether t is a (asin t1) expression. More...
|
|
int | msat_term_is_array_read (msat_env e, msat_term t) |
| Checks whether t is an array read. More...
|
|
int | msat_term_is_array_write (msat_env e, msat_term t) |
| Checks whether t is an array write. More...
|
|
int | msat_term_is_array_const (msat_env e, msat_term t) |
| Checks whether t is a constant array. More...
|
|
int | msat_term_is_bv_concat (msat_env e, msat_term t) |
| Checks whether t is a BV concatenation. More...
|
|
int | msat_term_is_bv_extract (msat_env e, msat_term t, size_t *out_msb, size_t *out_lsb) |
| Checks whether t is a BV extraction. More...
|
|
int | msat_term_is_bv_or (msat_env e, msat_term t) |
| Checks whether t is a bit-wise or. More...
|
|
int | msat_term_is_bv_xor (msat_env e, msat_term t) |
| Checks whether t is a bit-wise xor. More...
|
|
int | msat_term_is_bv_and (msat_env e, msat_term t) |
| Checks whether t is a bit-wise and. More...
|
|
int | msat_term_is_bv_not (msat_env e, msat_term t) |
| Checks whether t is a bit-wise not. More...
|
|
int | msat_term_is_bv_plus (msat_env e, msat_term t) |
| Checks whether t is a bit-vector addition. More...
|
|
int | msat_term_is_bv_minus (msat_env e, msat_term t) |
| Checks whether t is a bit-vector subtraction. More...
|
|
int | msat_term_is_bv_times (msat_env e, msat_term t) |
| Checks whether t is a bit-vector multiplication. More...
|
|
int | msat_term_is_bv_neg (msat_env e, msat_term t) |
| Checks whether t is a bit-vector unary negation. More...
|
|
int | msat_term_is_bv_udiv (msat_env e, msat_term t) |
| Checks whether t is a bit-vector unsigned division. More...
|
|
int | msat_term_is_bv_urem (msat_env e, msat_term t) |
| Checks whether t is a bit-vector unsigned remainder. More...
|
|
int | msat_term_is_bv_sdiv (msat_env e, msat_term t) |
| Checks whether t is a bit-vector signed division. More...
|
|
int | msat_term_is_bv_srem (msat_env e, msat_term t) |
| Checks whether t is a bit-vector signed remainder. More...
|
|
int | msat_term_is_bv_ult (msat_env e, msat_term t) |
| Checks whether t is a bit-vector unsigned lt. More...
|
|
int | msat_term_is_bv_uleq (msat_env e, msat_term t) |
| Checks whether t is a bit-vector unsigned leq. More...
|
|
int | msat_term_is_bv_slt (msat_env e, msat_term t) |
| Checks whether t is a bit-vector signed lt. More...
|
|
int | msat_term_is_bv_sleq (msat_env e, msat_term t) |
| Checks whether t is a bit-vector signed leq. More...
|
|
int | msat_term_is_bv_lshl (msat_env e, msat_term t) |
| Checks whether t is a logical shift left. More...
|
|
int | msat_term_is_bv_lshr (msat_env e, msat_term t) |
| Checks whether t is a logical shift right. More...
|
|
int | msat_term_is_bv_ashr (msat_env e, msat_term t) |
| Checks whether t is an arithmetic shift right. More...
|
|
int | msat_term_is_bv_zext (msat_env e, msat_term t, size_t *out_amount) |
| Checks whether t is a zero extension. More...
|
|
int | msat_term_is_bv_sext (msat_env e, msat_term t, size_t *out_amount) |
| Checks whether t is a sign extension. More...
|
|
int | msat_term_is_bv_rol (msat_env e, msat_term t, size_t *out_amount) |
| Checks whether t is a rotate left. More...
|
|
int | msat_term_is_bv_ror (msat_env e, msat_term t, size_t *out_amount) |
| Checks whether t is a rotate right. More...
|
|
int | msat_term_is_bv_comp (msat_env e, msat_term t) |
| Checks whether t is a BV comparison. More...
|
|
int | msat_term_is_fp_roundingmode_nearest_even (msat_env e, msat_term t) |
| Checks whether t is the ROUND_TO_NEAREST_EVEN FP rounding mode constant. More...
|
|
int | msat_term_is_fp_roundingmode_zero (msat_env e, msat_term t) |
| Checks whether t is the ROUND_TO_ZERO FP rounding mode constant. More...
|
|
int | msat_term_is_fp_roundingmode_plus_inf (msat_env e, msat_term t) |
| Checks whether t is the ROUND_TO_PLUS_INF FP rounding mode constant. More...
|
|
int | msat_term_is_fp_roundingmode_minus_inf (msat_env e, msat_term t) |
| Checks whether t is the ROUND_TO_MINUS_INF FP rounding mode constant. More...
|
|
int | msat_term_is_fp_equal (msat_env e, msat_term t) |
| Checks whether t is a FP equality. More...
|
|
int | msat_term_is_fp_lt (msat_env e, msat_term t) |
| Checks whether t is a FP less than. More...
|
|
int | msat_term_is_fp_leq (msat_env e, msat_term t) |
| Checks whether t is a FP <=. More...
|
|
int | msat_term_is_fp_neg (msat_env e, msat_term t) |
| Checks whether t is a FP negation. More...
|
|
int | msat_term_is_fp_plus (msat_env e, msat_term t) |
| Checks whether t is a FP plus. More...
|
|
int | msat_term_is_fp_minus (msat_env e, msat_term t) |
| Checks whether t is a FP minus. More...
|
|
int | msat_term_is_fp_times (msat_env e, msat_term t) |
| Checks whether t is a FP times. More...
|
|
int | msat_term_is_fp_div (msat_env e, msat_term t) |
| Checks whether t is a FP div. More...
|
|
int | msat_term_is_fp_sqrt (msat_env e, msat_term t) |
| Checks whether t is a FP sqrt. More...
|
|
int | msat_term_is_fp_abs (msat_env e, msat_term t) |
| Checks whether t is a FP abs. More...
|
|
int | msat_term_is_fp_min (msat_env e, msat_term t) |
| Checks whether t is a FP min. More...
|
|
int | msat_term_is_fp_max (msat_env e, msat_term t) |
| Checks whether t is a FP max. More...
|
|
int | msat_term_is_fp_round_to_int (msat_env e, msat_term t) |
| Checks whether t is a FP round to integer. More...
|
|
int | msat_term_is_fp_cast (msat_env e, msat_term t) |
| Checks whether t is a FP cast. More...
|
|
int | msat_term_is_fp_to_sbv (msat_env e, msat_term t) |
| Checks whether t is a FP to signed BV conversion. More...
|
|
int | msat_term_is_fp_to_bv (msat_env e, msat_term t) |
|
int | msat_term_is_fp_to_ubv (msat_env e, msat_term t) |
| Checks whether t is a FP to unsigned BV conversion. More...
|
|
int | msat_term_is_fp_from_sbv (msat_env e, msat_term t) |
| Checks whether t is a FP from signed BV conversion. More...
|
|
int | msat_term_is_fp_from_ubv (msat_env e, msat_term t) |
| Checks whether t is a FP from unsigned BV conversion. More...
|
|
int | msat_term_is_fp_as_ieeebv (msat_env e, msat_term t) |
| Checks whether t is a FP as BV conversion. More...
|
|
int | msat_term_is_fp_from_ieeebv (msat_env e, msat_term t) |
| Checks whether t is a FP from IEEE BV conversion. More...
|
|
int | msat_term_is_fp_isnan (msat_env e, msat_term t) |
| Checks whether t is a FP isnan predicate. More...
|
|
int | msat_term_is_fp_isinf (msat_env e, msat_term t) |
| Checks whether t is a FP isinf predicate. More...
|
|
int | msat_term_is_fp_iszero (msat_env e, msat_term t) |
| Checks whether t is a FP iszero predicate. More...
|
|
int | msat_term_is_fp_issubnormal (msat_env e, msat_term t) |
| Checks whether t is a FP issubnormal predicate. More...
|
|
int | msat_term_is_fp_isnormal (msat_env e, msat_term t) |
| Checks whether t is a FP isnormal predicate. More...
|
|
int | msat_term_is_fp_isneg (msat_env e, msat_term t) |
| Checks whether t is a FP isneg predicate. More...
|
|
int | msat_term_is_fp_ispos (msat_env e, msat_term t) |
| Checks whether t is a FP ispos predicate. More...
|
|
int | msat_term_is_int_to_bv (msat_env e, msat_term t) |
| Checks whether t is a int to BV conversion. More...
|
|
int | msat_term_is_int_from_ubv (msat_env e, msat_term t) |
| Checks whether t is an unsigned BV to int conversion. More...
|
|
int | msat_term_is_int_from_sbv (msat_env e, msat_term t) |
| Checks whether t is a signed BV to int conversion. More...
|
|
int | msat_term_is_quantifier (msat_env e, msat_term t) |
| Checks whether t is a quantifier. More...
|
|
int | msat_term_is_forall (msat_env e, msat_term t) |
| Checks whether t is a universal quantifier. More...
|
|
int | msat_term_is_exists (msat_env e, msat_term t) |
| Checks whether t is an existential quantifier. More...
|
|
int | msat_term_is_variable (msat_env e, msat_term t) |
| Checks whether t is a (free or bound) variable. More...
|
|
int | msat_visit_term (msat_env e, msat_term t, msat_visit_term_callback func, void *user_data) |
| visits the DAG of the given term t, calling the callback func for every suberm More...
|
|
msat_term | msat_apply_substitution (msat_env e, msat_term t, size_t n, msat_term *to_subst, msat_term *values) |
| substitutes the terms in to_subst with values in t More...
|
|
msat_decl | msat_find_decl (msat_env e, const char *symbol) |
| Returns the declaration of the given symbol in the given environment (if any) More...
|
|
msat_decl | msat_term_get_decl (msat_term t) |
| Returns the declaration associated to t (if any) More...
|
|
size_t | msat_decl_id (msat_decl d) |
| Returns a numeric identifier for the input declaration. More...
|
|
msat_symbol_tag | msat_decl_get_tag (msat_env e, msat_decl d) |
| Returns the symbol tag associated to the given declaration. More...
|
|
msat_type | msat_decl_get_return_type (msat_decl d) |
| Returns the return type of the given declaration. More...
|
|
size_t | msat_decl_get_arity (msat_decl d) |
| Returns the arity (number of arguments) of the given declaration. More...
|
|
msat_type | msat_decl_get_arg_type (msat_decl d, size_t n) |
| Returns the type of the given argument for the input declaration. More...
|
|
char * | msat_decl_get_name (msat_decl d) |
| Returns the name corresponding to the given declaration. More...
|
|
char * | msat_decl_repr (msat_decl d) |
| Returns an internal string representation of a declaration. More...
|
|
char * | msat_term_repr (msat_term t) |
| Returns an internal string representation of a term. More...
|
|
|
msat_term | msat_from_string (msat_env e, const char *data) |
| Creates a term from its string representation. More...
|
|
msat_term | msat_from_smtlib1 (msat_env e, const char *data) |
| Creates a term from a string in SMT-LIB v1 format. More...
|
|
msat_term | msat_from_smtlib1_file (msat_env e, FILE *f) |
| Creates a term from a file in SMT-LIB v1 format. More...
|
|
msat_term | msat_from_smtlib2 (msat_env e, const char *data) |
| Creates a term from a string in SMT-LIB v2 format. More...
|
|
msat_term | msat_from_smtlib2_file (msat_env e, FILE *f) |
| Creates a term from a file in SMT-LIB v2 format. More...
|
|
char * | msat_to_smtlib1 (msat_env e, msat_term term) |
| Converts the given term to SMT-LIB v1 format. More...
|
|
int | msat_to_smtlib1_file (msat_env e, msat_term term, FILE *out) |
| Dumps the given term in SMT-LIB v1 format to the given output file. More...
|
|
char * | msat_to_smtlib2 (msat_env e, msat_term term) |
| Converts the given term to SMT-LIB v2 format. More...
|
|
int | msat_to_smtlib2_file (msat_env e, msat_term term, FILE *out) |
| Dumps the given term in SMT-LIB v2 format to the given output file. More...
|
|
char * | msat_to_smtlib2_ext (msat_env e, msat_term term, const char *logic_name, int use_defines) |
| Converts the given term to SMT-LIB v2 format. More...
|
|
char * | msat_to_smtlib2_term (msat_env e, msat_term term) |
| Prints a single term in SMT-LIB v2 format. More...
|
|
int | msat_to_smtlib2_ext_file (msat_env e, msat_term term, const char *logic_name, int use_defines, FILE *out) |
| Dumps the given term in SMT-LIB v2 format to the given output file. More...
|
|
int | msat_named_list_from_smtlib2 (msat_env e, const char *data, size_t *out_n, char ***out_names, msat_term **out_terms) |
| Parses a list of named terms from a string in SMT-LIB v2 format. More...
|
|
int | msat_named_list_from_smtlib2_file (msat_env e, FILE *f, size_t *out_n, char ***out_names, msat_term **out_terms) |
| Like msat_named_list_from_smtlib2(), but reads from a file instead of a string. More...
|
|
char * | msat_named_list_to_smtlib2 (msat_env e, size_t n, const char **names, msat_term *terms) |
| Converts the given list of named terms to SMT-LIB v2 format. More...
|
|
int | msat_named_list_to_smtlib2_file (msat_env e, size_t n, const char **names, msat_term *terms, FILE *out) |
| Dumps the given list of named terms in SMT-LIB v2 format to the given output file. More...
|
|
int | msat_annotated_list_from_smtlib2 (msat_env e, const char *data, size_t *out_n, msat_term **out_terms, char ***out_annots) |
| Parses a list of annotated terms from a string in SMT-LIB v2 format. More...
|
|
int | msat_annotated_list_from_smtlib2_file (msat_env e, FILE *f, size_t *out_n, msat_term **out_terms, char ***out_annots) |
| Like msat_annotated_list_from_smtlib2(), but reads from a file instead of a string. More...
|
|
char * | msat_annotated_list_to_smtlib2 (msat_env e, size_t n, msat_term *terms, const char **annots) |
| Converts the given list of annotated terms to SMT-LIB v2 format. More...
|
|
int | msat_annotated_list_to_smtlib2_file (msat_env e, size_t n, msat_term *terms, const char **annots, FILE *out) |
| Like msat_annotated_list_to_smtlib2(), but writes to a FILE instead of returning a string. More...
|
|
|
int | msat_push_backtrack_point (msat_env e) |
| Pushes a checkpoint for backtracking in an environment. More...
|
|
int | msat_pop_backtrack_point (msat_env e) |
| Backtracks to the last checkpoint set in the environment e. More...
|
|
size_t | msat_num_backtrack_points (msat_env e) |
| returns the number of backtrack points in the given environment More...
|
|
int | msat_reset_env (msat_env e) |
| Resets an environment. More...
|
|
int | msat_assert_formula (msat_env e, msat_term formula) |
| Adds a logical formula to an environment. More...
|
|
int | msat_add_preferred_for_branching (msat_env e, msat_term boolvar, msat_truth_value phase) |
| Adds a Boolean variable at the end of the list of preferred variables for branching when solving the problem. More...
|
|
int | msat_clear_preferred_for_branching (msat_env e) |
| Clears the list of preferred variables for branching. More...
|
|
msat_result | msat_solve (msat_env e) |
| Checks the satiafiability of the given environment. More...
|
|
msat_result | msat_solve_with_assumptions (msat_env e, msat_term *assumptions, size_t num_assumptions) |
| Checks the satiafiability of the given environment under the given assumptions. More...
|
|
int | msat_all_sat (msat_env e, msat_term *important, size_t num_important, msat_all_sat_model_callback func, void *user_data) |
| Performs AllSat over the important atoms of the conjunction of all formulas asserted in e (see msat_assert_formula). When used in incremental mode, a backtrack point should be pushed before calling this function, and popped after this call has completed. Not doing this changes the satisfiability of the formula. More...
|
|
int | msat_all_sat_ext (msat_env e, msat_term *important, size_t num_important, msat_truth_value phase, msat_all_sat_model_callback func, void *user_data) |
|
int | msat_solve_diversify (msat_env e, msat_term *diversifiers, size_t num_diversifiers, msat_solve_diversify_model_callback func, void *user_data) |
| Enumerates diverse models over the asserted stack. More...
|
|
msat_term * | msat_get_asserted_formulas (msat_env e, size_t *num_asserted) |
| Returns the list of formulas in the assertion stack. More...
|
|
msat_term * | msat_get_theory_lemmas (msat_env e, size_t *num_tlemmas) |
| Retrieves the theory lemmas used in the last search (see msat_solve). More...
|
|
char * | msat_get_search_stats (msat_env e) |
| Returns a string with search statistics for the given environment. More...
|
|
msat_term | msat_simplify (msat_env e, msat_term formula, msat_term *to_protect, size_t num_to_protect) |
| Simplify the input formula by performing variable elimination with toplevel equalities. More...
|
|
|
int | msat_create_itp_group (msat_env e) |
| Creates a new group for interpolation. More...
|
|
int | msat_set_itp_group (msat_env e, int group) |
| Sets the current interpolation group. More...
|
|
msat_term | msat_get_interpolant (msat_env e, int *groups_of_a, size_t n) |
| Computes an interpolant for a pair (A, B) of formulas. More...
|
|
|
msat_term | msat_get_model_value (msat_env e, msat_term term) |
| Returns the value of the term term in the current model. More...
|
|
msat_model_iterator | msat_create_model_iterator (msat_env e) |
| Creates a model iterator. More...
|
|
int | msat_model_iterator_has_next (msat_model_iterator i) |
| Checks whether i can be incremented. More...
|
|
int | msat_model_iterator_next (msat_model_iterator i, msat_term *t, msat_term *v) |
| Returns the next (term, value) pair in the model, and increments the given iterator. More...
|
|
void | msat_destroy_model_iterator (msat_model_iterator i) |
| Destroys a model iterator. More...
|
|
msat_model | msat_get_model (msat_env e) |
| Creates a model object. More...
|
|
void | msat_destroy_model (msat_model m) |
| Destroys the given model object. More...
|
|
msat_term | msat_model_eval (msat_model m, msat_term t) |
| Evaluates the input term in the given model. More...
|
|
msat_model_iterator | msat_model_create_iterator (msat_model m) |
| Creates an iterator for the given model. More...
|
|
|
msat_term * | msat_get_unsat_core (msat_env e, size_t *core_size) |
| Returns the unsatisfiable core of the last search (see msat_solve) as a subset of the asserted formulas, if the problem was unsatisfiable. More...
|
|
msat_term * | msat_get_unsat_core_ext (msat_env e, size_t *core_size, msat_ext_unsat_core_extractor extractor, void *user_data) |
| Returns the unsatisfiable core of the last search (see msat_solve) as a subset of the asserted formulas, computed using an external Boolean unsat core extractor (see msat_ext_unsat_core_extractor). More...
|
|
msat_term * | msat_get_unsat_assumptions (msat_env e, size_t *assumps_size) |
| Returns the list of assumptions resposible for the unsatisfiability detected by the last search (see msat_solve_with_assumptions). More...
|
|
msat_proof_manager | msat_get_proof_manager (msat_env e) |
| Returns a proof manager for the given environment. More...
|
|
void | msat_destroy_proof_manager (msat_proof_manager m) |
| Destroys a proof manager. More...
|
|
msat_proof | msat_get_proof (msat_proof_manager m) |
| Returns a proof of unsatisfiability. More...
|
|
size_t | msat_proof_id (msat_proof p) |
| Returns a numeric identifier for p. More...
|
|
int | msat_proof_is_term (msat_proof p) |
| Checks whether a proof object is a term. More...
|
|
msat_term | msat_proof_get_term (msat_proof p) |
| Retrieves the term associated to a term proof. More...
|
|
const char * | msat_proof_get_name (msat_proof p) |
| Retrieves the name of a non-term proof. More...
|
|
size_t | msat_proof_get_arity (msat_proof p) |
| Retrieves the number of children of a non-term proof. More...
|
|
msat_proof | msat_proof_get_child (msat_proof p, size_t i) |
| Retrieves a sub-proof of a given proof. More...
|
|
|
int | msat_set_external_dpll_engine (msat_env env, msat_ext_dpll_interface *engine) |
| Sets an external dpll engine to be used by an environment. More...
|
|
int | msat_dpll_callback_no_conflict_after_bcp (msat_dpll_callback cb, msat_truth_value *code, int **conflict) |
| Callback function that the external SAT solver must call when a round of BCP has been completed without finding a Boolean conflict. More...
|
|
int | msat_dpll_callback_model_found (msat_dpll_callback cb, msat_truth_value *code, int **conflict) |
| Callback function that the external SAT solver must call when a Boolean model has been found. More...
|
|
int | msat_dpll_callback_notify_assignment (msat_dpll_callback cb, int lit) |
| Callback function that the external SAT solver must call whenever a literal is added to the trail. More...
|
|
int | msat_dpll_callback_notify_new_level (msat_dpll_callback cb) |
| Callback function that the external SAT solver must call whenever a new decision level is opened. More...
|
|
int | msat_dpll_callback_notify_backtrack (msat_dpll_callback cb, int level) |
| Callback function that the external SAT solver must call whenever it backtracks. More...
|
|
int | msat_dpll_callback_ask_theory_reason (msat_dpll_callback cb, int lit, int **reason) |
| Callback function that the external SAT solver must call for asking MathSAT the reason for a theory-deduced literal, during conflict analysis. More...
|
|
|
#define | MSAT_TAG_FP_TO_BV MSAT_TAG_FP_TO_SBV |
|
#define | MSAT_ERROR_CONFIG(cfg) ((cfg).repr == NULL) |
| Error checking for configurations. More...
|
|
#define | MSAT_ERROR_ENV(env) ((env).repr == NULL) |
| Error checking for environments. More...
|
|
#define | MSAT_ERROR_TERM(term) ((term).repr == NULL) |
| Error checking for terms. More...
|
|
#define | MSAT_MAKE_ERROR_TERM(term) ((term).repr = NULL) |
| Sets given term to be an error term. More...
|
|
#define | MSAT_ERROR_DECL(decl) ((decl).repr == NULL) |
| Error checking for declarations. More...
|
|
#define | MSAT_ERROR_TYPE(tp) ((tp).repr == NULL) |
| Error checking for types. More...
|
|
#define | MSAT_ERROR_MODEL_ITERATOR(iter) ((iter).repr == NULL) |
| Error checking for model iterators. More...
|
|
#define | MSAT_ERROR_MODEL(model) ((model).repr == NULL) |
| Error checking for models. More...
|
|
#define | MSAT_ERROR_PROOF_MANAGER(mgr) ((mgr).repr == NULL) |
| Error checking for proof managers. More...
|
|
#define | MSAT_ERROR_PROOF(p) ((p).repr == NULL) |
| Error checking for proofs. More...
|
|
#define | MSAT_ERROR_OBJECTIVE(objective) ((objective).repr == NULL) |
| Error checking for objectives. More...
|
|
#define | MSAT_ERROR_OBJECTIVE_ITERATOR(iter) ((iter).repr == NULL) |
| Error checking for objective iterators. More...
|
|
enum | msat_result { MSAT_UNKNOWN = -1,
MSAT_UNSAT,
MSAT_SAT
} |
|
enum | msat_truth_value { MSAT_UNDEF = -1,
MSAT_FALSE,
MSAT_TRUE
} |
|
enum | msat_symbol_tag {
MSAT_TAG_ERROR = -1,
MSAT_TAG_UNKNOWN = 0,
MSAT_TAG_TRUE,
MSAT_TAG_FALSE,
MSAT_TAG_AND,
MSAT_TAG_OR,
MSAT_TAG_NOT,
MSAT_TAG_IFF,
MSAT_TAG_PLUS,
MSAT_TAG_TIMES,
MSAT_TAG_DIVIDE,
MSAT_TAG_FLOOR,
MSAT_TAG_LEQ,
MSAT_TAG_EQ,
MSAT_TAG_ITE,
MSAT_TAG_INT_MOD_CONGR,
MSAT_TAG_BV_CONCAT,
MSAT_TAG_BV_EXTRACT,
MSAT_TAG_BV_NOT,
MSAT_TAG_BV_AND,
MSAT_TAG_BV_OR,
MSAT_TAG_BV_XOR,
MSAT_TAG_BV_ULT,
MSAT_TAG_BV_SLT,
MSAT_TAG_BV_ULE,
MSAT_TAG_BV_SLE,
MSAT_TAG_BV_COMP,
MSAT_TAG_BV_NEG,
MSAT_TAG_BV_ADD,
MSAT_TAG_BV_SUB,
MSAT_TAG_BV_MUL,
MSAT_TAG_BV_UDIV,
MSAT_TAG_BV_SDIV,
MSAT_TAG_BV_UREM,
MSAT_TAG_BV_SREM,
MSAT_TAG_BV_LSHL,
MSAT_TAG_BV_LSHR,
MSAT_TAG_BV_ASHR,
MSAT_TAG_BV_ROL,
MSAT_TAG_BV_ROR,
MSAT_TAG_BV_ZEXT,
MSAT_TAG_BV_SEXT,
MSAT_TAG_ARRAY_READ,
MSAT_TAG_ARRAY_WRITE,
MSAT_TAG_ARRAY_CONST,
MSAT_TAG_FP_EQ,
MSAT_TAG_FP_LT,
MSAT_TAG_FP_LE,
MSAT_TAG_FP_NEG,
MSAT_TAG_FP_ADD,
MSAT_TAG_FP_SUB,
MSAT_TAG_FP_MUL,
MSAT_TAG_FP_DIV,
MSAT_TAG_FP_SQRT,
MSAT_TAG_FP_ABS,
MSAT_TAG_FP_MIN,
MSAT_TAG_FP_MAX,
MSAT_TAG_FP_CAST,
MSAT_TAG_FP_ROUND_TO_INT,
MSAT_TAG_FP_FROM_SBV,
MSAT_TAG_FP_FROM_UBV,
MSAT_TAG_FP_TO_SBV,
MSAT_TAG_FP_TO_UBV,
MSAT_TAG_FP_AS_IEEEBV,
MSAT_TAG_FP_ISNAN,
MSAT_TAG_FP_ISINF,
MSAT_TAG_FP_ISZERO,
MSAT_TAG_FP_ISSUBNORMAL,
MSAT_TAG_FP_ISNORMAL,
MSAT_TAG_FP_ISNEG,
MSAT_TAG_FP_ISPOS,
MSAT_TAG_FP_FROM_IEEEBV,
MSAT_TAG_INT_FROM_UBV,
MSAT_TAG_INT_FROM_SBV,
MSAT_TAG_INT_TO_BV,
MSAT_TAG_PI,
MSAT_TAG_EXP,
MSAT_TAG_SIN,
MSAT_TAG_LOG,
MSAT_TAG_POW,
MSAT_TAG_ASIN,
MSAT_TAG_FORALL,
MSAT_TAG_EXISTS
} |
|
enum | msat_visit_status { MSAT_VISIT_PROCESS = 0,
MSAT_VISIT_SKIP = 1,
MSAT_VISIT_ABORT = 2
} |
|
typedef int(* | msat_all_sat_model_callback) (msat_term *model, int size, void *user_data) |
| Callback function to be notified about models found by msat_all_sat. More...
|
|
typedef int(* | msat_solve_diversify_model_callback) (msat_model_iterator it, void *user_data) |
| Callback function to be notified about models found by msat_solve_diversify. More...
|
|
typedef msat_visit_status(* | msat_visit_term_callback) (msat_env e, msat_term t, int preorder, void *user_data) |
| Callback function to visit a term DAG with msat_visit_term. More...
|
|
typedef int(* | msat_termination_test) (void *user_data) |
| Custom test for early termination of search. More...
|
|
typedef int(* | msat_ext_unsat_core_extractor) (int *cnf_in, int *groups_in_out, size_t *size_in_out, void *user_data) |
| External Boolean unsat core extraction function, to be used with msat_get_unsat_core_ext. More...
|
|
void | msat_free (void *ptr) |
| Function for deallocating the memory accessible by pointers returned by MathSAT. More...
|
|
char * | msat_get_version (void) |
| Gets the current MathSAT version. More...
|
|
const char * | msat_get_version_id (void) |
|
const char * | msat_last_error_message (msat_env env) |
| Retrieves the last error message generated while operating in the given enviroment. More...
|
|
API for the MathSAT SMT solver.
◆ MSAT_ERROR_CONFIG
#define MSAT_ERROR_CONFIG |
( |
|
cfg | ) |
((cfg).repr == NULL) |
Error checking for configurations.
Use this macro to check whether returned values of type msat_config are valid
◆ MSAT_ERROR_DECL
#define MSAT_ERROR_DECL |
( |
|
decl | ) |
((decl).repr == NULL) |
Error checking for declarations.
Use this macro to check whether returned values of type msat_decl are valid
◆ MSAT_ERROR_ENV
#define MSAT_ERROR_ENV |
( |
|
env | ) |
((env).repr == NULL) |
Error checking for environments.
Use this macro to check whether returned values of type msat_env are valid
◆ MSAT_ERROR_MODEL
#define MSAT_ERROR_MODEL |
( |
|
model | ) |
((model).repr == NULL) |
Error checking for models.
Use this macro to check whether returned values of type msat_model are valid
◆ MSAT_ERROR_MODEL_ITERATOR
#define MSAT_ERROR_MODEL_ITERATOR |
( |
|
iter | ) |
((iter).repr == NULL) |
Error checking for model iterators.
Use this macro to check whether returned values of type msat_model_iterator are valid
◆ MSAT_ERROR_OBJECTIVE
#define MSAT_ERROR_OBJECTIVE |
( |
|
objective | ) |
((objective).repr == NULL) |
Error checking for objectives.
Use this macro to check whether returned values of type ::msat_objective are valid
◆ MSAT_ERROR_OBJECTIVE_ITERATOR
#define MSAT_ERROR_OBJECTIVE_ITERATOR |
( |
|
iter | ) |
((iter).repr == NULL) |
Error checking for objective iterators.
Use this macro to check whether returned values of type ::msat_objective_iterator are valid
◆ MSAT_ERROR_PROOF
#define MSAT_ERROR_PROOF |
( |
|
p | ) |
((p).repr == NULL) |
Error checking for proofs.
Use this macro to check whether returned values of type msat_proof are valid
◆ MSAT_ERROR_PROOF_MANAGER
#define MSAT_ERROR_PROOF_MANAGER |
( |
|
mgr | ) |
((mgr).repr == NULL) |
Error checking for proof managers.
Use this macro to check whether returned values of type msat_proof_manager are valid
◆ MSAT_ERROR_TERM
#define MSAT_ERROR_TERM |
( |
|
term | ) |
((term).repr == NULL) |
Error checking for terms.
Use this macro to check whether returned values of type msat_term are valid
◆ MSAT_ERROR_TYPE
#define MSAT_ERROR_TYPE |
( |
|
tp | ) |
((tp).repr == NULL) |
Error checking for types.
Use this macro to check whether returned values of type msat_type are valid
◆ MSAT_MAKE_ERROR_TERM
#define MSAT_MAKE_ERROR_TERM |
( |
|
term | ) |
((term).repr = NULL) |
Sets given term to be an error term.
Use this macro to make terms error terms.
◆ msat_all_sat_model_callback
typedef int(* msat_all_sat_model_callback) (msat_term *model, int size, void *user_data) |
Callback function to be notified about models found by msat_all_sat.
This callback function can be used to be notified about the models found by the AllSat algorithm. Such models contain the truth values of the important atoms, as specified with msat_all_sat. Each term in the model array is either an important atom or its negation, according to the truth value in the model. Notice that the model array is read-only, and will be valid only until the callback function returns. If the function returns zero, then the current search is aborted
◆ msat_ext_unsat_core_extractor
typedef int(* msat_ext_unsat_core_extractor) (int *cnf_in, int *groups_in_out, size_t *size_in_out, void *user_data) |
External Boolean unsat core extraction function, to be used with msat_get_unsat_core_ext.
The function accepts as input an array of integers representing the input problem in DIMACS format (with different clauses separated by a 0) and an array of group indices (positive integers, with index 0 reserved for the "background" group), and it must modify the array of groups in-place for storing the indices of the groups in the unsat core. The parameter size_in_out gives the number of clauses in the input cnf, and should be modified to store the number of groups in the computed core. The function should return a non-zero value to signal an error. See also http://www.satcompetition.org/2011/rules.pdf (MUS track)
◆ msat_solve_diversify_model_callback
typedef int(* msat_solve_diversify_model_callback) (msat_model_iterator it, void *user_data) |
Callback function to be notified about models found by msat_solve_diversify.
This callback function can be used to be notified about the models found by the diversification algorithm. If the function returns non-zero, then the current search is aborted
◆ msat_termination_test
typedef int(* msat_termination_test) (void *user_data) |
◆ msat_visit_term_callback
typedef msat_visit_status(* msat_visit_term_callback) (msat_env e, msat_term t, int preorder, void *user_data) |
Callback function to visit a term DAG with msat_visit_term.
This callback function gets called by the term visitor for each visited subterm. The preorder flag tells whether the function is called before or after visiting the subterms. The return value of this function determines how the visit should continue (see msat_visit_status)
◆ msat_result
MathSAT result.
Enumerator |
---|
MSAT_UNKNOWN | Unknown.
|
MSAT_UNSAT | Unsatisfiable.
|
MSAT_SAT | Satisfiable.
|
◆ msat_symbol_tag
MathSAT symbol tag.
Enumerator |
---|
MSAT_TAG_TRUE | the Boolean constant True
|
MSAT_TAG_FALSE | the Boolean constant False
|
MSAT_TAG_AND | the AND Boolean connective
|
MSAT_TAG_OR | the OR Boolean connective
|
MSAT_TAG_NOT | the NOT Boolean connective
|
MSAT_TAG_IFF | the IFF Boolean connective
|
MSAT_TAG_PLUS | arithmetic addition
|
MSAT_TAG_TIMES | arithmetic multiplication
|
MSAT_TAG_DIVIDE | arithmetic division
|
MSAT_TAG_FLOOR | floor function
|
MSAT_TAG_LEQ | arithmetic <=
|
MSAT_TAG_EQ | equality
|
MSAT_TAG_ITE | term-level if-then-else
|
MSAT_TAG_INT_MOD_CONGR | integer modular congruence
|
MSAT_TAG_BV_CONCAT | BV concatenation
|
MSAT_TAG_BV_EXTRACT | BV selection
|
MSAT_TAG_BV_NOT | BV bitwise not
|
MSAT_TAG_BV_AND | BV bitwise and
|
MSAT_TAG_BV_OR | BV bitwise or
|
MSAT_TAG_BV_XOR | BV bitwise xor
|
MSAT_TAG_BV_ULT | BV unsigned <
|
MSAT_TAG_BV_SLT | BV signed <
|
MSAT_TAG_BV_ULE | BV unsigned <=
|
MSAT_TAG_BV_SLE | BV signed <
|
MSAT_TAG_BV_COMP | BV bit comparison
|
MSAT_TAG_BV_NEG | BV unary minus
|
MSAT_TAG_BV_ADD | BV addition
|
MSAT_TAG_BV_SUB | BV subtraction
|
MSAT_TAG_BV_MUL | BV multiplication
|
MSAT_TAG_BV_UDIV | BV unsigned division
|
MSAT_TAG_BV_SDIV | BV signed division
|
MSAT_TAG_BV_UREM | BV unsigned remainder
|
MSAT_TAG_BV_SREM | BV signed remainder
|
MSAT_TAG_BV_LSHL | BV logical left shift
|
MSAT_TAG_BV_LSHR | BV logical right shift
|
MSAT_TAG_BV_ASHR | BV arithmetic right shift
|
MSAT_TAG_BV_ROL | BV rotate left
|
MSAT_TAG_BV_ROR | BV rotate right
|
MSAT_TAG_BV_ZEXT | BV zero extension
|
MSAT_TAG_BV_SEXT | BV sign extension
|
MSAT_TAG_ARRAY_READ | Array read/select operation
|
MSAT_TAG_ARRAY_WRITE | Array write/store operation
|
MSAT_TAG_ARRAY_CONST | Constant arrays
|
MSAT_TAG_FP_EQ | FP IEEE equality
|
MSAT_TAG_FP_LT | FP <
|
MSAT_TAG_FP_LE | FP <=
|
MSAT_TAG_FP_NEG | FP unary minus
|
MSAT_TAG_FP_ADD | FP addition
|
MSAT_TAG_FP_SUB | FP subtraction
|
MSAT_TAG_FP_MUL | FP multiplication
|
MSAT_TAG_FP_DIV | FP division
|
MSAT_TAG_FP_SQRT | FP square root
|
MSAT_TAG_FP_ABS | FP absolute value
|
MSAT_TAG_FP_MIN | FP min
|
MSAT_TAG_FP_MAX | FP max
|
MSAT_TAG_FP_CAST | FP format conversion
|
MSAT_TAG_FP_ROUND_TO_INT | FP round to integer
|
MSAT_TAG_FP_FROM_SBV | FP conversion from a signed BV
|
MSAT_TAG_FP_FROM_UBV | FP conversion from an unsigned BV
|
MSAT_TAG_FP_TO_SBV | FP conversion to signed BV
|
MSAT_TAG_FP_TO_UBV | FP conversion to unsigned BV
|
MSAT_TAG_FP_AS_IEEEBV | FP as IEEE BV (access to the bits)
|
MSAT_TAG_FP_ISNAN | FP check for NaN
|
MSAT_TAG_FP_ISINF | FP check for infinity
|
MSAT_TAG_FP_ISZERO | FP check for zero
|
MSAT_TAG_FP_ISSUBNORMAL | FP check for subnormal
|
MSAT_TAG_FP_ISNORMAL | FP check for normal
|
MSAT_TAG_FP_ISNEG | FP check for negative
|
MSAT_TAG_FP_ISPOS | FP check for positive
|
MSAT_TAG_FP_FROM_IEEEBV | FP conversion from IEEE BV
|
MSAT_TAG_INT_FROM_UBV | Unsigned BV -> INT conversion
|
MSAT_TAG_INT_FROM_SBV | Signed BV -> INT conversion
|
MSAT_TAG_INT_TO_BV | INT -> BV conversion
|
MSAT_TAG_PI | Pi constant
|
MSAT_TAG_EXP | Exponential function
|
MSAT_TAG_SIN | Sine function
|
MSAT_TAG_LOG | Natural logarithm function
|
MSAT_TAG_POW | Power function
|
MSAT_TAG_ASIN | Arcsin function
|
MSAT_TAG_FORALL | Universal quantifier
|
MSAT_TAG_EXISTS | Existential quantifier
|
◆ msat_truth_value
MathSAT truth value.
Enumerator |
---|
MSAT_UNDEF | Undefined/unknown.
|
MSAT_FALSE | False.
|
MSAT_TRUE | True.
|
◆ msat_visit_status
MathSAT status for the callback passed to msat_visit_term
Enumerator |
---|
MSAT_VISIT_PROCESS | Continue visiting
|
MSAT_VISIT_SKIP | Skip this term and the subterms
|
MSAT_VISIT_ABORT | Abort visit immediately
|
◆ msat_add_preferred_for_branching()
int msat_add_preferred_for_branching |
( |
msat_env |
e, |
|
|
msat_term |
boolvar, |
|
|
msat_truth_value |
phase |
|
) |
| |
Adds a Boolean variable at the end of the list of preferred variables for branching when solving the problem.
- Parameters
-
e | The environment in which to operate |
boolvar | The Boolean variable to add to the preferred list |
phase | The phase of the variable for branching. If MSAT_UNDEF, the phase is determined by the currently configured heuristics |
- Returns
- zero on success, nonzero on error
◆ msat_all_sat()
Performs AllSat over the important atoms of the conjunction of all formulas asserted in e (see msat_assert_formula). When used in incremental mode, a backtrack point should be pushed before calling this function, and popped after this call has completed. Not doing this changes the satisfiability of the formula.
- Parameters
-
e | The environment to use |
important | An array of important atoms. If NULL, all atoms are considered important |
num_important | The size of the important array. If important is NULL, set this to zero |
func | The callback function to be notified about models found (see msat_all_sat_model_callback). Cannot be NULL |
user_data | Generic data pointer which will be passed to func. Can be anything, its value will not be interpreted |
- Returns
- The number of models found, or -1 on error. If the solver detects that the formula is a tautology, -2 is returned. Note however that:
- not all tautologies are detected by the solver. I.e., sometimes the solver will explicitly enumerate all the models of the formula even for tautologies
- the number returned might be an over-approximation of the actual number of models. This can happen because the solver might sometimes report the same model more than once. In these cases, the callback function will be called multiple times with the same input.
◆ msat_annotated_list_from_smtlib2()
int msat_annotated_list_from_smtlib2 |
( |
msat_env |
e, |
|
|
const char * |
data, |
|
|
size_t * |
out_n, |
|
|
msat_term ** |
out_terms, |
|
|
char *** |
out_annots |
|
) |
| |
Parses a list of annotated terms from a string in SMT-LIB v2 format.
Given a string in SMT-LIB v2 format, collect and return all and only the terms with an annotation.
- Parameters
-
e | Then environment in which terms are created |
data | The input string in SMT-LIBv2 format |
out_n | On success, the number of terms is stored here. Must not be NULL. Notice that terms with multiple annotations are counted multiple times (see out_names below) |
out_terms | On success, the parsed annotated terms are stored here. Must not be NULL. The array is dynamically allocated, and must be deallocated by the user with msat_free(). If a term contains multiple annotations, it will occur multiple times here (once for each annotation). |
out_annots | On success, the annotations of the parsed terms are stored here. Must not be NULL. Both the array and its elements are dynamically allocated, and must be deallocated by the user with msat_free(). For each term at index i in out_terms, the corresponding annotation is stored as a key, value pair at indices 2*i and 2*i+1 in out_annots. |
- Returns
- zero on success, nonzero on error.
◆ msat_annotated_list_from_smtlib2_file()
int msat_annotated_list_from_smtlib2_file |
( |
msat_env |
e, |
|
|
FILE * |
f, |
|
|
size_t * |
out_n, |
|
|
msat_term ** |
out_terms, |
|
|
char *** |
out_annots |
|
) |
| |
Like msat_annotated_list_from_smtlib2(), but reads from a file instead of a string.
Given a FILE in SMT-LIB v2 format, collect and return all and only the terms with an annotation.
- Parameters
-
e | Then environment in which terms are created |
data | The input string in SMT-LIBv2 format |
out_n | On success, the number of terms is stored here. Must not be NULL. Notice that terms with multiple annotations are counted multiple times (see out_names below) |
out_terms | On success, the parsed annotated terms are stored here. Must not be NULL. The array is dynamically allocated, and must be deallocated by the user with msat_free(). If a term contains multiple annotations, it will occur multiple times here (once for each annotation). |
out_annots | On success, the annotations of the parsed terms are stored here. Must not be NULL. Both the array and its elements are dynamically allocated, and must be deallocated by the user with msat_free(). For each term at index i in out_terms, the corresponding annotation is stored as a key, value pair at indices 2*i and 2*i+1 in out_annots. |
- Returns
- zero on success, nonzero on error.
◆ msat_annotated_list_to_smtlib2()
char* msat_annotated_list_to_smtlib2 |
( |
msat_env |
e, |
|
|
size_t |
n, |
|
|
msat_term * |
terms, |
|
|
const char ** |
annots |
|
) |
| |
Converts the given list of annotated terms to SMT-LIB v2 format.
- Parameters
-
e | The environment in which the terms are defined |
n | The number of terms to dump |
terms | The terms to convert |
annots | An array of annotations for the terms. For each term at index i in terms, the corresponding (key, value) annotation is stored at indices 2*i and 2*i+1 in annots. Terms with multiple annotations should be listed multiple times in terms (once for each annotation). |
- Returns
- a string in SMT-LIB v2 format storing all the annotated input terms, or NULL in case of errors. If not NULL, the returned string must be deallocated by the user with msat_free().
◆ msat_annotated_list_to_smtlib2_file()
int msat_annotated_list_to_smtlib2_file |
( |
msat_env |
e, |
|
|
size_t |
n, |
|
|
msat_term * |
terms, |
|
|
const char ** |
annots, |
|
|
FILE * |
out |
|
) |
| |
Like msat_annotated_list_to_smtlib2(), but writes to a FILE instead of returning a string.
- Parameters
-
e | The environment in which the terms are defined |
n | The number of terms to dump |
terms | The terms to convert |
annots | An array of annotations for the terms. For each term at index i in terms, the corresponding (key, value) annotation is stored at indices 2*i and 2*i+1 in annots. Terms with multiple annotations should be listed multiple times in terms (once for each annotation). |
out | The output file |
- Returns
- zero on success, nonzero on error.
◆ msat_apply_substitution()
msat_term msat_apply_substitution |
( |
msat_env |
e, |
|
|
msat_term |
t, |
|
|
size_t |
n, |
|
|
msat_term * |
to_subst, |
|
|
msat_term * |
values |
|
) |
| |
substitutes the terms in to_subst with values in t
- Parameters
-
e | The environment in which to operate |
t | The term to apply the substitution to |
n | The number of terms to substitute |
to_subst | The terms to substitute |
values | The values to substitute |
- Returns
- The result of the substitution, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_assert_formula()
int msat_assert_formula |
( |
msat_env |
e, |
|
|
msat_term |
formula |
|
) |
| |
Adds a logical formula to an environment.
- Parameters
-
e | The environment in which the formula is asserted |
formula | The formula to assert. Must have been created in e, otherwise bad things will happen (probably a crash) |
- Returns
- zero on success, nonzero on error
◆ msat_clear_preferred_for_branching()
int msat_clear_preferred_for_branching |
( |
msat_env |
e | ) |
|
Clears the list of preferred variables for branching.
- Parameters
-
e | The environment in which to operate |
- Returns
- zero on success, nonzero on error
◆ msat_create_config()
msat_config msat_create_config |
( |
void |
| ) |
|
Creates a new MathSAT configuration.
- Returns
- A new configuration.
◆ msat_create_default_config()
msat_config msat_create_default_config |
( |
const char * |
logic | ) |
|
Creates a new MathSAT configuration with the default settings for the given logic.
- Parameters
-
logic | An SMT-LIB logic name |
- Returns
- A new configuration. In case of errors, a cfg s.t. MSAT_ERROR_CONFIG(cfg) is true is returned
◆ msat_create_env()
msat_env msat_create_env |
( |
msat_config |
cfg | ) |
|
Creates a new MathSAT environment from the given configuration.
- Parameters
-
cfg | The configuration to use. |
- Returns
- A new environment. Use MSAT_ERROR_ENV to check for errors
◆ msat_create_itp_group()
int msat_create_itp_group |
( |
msat_env |
e | ) |
|
Creates a new group for interpolation.
When computing an interpolant, formulas are organized into several groups, which are partitioned into two sets GA and GB. The conjuction of formulas in GA will play the role of A, and that of formulas in GB will play the role of B (see msat_set_itp_group, msat_get_interpolant).
- Parameters
-
e | The environment in which to operate. |
- Returns
- an identifier for the new group, or -1 in case of error.
◆ msat_create_model_iterator()
msat_model_iterator msat_create_model_iterator |
( |
msat_env |
e | ) |
|
Creates a model iterator.
- Parameters
-
- Returns
- an iterator for the current model
◆ msat_create_shared_env()
msat_env msat_create_shared_env |
( |
msat_config |
cfg, |
|
|
msat_env |
sibling |
|
) |
| |
Creates an environment that can share terms with its sibling.
- Parameters
-
cfg | The configuration to use. |
sibling | The environment with which to share terms. |
- Returns
- A new environment. Use MSAT_ERROR_ENV to check for errors
◆ msat_decl_get_arg_type()
msat_type msat_decl_get_arg_type |
( |
msat_decl |
d, |
|
|
size_t |
n |
|
) |
| |
Returns the type of the given argument for the input declaration.
- Parameters
-
d | A declaration |
n | The index of the argument for which the type is needed |
- Returns
- The type of the given argument, or MSAT_U on error.
◆ msat_decl_get_arity()
size_t msat_decl_get_arity |
( |
msat_decl |
d | ) |
|
Returns the arity (number of arguments) of the given declaration.
- Parameters
-
- Returns
- The arity of the declaration.
◆ msat_decl_get_name()
char* msat_decl_get_name |
( |
msat_decl |
d | ) |
|
Returns the name corresponding to the given declaration.
- Parameters
-
- Returns
- The name of the given declaration. The returned string must be deallocated by the user with msat_free(). NULL is returned in case of error.
◆ msat_decl_get_return_type()
msat_type msat_decl_get_return_type |
( |
msat_decl |
d | ) |
|
Returns the return type of the given declaration.
The return type for a constant is simply the constant's type.
- Parameters
-
- Returns
- The return type. In case of error, MSAT_U is returned.
◆ msat_decl_get_tag()
Returns the symbol tag associated to the given declaration.
- Parameters
-
e | The environment in which to operate |
d | A declaration |
- Returns
- the tag of the declaration
◆ msat_decl_id()
size_t msat_decl_id |
( |
msat_decl |
d | ) |
|
Returns a numeric identifier for the input declaration.
The returned value is guaranteed to be unique within the environment in which d was defined. Therefore, it can be used to test two declarations for equality, as well as a hash value.
- Parameters
-
- Returns
- a unique (within the defining env) numeric identifier
◆ msat_decl_repr()
char* msat_decl_repr |
( |
msat_decl |
d | ) |
|
Returns an internal string representation of a declaration.
The returned string can be useful for debugging purposes only, as it is an internal representation of a declaration
- Parameters
-
- Returns
- a string reprsentation of d, or NULL in case of errors. The string must be dellocated by the caller with msat_free().
◆ msat_declare_function()
msat_decl msat_declare_function |
( |
msat_env |
e, |
|
|
const char * |
name, |
|
|
msat_type |
type |
|
) |
| |
Declares a new uninterpreted function/constant.
- Parameters
-
e | The environment of the declaration. |
name | A name for the function. It must be unique in the environment. |
type | The type of the function. |
- Returns
- A constant declaration, or a val s.t. MSAT_ERROR_DECL(val) is true in case of errors.
◆ msat_destroy_config()
void msat_destroy_config |
( |
msat_config |
cfg | ) |
|
Destroys a configuration.
It is an error to destroy a configuration that is still being used by an environment.
- Parameters
-
cfg | The configuration to destroy. |
◆ msat_destroy_env()
void msat_destroy_env |
( |
msat_env |
e | ) |
|
Destroys an environment.
- Parameters
-
e | The environment to destroy. |
◆ msat_destroy_model()
void msat_destroy_model |
( |
msat_model |
m | ) |
|
Destroys the given model object.
- Parameters
-
◆ msat_destroy_model_iterator()
void msat_destroy_model_iterator |
( |
msat_model_iterator |
i | ) |
|
Destroys a model iterator.
- Parameters
-
i | The iterator to destroy. |
◆ msat_destroy_proof_manager()
void msat_destroy_proof_manager |
( |
msat_proof_manager |
m | ) |
|
Destroys a proof manager.
Destroying a proof manager will also destroy all the proofs associated with it.
- Parameters
-
m | The proof manager to destroy. |
◆ msat_dpll_callback_ask_theory_reason()
int msat_dpll_callback_ask_theory_reason |
( |
msat_dpll_callback |
cb, |
|
|
int |
lit, |
|
|
int ** |
reason |
|
) |
| |
Callback function that the external SAT solver must call for asking MathSAT the reason for a theory-deduced literal, during conflict analysis.
- Parameters
-
cb | The callback object to use. |
level | The literal whose reason needs to be computed. |
reason | Pointer to the zero-terminated reason clause for lit, with the first element being lit itself. |
- Returns
- zero on success, nonzero on error.
◆ msat_dpll_callback_model_found()
int msat_dpll_callback_model_found |
( |
msat_dpll_callback |
cb, |
|
|
msat_truth_value * |
code, |
|
|
int ** |
conflict |
|
) |
| |
Callback function that the external SAT solver must call when a Boolean model has been found.
The code value set by callback function tells the SAT solver what to do.
- if it is MSAT_TRUE, the model is theory satisfiable, so the formula is satisfiable.
- if it is MSAT_FALSE, MathSAT found a theory conflict, which is stored in conflict. The SAT solver is expected to perform conflict analysis on it and backjump.
- if it is MSAT_UNDEF, MathSAT created some new variables that need to be assigned by the SAT solver, so the search should continue.
- Parameters
-
cb | The callback object to use. |
code | Pointer to a variable set by the callback function. |
conflict | Pointer for retrieving the theory conflict, when the code value is set to MSAT_FALSE. |
- Returns
- zero on success, nonzero on error.
◆ msat_dpll_callback_no_conflict_after_bcp()
int msat_dpll_callback_no_conflict_after_bcp |
( |
msat_dpll_callback |
cb, |
|
|
msat_truth_value * |
code, |
|
|
int ** |
conflict |
|
) |
| |
Callback function that the external SAT solver must call when a round of BCP has been completed without finding a Boolean conflict.
The code value set by callback function tells the SAT solver what to do.
- if it is MSAT_TRUE, the SAT solver can go on.
- if it is MSAT_FALSE, MathSAT found a theory conflict, which is stored in conflict. The SAT solver is expected to perform conflict analysis on it and backjump.
- if it is MSAT_UNDEF, the SAT solver needs to perform another round of BCP, because MathSAT enqueued some new literals on the trail.
- Parameters
-
cb | The callback object to use. |
code | Pointer to a variable set by the callback function. |
conflict | Pointer for retrieving the theory conflict, when the code value is set to MSAT_FALSE. |
- Returns
- zero on success, nonzero on error.
◆ msat_dpll_callback_notify_assignment()
int msat_dpll_callback_notify_assignment |
( |
msat_dpll_callback |
cb, |
|
|
int |
lit |
|
) |
| |
Callback function that the external SAT solver must call whenever a literal is added to the trail.
- Parameters
-
cb | The callback object to use. |
lit | The assigned literal in DIMACS format. |
- Returns
- zero on success, nonzero on error.
◆ msat_dpll_callback_notify_backtrack()
int msat_dpll_callback_notify_backtrack |
( |
msat_dpll_callback |
cb, |
|
|
int |
level |
|
) |
| |
Callback function that the external SAT solver must call whenever it backtracks.
- Parameters
-
cb | The callback object to use. |
level | The target decision level for backtracking. |
- Returns
- zero on success, nonzero on error.
◆ msat_dpll_callback_notify_new_level()
int msat_dpll_callback_notify_new_level |
( |
msat_dpll_callback |
cb | ) |
|
Callback function that the external SAT solver must call whenever a new decision level is opened.
- Parameters
-
cb | The callback object to use. |
- Returns
- zero on success, nonzero on error.
◆ msat_existentially_quantify()
msat_term msat_existentially_quantify |
( |
msat_env |
e, |
|
|
msat_term |
t, |
|
|
msat_term |
args[], |
|
|
size_t |
n |
|
) |
| |
Returns a term resulting from existentially quantifying the given constants in the given term.
- Parameters
-
e | The environment of the definition |
t | The term whose constants should be existentially quantified. |
args | The list of constants to quantify. |
n | The size of the list of constants. |
- Returns
- The term exists constants body, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_find_decl()
msat_decl msat_find_decl |
( |
msat_env |
e, |
|
|
const char * |
symbol |
|
) |
| |
Returns the declaration of the given symbol in the given environment (if any)
If symbol is not declared in e, the returned value ret will be s.t. MSAT_ERROR_DECL(ret) is true
- Parameters
-
e | The environment in which to operate |
- Returns
- The declaration of symbol in e, or a ret s.t. MSAT_ERROR_DECL(ret) is true
◆ msat_free()
void msat_free |
( |
void * |
ptr | ) |
|
Function for deallocating the memory accessible by pointers returned by MathSAT.
◆ msat_from_smtlib1()
msat_term msat_from_smtlib1 |
( |
msat_env |
e, |
|
|
const char * |
data |
|
) |
| |
Creates a term from a string in SMT-LIB v1 format.
- Parameters
-
e | The environment in which to create the term. |
data | The string representation in SMT-LIB v1 format. |
- Returns
- The created term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_from_smtlib1_file()
msat_term msat_from_smtlib1_file |
( |
msat_env |
e, |
|
|
FILE * |
f |
|
) |
| |
Creates a term from a file in SMT-LIB v1 format.
- Parameters
-
e | The environment in which to create the term. |
f | The file in SMT-LIB v1 format. |
- Returns
- The created term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_from_smtlib2()
msat_term msat_from_smtlib2 |
( |
msat_env |
e, |
|
|
const char * |
data |
|
) |
| |
Creates a term from a string in SMT-LIB v2 format.
- Parameters
-
e | The environment in which to create the term. |
data | The string representation in SMT-LIB v2 format. It can't contain commands other than functions and type declarations, definitions, and assertions |
- Returns
- The created term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_from_smtlib2_file()
msat_term msat_from_smtlib2_file |
( |
msat_env |
e, |
|
|
FILE * |
f |
|
) |
| |
Creates a term from a file in SMT-LIB v2 format.
- Parameters
-
e | The environment in which to create the term. |
f | The file in SMT-LIB v2 format. It can't contain commands other than functions and type declarations, definitions, and assertions |
- Returns
- The created term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_from_string()
msat_term msat_from_string |
( |
msat_env |
e, |
|
|
const char * |
data |
|
) |
| |
Creates a term from its string representation.
The syntax of repr is that of the SMT-LIB v2. All the variables and functions must have been previously declared in e.
- Parameters
-
e | The environment of the definition |
repr | The string to parse, in SMT-LIB v2 syntax |
- Returns
- The created term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_gc_env()
int msat_gc_env |
( |
msat_env |
env, |
|
|
msat_term * |
tokeep, |
|
|
size_t |
num_tokeep |
|
) |
| |
Performs garbage collection on the given environment.
This function will perform garbage collection on the given environment. All the internal caches of the environment will be cleared (including those in the active solvers and preprocessors). If the environment is not shared, all the terms that are not either in tokeep or in the current asserted formulas will be deleted.
- Parameters
-
env | The environment in which to operate. |
tokeep | List of terms to not delete. |
num_tokeep | Size of the tokeep array. |
- Returns
- zero on success, nonzero on error.
◆ msat_get_array_type()
msat_type msat_get_array_type |
( |
msat_env |
env, |
|
|
msat_type |
itp, |
|
|
msat_type |
etp |
|
) |
| |
returns the type for arrays with indices of itp type and elements of etp type.
◆ msat_get_asserted_formulas()
msat_term* msat_get_asserted_formulas |
( |
msat_env |
e, |
|
|
size_t * |
num_asserted |
|
) |
| |
Returns the list of formulas in the assertion stack.
The return value is a dynamically-allocated array of *num_asserted elements, which must be deallocated by the user. NULL is returned in case of errors. The array elements are formulas that are logically equivalent to the one asserted using msat_assert_formula
- Parameters
-
e | The environment in which to operate. |
num_asserted | Pointer to a valid address for storing the number of formulas currently in the assertion stack. |
- Returns
- An array with the asserted formulas, or NULL in case of errors. The array is must be deallocated by allocated the user with msat_free().
◆ msat_get_bool_type()
msat_type msat_get_bool_type |
( |
msat_env |
env | ) |
|
returns the type for Booleans in the given env.
◆ msat_get_bv_type()
msat_type msat_get_bv_type |
( |
msat_env |
env, |
|
|
size_t |
width |
|
) |
| |
returns the type for bit-vectors of the given width.
◆ msat_get_enum_type()
msat_type msat_get_enum_type |
( |
msat_env |
env, |
|
|
const char * |
name, |
|
|
size_t |
domain_size, |
|
|
const char ** |
domain |
|
) |
| |
returns an enum type in the given env.
- Parameters
-
env | The environment in which to operate |
name | The name of the enum type |
domain_size | The number of values of the enum |
domain | The possible values of the enum |
- Returns
- an enum type
◆ msat_get_fp_roundingmode_type()
msat_type msat_get_fp_roundingmode_type |
( |
msat_env |
env | ) |
|
returns the type for float rounding modes in the given env.
◆ msat_get_fp_type()
msat_type msat_get_fp_type |
( |
msat_env |
env, |
|
|
size_t |
exp_width, |
|
|
size_t |
mant_width |
|
) |
| |
returns the type for floats with the given exponent and significand/mantissa width.
◆ msat_get_function_type()
msat_type msat_get_function_type |
( |
msat_env |
env, |
|
|
msat_type * |
param_types, |
|
|
size_t |
num_params, |
|
|
msat_type |
return_type |
|
) |
| |
returns a function type in the given env.
- Parameters
-
env | The environment in which to operate |
param_types | The types of the function arguments |
num_params | The arity of the function type |
return_type | The type of the return value |
- Returns
- a function type
◆ msat_get_integer_type()
msat_type msat_get_integer_type |
( |
msat_env |
env | ) |
|
returns the type for integers in the given env.
◆ msat_get_interpolant()
msat_term msat_get_interpolant |
( |
msat_env |
e, |
|
|
int * |
groups_of_a, |
|
|
size_t |
n |
|
) |
| |
Computes an interpolant for a pair (A, B) of formulas.
A is the conjucntion of all the assumed formulas in the groups_of_a groups (see msat_create_itp_group), and B is the rest of assumed formulas.
This function must be called only after msat_solve, and only if MSAT_UNSAT was returned. Moreover, interpolation must have been enabled in the configuration for the environment
- Parameters
-
e | The environment in which to operate. |
groups_of_a | An array of group identifiers. |
n | The size of the groups_of_a array. |
- Returns
- The interpolating term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_get_model()
msat_model msat_get_model |
( |
msat_env |
e | ) |
|
Creates a model object.
- Parameters
-
- Returns
- A model object. Use MSAT_ERROR_MODEL() to check for errors.
◆ msat_get_model_value()
msat_term msat_get_model_value |
( |
msat_env |
e, |
|
|
msat_term |
term |
|
) |
| |
Returns the value of the term term in the current model.
Preconditions:
- model computation was enabled in the configuration of the environment
- the last call to msat_solve returned a MSAT_SAT result
- no assert/push/pop/allsat commands have been issued in the meantime
- Parameters
-
e | The environment in use |
term | The term of interest. |
- Returns
- The model value for term. If an error occurs, the return value ret is such that MSAT_ERROR_TERM(ret) is true
◆ msat_get_proof()
msat_proof msat_get_proof |
( |
msat_proof_manager |
m | ) |
|
Returns a proof of unsatisfiability.
a proof is recursively defined as:
msat_proof ::= msat_term | name msat_proof*
i.e., it is either a term or a list of a name and children proofs. Proofs can be distinguished by their name, or by whether they are terms. Relevant proofs include:
"clause-hyp", which are the clauses of the (CNF conversion of the) input problem. They have a list of terms as children
"res-chain", representing Boolean resolution chains. The children are an interleaving of proofs and terms, where terms are the pivots for the resolution. For example: "res-chain p1 v p2" represents a resolution step between p1 and p2 on the pivot v
"theory-lemma", representing theory lemmas. They have as children a list of terms that consititute the lemma, plus an optional last element which is a more detailed proof produced by a theory solver.
- Parameters
-
m | The proof manager in which to operate. |
- Returns
- The proof of unsatisfiability associated to the latest msat_solve() call, or an object p s.t. MSAT_ERROR_PROOF(p) is true in case of errors.
◆ msat_get_proof_manager()
msat_proof_manager msat_get_proof_manager |
( |
msat_env |
e | ) |
|
Returns a proof manager for the given environment.
The manager must be destroyed by the user, with msat_destroy_proof_manager. In order to obtain a non-error result, the option "proof_generation" must be set to "true" in the configuration used for creating the environment.
- Parameters
-
e | The environment in which to operate. |
- Returns
- A proof manager for the environment. MSAT_ERROR_PROOF_MANAGER can be used to check whether an error occurred.
◆ msat_get_rational_type()
msat_type msat_get_rational_type |
( |
msat_env |
env | ) |
|
returns the type for rationals in the given env.
◆ msat_get_search_stats()
char* msat_get_search_stats |
( |
msat_env |
e | ) |
|
Returns a string with search statistics for the given environment.
The returned string will contain newline-separated statistics for the DPLL engine and the active theory solvers in the given environment.
- Parameters
-
e | The environment in which to operate. |
- Returns
- A string with search statistics, or NULL in case of errors. The string must be deallocated by the user with msat_free().
◆ msat_get_simple_type()
msat_type msat_get_simple_type |
( |
msat_env |
env, |
|
|
const char * |
name |
|
) |
| |
returns an atomic type with the given name in the given env.
◆ msat_get_theory_lemmas()
msat_term* msat_get_theory_lemmas |
( |
msat_env |
e, |
|
|
size_t * |
num_tlemmas |
|
) |
| |
Retrieves the theory lemmas used in the last search (see msat_solve).
For the function to work, the option "dpll.store_tlemmas" must be set to "true" in the configuration object for the environment.
- Parameters
-
e | The environment in which to operate. |
num_tlemmas | Pointer to a valid address for storing the number of theory lemmas returned. |
- Returns
- An array with the theory lemmas, or NULL in case of errors. The array must be deallocated by the user with msat_free().
◆ msat_get_unsat_assumptions()
msat_term* msat_get_unsat_assumptions |
( |
msat_env |
e, |
|
|
size_t * |
assumps_size |
|
) |
| |
Returns the list of assumptions resposible for the unsatisfiability detected by the last search (see msat_solve_with_assumptions).
- Parameters
-
e | The environment in which to operate. |
assumps_size | Pointer to a valid address for storing the number of formulas in the returned array. |
- Returns
- An array with the list of inconsistent assumptions, or NULL in case of errors. The array must be deallocated by the user with msat_free().
◆ msat_get_unsat_core()
msat_term* msat_get_unsat_core |
( |
msat_env |
e, |
|
|
size_t * |
core_size |
|
) |
| |
Returns the unsatisfiable core of the last search (see msat_solve) as a subset of the asserted formulas, if the problem was unsatisfiable.
- Parameters
-
e | The environment in which to operate. |
core_size | Pointer to a valid address for storing the number of formulas in the unsat core. |
- Returns
- An array with the unsat core, or NULL in case of errors. The array must be deallocated by the user with msat_free().
◆ msat_get_unsat_core_ext()
Returns the unsatisfiable core of the last search (see msat_solve) as a subset of the asserted formulas, computed using an external Boolean unsat core extractor (see msat_ext_unsat_core_extractor).
- Parameters
-
e | The environment in which to operate. |
core_size | Pointer to a valid address for storing the number of formulas in the unsat core. |
extractor | The external Boolean core extractor. |
user_data | Generic data pointer which will be passed to extractor. Can be anything, its value will not be interpreted. |
- Returns
- An array with the unsat core, or NULL in case of errors. The array must be deallocated by the user with msat_free().
◆ msat_get_version()
char* msat_get_version |
( |
void |
| ) |
|
Gets the current MathSAT version.
- Returns
- A version string, with version information about MathSAT, the GMP library and the compiler used. The string must be deallocated by the user with msat_free().
◆ msat_is_array_type()
int msat_is_array_type |
( |
msat_env |
env, |
|
|
msat_type |
tp, |
|
|
msat_type * |
out_itp, |
|
|
msat_type * |
out_etp |
|
) |
| |
checks whether the given type is an array.
- Parameters
-
env | The environment in which to operate |
tp | The type to check |
out_itp | Pointer to a variable where to store the type of the array indices (can be NULL) |
out_itp | Pointer to a variable where to store the type of the array elements (can be NULL) |
- Returns
- 1 if the type is an array, 0 otherwise
◆ msat_is_bool_type()
int msat_is_bool_type |
( |
msat_env |
env, |
|
|
msat_type |
tp |
|
) |
| |
checks whether the given type is bool.
- Parameters
-
env | The environment in which to operate |
tp | The type to check |
- Returns
- 1 if the type is bool, 0 otherwise
◆ msat_is_bv_type()
int msat_is_bv_type |
( |
msat_env |
env, |
|
|
msat_type |
tp, |
|
|
size_t * |
out_width |
|
) |
| |
checks whether the given type is a bit-vector.
- Parameters
-
env | The environment in which to operate |
tp | The type to check |
out_width | Pointer to a variable where to store the width of the BV type in case of success (can be NULL) |
- Returns
- 1 if the type is a bit-vector, 0 otherwise
◆ msat_is_enum_type()
int msat_is_enum_type |
( |
msat_env |
env, |
|
|
msat_type |
tp, |
|
|
size_t * |
out_domain_size, |
|
|
msat_decl ** |
out_domain |
|
) |
| |
checks whether the given type is an enum
- Parameters
-
env | The environment in which to operate |
tp | The type to check |
out_exp_width | Pointer to a variable where to store the number of values in the enum (can be NULL) |
out_mant_width | Pointer to a variable where to store the list of values in the enum (can be NULL) |
- Returns
- 1 if the type is an enum, 0 otherwise
◆ msat_is_fp_roundingmode_type()
int msat_is_fp_roundingmode_type |
( |
msat_env |
env, |
|
|
msat_type |
tp |
|
) |
| |
checks whether the given type is a float rounding mode type.
- Parameters
-
env | The environment in which to operate |
tp | The type to check |
◆ msat_is_fp_type()
int msat_is_fp_type |
( |
msat_env |
env, |
|
|
msat_type |
tp, |
|
|
size_t * |
out_exp_width, |
|
|
size_t * |
out_mant_width |
|
) |
| |
checks whether the given type is a float.
- Parameters
-
env | The environment in which to operate |
tp | The type to check |
out_exp_width | Pointer to a variable where to store the width of the exponent of the float in case of success (can be NULL) |
out_mant_width | Pointer to a variable where to store the width of the significand/mantissa of the float in case of success (can be NULL) |
- Returns
- 1 if the type is a float, 0 otherwise
◆ msat_is_integer_type()
int msat_is_integer_type |
( |
msat_env |
env, |
|
|
msat_type |
tp |
|
) |
| |
checks whether the given type is int.
- Parameters
-
env | The environment in which to operate |
tp | The type to check |
- Returns
- 1 if the type is int, 0 otherwise
◆ msat_is_rational_type()
int msat_is_rational_type |
( |
msat_env |
env, |
|
|
msat_type |
tp |
|
) |
| |
checks whether the given type is rat.
- Parameters
-
env | The environment in which to operate |
tp | The type to check |
- Returns
- 1 if the type is rat, 0 otherwise
◆ msat_last_error_message()
const char* msat_last_error_message |
( |
msat_env |
env | ) |
|
Retrieves the last error message generated while operating in the given enviroment.
- Parameters
-
env | The environment in which the error occurred. |
- Returns
- A pointer to the last error message generated.
◆ msat_make_and()
msat_term msat_make_and |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the logical AND of t1 and t2.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. Must have type ::MSAT_BOOL. |
t2 | The second argument. Must have type ::MSAT_BOOL. |
- Returns
- The term t1 & t2, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_array_const()
msat_term msat_make_array_const |
( |
msat_env |
e, |
|
|
msat_type |
arrtp, |
|
|
msat_term |
elem |
|
) |
| |
Creates a constant array.
- Parameters
-
e | The environment of the definition |
arrtp | The type of the return array |
elem | The element term |
- Returns
- The term representing the constant array filled with "elem", or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_array_read()
msat_term msat_make_array_read |
( |
msat_env |
e, |
|
|
msat_term |
arr, |
|
|
msat_term |
idx |
|
) |
| |
Creates an array read operation.
- Parameters
-
e | The environment of the definition |
arr | The array term |
idx | The index term |
- Returns
- The term representing the array read, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_array_write()
msat_term msat_make_array_write |
( |
msat_env |
e, |
|
|
msat_term |
arr, |
|
|
msat_term |
idx, |
|
|
msat_term |
elem |
|
) |
| |
Creates an array write operation.
- Parameters
-
e | The environment of the definition |
arr | The array term |
idx | The index term |
elem | The element term |
- Returns
- The term representing the array write, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_asin()
msat_term msat_make_asin |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Returns an expression representing arcsin(t)
- Parameters
-
e | The environment of the definition |
t | The argument |
- Returns
- The created term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_and()
msat_term msat_make_bv_and |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the bit-wise AND of t1 and t2.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. |
t2 | The second argument. |
- Precondition
t1 and t2 must have the same width.
- Returns
- The term t1 & t2, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_ashr()
msat_term msat_make_bv_ashr |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the arithmetic right shift of t1 by t2.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. |
t2 | The second argument. |
- Precondition
t1 and t2 must have the same width.
- Returns
- The term t1 >> t2, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_comp()
msat_term msat_make_bv_comp |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the comparison of t1 and t2, resulting in a bit-vector of size 1.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. |
t2 | The second argument. |
- Precondition
t1 and t2 must have the same width.
- Returns
- The term bvcomp(t1, t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_concat()
msat_term msat_make_bv_concat |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the concatenation of t1 and t2.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. |
t2 | The second argument. |
- Returns
- The term t1 :: t2, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_extract()
msat_term msat_make_bv_extract |
( |
msat_env |
e, |
|
|
size_t |
msb, |
|
|
size_t |
lsb, |
|
|
msat_term |
t |
|
) |
| |
Returns a term representing the selection of t[msb:lsb].
- Parameters
-
e | The environment of the definition |
msb | The most significant bit of the selection. |
lsb | The least significant bit of the selection. |
t | The argument. |
- Returns
- The term t[msb:lsb], or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_int_number()
msat_term msat_make_bv_int_number |
( |
msat_env |
e, |
|
|
int |
value, |
|
|
size_t |
width |
|
) |
| |
Returns an expression representing a bit-vector number.
- Parameters
-
e | The environment of the definition |
value | The value for the number. It must be non-negative. |
width | The width in bits of the number |
- Returns
- The numeric term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_lshl()
msat_term msat_make_bv_lshl |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the logical left shift of t1 by t2.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. |
t2 | The second argument. |
- Precondition
- t1 and t2 must have the same width.
- Returns
- The term t1 << t2, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_lshr()
msat_term msat_make_bv_lshr |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the logical right shift of t1 by t2.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. |
t2 | The second argument. |
- Precondition
t1 and t2 must have the same width.
- Returns
- The term t1 >> t2, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_minus()
msat_term msat_make_bv_minus |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the subtraction of t1 by t2.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. |
t2 | The second argument. |
- Precondition
t1 and t2 must have the same width.
- Returns
- The term t1 - t2, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_mpz_number()
msat_term msat_make_bv_mpz_number |
( |
msat_env |
e, |
|
|
mpz_t |
value, |
|
|
size_t |
width |
|
) |
| |
Returns an expression representing a bit-vector number.
- Parameters
-
e | The environment of the definition |
value | The value for the number. It must be non-negative. |
width | The width in bits of the number |
- Returns
- The numeric term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_neg()
msat_term msat_make_bv_neg |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Returns a term representing the negation of t, te two's-complement.
- Parameters
-
e | The environment of the definition |
t | The argument. |
- Returns
- The term -t, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_not()
msat_term msat_make_bv_not |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Returns a term representing the bit-wise negation of t.
- Parameters
-
e | The environment of the definition |
t | The argument to negate. |
- Returns
- The term !t, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_number()
msat_term msat_make_bv_number |
( |
msat_env |
e, |
|
|
const char * |
num_rep, |
|
|
size_t |
width, |
|
|
size_t |
base |
|
) |
| |
Returns an expression representing a bit-vector number.
- Parameters
-
e | The environment of the definition |
num_rep | A string representation for the number. The number must be non-negative. |
width | The width in bits of the number |
base | The base of the representation. Can be 2, 10 or 16. |
- Returns
- The numeric term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_or()
msat_term msat_make_bv_or |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the bit-wise OR of t1 and t2.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. |
t2 | The second argument. |
- Precondition
t1 and t2 must have the same width.
- Returns
- The term t1 | t2, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_plus()
msat_term msat_make_bv_plus |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the addition of t1 and t2.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. |
t2 | The second argument. |
- Precondition
t1 and t2 must have the same width.
- Returns
- The term t1 + t2, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_rol()
msat_term msat_make_bv_rol |
( |
msat_env |
e, |
|
|
size_t |
amount, |
|
|
msat_term |
t |
|
) |
| |
Returns a term representing the left rotation of 1 by amount bits.
- Parameters
-
e | The environment of the definition |
amount | The amount of the rotation |
t | The argument of the rotation. |
- Returns
- The term rol(amount, t), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_ror()
msat_term msat_make_bv_ror |
( |
msat_env |
e, |
|
|
size_t |
amount, |
|
|
msat_term |
t |
|
) |
| |
Returns a term representing the right rotation of 1 by amount bits.
- Parameters
-
e | The environment of the definition |
amount | The amount of the rotation |
t | The argument of the rotation. |
- Returns
- The term ror(amount, t), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_sdiv()
msat_term msat_make_bv_sdiv |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the signed division of t1 by t2.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. |
t2 | The second argument. |
- Precondition
t1 and t2 must have the same width.
- Returns
- The term t1 / t2, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_sext()
msat_term msat_make_bv_sext |
( |
msat_env |
e, |
|
|
size_t |
amount, |
|
|
msat_term |
t |
|
) |
| |
Returns a term representing the sign extension of t1 by amount.
- Parameters
-
e | The environment of the definition |
amount | The amount of the extension |
t | The first argument. |
- Returns
- The term sext(amount, t), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_sleq()
msat_term msat_make_bv_sleq |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the signed t1 <= t2.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. |
t2 | The second argument. |
- Precondition
t1 and t2 must have the same width.
- Returns
- The term t1 <= t2, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_slt()
msat_term msat_make_bv_slt |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the signed t1 < t2.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. |
t2 | The second argument. |
- Precondition
t1 and t2 must have the same width.
- Returns
- The term t1 < t2, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_srem()
msat_term msat_make_bv_srem |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the signed remainder of t1 by t2.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. |
t2 | The second argument. |
- Precondition
t1 and t2 must have the same width.
- Returns
- The term t1 % t2, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_times()
msat_term msat_make_bv_times |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the multiplication of t1 and t2.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. |
t2 | The second argument. |
- Precondition
t1 and t2 must have the same width.
- Returns
- The term t1 * t2, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_udiv()
msat_term msat_make_bv_udiv |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the unsigned division of t1 by t2.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. |
t2 | The second argument. |
- Precondition
t1 and t2 must have the same width.
- Returns
- The term t1 / t2, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_uleq()
msat_term msat_make_bv_uleq |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the unsigned t1 <= t2.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. |
t2 | The second argument. |
- Precondition
t1 and t2 must have the same width.
- Returns
- The term t1 <= t2, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_ult()
msat_term msat_make_bv_ult |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the unsigned t1 < t2.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. |
t2 | The second argument. |
- Precondition
t1 and t2 must have the same width.
- Returns
- The term t1 < t2, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_urem()
msat_term msat_make_bv_urem |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the unsigned remainder of t1 by t2.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. |
t2 | The second argument. |
- Precondition
t1 and t2 must have the same width.
- Returns
- The term t1 % t2, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_xor()
msat_term msat_make_bv_xor |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the bit-wise XOR of t1 and t2.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. |
t2 | The second argument. |
- Precondition
t1 and t2 must have the same width.
- Returns
- The term t1 xor t2, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_bv_zext()
msat_term msat_make_bv_zext |
( |
msat_env |
e, |
|
|
size_t |
amount, |
|
|
msat_term |
t |
|
) |
| |
Returns a term representing the zero extension of t.
- Parameters
-
e | The environment of the definition |
amount | The amount of the extension |
t | The first argument. |
- Returns
- The term zext(amount, t), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_constant()
msat_term msat_make_constant |
( |
msat_env |
e, |
|
|
msat_decl |
var |
|
) |
| |
Creates a constant from a declaration.
- Parameters
-
e | The environment of the definition |
var | The declaration of the constant. Must come from the same environment |
- Returns
- The term representing the constant, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_copy_from()
msat_term msat_make_copy_from |
( |
msat_env |
e, |
|
|
msat_term |
t, |
|
|
msat_env |
src |
|
) |
| |
Creates a term in e from an equivalent term t that was created in src.
- Parameters
-
e | The environment in which to create the term |
t | The term to copy |
src | The environment in which t was created |
- Returns
- The created term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_divide()
msat_term msat_make_divide |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns an expression representing (t1 / t2).
The arguments must have the same type, with the usual exception for integer numbers.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. Must be of type rational or integer |
t2 | The second argument. Must be of type rational or integer |
- Returns
- The term (t1 / t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_eq()
msat_term msat_make_eq |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the equivalence of t1 and t2.
This is a convenience function that calls either msat_make_equal() or msat_make_iff(), according to the type of the arguments.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. |
t2 | The second argument. |
- Returns
- The term (t1 = t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_equal()
msat_term msat_make_equal |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the equivalence of t1 and t2.
Note that this does not work If ::t1 and ::t2 have Boolean type (use msat_make_iff() in that case).
- Parameters
-
e | The environment of the definition |
t1 | The first argument. |
t2 | The second argument. |
- Returns
- The term (t1 = t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_exists()
msat_term msat_make_exists |
( |
msat_env |
e, |
|
|
msat_term |
var, |
|
|
msat_term |
body |
|
) |
| |
Returns a term resulting from existentially quantifying the variable var in the term body.
- Parameters
-
e | The environment of the definition |
var | The term representing the quantified variable. |
body | The body of the quantifier. Must have type ::MSAT_BOOL. |
- Returns
- The term exists var body, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_exp()
msat_term msat_make_exp |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Returns an expression representing exp(t)
- Parameters
-
e | The environment of the definition |
t | The argument. |
- Returns
- The created term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_false()
msat_term msat_make_false |
( |
msat_env |
e | ) |
|
Returns a term representing logical falsity.
- Parameters
-
e | The environment of the definition |
- Returns
- The term FALSE, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_floor()
msat_term msat_make_floor |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Returns an expression representing (floor t)
- Parameters
-
e | The environment of the definition |
t | The argument. |
- Returns
- The created term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_forall()
msat_term msat_make_forall |
( |
msat_env |
e, |
|
|
msat_term |
var, |
|
|
msat_term |
body |
|
) |
| |
Returns a term resulting from universally quantifying the variable var in the term body.
- Parameters
-
e | The environment of the definition |
var | The term representing the quantified variable. |
body | The body of the quantifier. Must have type ::MSAT_BOOL. |
- Returns
- The term forall var body, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_abs()
msat_term msat_make_fp_abs |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Returns a term representing the FP absolute value of t.
- Parameters
-
e | The environment of the definition |
t | The abs argument. |
- Returns
- The term (abs t), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_as_ieeebv()
msat_term msat_make_fp_as_ieeebv |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Returns a term for interpreting a FP term as a bit-vector.
This is different from ::make_fp_to_sbv in that the latter takes the integer part of the FP number and stores it in a bit-vector, while this function simply takes the bits of the representation of the input and interprets them as a bit-vector (of size 1+ width of exponent + width of mantissa).
- Parameters
-
e | The environment of the definition |
t | The argument to convert. |
- Returns
- The term representing the conversion, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_bits_number()
msat_term msat_make_fp_bits_number |
( |
msat_env |
e, |
|
|
const char * |
bits, |
|
|
size_t |
exp_w, |
|
|
size_t |
mant_w |
|
) |
| |
Creates an FP number from a string of bits.
- Parameters
-
e | The environment of the definition |
num_rep | A string representation of a base-10 integer number |
exp_w | The desired exponent width |
mant_w | The desired mantissa width |
- Returns
- The numeric term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_cast()
msat_term msat_make_fp_cast |
( |
msat_env |
e, |
|
|
size_t |
exp_w, |
|
|
size_t |
mant_w, |
|
|
msat_term |
rounding, |
|
|
msat_term |
t |
|
) |
| |
Returns a term representing the FP format conversion of the given input term.
- Parameters
-
e | The environment of the definition |
exp_w | The target exponent width. |
mant_w | The target mantissa width. |
rounding | The desired rounding mode. |
t | The argument to convert. |
- Returns
- The term representing the conversion, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_div()
msat_term msat_make_fp_div |
( |
msat_env |
e, |
|
|
msat_term |
rounding, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the FP division of t1 and t2, according to the given rounding mode.
- Parameters
-
e | The environment of the definition |
rounding | The desired rounding mode. |
t1 | The first argument. |
t2 | The second argument. |
- Returns
- The term (/ rounding t1 t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_equal()
msat_term msat_make_fp_equal |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the FP equality predicate between t1 and t2.
FP equality is different from the "regular" equality predicate in the handling of NaN values: (fpeq NaN NaN) is always false, whereas (= NaN NaN) is always true
- Parameters
-
e | The environment of the definition |
t1 | The first argument. |
t2 | The second argument. |
- Returns
- The term (fpeq t1 t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_from_ieeebv()
msat_term msat_make_fp_from_ieeebv |
( |
msat_env |
e, |
|
|
size_t |
exp_w, |
|
|
size_t |
mant_w, |
|
|
msat_term |
t |
|
) |
| |
Returns a term representing the FP number whose IEEE 754 encoding is the given bit-vector.
- Parameters
-
e | The environment of the definition |
exp_w | The target exponent width. |
mant_w | The target mantissa width. |
t | The argument to convert. |
- Returns
- The term representing the conversion, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_from_sbv()
msat_term msat_make_fp_from_sbv |
( |
msat_env |
e, |
|
|
size_t |
exp_w, |
|
|
size_t |
mant_w, |
|
|
msat_term |
rounding, |
|
|
msat_term |
t |
|
) |
| |
Returns a term representing the conversion of a signed bit-vector term to FP.
- Parameters
-
e | The environment of the definition |
exp_w | The target exponent width. |
mant_w | The target mantissa width. |
rounding | The desired rounding mode. |
t | The argument to convert. |
- Returns
- The term representing the conversion, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_from_ubv()
msat_term msat_make_fp_from_ubv |
( |
msat_env |
e, |
|
|
size_t |
exp_w, |
|
|
size_t |
mant_w, |
|
|
msat_term |
rounding, |
|
|
msat_term |
t |
|
) |
| |
Returns a term representing the conversion of an unsigned bit-vector term to FP.
- Parameters
-
e | The environment of the definition |
exp_w | The target exponent width. |
mant_w | The target mantissa width. |
rounding | The desired rounding mode. |
t | The argument to convert. |
- Returns
- The term representing the conversion, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_isinf()
msat_term msat_make_fp_isinf |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Returns the predicate for testing whether a FP term is infinity.
- Parameters
-
e | The environment of the definition |
t | The argument to test. |
- Returns
- The term representing (isinf t), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_isnan()
msat_term msat_make_fp_isnan |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Returns the predicate for testing whether a FP term is NaN.
- Parameters
-
e | The environment of the definition |
t | The argument to test. |
- Returns
- The term representing (isnan t), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_isneg()
msat_term msat_make_fp_isneg |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Returns the predicate for testing whether a FP term is negative.
- Parameters
-
e | The environment of the definition |
t | The argument to test. |
- Returns
- The term representing (isneg t), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_isnormal()
msat_term msat_make_fp_isnormal |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Returns the predicate for testing whether a FP term is a normal.
- Parameters
-
e | The environment of the definition |
t | The argument to test. |
- Returns
- The term representing (isnormal t), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_ispos()
msat_term msat_make_fp_ispos |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Returns the predicate for testing whether a FP term is positive.
- Parameters
-
e | The environment of the definition |
t | The argument to test. |
- Returns
- The term representing (ispos t), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_issubnormal()
msat_term msat_make_fp_issubnormal |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Returns the predicate for testing whether a FP term is a subnormal.
- Parameters
-
e | The environment of the definition |
t | The argument to test. |
- Returns
- The term representing (issubnormal t), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_iszero()
msat_term msat_make_fp_iszero |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Returns the predicate for testing whether a FP term is zero.
- Parameters
-
e | The environment of the definition |
t | The argument to test. |
- Returns
- The term representing (iszero t), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_leq()
msat_term msat_make_fp_leq |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the FP <= predicate between t1 and t2.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. |
t2 | The second argument. |
- Returns
- The term (fpleq t1 t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_lt()
msat_term msat_make_fp_lt |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the FP < predicate between t1 and t2.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. |
t2 | The second argument. |
- Returns
- The term (fplt t1 t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_max()
msat_term msat_make_fp_max |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the FP max between t1 and t2.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. |
t2 | The second argument. |
- Returns
- The term (max t1 t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_min()
msat_term msat_make_fp_min |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the FP min between t1 and t2.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. |
t2 | The second argument. |
- Returns
- The term (min t1 t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_minus()
msat_term msat_make_fp_minus |
( |
msat_env |
e, |
|
|
msat_term |
rounding, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the FP subtraction of t1 and t2, according to the given rounding mode.
- Parameters
-
e | The environment of the definition |
rounding | The desired rounding mode. |
t1 | The first argument. |
t2 | The second argument. |
- Returns
- The term (- rounding t1 t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_minus_inf()
msat_term msat_make_fp_minus_inf |
( |
msat_env |
e, |
|
|
size_t |
exp_w, |
|
|
size_t |
mant_w |
|
) |
| |
Returns the FP term representing -Inf of the given format.
- Parameters
-
e | The environment of the definition |
exp_w | The desired exponent width |
mant_w | The desired mantissa width |
- Returns
- A term representing -Inf, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_nan()
msat_term msat_make_fp_nan |
( |
msat_env |
e, |
|
|
size_t |
exp_w, |
|
|
size_t |
mant_w |
|
) |
| |
Returns the FP term representing NaN of the given format.
- Parameters
-
e | The environment of the definition |
exp_w | The desired exponent width |
mant_w | The desired mantissa width |
- Returns
- A term representing NaN, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_neg()
msat_term msat_make_fp_neg |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Returns a term representing the FP negation of t.
- Parameters
-
e | The environment of the definition |
t | The argument to negate. |
- Returns
- The term (fpneg t), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_plus()
msat_term msat_make_fp_plus |
( |
msat_env |
e, |
|
|
msat_term |
rounding, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the FP addition of t1 and t2, according to the given rounding mode.
- Parameters
-
e | The environment of the definition |
rounding | The desired rounding mode. |
t1 | The first argument. |
t2 | The second argument. |
- Returns
- The term (+ rounding t1 t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_plus_inf()
msat_term msat_make_fp_plus_inf |
( |
msat_env |
e, |
|
|
size_t |
exp_w, |
|
|
size_t |
mant_w |
|
) |
| |
Returns the FP term representing +Inf of the given format.
- Parameters
-
e | The environment of the definition |
exp_w | The desired exponent width |
mant_w | The desired mantissa width |
- Returns
- A term representing +Inf, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_rat_number()
msat_term msat_make_fp_rat_number |
( |
msat_env |
e, |
|
|
const char * |
num_rep, |
|
|
size_t |
exp_w, |
|
|
size_t |
mant_w, |
|
|
msat_term |
rounding |
|
) |
| |
Creates an FP number from a rational number.
- Parameters
-
e | The environment of the definition |
num_rep | A string representation for the rational number |
exp_w | The desired exponent width |
mant_w | The desired mantissa width |
rounding | The desired rounding mode. |
- Returns
- The numeric term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_round_to_int()
msat_term msat_make_fp_round_to_int |
( |
msat_env |
e, |
|
|
msat_term |
rounding, |
|
|
msat_term |
t |
|
) |
| |
Returns a term representing the FP round to integral of t, according to the given rounding mode.
- Parameters
-
e | The environment of the definition |
rounding | The desired rounding mode. |
t | The argument. |
- Returns
- The term (fp.roundToIntegral rounding t), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_roundingmode_minus_inf()
msat_term msat_make_fp_roundingmode_minus_inf |
( |
msat_env |
e | ) |
|
Returns a term representing the FP rounding mode ROUND_TO_MINUS_INF.
- Parameters
-
e | The environment of the definition |
- Returns
- The term ROUND_TO_MINUS_INF, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_roundingmode_nearest_even()
msat_term msat_make_fp_roundingmode_nearest_even |
( |
msat_env |
e | ) |
|
Returns a term representing the FP rounding mode ROUND_TO_NEAREST_EVEN.
- Parameters
-
e | The environment of the definition |
- Returns
- The term ROUND_TO_NEAREST_EVEN, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_roundingmode_plus_inf()
msat_term msat_make_fp_roundingmode_plus_inf |
( |
msat_env |
e | ) |
|
Returns a term representing the FP rounding mode ROUND_TO_PLUS_INF.
- Parameters
-
e | The environment of the definition |
- Returns
- The term ROUND_TO_PLUS_INF, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_roundingmode_zero()
msat_term msat_make_fp_roundingmode_zero |
( |
msat_env |
e | ) |
|
Returns a term representing the FP rounding mode ROUND_TO_ZERO.
- Parameters
-
e | The environment of the definition |
- Returns
- The term ROUND_TO_ZERO, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_sqrt()
msat_term msat_make_fp_sqrt |
( |
msat_env |
e, |
|
|
msat_term |
rounding, |
|
|
msat_term |
t |
|
) |
| |
Returns a term representing the FP square root of t, according to the given rounding mode.
- Parameters
-
e | The environment of the definition |
rounding | The desired rounding mode. |
t | The sqrt argument. |
- Returns
- The term (sqrt rounding t), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_times()
msat_term msat_make_fp_times |
( |
msat_env |
e, |
|
|
msat_term |
rounding, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the FP multiplication of t1 and t2, according to the given rounding mode.
- Parameters
-
e | The environment of the definition |
rounding | The desired rounding mode. |
t1 | The first argument. |
t2 | The second argument. |
- Returns
- The term (* rounding t1 t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_to_sbv()
msat_term msat_make_fp_to_sbv |
( |
msat_env |
e, |
|
|
size_t |
width, |
|
|
msat_term |
rounding, |
|
|
msat_term |
t |
|
) |
| |
Returns a term representing the conversion of a FP term to a signed bit-vector.
- Parameters
-
e | The environment of the definition |
width | The target bit-vector width. |
rounding | The desired rounding mode. |
t | The argument to convert. |
- Returns
- The term representing the conversion, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_fp_to_ubv()
msat_term msat_make_fp_to_ubv |
( |
msat_env |
e, |
|
|
size_t |
width, |
|
|
msat_term |
rounding, |
|
|
msat_term |
t |
|
) |
| |
Returns a term representing the conversion of a FP term to an unsigned bit-vector.
- Parameters
-
e | The environment of the definition |
width | The target bit-vector width. |
rounding | The desired rounding mode. |
t | The argument to convert. |
- Returns
- The term representing the conversion, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_iff()
msat_term msat_make_iff |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the equivalence of t1 and t2.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. Must have type ::MSAT_BOOL. |
t2 | The second argument. Must have type ::MSAT_BOOL. |
- Returns
- The term t1 <-> t2, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_int_from_sbv()
msat_term msat_make_int_from_sbv |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Returns a term representing the conversion of a signed bit-vector to an int.
- Parameters
-
e | The environment of the definition |
t | The argument to convert. |
- Returns
- The term representing the conversion, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_int_from_ubv()
msat_term msat_make_int_from_ubv |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Returns a term representing the conversion of an unsigned bit-vector to an int.
- Parameters
-
e | The environment of the definition |
t | The argument to convert. |
- Returns
- The term representing the conversion, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_int_modular_congruence()
msat_term msat_make_int_modular_congruence |
( |
msat_env |
e, |
|
|
mpz_t |
modulus, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns an expression representing (t1 = t2 mod modulus).
- Parameters
-
e | The environment of the definition |
modulus | The value of the modulus. Must be > 0 |
t1 | The first argument. |
t2 | The second argument. |
- Returns
- The created term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_int_number()
msat_term msat_make_int_number |
( |
msat_env |
e, |
|
|
int |
value |
|
) |
| |
Returns an expression representing an integer or rational number.
- Parameters
-
e | The environment of the definition |
value | The value for the number |
- Returns
- The numeric term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_int_to_bv()
msat_term msat_make_int_to_bv |
( |
msat_env |
e, |
|
|
size_t |
width, |
|
|
msat_term |
t |
|
) |
| |
Returns a term representing the conversion of an int to a bit-vector.
- Parameters
-
e | The environment of the definition |
width | The target bit-vector width. |
t | The argument to convert. |
- Returns
- The term representing the conversion, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_leq()
msat_term msat_make_leq |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns an atom representing (t1 <= t2).
The arguments must have the same type. The exception is for integer numbers, which can be casted to rational if necessary.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. Must be of type rational or integer |
t2 | The second argument. Must be of type rational or integer |
- Returns
- The term (t1 <= t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_log()
msat_term msat_make_log |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Returns an expression representing the natural log of t.
- Parameters
-
e | The environment of the definition |
t | The argument. |
- Returns
- The created term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_mpq_number()
msat_term msat_make_mpq_number |
( |
msat_env |
e, |
|
|
mpq_t |
value |
|
) |
| |
Returns an expression representing an integer or rational number.
- Parameters
-
e | The environment of the definition |
value | The value for the number |
- Returns
- The numeric term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_not()
msat_term msat_make_not |
( |
msat_env |
e, |
|
|
msat_term |
t1 |
|
) |
| |
Returns a term representing the logical negation of t1.
- Parameters
-
e | The environment of the definition |
t1 | The argument to negate. Must have type ::MSAT_BOOL. |
- Returns
- The term !t1, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_number()
msat_term msat_make_number |
( |
msat_env |
e, |
|
|
const char * |
num_rep |
|
) |
| |
Returns an expression representing an integer or rational number.
- Parameters
-
e | The environment of the definition |
num_rep | A string representation for the number |
- Returns
- The numeric term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_or()
msat_term msat_make_or |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns a term representing the logical OR of t1 and t2.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. Must have type ::MSAT_BOOL. |
t2 | The second argument. Must have type ::MSAT_BOOL. |
- Returns
- The term t1 | t2, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_pi()
msat_term msat_make_pi |
( |
msat_env |
e | ) |
|
Returns the constant representing the pi number.
- Parameters
-
e | The environment of the definition |
- Returns
- The created term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_plus()
msat_term msat_make_plus |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns an expression representing (t1 + t2).
The arguments must have the same type. The exception is for integer numbers, which can be casted to rational if necessary.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. Must be of type rational or integer |
t2 | The second argument. Must be of type rational or integer |
- Returns
- The term (t1 + t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_pow()
msat_term msat_make_pow |
( |
msat_env |
e, |
|
|
msat_term |
tb, |
|
|
msat_term |
te |
|
) |
| |
Returns an expression representing tb to the power of te.
- Parameters
-
e | The environment of the definition |
tb | The base of the power |
te | The exponent of the power |
- Returns
- The created term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_sin()
msat_term msat_make_sin |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Returns an expression representing sin(t)
- Parameters
-
e | The environment of the definition |
t | The argument. |
- Returns
- The created term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_term()
msat_term msat_make_term |
( |
msat_env |
e, |
|
|
msat_decl |
d, |
|
|
msat_term |
args[] |
|
) |
| |
Creates a term from a declaration and a list of arguments.
- Parameters
-
e | The environment in which to create the term |
d | The declaration |
args | The arguments |
- Precondition
- The length of args should be equal to the arity of d
- Returns
- The created term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_term_ite()
msat_term msat_make_term_ite |
( |
msat_env |
e, |
|
|
msat_term |
c, |
|
|
msat_term |
tt, |
|
|
msat_term |
te |
|
) |
| |
Returns an expression representing a term if-then-else construct.
The two arguments ::tt and ::te must have compatible types.
- Parameters
-
e | The environment of the definition |
c | The condition of the test. Must be of type ::MSAT_BOOL |
tt | The "then" branch |
te | The "else" branch |
- Returns
- The term representing the if-then-else, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_times()
msat_term msat_make_times |
( |
msat_env |
e, |
|
|
msat_term |
t1, |
|
|
msat_term |
t2 |
|
) |
| |
Returns an expression representing (t1 * t2).
The arguments must have the same type, with the usual exception for integer numbers.
- Parameters
-
e | The environment of the definition |
t1 | The first argument. Must be of type rational or integer |
t2 | The second argument. Must be of type rational or integer |
- Returns
- The term (t1 * t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_true()
msat_term msat_make_true |
( |
msat_env |
e | ) |
|
Returns a term representing logical truth.
- Parameters
-
e | The environment of the definition |
- Returns
- The term TRUE, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_uf()
msat_term msat_make_uf |
( |
msat_env |
e, |
|
|
msat_decl |
func, |
|
|
msat_term |
args[] |
|
) |
| |
Creates an uninterpreted function application.
The number and type of the arguments must match those of the declaration.
- Parameters
-
e | The environment of the definition |
func | The declaration of the function |
args | The actual parameters |
- Returns
- The term representing the function/predicate call, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_make_variable()
msat_term msat_make_variable |
( |
msat_env |
e, |
|
|
const char * |
name, |
|
|
msat_type |
type |
|
) |
| |
Returns a term representing a variable, which can be used for existential or universal quantification.
- Parameters
-
e | The environment of the definition |
name | The name of the variable. |
type | The type of the variable. |
- Returns
- The term for the variable, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
◆ msat_model_create_iterator()
msat_model_iterator msat_model_create_iterator |
( |
msat_model |
m | ) |
|
◆ msat_model_eval()
msat_term msat_model_eval |
( |
msat_model |
m, |
|
|
msat_term |
t |
|
) |
| |
Evaluates the input term in the given model.
- Parameters
-
m | The model used for the evaluation. |
t | The term to evaluate. |
- Returns
- the value for t in m. Use MSAT_ERROR_TERM() to check for errors.
◆ msat_model_iterator_has_next()
int msat_model_iterator_has_next |
( |
msat_model_iterator |
i | ) |
|
Checks whether i can be incremented.
- Parameters
-
- Returns
- nonzero if i can be incremented, zero otherwise
◆ msat_model_iterator_next()
int msat_model_iterator_next |
( |
msat_model_iterator |
i, |
|
|
msat_term * |
t, |
|
|
msat_term * |
v |
|
) |
| |
Returns the next (term, value) pair in the model, and increments the given iterator.
- Parameters
-
i | The model iterator to increment. |
t | Output value for the next variable/function call in the model. |
v | Output value for the next value in the model. |
- Returns
- nonzero in case of error.
◆ msat_named_list_from_smtlib2()
int msat_named_list_from_smtlib2 |
( |
msat_env |
e, |
|
|
const char * |
data, |
|
|
size_t * |
out_n, |
|
|
char *** |
out_names, |
|
|
msat_term ** |
out_terms |
|
) |
| |
Parses a list of named terms from a string in SMT-LIB v2 format.
Given a string in SMT-LIB v2 format, collect and return all the terms with a :named annotation.
- Parameters
-
e | Then environment in which terms are created |
data | The input string in SMT-LIBv2 format |
out_n | On success, the number of named terms is stored here. Must not be NULL. |
out_names | On success, the names of the parsed terms are stored here. Must not be NULL. Both the array and its elements are dynamically allocated, and must be deallocated by the user with msat_free() |
out_terms | On success, the parsed named terms are stored here. Must not be NULL. The array is dynamically allocated, and must be deallocated by the user with msat_free() |
- Returns
- zero on success, nonzero on error.
◆ msat_named_list_from_smtlib2_file()
int msat_named_list_from_smtlib2_file |
( |
msat_env |
e, |
|
|
FILE * |
f, |
|
|
size_t * |
out_n, |
|
|
char *** |
out_names, |
|
|
msat_term ** |
out_terms |
|
) |
| |
Like msat_named_list_from_smtlib2(), but reads from a file instead of a string.
Given a FILE in SMT-LIB v2 format, collect and return all the terms with a :named annotation.
- Parameters
-
e | Then environment in which terms are created |
f | The input file in SMT-LIBv2 format |
out_n | On success, the number of named terms is stored here. Must not be NULL. |
out_names | On success, the names of the parsed terms are stored here. Must not be NULL. Both the array and its elements are dynamically allocated, and must be deallocated by the user with msat_free() |
out_terms | On success, the parsed named terms are stored here. Must not be NULL. The array is dynamically allocated, and must be deallocated by the user with msat_free() |
- Returns
- zero on success, nonzero on error.
◆ msat_named_list_to_smtlib2()
char* msat_named_list_to_smtlib2 |
( |
msat_env |
e, |
|
|
size_t |
n, |
|
|
const char ** |
names, |
|
|
msat_term * |
terms |
|
) |
| |
Converts the given list of named terms to SMT-LIB v2 format.
- Parameters
-
e | The environment in which the terms are defined |
n | The number of terms/names to dump |
names | An array of names for the terms |
terms | The terms to convert |
- Returns
- a string in SMT-LIB v2 format storing all the named input terms, or NULL in case of errors. If not NULL, the returned string must be deallocated by the user with msat_free().
◆ msat_named_list_to_smtlib2_file()
int msat_named_list_to_smtlib2_file |
( |
msat_env |
e, |
|
|
size_t |
n, |
|
|
const char ** |
names, |
|
|
msat_term * |
terms, |
|
|
FILE * |
out |
|
) |
| |
Dumps the given list of named terms in SMT-LIB v2 format to the given output file.
- Parameters
-
e | The environment in which the terms are defined |
n | The number of terms/names to dump |
names | An array of names for the terms |
terms | The terms to convert |
out | The output file |
- Returns
- zero on success, nonzero on error.
◆ msat_num_backtrack_points()
size_t msat_num_backtrack_points |
( |
msat_env |
e | ) |
|
returns the number of backtrack points in the given environment
◆ msat_parse_config()
msat_config msat_parse_config |
( |
const char * |
data | ) |
|
Creates a new MathSAT configuration by parsing the given data.
The format for the configuration data is simply one "key = value" entry per line. The data may include comments, prefixed by the # character (and extending until the end of the line).
- Parameters
-
data | The configuration data to parse |
- Returns
- A new configuration. In case of errors, a cfg s.t. MSAT_ERROR_CONFIG(cfg) is true is returned
◆ msat_parse_config_file()
msat_config msat_parse_config_file |
( |
FILE * |
f | ) |
|
Creates a new MathSAT configuration by parsing the given file.
See msat_parse_config for the format of the config file.
- Parameters
-
f | The configuration file to parse |
- Returns
- A new configuration. In case of errors, a cfg s.t. MSAT_ERROR_CONFIG(cfg) is true is returned
◆ msat_pop_backtrack_point()
int msat_pop_backtrack_point |
( |
msat_env |
e | ) |
|
Backtracks to the last checkpoint set in the environment e.
- Parameters
-
e | The environment in which to operate |
- Returns
- zero on success, nonzero on error
◆ msat_proof_get_arity()
size_t msat_proof_get_arity |
( |
msat_proof |
p | ) |
|
Retrieves the number of children of a non-term proof.
- Parameters
-
- Returns
- The arity of the given proof.
◆ msat_proof_get_child()
msat_proof msat_proof_get_child |
( |
msat_proof |
p, |
|
|
size_t |
i |
|
) |
| |
Retrieves a sub-proof of a given proof.
- Parameters
-
p | A non-term proof. |
i | The index of the child proof to retrieve. |
- Returns
- a Child proof of the given proof.
◆ msat_proof_get_name()
const char* msat_proof_get_name |
( |
msat_proof |
p | ) |
|
Retrieves the name of a non-term proof.
- Parameters
-
- Returns
- The name of the given proof.
◆ msat_proof_get_term()
msat_term msat_proof_get_term |
( |
msat_proof |
p | ) |
|
Retrieves the term associated to a term proof.
- Parameters
-
p | The proof from which to get the term. Must be a term proof. |
- Returns
- The term associated with the input proof.
◆ msat_proof_id()
size_t msat_proof_id |
( |
msat_proof |
p | ) |
|
Returns a numeric identifier for p.
The returned value is guaranteed to be unique within the proof manager in which p was defined. Therefore, it can be used to test two proofs for equality, as well as a hash value.
- Parameters
-
- Returns
- a unique (within the defining manager) numeric identifier
◆ msat_proof_is_term()
int msat_proof_is_term |
( |
msat_proof |
p | ) |
|
Checks whether a proof object is a term.
- Parameters
-
- Returns
- nonzero if p is a term proof, zero otherwise.
◆ msat_push_backtrack_point()
int msat_push_backtrack_point |
( |
msat_env |
e | ) |
|
Pushes a checkpoint for backtracking in an environment.
- Parameters
-
e | The environment in which to operate |
- Returns
- zero on success, nonzero on error
◆ msat_reset_env()
int msat_reset_env |
( |
msat_env |
e | ) |
|
◆ msat_set_external_dpll_engine()
Sets an external dpll engine to be used by an environment.
- Parameters
-
env | The environment in which to operate. |
engine | The engine to use |
- Returns
- zero on success, nonzero on error
◆ msat_set_itp_group()
int msat_set_itp_group |
( |
msat_env |
e, |
|
|
int |
group |
|
) |
| |
Sets the current interpolation group.
All the formulas asserted after this call (with msat_assert_formula) will belong to group.
- Parameters
-
e | The environment in which to operate. |
group | The group. Must have been previously created with msat_create_itp_group. |
- Returns
- zero on success, nonzero on error.
◆ msat_set_option()
int msat_set_option |
( |
msat_config |
cfg, |
|
|
const char * |
option, |
|
|
const char * |
value |
|
) |
| |
Sets an option in the given configuration.
Notice that the best thing to do is set options right after having created a configuration, before creating an environment with it. The library tries to capture and report errors, but it does not always succeed.
- Parameters
-
cfg | The configuration in which to operate. |
option | The name of the option to set. |
value | The value for the option. For boolean options, use "true" or "false" (case matters). For flags, the value can be anything. |
- Returns
- zero on success, nonzero on error.
◆ msat_set_termination_test()
Installs a custom termination test in the given environment.
The func function will be polled periodically by env, terminating the current search as soon as func returns non-zero.
- Parameters
-
env | The environment in which to operate. |
func | The user-defined termination criterion. If it is NULL, no termination criterion will be used. |
user_data | Generic data pointer which will be passed to func. Can be anything, its value will not be interpreted. |
- Returns
- zero on success, nonzero on error
◆ msat_simplify()
msat_term msat_simplify |
( |
msat_env |
e, |
|
|
msat_term |
formula, |
|
|
msat_term * |
to_protect, |
|
|
size_t |
num_to_protect |
|
) |
| |
Simplify the input formula by performing variable elimination with toplevel equalities.
Apply rewriting and "toplevel propagation", i.e. inlining of toplevel equalities, until a fixpoint is reached. The constants occurring in to_protect will not be eliminated. If to_protect is NULL, only rewriting is performed.
- Parameters
-
e | The environment in which to operate. |
formula | The formula to simplify. |
to_protect | The constants that should never be eliminated. |
num_to_protect | The size of the to_protect array. |
- Returns
- The simplified formula, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors
◆ msat_solve()
Checks the satiafiability of the given environment.
Checks the satisfiability of the conjunction of all the formulas asserted in e (see msat_assert_formula). Before calling this function, the right theory solvers must have been enabled (see ::msat_add_theory).
- Parameters
-
e | The environment to check. |
- Returns
- MSAT_SAT if the problem is satisfiable, MSAT_UNSAT if it is unsatisfiable, and MSAT_UNKNOWN if there was some error or if the satisfiability can't be determined.
◆ msat_solve_diversify()
Enumerates diverse models over the asserted stack.
Can only be called when model generation is on and proof generation is off.
Notice that this function changes the asserted formula in order to generate the diverse models, by adding clauses based on the diversifiers. When used in incremental mode a backtrack point should be pushed before calling this function, and popped after this call has completed. Not doing this changes the satisfiability of the formula.
- Parameters
-
e | The environment to use |
diversifiers | the terms over which to diversify. On each succesive model, at least one of these terms will have a different value. |
num_diversifiers | the size of the diversifiers array. |
func | The callback function to be notified about models found (see msat_solve_diversify_model_callback). Cannot be NULL. |
user_data | Generic data pointer which will be passed to func. Can be anything, its value will not be interpreted |
- Returns
- The number of models found, or -1 on error. (If the formula is unsat, 0 is returned).
◆ msat_solve_with_assumptions()
msat_result msat_solve_with_assumptions |
( |
msat_env |
e, |
|
|
msat_term * |
assumptions, |
|
|
size_t |
num_assumptions |
|
) |
| |
Checks the satiafiability of the given environment under the given assumptions.
Checks the satisfiability of the conjunction of all the formulas asserted in e (see msat_assert_formula), plus the conjunction of the given assumptions, which can only be (negated) Boolean constants. If MSAT_UNSAT is returned, the function msat_get_unsat_assumptions() can be used to retrieve the list of assumptions responsible for the inconsistency.
- Parameters
-
e | The environment to check. |
assumptions | The list of assumptions. Can only be (negated) Boolean constants |
num_assumptions | The number of assumptions. |
- Returns
- MSAT_SAT if the problem is satisfiable, MSAT_UNSAT if it is unsatisfiable, and MSAT_UNKNOWN if there was some error or if the satisfiability can't be determined.
◆ msat_term_arity()
size_t msat_term_arity |
( |
msat_term |
t | ) |
|
Returns the arity of t.
- Parameters
-
- Returns
- The number of arguments of t
◆ msat_term_get_arg()
msat_term msat_term_get_arg |
( |
msat_term |
t, |
|
|
size_t |
n |
|
) |
| |
Returns the nth argument of t.
- Parameters
-
t | A term. |
n | The index of the argument. Must be lower than the arity of t |
- Returns
- The nth argument of arguments of t
◆ msat_term_get_decl()
msat_decl msat_term_get_decl |
( |
msat_term |
t | ) |
|
Returns the declaration associated to t (if any)
If t is not a constant or a function application, the returned value ret will be s.t. MSAT_ERROR_DECL(ret) is true
- Parameters
-
t | The term for which to retrieve the declaration |
- Returns
- If t is a constant, its declaration is returned; if it is an uif, the declaration of the function is returned; otherwise, a ret s.t. MSAT_ERROR_DECL(ret) is true is returned
◆ msat_term_get_type()
msat_type msat_term_get_type |
( |
msat_term |
t | ) |
|
Returns the type of t.
- Parameters
-
- Returns
- The type of t
◆ msat_term_id()
size_t msat_term_id |
( |
msat_term |
t | ) |
|
Returns a numeric identifier for t.
The returned value is guaranteed to be unique within the environment in which t was defined. Therefore, it can be used to test two terms for equality, as well as a hash value.
- Parameters
-
- Returns
- a unique (within the defining env) numeric identifier
◆ msat_term_is_and()
int msat_term_is_and |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is an AND.
- Parameters
-
- Returns
- nonzero if t is an AND
◆ msat_term_is_array_const()
int msat_term_is_array_const |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a constant array.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a constant array
◆ msat_term_is_array_read()
int msat_term_is_array_read |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is an array read.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is an array read
◆ msat_term_is_array_write()
int msat_term_is_array_write |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is an array write.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is an array write
◆ msat_term_is_asin()
int msat_term_is_asin |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a (asin t1) expression.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a asin expression
◆ msat_term_is_atom()
int msat_term_is_atom |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is an atom.
- Parameters
-
- Returns
- nonzero if t is an atom, i.e. either a boolean constant or a relation between terms
◆ msat_term_is_boolean_constant()
int msat_term_is_boolean_constant |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a boolean constant.
- Parameters
-
- Returns
- nonzero if t is a constant of type ::MSAT_BOOL
◆ msat_term_is_bv_and()
int msat_term_is_bv_and |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a bit-wise and.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a bit-wise and
◆ msat_term_is_bv_ashr()
int msat_term_is_bv_ashr |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is an arithmetic shift right.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is an arithmetic shift right
◆ msat_term_is_bv_comp()
int msat_term_is_bv_comp |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a BV comparison.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a BV comparison
◆ msat_term_is_bv_concat()
int msat_term_is_bv_concat |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a BV concatenation.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a concatenation
◆ msat_term_is_bv_extract()
int msat_term_is_bv_extract |
( |
msat_env |
e, |
|
|
msat_term |
t, |
|
|
size_t * |
out_msb, |
|
|
size_t * |
out_lsb |
|
) |
| |
Checks whether t is a BV extraction.
- Parameters
-
e | The environment in which to operate |
t | A term. |
out_msb | If not NULL, the msb of the selection will be stored here |
out_lsb | If not NULL, the lsb of the selection will be stored here |
- Returns
- nonzero if t is an extraction
◆ msat_term_is_bv_lshl()
int msat_term_is_bv_lshl |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a logical shift left.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a logical shift left
◆ msat_term_is_bv_lshr()
int msat_term_is_bv_lshr |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a logical shift right.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a logical shift right
◆ msat_term_is_bv_minus()
int msat_term_is_bv_minus |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a bit-vector subtraction.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a bit-vector subtraction
◆ msat_term_is_bv_neg()
int msat_term_is_bv_neg |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a bit-vector unary negation.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a bit-vector unary negation
◆ msat_term_is_bv_not()
int msat_term_is_bv_not |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a bit-wise not.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a bit-wise not
◆ msat_term_is_bv_or()
int msat_term_is_bv_or |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a bit-wise or.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a bit-wise or
◆ msat_term_is_bv_plus()
int msat_term_is_bv_plus |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a bit-vector addition.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a bit-vector addition
◆ msat_term_is_bv_rol()
int msat_term_is_bv_rol |
( |
msat_env |
e, |
|
|
msat_term |
t, |
|
|
size_t * |
out_amount |
|
) |
| |
Checks whether t is a rotate left.
- Parameters
-
e | The environment in which to operate |
t | A term. |
out_amount | If not NULL, the amount of the left rotation will be stored here |
- Returns
- nonzero if t is a rotate left
◆ msat_term_is_bv_ror()
int msat_term_is_bv_ror |
( |
msat_env |
e, |
|
|
msat_term |
t, |
|
|
size_t * |
out_amount |
|
) |
| |
Checks whether t is a rotate right.
- Parameters
-
e | The environment in which to operate |
t | A term. |
out_amount | If not NULL, the amount of the right rotation will be stored here |
- Returns
- nonzero if t is a rotate right
◆ msat_term_is_bv_sdiv()
int msat_term_is_bv_sdiv |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a bit-vector signed division.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a bit-vector signed division
◆ msat_term_is_bv_sext()
int msat_term_is_bv_sext |
( |
msat_env |
e, |
|
|
msat_term |
t, |
|
|
size_t * |
out_amount |
|
) |
| |
Checks whether t is a sign extension.
- Parameters
-
e | The environment in which to operate |
t | A term. |
out_amount | If not NULL, the amount of the sign extension will be stored here |
- Returns
- nonzero if t is a sign extension
◆ msat_term_is_bv_sleq()
int msat_term_is_bv_sleq |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a bit-vector signed leq.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a bit-vector signed leq
◆ msat_term_is_bv_slt()
int msat_term_is_bv_slt |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a bit-vector signed lt.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a bit-vector signed lt
◆ msat_term_is_bv_srem()
int msat_term_is_bv_srem |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a bit-vector signed remainder.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a bit-vector signed remainder
◆ msat_term_is_bv_times()
int msat_term_is_bv_times |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a bit-vector multiplication.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a bit-vector multiplication
◆ msat_term_is_bv_udiv()
int msat_term_is_bv_udiv |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a bit-vector unsigned division.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a bit-vector unsigned division
◆ msat_term_is_bv_uleq()
int msat_term_is_bv_uleq |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a bit-vector unsigned leq.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a bit-vector unsigned leq
◆ msat_term_is_bv_ult()
int msat_term_is_bv_ult |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a bit-vector unsigned lt.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a bit-vector unsigned lt
◆ msat_term_is_bv_urem()
int msat_term_is_bv_urem |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a bit-vector unsigned remainder.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a bit-vector unsigned remainder
◆ msat_term_is_bv_xor()
int msat_term_is_bv_xor |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a bit-wise xor.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a bit-wise xor
◆ msat_term_is_bv_zext()
int msat_term_is_bv_zext |
( |
msat_env |
e, |
|
|
msat_term |
t, |
|
|
size_t * |
out_amount |
|
) |
| |
Checks whether t is a zero extension.
- Parameters
-
e | The environment in which to operate |
t | A term. |
out_amount | If not NULL, the amount of the zero extension will be stored here |
- Returns
- nonzero if t is a zero extension
◆ msat_term_is_constant()
int msat_term_is_constant |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a constant.
- Parameters
-
- Returns
- nonzero if t is a constant
◆ msat_term_is_divide()
int msat_term_is_divide |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a (t1 / t2) expression.
- Parameters
-
- Returns
- nonzero if t is a (t1 / t2) expression
◆ msat_term_is_enum_value()
int msat_term_is_enum_value |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a value for an enum type.
- Parameters
-
- Returns
- nonzero if t is an enum value
◆ msat_term_is_equal()
int msat_term_is_equal |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is an equality.
- Parameters
-
- Returns
- nonzero if t is an equality atom
◆ msat_term_is_exists()
int msat_term_is_exists |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is an existential quantifier.
- Parameters
-
- Returns
- nonzero if t is an existential quantifier
◆ msat_term_is_exp()
int msat_term_is_exp |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a (exp t1) expression.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a exp expression
◆ msat_term_is_false()
int msat_term_is_false |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is the FALSE term.
- Parameters
-
- Returns
- nonzero if t is FALSE
◆ msat_term_is_floor()
int msat_term_is_floor |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a (floor t1) expression.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a floor expression
◆ msat_term_is_forall()
int msat_term_is_forall |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a universal quantifier.
- Parameters
-
- Returns
- nonzero if t is a universal quantifier
◆ msat_term_is_fp_abs()
int msat_term_is_fp_abs |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP abs.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP abs
◆ msat_term_is_fp_as_ieeebv()
int msat_term_is_fp_as_ieeebv |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP as BV conversion.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP as BV conversion
◆ msat_term_is_fp_cast()
int msat_term_is_fp_cast |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP cast.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP cast
◆ msat_term_is_fp_div()
int msat_term_is_fp_div |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP div.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP div
◆ msat_term_is_fp_equal()
int msat_term_is_fp_equal |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP equality.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP equality
◆ msat_term_is_fp_from_ieeebv()
int msat_term_is_fp_from_ieeebv |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP from IEEE BV conversion.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP from unsigned BV conversion
◆ msat_term_is_fp_from_sbv()
int msat_term_is_fp_from_sbv |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP from signed BV conversion.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP from signed BV conversion
◆ msat_term_is_fp_from_ubv()
int msat_term_is_fp_from_ubv |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP from unsigned BV conversion.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP from unsigned BV conversion
◆ msat_term_is_fp_isinf()
int msat_term_is_fp_isinf |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP isinf predicate.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP isinf predicate
◆ msat_term_is_fp_isnan()
int msat_term_is_fp_isnan |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP isnan predicate.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP isnan predicate
◆ msat_term_is_fp_isneg()
int msat_term_is_fp_isneg |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP isneg predicate.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP isneg predicate
◆ msat_term_is_fp_isnormal()
int msat_term_is_fp_isnormal |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP isnormal predicate.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP isnormal predicate
◆ msat_term_is_fp_ispos()
int msat_term_is_fp_ispos |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP ispos predicate.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP ispos predicate
◆ msat_term_is_fp_issubnormal()
int msat_term_is_fp_issubnormal |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP issubnormal predicate.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP iszero predicate
◆ msat_term_is_fp_iszero()
int msat_term_is_fp_iszero |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP iszero predicate.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP iszero predicate
◆ msat_term_is_fp_leq()
int msat_term_is_fp_leq |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP <=.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP <=
◆ msat_term_is_fp_lt()
int msat_term_is_fp_lt |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP less than.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP less than
◆ msat_term_is_fp_max()
int msat_term_is_fp_max |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP max.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP max
◆ msat_term_is_fp_min()
int msat_term_is_fp_min |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP min.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP min
◆ msat_term_is_fp_minus()
int msat_term_is_fp_minus |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP minus.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP minus
◆ msat_term_is_fp_neg()
int msat_term_is_fp_neg |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP negation.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP negation
◆ msat_term_is_fp_plus()
int msat_term_is_fp_plus |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP plus.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP plus
◆ msat_term_is_fp_round_to_int()
int msat_term_is_fp_round_to_int |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP round to integer.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP round to integer
◆ msat_term_is_fp_roundingmode_minus_inf()
int msat_term_is_fp_roundingmode_minus_inf |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is the ROUND_TO_MINUS_INF FP rounding mode constant.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is ROUND_TO_MINUS_INF
◆ msat_term_is_fp_roundingmode_nearest_even()
int msat_term_is_fp_roundingmode_nearest_even |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is the ROUND_TO_NEAREST_EVEN FP rounding mode constant.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is ROUND_TO_NEAREST_EVEN
◆ msat_term_is_fp_roundingmode_plus_inf()
int msat_term_is_fp_roundingmode_plus_inf |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is the ROUND_TO_PLUS_INF FP rounding mode constant.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is ROUND_TO_PLUS_INF
◆ msat_term_is_fp_roundingmode_zero()
int msat_term_is_fp_roundingmode_zero |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is the ROUND_TO_ZERO FP rounding mode constant.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is ROUND_TO_ZERO
◆ msat_term_is_fp_sqrt()
int msat_term_is_fp_sqrt |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP sqrt.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP sqrt
◆ msat_term_is_fp_times()
int msat_term_is_fp_times |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP times.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP times
◆ msat_term_is_fp_to_sbv()
int msat_term_is_fp_to_sbv |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP to signed BV conversion.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP to BV conversion
◆ msat_term_is_fp_to_ubv()
int msat_term_is_fp_to_ubv |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a FP to unsigned BV conversion.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a FP to BV conversion
◆ msat_term_is_iff()
int msat_term_is_iff |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is an equivalence between boolean terms.
- Parameters
-
- Returns
- nonzero if t is an IFF
◆ msat_term_is_int_from_sbv()
int msat_term_is_int_from_sbv |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a signed BV to int conversion.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a signed BV to int conversion
◆ msat_term_is_int_from_ubv()
int msat_term_is_int_from_ubv |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is an unsigned BV to int conversion.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is an unsigned BV to int conversion
◆ msat_term_is_int_modular_congruence()
int msat_term_is_int_modular_congruence |
( |
msat_env |
e, |
|
|
msat_term |
t, |
|
|
mpz_t |
out_mod |
|
) |
| |
Checks whether t is an integer modular congruence expression. If so, stores in out_mod the value of the modulus as a GMP bigint.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is an integer modular congruence
◆ msat_term_is_int_to_bv()
int msat_term_is_int_to_bv |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a int to BV conversion.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a int to BV conversion
◆ msat_term_is_leq()
int msat_term_is_leq |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a (t1 <= t2) atom.
- Parameters
-
- Returns
- nonzero if t is a (t1 <= t2) atom
◆ msat_term_is_log()
int msat_term_is_log |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a (log t1) expression.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a log expression
◆ msat_term_is_not()
int msat_term_is_not |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a NOT.
- Parameters
-
- Returns
- nonzero if t is a NOT
◆ msat_term_is_number()
int msat_term_is_number |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a number.
- Parameters
-
- Returns
- nonzero if t is a number
◆ msat_term_is_or()
int msat_term_is_or |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is an OR.
- Parameters
-
- Returns
- nonzero if t is an OR
◆ msat_term_is_pi()
int msat_term_is_pi |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a the pi constant.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is the pi constant
◆ msat_term_is_plus()
int msat_term_is_plus |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a (t1 + t2) expression.
- Parameters
-
- Returns
- nonzero if t is a (t1 + t2) expression
◆ msat_term_is_pow()
int msat_term_is_pow |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a (pow t1 t2) expression.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a pow expression
◆ msat_term_is_quantifier()
int msat_term_is_quantifier |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a quantifier.
- Parameters
-
- Returns
- nonzero if t is a quantifier
◆ msat_term_is_sin()
int msat_term_is_sin |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a (sin t1) expression.
- Parameters
-
e | The environment in which to operate |
t | A term. |
- Returns
- nonzero if t is a sin expression
◆ msat_term_is_term_ite()
int msat_term_is_term_ite |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a term if-then-else.
- Parameters
-
- Returns
- nonzero if t is a term if-then-else
◆ msat_term_is_times()
int msat_term_is_times |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a (t1 * t2) expression.
- Parameters
-
- Returns
- nonzero if t is a (t1 * t2) expression
◆ msat_term_is_true()
int msat_term_is_true |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is the TRUE term.
- Parameters
-
- Returns
- nonzero if t is TRUE
◆ msat_term_is_uf()
int msat_term_is_uf |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is an uninterpreted function application.
- Parameters
-
- Returns
- nonzero if t is a uf application
◆ msat_term_is_variable()
int msat_term_is_variable |
( |
msat_env |
e, |
|
|
msat_term |
t |
|
) |
| |
Checks whether t is a (free or bound) variable.
- Parameters
-
- Returns
- nonzero if t is a variable
◆ msat_term_repr()
char* msat_term_repr |
( |
msat_term |
t | ) |
|
Returns an internal string representation of a term.
The returned string can be useful for debugging purposes only, as it is an internal representation of a term
- Parameters
-
- Returns
- a string reprsentation of t, or NULL in case of errors. The string must be dellocated by the caller with msat_free().
◆ msat_term_to_number()
int msat_term_to_number |
( |
msat_env |
e, |
|
|
msat_term |
t, |
|
|
mpq_t |
out |
|
) |
| |
converts the given term to an mpq_t rational number
The term must be a number, otherwise an error is reported.
- Parameters
-
e | the environment in which to operate |
t | the number to convert |
out | the result of the conversion. Before calling this function, out should be initialized with a call to mpq_init() |
- Returns
- zero on success, nonzero on error
◆ msat_to_smtlib1()
char* msat_to_smtlib1 |
( |
msat_env |
e, |
|
|
msat_term |
term |
|
) |
| |
Converts the given term to SMT-LIB v1 format.
- Parameters
-
e | The environment in which term is defined |
term | The term to convert |
- Returns
- a string in SMT-LIB v1 format for the formula represented by term, or NULL in case of errors. If not NULL, the returned string must be deallocated by the user with msat_free().
◆ msat_to_smtlib1_file()
int msat_to_smtlib1_file |
( |
msat_env |
e, |
|
|
msat_term |
term, |
|
|
FILE * |
out |
|
) |
| |
Dumps the given term in SMT-LIB v1 format to the given output file.
- Parameters
-
e | The environment in which term is defined |
term | The term to convert |
out | The output file |
- Returns
- zero on success, nonzero on error.
◆ msat_to_smtlib2()
char* msat_to_smtlib2 |
( |
msat_env |
e, |
|
|
msat_term |
term |
|
) |
| |
Converts the given term to SMT-LIB v2 format.
- Parameters
-
e | The environment in which term is defined |
term | The term to convert |
- Returns
- a string in SMT-LIB v2 format for the formula represented by term, or NULL in case of errors. If not NULL, the returned string must be deallocated by the user with msat_free().
◆ msat_to_smtlib2_ext()
char* msat_to_smtlib2_ext |
( |
msat_env |
e, |
|
|
msat_term |
term, |
|
|
const char * |
logic_name, |
|
|
int |
use_defines |
|
) |
| |
Converts the given term to SMT-LIB v2 format.
- Parameters
-
e | The environment in which term is defined |
term | The term to convert |
logic_name | Name of the SMT-LIBv2 logic for the output. Can be NULL |
use_defines | If nonzero, the output will contain define-funs instead of let bindings |
- Returns
- a string in SMT-LIB v2 format for the formula represented by term, or NULL in case of errors. If not NULL, the returned string must be deallocated by the user with msat_free().
◆ msat_to_smtlib2_ext_file()
int msat_to_smtlib2_ext_file |
( |
msat_env |
e, |
|
|
msat_term |
term, |
|
|
const char * |
logic_name, |
|
|
int |
use_defines, |
|
|
FILE * |
out |
|
) |
| |
Dumps the given term in SMT-LIB v2 format to the given output file.
- Parameters
-
e | The environment in which term is defined |
term | The term to convert |
logic_name | Name of the SMT-LIBv2 logic for the output. Can be NULL |
use_defines | If nonzero, the output will contain define-funs instead of let bindings |
out | The output file |
- Returns
- zero on success, nonzero on error.
◆ msat_to_smtlib2_file()
int msat_to_smtlib2_file |
( |
msat_env |
e, |
|
|
msat_term |
term, |
|
|
FILE * |
out |
|
) |
| |
Dumps the given term in SMT-LIB v2 format to the given output file.
- Parameters
-
e | The environment in which term is defined |
term | The term to convert |
out | The output file |
- Returns
- zero on success, nonzero on error.
◆ msat_to_smtlib2_term()
char* msat_to_smtlib2_term |
( |
msat_env |
e, |
|
|
msat_term |
term |
|
) |
| |
Prints a single term in SMT-LIB v2 format.
Contrary to msat_to_smtlib2(), this function does not print symbol declarations, and so it can be used to obtain a valid SMT-LIBv2 representation of the given term.
- Parameters
-
The | environment in which term is defined |
term | The term to print |
- Returns
- a string in SMT-LIB v2 format for the given term, or NULL in case of errors. If not NULL, the returned string must be deallocated by the user with msat_free().
◆ msat_type_equals()
int msat_type_equals |
( |
msat_type |
t1, |
|
|
msat_type |
t2 |
|
) |
| |
checks whether two types are the same
- Returns
- 1 if the types are the same, 0 otherwise
◆ msat_type_id()
size_t msat_type_id |
( |
msat_type |
t | ) |
|
Returns a numeric identifier for the input type.
The returned value is guaranteed to be unique within the environment in which t was defined. Therefore, it can be used to test two type for equality, as well as a hash value.
- Parameters
-
- Returns
- a unique (within the defining env) numeric identifier
◆ msat_type_repr()
char* msat_type_repr |
( |
msat_type |
t | ) |
|
Returns an internal string representation of a type.
The returned string can be useful for debugging purposes only, as it is an internal representation of a type
- Parameters
-
- Returns
- a string reprsentation of t, or NULL in case of errors. The string must be dellocated by the caller with msat_free().
◆ msat_visit_term()
visits the DAG of the given term t, calling the callback func for every suberm
- Parameters
-
e | The environment in which to operate |
t | The term to visit |
func | The callback function |
user_data | Generic data pointer which will be passed to func. Can be anything, its value will not be interpreted |
- Returns
- zero on success, nonzero on error
msat_ext_dpll_interface Struct Reference
Interface that external SAT solvers must implement.
More...
|
int(* | new_var )(void *self) |
| Creates a new variable in the SAT solver. More...
|
|
int(* | set_decision_var )(void *self, int var, int yes) |
| Marks a variable as a decision variable. More...
|
|
int(* | set_frozen )(void *self, int var, int yes) |
| Sets the frozen status of a variable. More...
|
|
int(* | add_clause )(void *self, int *clause, int permanent, int during_callback) |
| Adds a clause to the SAT solver. More...
|
|
msat_result(* | solve )(void *self, int *assumptions, int **out_conflicting_assumptions) |
| Checks the satisfiability (possibly under assumptions) of the list of added clauses. More...
|
|
msat_truth_value(* | model_value )(void *self, int lit) |
| Retrieves the model value for the given literal. More...
|
|
int(* | enqueue_assignment )(void *self, int lit) |
| Adds a (theory-deduced) literal to the current trail. More...
|
|
int(* | remove_clauses_containing )(void *self, int var) |
| Tells the solver to delete all the clauses containing the given variable. More...
|
|
int(* | reset )(void *self) |
| Completely resets the state of the solver. More...
|
|
int(* | set_callback )(void *self, msat_dpll_callback cb) |
| Associates to the solver a callback object for interacting with MathSAT. More...
|
|
◆ add_clause
int(* msat_ext_dpll_interface::add_clause) (void *self, int *clause, int permanent, int during_callback) |
Adds a clause to the SAT solver.
- Parameters
-
self | Pointer to the SAT solver. |
clause | array of literals in DIMACS format, terminated by 0. |
permanent | If nonzero, the clause is meant to be permanent. |
during_callback | If nonzero, the function is called by one of the msat_dpll_callback methods |
- Returns
- zero on success, nonzero on error
◆ enqueue_assignment
int(* msat_ext_dpll_interface::enqueue_assignment) (void *self, int lit) |
Adds a (theory-deduced) literal to the current trail.
- Parameters
-
self | Pointer to the SAT solver. |
lit | literal in DIMACS format. |
- Returns
- zero on success, nonzero on error.
◆ model_value
Retrieves the model value for the given literal.
- Parameters
-
self | Pointer to the SAT solver. |
lit | literal in DIMACS format. |
- Returns
- The truth value for the literal.
◆ new_var
int(* msat_ext_dpll_interface::new_var) (void *self) |
Creates a new variable in the SAT solver.
- Parameters
-
self | Pointer to the SAT solver. |
- Returns
- the DIMACS index of the new variable, or -1 in case of errors.
◆ remove_clauses_containing
int(* msat_ext_dpll_interface::remove_clauses_containing) (void *self, int var) |
Tells the solver to delete all the clauses containing the given variable.
- Parameters
-
self | Pointer to the SAT solver. |
var | variable in DIMACS format. |
- Returns
- zero on success, nonzero on error.
◆ reset
int(* msat_ext_dpll_interface::reset) (void *self) |
Completely resets the state of the solver.
- Parameters
-
self | Pointer to the SAT solver. |
- Returns
- zero on success, nonzero on error.
◆ set_callback
Associates to the solver a callback object for interacting with MathSAT.
- Parameters
-
- Returns
- zero on success, nonzero on error.
◆ set_decision_var
int(* msat_ext_dpll_interface::set_decision_var) (void *self, int var, int yes) |
Marks a variable as a decision variable.
- Parameters
-
self | Pointer to the SAT solver. |
var | the DIMACS index for the variable. |
yes | decision flag. |
- Returns
- zero on success, nonzero on error.
◆ set_frozen
int(* msat_ext_dpll_interface::set_frozen) (void *self, int var, int yes) |
Sets the frozen status of a variable.
- Parameters
-
self | Pointer to the SAT solver. |
var | the DIMACS index for the variable. |
yes | frozen flag. |
- Returns
- zero on success, nonzero on error.
◆ solve
msat_result(* msat_ext_dpll_interface::solve) (void *self, int *assumptions, int **out_conflicting_assumptions) |
Checks the satisfiability (possibly under assumptions) of the list of added clauses.
- Parameters
-
self | Pointer to the SAT solver. |
assumptions | array of literals in DIMACS format, terminated by 0. |
out_conflicting_assumptions | if the problem is unsatisfiable, this pointer should be set to a (zero-terminated) list of the assumptions responsible for the unsatisfiability. The solver should use its own internal storage for the array. |
- Returns
- MSAT_SAT if the problem is satisfiable, MSAT_UNSAT if it is unsat, or MSAT_UNKNOWN in case of errors.
|
Contents
Home
People
Documentation
Download
Publications
Links
|