MathSAT 5

ES FBK
UniTN
An SMT Solver for Formal Verification & More

MathSAT API Reference

API for the MathSAT SMT solver. More...

Data Structures

struct  msat_config
 MathSAT configuration.
 
struct  msat_env
 MathSAT environment.
 
struct  msat_term
 MathSAT term.
 
struct  msat_decl
 MathSAT declaration.
 
struct  msat_type
 MathSAT data 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.
 

Functions

Environment creation
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 data type for Booleans in the given env. More...
 
msat_type msat_get_rational_type (msat_env env)
 returns the data type for rationals in the given env. More...
 
msat_type msat_get_integer_type (msat_env env)
 returns the data type for integers in the given env. More...
 
msat_type msat_get_bv_type (msat_env env, size_t width)
 returns the data 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 data 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 data 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...
 
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_type_equals (msat_type t1, msat_type t2)
 checks whether two data types are the same More...
 
char * msat_type_repr (msat_type t)
 Returns an internal string representation of a type. More...
 
msat_decl msat_declare_function (msat_env e, const char *name, msat_type type)
 Declares a new uninterpreted function/constant. More...
 
Term creation
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_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_number (msat_env e, const char *num_rep)
 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_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_bv (msat_env e, size_t width, msat_term rounding, msat_term t)
 Returns a term representing the conversion of a FP term to 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_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...
 
Term access and navigation
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_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_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_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_bv (msat_env e, msat_term t)
 Checks whether t is a FP to 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_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...
 
Term parsing/printing
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...
 
Problem solving
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_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...
 
Interpolation
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...
 
Model Computation
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...
 
Unsat Core Computation
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...
 
External SAT Solver Interface
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...
 

Data types and special values

#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 data 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...
 
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_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_BV, 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
}
 
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_last_error_message (msat_env env)
 Retrieves the last error message generated while operating in the given enviroment. More...
 

Detailed Description

API for the MathSAT SMT solver.

Macro Definition Documentation

#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

#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

#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

#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

#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

#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

#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

#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

#define MSAT_ERROR_TYPE (   tp)    ((tp).repr == NULL)

Error checking for data types.

Use this macro to check whether returned values of type msat_type are valid

#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.

Typedef Documentation

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

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)

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

typedef int(* msat_termination_test)(void *user_data)

Custom test for early termination of search.

See msat_set_termination_test

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)

Enumeration Type Documentation

MathSAT result.

Enumerator
MSAT_UNKNOWN 

Unknown.

MSAT_UNSAT 

Unsatisfiable.

MSAT_SAT 

Satisfiable.

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_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_BV 

FP conversion to 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

MathSAT truth value.

Enumerator
MSAT_UNDEF 

Undefined/unknown.

MSAT_FALSE 

False.

MSAT_TRUE 

True.

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

Function Documentation

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
eThe environment in which to operate
boolvarThe Boolean variable to add to the preferred list
phaseThe 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
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.

Parameters
eThe environment to use
importantAn array of important atoms. If NULL, all atoms are considered important
num_importantThe size of the important array. If important is NULL, set this to zero
funcThe callback function to be notified about models found (see msat_all_sat_model_callback). Cannot be NULL
user_dataGeneric 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:
  1. 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
  2. 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.
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
eThen environment in which terms are created
dataThe input string in SMT-LIBv2 format
out_nOn 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_termsOn 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_annotsOn 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.
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
eThen environment in which terms are created
dataThe input string in SMT-LIBv2 format
out_nOn 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_termsOn 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_annotsOn 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.
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
eThe environment in which the terms are defined
nThe number of terms to dump
termsThe terms to convert
annotsAn 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().
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
eThe environment in which the terms are defined
nThe number of terms to dump
termsThe terms to convert
annotsAn 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).
outThe output file
Returns
zero on success, nonzero on error.
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
eThe environment in which to operate
tThe term to apply the substitution to
nThe number of terms to substitute
to_substThe terms to substitute
valuesThe values to substitute
Returns
The result of the substitution, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
int msat_assert_formula ( msat_env  e,
msat_term  formula 
)

Adds a logical formula to an environment.

Parameters
eThe environment in which the formula is asserted
formulaThe formula to assert. Must have been created in e, otherwise bad things will happen (probably a crash)
Returns
zero on success, nonzero on error
int msat_clear_preferred_for_branching ( msat_env  e)

Clears the list of preferred variables for branching.

Parameters
eThe environment in which to operate
Returns
zero on success, nonzero on error
msat_config msat_create_config ( void  )

Creates a new MathSAT configuration.

Returns
A new configuration.
msat_config msat_create_default_config ( const char *  logic)

Creates a new MathSAT configuration with the default settings for the given logic.

Parameters
logicAn 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_env msat_create_env ( msat_config  cfg)

Creates a new MathSAT environment from the given configuration.

Parameters
cfgThe configuration to use.
Returns
A new environment. Use MSAT_ERROR_ENV to check for errors
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
eThe environment in which to operate.
Returns
an identifier for the new group, or -1 in case of error.
msat_model_iterator msat_create_model_iterator ( msat_env  e)

Creates a model iterator.

Parameters
eThe environment in use
Returns
an iterator for the current model
msat_env msat_create_shared_env ( msat_config  cfg,
msat_env  sibling 
)

Creates an environment that can share terms with its sibling.

Parameters
cfgThe configuration to use.
siblingThe environment with which to share terms.
Returns
A new environment. Use MSAT_ERROR_ENV to check for errors
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
dA declaration
nThe index of the argument for which the type is needed
Returns
The type of the given argument, or MSAT_U on error.
size_t msat_decl_get_arity ( msat_decl  d)

Returns the arity (number of arguments) of the given declaration.

Parameters
dA declaration
Returns
The arity of the declaration.
char* msat_decl_get_name ( msat_decl  d)

Returns the name corresponding to the given declaration.

Parameters
dA declaration
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_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
dA declaration
Returns
The return type. In case of error, MSAT_U is returned.
msat_symbol_tag msat_decl_get_tag ( msat_env  e,
msat_decl  d 
)

Returns the symbol tag associated to the given declaration.

Parameters
eThe environment in which to operate
dA declaration
Returns
the tag of the declaration
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
dA declaration.
Returns
a unique (within the defining env) numeric identifier
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
dA declaration.
Returns
a string reprsentation of d, or NULL in case of errors. The string must be dellocated by the caller with msat_free().
msat_decl msat_declare_function ( msat_env  e,
const char *  name,
msat_type  type 
)

Declares a new uninterpreted function/constant.

Parameters
eThe environment of the declaration.
nameA name for the function. It must be unique in the environment.
typeThe type of the function.
Returns
A constant declaration, or a val s.t. MSAT_ERROR_DECL(val) is true in case of errors.
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
cfgThe configuration to destroy.
void msat_destroy_env ( msat_env  e)

Destroys an environment.

Parameters
eThe environment to destroy.
void msat_destroy_model ( msat_model  m)

Destroys the given model object.

Parameters
mA model object.
void msat_destroy_model_iterator ( msat_model_iterator  i)

Destroys a model iterator.

Parameters
iThe iterator to destroy.
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
mThe proof manager to destroy.
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
cbThe callback object to use.
levelThe literal whose reason needs to be computed.
reasonPointer to the zero-terminated reason clause for lit, with the first element being lit itself.
Returns
zero on success, nonzero on error.
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
cbThe callback object to use.
codePointer to a variable set by the callback function.
conflictPointer for retrieving the theory conflict, when the code value is set to MSAT_FALSE.
Returns
zero on success, nonzero on error.
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
cbThe callback object to use.
codePointer to a variable set by the callback function.
conflictPointer for retrieving the theory conflict, when the code value is set to MSAT_FALSE.
Returns
zero on success, nonzero on error.
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
cbThe callback object to use.
litThe assigned literal in DIMACS format.
Returns
zero on success, nonzero on error.
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
cbThe callback object to use.
levelThe target decision level for backtracking.
Returns
zero on success, nonzero on error.
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
cbThe callback object to use.
Returns
zero on success, nonzero on error.
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
eThe environment in which to operate
Returns
The declaration of symbol in e, or a ret s.t. MSAT_ERROR_DECL(ret) is true
void msat_free ( void *  ptr)

Function for deallocating the memory accessible by pointers returned by MathSAT.

msat_term msat_from_smtlib1 ( msat_env  e,
const char *  data 
)

Creates a term from a string in SMT-LIB v1 format.

Parameters
eThe environment in which to create the term.
dataThe 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_term msat_from_smtlib1_file ( msat_env  e,
FILE *  f 
)

Creates a term from a file in SMT-LIB v1 format.

Parameters
eThe environment in which to create the term.
fThe 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_term msat_from_smtlib2 ( msat_env  e,
const char *  data 
)

Creates a term from a string in SMT-LIB v2 format.

Parameters
eThe environment in which to create the term.
dataThe 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_term msat_from_smtlib2_file ( msat_env  e,
FILE *  f 
)

Creates a term from a file in SMT-LIB v2 format.

Parameters
eThe environment in which to create the term.
fThe 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_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
eThe environment of the definition
reprThe 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.
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
envThe environment in which to operate.
tokeepList of terms to not delete.
num_tokeepSize of the tokeep array.
Returns
zero on success, nonzero on error.
msat_type msat_get_array_type ( msat_env  env,
msat_type  itp,
msat_type  etp 
)

returns the data type for arrays with indices of itp type and elements of etp type.

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
eThe environment in which to operate.
num_assertedPointer 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_type msat_get_bool_type ( msat_env  env)

returns the data type for Booleans in the given env.

msat_type msat_get_bv_type ( msat_env  env,
size_t  width 
)

returns the data type for bit-vectors of the given width.

msat_type msat_get_fp_roundingmode_type ( msat_env  env)

returns the type for float rounding modes in the given env.

msat_type msat_get_fp_type ( msat_env  env,
size_t  exp_width,
size_t  mant_width 
)

returns the data type for floats with the given exponent and significand/mantissa width.

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
envThe environment in which to operate
param_typesThe types of the function arguments
num_paramsThe arity of the function type
return_typeThe type of the return value
Returns
a function type
msat_type msat_get_integer_type ( msat_env  env)

returns the data type for integers in the given env.

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
eThe environment in which to operate.
groups_of_aAn array of group identifiers.
nThe 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_model msat_get_model ( msat_env  e)

Creates a model object.

Parameters
eThe environment in use.
Returns
A model object. Use MSAT_ERROR_MODEL() to check for errors.
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
eThe environment in use
termThe 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_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
mThe 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_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
eThe 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_type msat_get_rational_type ( msat_env  env)

returns the data type for rationals in the given env.

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
eThe 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_type msat_get_simple_type ( msat_env  env,
const char *  name 
)

returns an atomic type with the given name in the given env.

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
eThe environment in which to operate.
num_tlemmasPointer 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_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
eThe environment in which to operate.
assumps_sizePointer 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_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
eThe environment in which to operate.
core_sizePointer 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_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).

Parameters
eThe environment in which to operate.
core_sizePointer to a valid address for storing the number of formulas in the unsat core.
extractorThe external Boolean core extractor.
user_dataGeneric 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().
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().
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
envThe environment in which to operate
tpThe data type to check
out_itpPointer to a variable where to store the type of the array indices (can be NULL)
out_itpPointer 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
int msat_is_bool_type ( msat_env  env,
msat_type  tp 
)

checks whether the given type is bool.

Parameters
envThe environment in which to operate
tpThe data type to check
Returns
1 if the type is bool, 0 otherwise
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
envThe environment in which to operate
tpThe data type to check
out_widthPointer 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
int msat_is_fp_roundingmode_type ( msat_env  env,
msat_type  tp 
)

checks whether the given type is a float rounding mode 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
envThe environment in which to operate
tpThe data type to check
out_exp_widthPointer to a variable where to store the width of the exponent of the float in case of success (can be NULL)
out_mant_widthPointer 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
int msat_is_integer_type ( msat_env  env,
msat_type  tp 
)

checks whether the given type is int.

Parameters
envThe environment in which to operate
tpThe data type to check
Returns
1 if the type is int, 0 otherwise
int msat_is_rational_type ( msat_env  env,
msat_type  tp 
)

checks whether the given type is rat.

Parameters
envThe environment in which to operate
tpThe data type to check
Returns
1 if the type is rat, 0 otherwise
const char* msat_last_error_message ( msat_env  env)

Retrieves the last error message generated while operating in the given enviroment.

Parameters
envThe environment in which the error occurred.
Returns
A pointer to the last error message generated.
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
eThe environment of the definition
t1The first argument. Must have type ::MSAT_BOOL.
t2The 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_term msat_make_array_const ( msat_env  e,
msat_type  arrtp,
msat_term  elem 
)

Creates a constant array.

Parameters
eThe environment of the definition
arrtpThe type of the return array
elemThe 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_term msat_make_array_read ( msat_env  e,
msat_term  arr,
msat_term  idx 
)

Creates an array read operation.

Parameters
eThe environment of the definition
arrThe array term
idxThe 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_term msat_make_array_write ( msat_env  e,
msat_term  arr,
msat_term  idx,
msat_term  elem 
)

Creates an array write operation.

Parameters
eThe environment of the definition
arrThe array term
idxThe index term
elemThe 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_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
eThe environment of the definition
t1The first argument.
t2The 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_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
eThe environment of the definition
t1The first argument.
t2The 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_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
eThe environment of the definition
t1The first argument.
t2The 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_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
eThe environment of the definition
t1The first argument.
t2The second argument.
Returns
The term t1 :: t2, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
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
eThe environment of the definition
msbThe most significant bit of the selection.
lsbThe least significant bit of the selection.
tThe argument.
Returns
The term t[msb:lsb], or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
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
eThe environment of the definition
t1The first argument.
t2The 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_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
eThe environment of the definition
t1The first argument.
t2The 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_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
eThe environment of the definition
t1The first argument.
t2The 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_term msat_make_bv_neg ( msat_env  e,
msat_term  t 
)

Returns a term representing the negation of t, te two's-complement.

Parameters
eThe environment of the definition
tThe argument.
Returns
The term -t, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
msat_term msat_make_bv_not ( msat_env  e,
msat_term  t 
)

Returns a term representing the bit-wise negation of t.

Parameters
eThe environment of the definition
tThe argument to negate.
Returns
The term !t, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
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
eThe environment of the definition
num_repA string representation for the number. The number must be non-negative.
widthThe width in bits of the number
baseThe 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_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
eThe environment of the definition
t1The first argument.
t2The 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_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
eThe environment of the definition
t1The first argument.
t2The 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_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
eThe environment of the definition
amountThe amount of the rotation
tThe 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_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
eThe environment of the definition
amountThe amount of the rotation
tThe 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_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
eThe environment of the definition
t1The first argument.
t2The 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_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
eThe environment of the definition
amountThe amount of the extension
tThe first argument.
Returns
The term sext(amount, t), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
msat_term msat_make_bv_sleq ( msat_env  e,
msat_term  t1,
msat_term  t2 
)

Returns a term representing the signed t1 <= t2.

Parameters
eThe environment of the definition
t1The first argument.
t2The 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_term msat_make_bv_slt ( msat_env  e,
msat_term  t1,
msat_term  t2 
)

Returns a term representing the signed t1 < t2.

Parameters
eThe environment of the definition
t1The first argument.
t2The 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_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
eThe environment of the definition
t1The first argument.
t2The 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_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
eThe environment of the definition
t1The first argument.
t2The 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_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
eThe environment of the definition
t1The first argument.
t2The 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_term msat_make_bv_uleq ( msat_env  e,
msat_term  t1,
msat_term  t2 
)

Returns a term representing the unsigned t1 <= t2.

Parameters
eThe environment of the definition
t1The first argument.
t2The 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_term msat_make_bv_ult ( msat_env  e,
msat_term  t1,
msat_term  t2 
)

Returns a term representing the unsigned t1 < t2.

Parameters
eThe environment of the definition
t1The first argument.
t2The 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_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
eThe environment of the definition
t1The first argument.
t2The 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_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
eThe environment of the definition
t1The first argument.
t2The 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_term msat_make_bv_zext ( msat_env  e,
size_t  amount,
msat_term  t 
)

Returns a term representing the zero extension of t.

Parameters
eThe environment of the definition
amountThe amount of the extension
tThe first argument.
Returns
The term zext(amount, t), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
msat_term msat_make_constant ( msat_env  e,
msat_decl  var 
)

Creates a constant from a declaration.

Parameters
eThe environment of the definition
varThe 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_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
eThe environment in which to create the term
tThe term to copy
srcThe 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_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
eThe environment of the definition
t1The first argument.
t2The second argument.
Returns
The term (t1 = t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
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
eThe environment of the definition
t1The first argument.
t2The second argument.
Returns
The term (t1 = t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
msat_term msat_make_false ( msat_env  e)

Returns a term representing logical falsity.

Parameters
eThe environment of the definition
Returns
The term FALSE, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
msat_term msat_make_floor ( msat_env  e,
msat_term  t 
)

Returns an expression representing (floor t)

Parameters
eThe environment of the definition
tThe argument.
Returns
The created term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
msat_term msat_make_fp_abs ( msat_env  e,
msat_term  t 
)

Returns a term representing the FP absolute value of t.

Parameters
eThe environment of the definition
tThe abs argument.
Returns
The term (abs t), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
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_bv 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
eThe environment of the definition
tThe 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_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
eThe environment of the definition
num_repA string representation of a base-10 integer number
exp_wThe desired exponent width
mant_wThe desired mantissa width
Returns
The numeric term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
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
eThe environment of the definition
exp_wThe target exponent width.
mant_wThe target mantissa width.
roundingThe desired rounding mode.
tThe 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_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
eThe environment of the definition
roundingThe desired rounding mode.
t1The first argument.
t2The second argument.
Returns
The term (/ rounding t1 t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
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
eThe environment of the definition
t1The first argument.
t2The second argument.
Returns
The term (fpeq t1 t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
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
eThe environment of the definition
exp_wThe target exponent width.
mant_wThe target mantissa width.
tThe 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_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
eThe environment of the definition
exp_wThe target exponent width.
mant_wThe target mantissa width.
roundingThe desired rounding mode.
tThe 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_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
eThe environment of the definition
exp_wThe target exponent width.
mant_wThe target mantissa width.
roundingThe desired rounding mode.
tThe 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_term msat_make_fp_isinf ( msat_env  e,
msat_term  t 
)

Returns the predicate for testing whether a FP term is infinity.

Parameters
eThe environment of the definition
tThe 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_term msat_make_fp_isnan ( msat_env  e,
msat_term  t 
)

Returns the predicate for testing whether a FP term is NaN.

Parameters
eThe environment of the definition
tThe 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_term msat_make_fp_isneg ( msat_env  e,
msat_term  t 
)

Returns the predicate for testing whether a FP term is negative.

Parameters
eThe environment of the definition
tThe 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_term msat_make_fp_isnormal ( msat_env  e,
msat_term  t 
)

Returns the predicate for testing whether a FP term is a normal.

Parameters
eThe environment of the definition
tThe 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_term msat_make_fp_ispos ( msat_env  e,
msat_term  t 
)

Returns the predicate for testing whether a FP term is positive.

Parameters
eThe environment of the definition
tThe 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_term msat_make_fp_issubnormal ( msat_env  e,
msat_term  t 
)

Returns the predicate for testing whether a FP term is a subnormal.

Parameters
eThe environment of the definition
tThe 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_term msat_make_fp_iszero ( msat_env  e,
msat_term  t 
)

Returns the predicate for testing whether a FP term is zero.

Parameters
eThe environment of the definition
tThe 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_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
eThe environment of the definition
t1The first argument.
t2The second argument.
Returns
The term (fpleq t1 t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
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
eThe environment of the definition
t1The first argument.
t2The second argument.
Returns
The term (fplt t1 t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
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
eThe environment of the definition
t1The first argument.
t2The second argument.
Returns
The term (max t1 t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
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
eThe environment of the definition
t1The first argument.
t2The second argument.
Returns
The term (min t1 t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
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
eThe environment of the definition
roundingThe desired rounding mode.
t1The first argument.
t2The second argument.
Returns
The term (- rounding t1 t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
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
eThe environment of the definition
exp_wThe desired exponent width
mant_wThe desired mantissa width
Returns
A term representing -Inf, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
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
eThe environment of the definition
exp_wThe desired exponent width
mant_wThe desired mantissa width
Returns
A term representing NaN, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
msat_term msat_make_fp_neg ( msat_env  e,
msat_term  t 
)

Returns a term representing the FP negation of t.

Parameters
eThe environment of the definition
tThe argument to negate.
Returns
The term (fpneg t), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
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
eThe environment of the definition
roundingThe desired rounding mode.
t1The first argument.
t2The second argument.
Returns
The term (+ rounding t1 t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
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
eThe environment of the definition
exp_wThe desired exponent width
mant_wThe desired mantissa width
Returns
A term representing +Inf, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
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
eThe environment of the definition
num_repA string representation for the rational number
exp_wThe desired exponent width
mant_wThe desired mantissa width
roundingThe desired rounding mode.
Returns
The numeric term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
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
eThe environment of the definition
roundingThe desired rounding mode.
tThe argument.
Returns
The term (fp.roundToIntegral rounding t), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
msat_term msat_make_fp_roundingmode_minus_inf ( msat_env  e)

Returns a term representing the FP rounding mode ROUND_TO_MINUS_INF.

Parameters
eThe 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_term msat_make_fp_roundingmode_nearest_even ( msat_env  e)

Returns a term representing the FP rounding mode ROUND_TO_NEAREST_EVEN.

Parameters
eThe 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_term msat_make_fp_roundingmode_plus_inf ( msat_env  e)

Returns a term representing the FP rounding mode ROUND_TO_PLUS_INF.

Parameters
eThe 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_term msat_make_fp_roundingmode_zero ( msat_env  e)

Returns a term representing the FP rounding mode ROUND_TO_ZERO.

Parameters
eThe 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_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
eThe environment of the definition
roundingThe desired rounding mode.
tThe sqrt argument.
Returns
The term (sqrt rounding t), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
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
eThe environment of the definition
roundingThe desired rounding mode.
t1The first argument.
t2The second argument.
Returns
The term (* rounding t1 t2), or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
msat_term msat_make_fp_to_bv ( msat_env  e,
size_t  width,
msat_term  rounding,
msat_term  t 
)

Returns a term representing the conversion of a FP term to bit-vector.

Parameters
eThe environment of the definition
widthThe target bit-vector width.
roundingThe desired rounding mode.
tThe 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_term msat_make_iff ( msat_env  e,
msat_term  t1,
msat_term  t2 
)

Returns a term representing the equivalence of t1 and t2.

Parameters
eThe environment of the definition
t1The first argument. Must have type ::MSAT_BOOL.
t2The 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_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
eThe environment of the definition
tThe 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_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
eThe environment of the definition
tThe 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_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
eThe environment of the definition
modulusThe value of the modulus. Must be > 0
t1The first argument.
t2The second argument.
Returns
The created term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
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
eThe environment of the definition
widthThe target bit-vector width.
tThe 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_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
eThe environment of the definition
t1The first argument. Must be of type rational or integer
t2The 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_term msat_make_not ( msat_env  e,
msat_term  t1 
)

Returns a term representing the logical negation of t1.

Parameters
eThe environment of the definition
t1The 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_term msat_make_number ( msat_env  e,
const char *  num_rep 
)

Returns an expression representing an integer or rational number.

Parameters
eThe environment of the definition
num_repA 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_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
eThe environment of the definition
t1The first argument. Must have type ::MSAT_BOOL.
t2The 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_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
eThe environment of the definition
t1The first argument. Must be of type rational or integer
t2The 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_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
eThe environment in which to create the term
dThe declaration
argsThe 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_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
eThe environment of the definition
cThe condition of the test. Must be of type ::MSAT_BOOL
ttThe "then" branch
teThe "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_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. Moreover, at least one of them must be a number.

Parameters
eThe environment of the definition
t1The first argument. Must be of type rational or integer
t2The 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_term msat_make_true ( msat_env  e)

Returns a term representing logical truth.

Parameters
eThe environment of the definition
Returns
The term TRUE, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.
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
eThe environment of the definition
funcThe declaration of the function
argsThe 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_model_iterator msat_model_create_iterator ( msat_model  m)

Creates an iterator for the given model.

Parameters
mThe model to iterate.
Returns
A model iterator. Use MSAT_ERROR_MODEL_ITERATOR() to check for errors.
msat_term msat_model_eval ( msat_model  m,
msat_term  t 
)

Evaluates the input term in the given model.

Parameters
mThe model used for the evaluation.
tThe term to evaluate.
Returns
the value for t in m. Use MSAT_ERROR_TERM() to check for errors.
int msat_model_iterator_has_next ( msat_model_iterator  i)

Checks whether i can be incremented.

Parameters
iA model iterator
Returns
nonzero if i can be incremented, zero otherwise
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
iThe model iterator to increment.
tOutput value for the next variable/function call in the model.
vOutput value for the next value in the model.
Returns
nonzero in case of error.
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
eThen environment in which terms are created
dataThe input string in SMT-LIBv2 format
out_nOn success, the number of named terms is stored here. Must not be NULL.
out_namesOn 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_termsOn 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.
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
eThen environment in which terms are created
fThe input file in SMT-LIBv2 format
out_nOn success, the number of named terms is stored here. Must not be NULL.
out_namesOn 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_termsOn 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.
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
eThe environment in which the terms are defined
nThe number of terms/names to dump
namesAn array of names for the terms
termsThe 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().
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
eThe environment in which the terms are defined
nThe number of terms/names to dump
namesAn array of names for the terms
termsThe terms to convert
outThe output file
Returns
zero on success, nonzero on error.
size_t msat_num_backtrack_points ( msat_env  e)

returns the number of backtrack points in the given environment

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
dataThe 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_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
fThe configuration file to parse
Returns
A new configuration. In case of errors, a cfg s.t. MSAT_ERROR_CONFIG(cfg) is true is returned
int msat_pop_backtrack_point ( msat_env  e)

Backtracks to the last checkpoint set in the environment e.

Parameters
eThe environment in which to operate
Returns
zero on success, nonzero on error
size_t msat_proof_get_arity ( msat_proof  p)

Retrieves the number of children of a non-term proof.

Parameters
pA non-term proof.
Returns
The arity of the given proof.
msat_proof msat_proof_get_child ( msat_proof  p,
size_t  i 
)

Retrieves a sub-proof of a given proof.

Parameters
pA non-term proof.
iThe index of the child proof to retrieve.
Returns
a Child proof of the given proof.
const char* msat_proof_get_name ( msat_proof  p)

Retrieves the name of a non-term proof.

Parameters
pA non-term proof.
Returns
The name of the given proof.
msat_term msat_proof_get_term ( msat_proof  p)

Retrieves the term associated to a term proof.

Parameters
pThe proof from which to get the term. Must be a term proof.
Returns
The term associated with the input proof.
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
pA proof.
Returns
a unique (within the defining manager) numeric identifier
int msat_proof_is_term ( msat_proof  p)

Checks whether a proof object is a term.

Parameters
pThe proof to test.
Returns
nonzero if p is a term proof, zero otherwise.
int msat_push_backtrack_point ( msat_env  e)

Pushes a checkpoint for backtracking in an environment.

Parameters
eThe environment in which to operate
Returns
zero on success, nonzero on error
int msat_reset_env ( msat_env  e)

Resets an environment.

Clears the assertion stack (see msat_assert_formula, msat_push_backtrack_point, msat_pop_backtrack_point) of e. However, terms created in e are still valid.

Parameters
eThe environment to reset
Returns
zero on success, nonzero on error
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.

Parameters
envThe environment in which to operate.
engineThe engine to use
Returns
zero on success, nonzero on error
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
eThe environment in which to operate.
groupThe group. Must have been previously created with msat_create_itp_group.
Returns
zero on success, nonzero on error.
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
cfgThe configuration in which to operate.
optionThe name of the option to set.
valueThe 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.
int msat_set_termination_test ( msat_env  env,
msat_termination_test  func,
void *  user_data 
)

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
envThe environment in which to operate.
funcThe user-defined termination criterion. If it is NULL, no termination criterion will be used.
user_dataGeneric 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_result msat_solve ( msat_env  e)

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
eThe 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.
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.

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
eThe environment to use
diversifiersthe terms over which to diversify. On each succesive model, at least one of these terms will have a different value.
num_diversifiersthe size of the diversifiers array.
funcThe callback function to be notified about models found (see msat_solve_diversify_model_callback). Cannot be NULL.
user_dataGeneric 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_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
eThe environment to check.
assumptionsThe list of assumptions. Can only be (negated) Boolean constants
num_assumptionsThe 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.
size_t msat_term_arity ( msat_term  t)

Returns the arity of t.

Parameters
tA term.
Returns
The number of arguments of t
msat_term msat_term_get_arg ( msat_term  t,
size_t  n 
)

Returns the nth argument of t.

Parameters
tA term.
nThe index of the argument. Must be lower than the arity of t
Returns
The nth argument of arguments of t
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
tThe 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_type msat_term_get_type ( msat_term  t)

Returns the type of t.

Parameters
tA term.
Returns
The type of t
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
tA term.
Returns
a unique (within the defining env) numeric identifier
int msat_term_is_and ( msat_env  e,
msat_term  t 
)

Checks whether t is an AND.

Parameters
tA term.
Returns
nonzero if t is an AND
int msat_term_is_array_const ( msat_env  e,
msat_term  t 
)

Checks whether t is a constant array.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a constant array
int msat_term_is_array_read ( msat_env  e,
msat_term  t 
)

Checks whether t is an array read.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is an array read
int msat_term_is_array_write ( msat_env  e,
msat_term  t 
)

Checks whether t is an array write.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is an array write
int msat_term_is_atom ( msat_env  e,
msat_term  t 
)

Checks whether t is an atom.

Parameters
tA term.
Returns
nonzero if t is an atom, i.e. either a boolean constant or a relation between terms
int msat_term_is_boolean_constant ( msat_env  e,
msat_term  t 
)

Checks whether t is a boolean constant.

Parameters
tA term.
Returns
nonzero if t is a constant of type ::MSAT_BOOL
int msat_term_is_bv_and ( msat_env  e,
msat_term  t 
)

Checks whether t is a bit-wise and.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a bit-wise and
int msat_term_is_bv_ashr ( msat_env  e,
msat_term  t 
)

Checks whether t is an arithmetic shift right.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is an arithmetic shift right
int msat_term_is_bv_comp ( msat_env  e,
msat_term  t 
)

Checks whether t is a BV comparison.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a BV comparison
int msat_term_is_bv_concat ( msat_env  e,
msat_term  t 
)

Checks whether t is a BV concatenation.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a concatenation
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
eThe environment in which to operate
tA term.
out_msbIf not NULL, the msb of the selection will be stored here
out_lsbIf not NULL, the lsb of the selection will be stored here
Returns
nonzero if t is an extraction
int msat_term_is_bv_lshl ( msat_env  e,
msat_term  t 
)

Checks whether t is a logical shift left.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a logical shift left
int msat_term_is_bv_lshr ( msat_env  e,
msat_term  t 
)

Checks whether t is a logical shift right.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a logical shift right
int msat_term_is_bv_minus ( msat_env  e,
msat_term  t 
)

Checks whether t is a bit-vector subtraction.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a bit-vector subtraction
int msat_term_is_bv_neg ( msat_env  e,
msat_term  t 
)

Checks whether t is a bit-vector unary negation.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a bit-vector unary negation
int msat_term_is_bv_not ( msat_env  e,
msat_term  t 
)

Checks whether t is a bit-wise not.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a bit-wise not
int msat_term_is_bv_or ( msat_env  e,
msat_term  t 
)

Checks whether t is a bit-wise or.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a bit-wise or
int msat_term_is_bv_plus ( msat_env  e,
msat_term  t 
)

Checks whether t is a bit-vector addition.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a bit-vector addition
int msat_term_is_bv_rol ( msat_env  e,
msat_term  t,
size_t *  out_amount 
)

Checks whether t is a rotate left.

Parameters
eThe environment in which to operate
tA term.
out_amountIf not NULL, the amount of the left rotation will be stored here
Returns
nonzero if t is a rotate left
int msat_term_is_bv_ror ( msat_env  e,
msat_term  t,
size_t *  out_amount 
)

Checks whether t is a rotate right.

Parameters
eThe environment in which to operate
tA term.
out_amountIf not NULL, the amount of the right rotation will be stored here
Returns
nonzero if t is a rotate right
int msat_term_is_bv_sdiv ( msat_env  e,
msat_term  t 
)

Checks whether t is a bit-vector signed division.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a bit-vector signed division
int msat_term_is_bv_sext ( msat_env  e,
msat_term  t,
size_t *  out_amount 
)

Checks whether t is a sign extension.

Parameters
eThe environment in which to operate
tA term.
out_amountIf not NULL, the amount of the sign extension will be stored here
Returns
nonzero if t is a sign extension
int msat_term_is_bv_sleq ( msat_env  e,
msat_term  t 
)

Checks whether t is a bit-vector signed leq.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a bit-vector signed leq
int msat_term_is_bv_slt ( msat_env  e,
msat_term  t 
)

Checks whether t is a bit-vector signed lt.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a bit-vector signed lt
int msat_term_is_bv_srem ( msat_env  e,
msat_term  t 
)

Checks whether t is a bit-vector signed remainder.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a bit-vector signed remainder
int msat_term_is_bv_times ( msat_env  e,
msat_term  t 
)

Checks whether t is a bit-vector multiplication.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a bit-vector multiplication
int msat_term_is_bv_udiv ( msat_env  e,
msat_term  t 
)

Checks whether t is a bit-vector unsigned division.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a bit-vector unsigned division
int msat_term_is_bv_uleq ( msat_env  e,
msat_term  t 
)

Checks whether t is a bit-vector unsigned leq.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a bit-vector unsigned leq
int msat_term_is_bv_ult ( msat_env  e,
msat_term  t 
)

Checks whether t is a bit-vector unsigned lt.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a bit-vector unsigned lt
int msat_term_is_bv_urem ( msat_env  e,
msat_term  t 
)

Checks whether t is a bit-vector unsigned remainder.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a bit-vector unsigned remainder
int msat_term_is_bv_xor ( msat_env  e,
msat_term  t 
)

Checks whether t is a bit-wise xor.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a bit-wise xor
int msat_term_is_bv_zext ( msat_env  e,
msat_term  t,
size_t *  out_amount 
)

Checks whether t is a zero extension.

Parameters
eThe environment in which to operate
tA term.
out_amountIf not NULL, the amount of the zero extension will be stored here
Returns
nonzero if t is a zero extension
int msat_term_is_constant ( msat_env  e,
msat_term  t 
)

Checks whether t is a constant.

Parameters
tA term.
Returns
nonzero if t is a constant
int msat_term_is_equal ( msat_env  e,
msat_term  t 
)

Checks whether t is an equality.

Parameters
tA term.
Returns
nonzero if t is an equality atom
int msat_term_is_false ( msat_env  e,
msat_term  t 
)

Checks whether t is the FALSE term.

Parameters
tA term.
Returns
nonzero if t is FALSE
int msat_term_is_floor ( msat_env  e,
msat_term  t 
)

Checks whether t is a (floor t1) expression.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a floor expression
int msat_term_is_fp_abs ( msat_env  e,
msat_term  t 
)

Checks whether t is a FP abs.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a FP abs
int msat_term_is_fp_as_ieeebv ( msat_env  e,
msat_term  t 
)

Checks whether t is a FP as BV conversion.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a FP as BV conversion
int msat_term_is_fp_cast ( msat_env  e,
msat_term  t 
)

Checks whether t is a FP cast.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a FP cast
int msat_term_is_fp_div ( msat_env  e,
msat_term  t 
)

Checks whether t is a FP div.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a FP div
int msat_term_is_fp_equal ( msat_env  e,
msat_term  t 
)

Checks whether t is a FP equality.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a FP equality
int msat_term_is_fp_from_ieeebv ( msat_env  e,
msat_term  t 
)

Checks whether t is a FP from IEEE BV conversion.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a FP from unsigned BV conversion
int msat_term_is_fp_from_sbv ( msat_env  e,
msat_term  t 
)

Checks whether t is a FP from signed BV conversion.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a FP from signed BV conversion
int msat_term_is_fp_from_ubv ( msat_env  e,
msat_term  t 
)

Checks whether t is a FP from unsigned BV conversion.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a FP from unsigned BV conversion
int msat_term_is_fp_isinf ( msat_env  e,
msat_term  t 
)

Checks whether t is a FP isinf predicate.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a FP isinf predicate
int msat_term_is_fp_isnan ( msat_env  e,
msat_term  t 
)

Checks whether t is a FP isnan predicate.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a FP isnan predicate
int msat_term_is_fp_isneg ( msat_env  e,
msat_term  t 
)

Checks whether t is a FP isneg predicate.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a FP isneg predicate
int msat_term_is_fp_isnormal ( msat_env  e,
msat_term  t 
)

Checks whether t is a FP isnormal predicate.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a FP isnormal predicate
int msat_term_is_fp_ispos ( msat_env  e,
msat_term  t 
)

Checks whether t is a FP ispos predicate.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a FP ispos predicate
int msat_term_is_fp_issubnormal ( msat_env  e,
msat_term  t 
)

Checks whether t is a FP issubnormal predicate.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a FP iszero predicate
int msat_term_is_fp_iszero ( msat_env  e,
msat_term  t 
)

Checks whether t is a FP iszero predicate.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a FP iszero predicate
int msat_term_is_fp_leq ( msat_env  e,
msat_term  t 
)

Checks whether t is a FP <=.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a FP <=
int msat_term_is_fp_lt ( msat_env  e,
msat_term  t 
)

Checks whether t is a FP less than.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a FP less than
int msat_term_is_fp_max ( msat_env  e,
msat_term  t 
)

Checks whether t is a FP max.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a FP max
int msat_term_is_fp_min ( msat_env  e,
msat_term  t 
)

Checks whether t is a FP min.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a FP min
int msat_term_is_fp_minus ( msat_env  e,
msat_term  t 
)

Checks whether t is a FP minus.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a FP minus
int msat_term_is_fp_neg ( msat_env  e,
msat_term  t 
)

Checks whether t is a FP negation.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a FP negation
int msat_term_is_fp_plus ( msat_env  e,
msat_term  t 
)

Checks whether t is a FP plus.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a FP plus
int msat_term_is_fp_round_to_int ( msat_env  e,
msat_term  t 
)

Checks whether t is a FP round to integer.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a FP round to integer
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
eThe environment in which to operate
tA term.
Returns
nonzero if t is ROUND_TO_MINUS_INF
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
eThe environment in which to operate
tA term.
Returns
nonzero if t is ROUND_TO_NEAREST_EVEN
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
eThe environment in which to operate
tA term.
Returns
nonzero if t is ROUND_TO_PLUS_INF
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
eThe environment in which to operate
tA term.
Returns
nonzero if t is ROUND_TO_ZERO
int msat_term_is_fp_sqrt ( msat_env  e,
msat_term  t 
)

Checks whether t is a FP sqrt.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a FP sqrt
int msat_term_is_fp_times ( msat_env  e,
msat_term  t 
)

Checks whether t is a FP times.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a FP times
int msat_term_is_fp_to_bv ( msat_env  e,
msat_term  t 
)

Checks whether t is a FP to BV conversion.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a FP to BV conversion
int msat_term_is_iff ( msat_env  e,
msat_term  t 
)

Checks whether t is an equivalence between boolean terms.

Parameters
tA term.
Returns
nonzero if t is an IFF
int msat_term_is_int_from_sbv ( msat_env  e,
msat_term  t 
)

Checks whether t is a signed BV to int conversion.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a signed BV to int conversion
int msat_term_is_int_from_ubv ( msat_env  e,
msat_term  t 
)

Checks whether t is an unsigned BV to int conversion.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is an unsigned BV to int conversion
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
eThe environment in which to operate
tA term.
Returns
nonzero if t is an integer modular congruence
int msat_term_is_int_to_bv ( msat_env  e,
msat_term  t 
)

Checks whether t is a int to BV conversion.

Parameters
eThe environment in which to operate
tA term.
Returns
nonzero if t is a int to BV conversion
int msat_term_is_leq ( msat_env  e,
msat_term  t 
)

Checks whether t is a (t1 <= t2) atom.

Parameters
tA term.
Returns
nonzero if t is a (t1 <= t2) atom
int msat_term_is_not ( msat_env  e,
msat_term  t 
)

Checks whether t is a NOT.

Parameters
tA term.
Returns
nonzero if t is a NOT
int msat_term_is_number ( msat_env  e,
msat_term  t 
)

Checks whether t is a number.

Parameters
tA term.
Returns
nonzero if t is a number
int msat_term_is_or ( msat_env  e,
msat_term  t 
)

Checks whether t is an OR.

Parameters
tA term.
Returns
nonzero if t is an OR
int msat_term_is_plus ( msat_env  e,
msat_term  t 
)

Checks whether t is a (t1 + t2) expression.

Parameters
tA term.
Returns
nonzero if t is a (t1 + t2) expression
int msat_term_is_term_ite ( msat_env  e,
msat_term  t 
)

Checks whether t is a term if-then-else.

Parameters
tA term.
Returns
nonzero if t is a term if-then-else
int msat_term_is_times ( msat_env  e,
msat_term  t 
)

Checks whether t is a (t1 * t2) expression.

Parameters
tA term.
Returns
nonzero if t is a (t1 * t2) expression
int msat_term_is_true ( msat_env  e,
msat_term  t 
)

Checks whether t is the TRUE term.

Parameters
tA term.
Returns
nonzero if t is TRUE
int msat_term_is_uf ( msat_env  e,
msat_term  t 
)

Checks whether t is an uninterpreted function application.

Parameters
tA term.
Returns
nonzero if t is a uf application
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
tA term.
Returns
a string reprsentation of t, or NULL in case of errors. The string must be dellocated by the caller with msat_free().
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
ethe environment in which to operate
tthe number to convert
outthe 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
char* msat_to_smtlib1 ( msat_env  e,
msat_term  term 
)

Converts the given term to SMT-LIB v1 format.

Parameters
eThe environment in which term is defined
termThe 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().
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
eThe environment in which term is defined
termThe term to convert
outThe output file
Returns
zero on success, nonzero on error.
char* msat_to_smtlib2 ( msat_env  e,
msat_term  term 
)

Converts the given term to SMT-LIB v2 format.

Parameters
eThe environment in which term is defined
termThe 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().
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
eThe environment in which term is defined
termThe term to convert
logic_nameName of the SMT-LIBv2 logic for the output. Can be NULL
use_definesIf 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().
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
eThe environment in which term is defined
termThe term to convert
logic_nameName of the SMT-LIBv2 logic for the output. Can be NULL
use_definesIf nonzero, the output will contain define-funs instead of let bindings
outThe output file
Returns
zero on success, nonzero on error.
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
eThe environment in which term is defined
termThe term to convert
outThe output file
Returns
zero on success, nonzero on error.
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
Theenvironment in which term is defined
termThe 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().
int msat_type_equals ( msat_type  t1,
msat_type  t2 
)

checks whether two data types are the same

Returns
1 if the types are the same, 0 otherwise
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
tA type.
Returns
a string reprsentation of t, or NULL in case of errors. The string must be dellocated by the caller with msat_free().
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

Parameters
eThe environment in which to operate
tThe term to visit
funcThe callback function
user_dataGeneric 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...
 

 

int(* msat_ext_dpll_interface::add_clause)(void *self, int *clause, int permanent, int during_callback)

Adds a clause to the SAT solver.

Parameters
selfPointer to the SAT solver.
clausearray of literals in DIMACS format, terminated by 0.
permanentIf nonzero, the clause is meant to be permanent.
during_callbackIf nonzero, the function is called by one of the msat_dpll_callback methods
Returns
zero on success, nonzero on error
int(* msat_ext_dpll_interface::enqueue_assignment)(void *self, int lit)

Adds a (theory-deduced) literal to the current trail.

Parameters
selfPointer to the SAT solver.
litliteral in DIMACS format.
Returns
zero on success, nonzero on error.
msat_truth_value(* msat_ext_dpll_interface::model_value)(void *self, int lit)

Retrieves the model value for the given literal.

Parameters
selfPointer to the SAT solver.
litliteral in DIMACS format.
Returns
The truth value for the literal.
int(* msat_ext_dpll_interface::new_var)(void *self)

Creates a new variable in the SAT solver.

Parameters
selfPointer to the SAT solver.
Returns
the DIMACS index of the new variable, or -1 in case of errors.
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
selfPointer to the SAT solver.
varvariable in DIMACS format.
Returns
zero on success, nonzero on error.
int(* msat_ext_dpll_interface::reset)(void *self)

Completely resets the state of the solver.

Parameters
selfPointer to the SAT solver.
Returns
zero on success, nonzero on error.
int(* msat_ext_dpll_interface::set_callback)(void *self, msat_dpll_callback cb)

Associates to the solver a callback object for interacting with MathSAT.

Parameters
selfPointer to the SAT solver.
cbThe msat_dpll_callback object.
Returns
zero on success, nonzero on error.
int(* msat_ext_dpll_interface::set_decision_var)(void *self, int var, int yes)

Marks a variable as a decision variable.

Parameters
selfPointer to the SAT solver.
varthe DIMACS index for the variable.
yesdecision flag.
Returns
zero on success, nonzero on error.
int(* msat_ext_dpll_interface::set_frozen)(void *self, int var, int yes)

Sets the frozen status of a variable.

Parameters
selfPointer to the SAT solver.
varthe DIMACS index for the variable.
yesfrozen flag.
Returns
zero on success, nonzero on error.
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
selfPointer to the SAT solver.
assumptionsarray of literals in DIMACS format, terminated by 0.
out_conflicting_assumptionsif 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
mathsat [AT] fbk [DOT] eu
mathsat-announce mailing list