MathSAT 5

Error checking for configurations.

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

Error checking for declarations.

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

Error checking for environments.

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

Error checking for models.

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

Error checking for model iterators.

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

Error checking for objectives.

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

Error checking for objective iterators.

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

Error checking for proofs.

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

Error checking for proof managers.

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

Error checking for terms.

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

Error checking for types.

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

Sets given term to be an error term.

Use this macro to make terms error terms.

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

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)

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

Custom test for early termination of search.

See msat_set_termination_test

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)

MathSAT result.

MathSAT symbol tag.

MathSAT truth value.

MathSAT status for the callback passed to msat_visit_term

Adds a Boolean variable at the end of the list of preferred variables for branching when solving the problem.

Parameters

e	The environment in which to operate
boolvar	The Boolean variable to add to the preferred list
phase	The phase of the variable for branching. If MSAT_UNDEF, the phase is determined by the currently configured heuristics

Returns

zero on success, nonzero on error

Performs AllSat over the important atoms of the conjunction of all formulas asserted in e (see msat_assert_formula). When used in incremental mode, a backtrack point should be pushed before calling this function, and popped after this call has completed. Not doing this changes the satisfiability of the formula.

Parameters

e	The environment to use
important	An array of important atoms. If NULL, all atoms are considered important
num_important	The size of the important array. If important is NULL, set this to zero
func	The callback function to be notified about models found (see msat_all_sat_model_callback). Cannot be NULL
user_data	Generic data pointer which will be passed to func. Can be anything, its value will not be interpreted

Returns

The number of models found, or -1 on error. If the solver detects that the formula is a tautology, -2 is returned. Note however that:

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.

Parses a list of annotated terms from a string in SMT-LIB v2 format.

Given a string in SMT-LIB v2 format, collect and return all and only the terms with an annotation.

Parameters

e	Then environment in which terms are created
data	The input string in SMT-LIBv2 format
out_n	On success, the number of terms is stored here. Must not be NULL. Notice that terms with multiple annotations are counted multiple times (see out_names below)
out_terms	On success, the parsed annotated terms are stored here. Must not be NULL. The array is dynamically allocated, and must be deallocated by the user with msat_free(). If a term contains multiple annotations, it will occur multiple times here (once for each annotation).
out_annots	On success, the annotations of the parsed terms are stored here. Must not be NULL. Both the array and its elements are dynamically allocated, and must be deallocated by the user with msat_free(). For each term at index i in out_terms, the corresponding annotation is stored as a key, value pair at indices 2*i and 2*i+1 in out_annots.

Returns

zero on success, nonzero on error.

Like msat_annotated_list_from_smtlib2(), but reads from a file instead of a string.

Given a FILE in SMT-LIB v2 format, collect and return all and only the terms with an annotation.

Parameters

e	Then environment in which terms are created
data	The input string in SMT-LIBv2 format
out_n	On success, the number of terms is stored here. Must not be NULL. Notice that terms with multiple annotations are counted multiple times (see out_names below)
out_terms	On success, the parsed annotated terms are stored here. Must not be NULL. The array is dynamically allocated, and must be deallocated by the user with msat_free(). If a term contains multiple annotations, it will occur multiple times here (once for each annotation).
out_annots	On success, the annotations of the parsed terms are stored here. Must not be NULL. Both the array and its elements are dynamically allocated, and must be deallocated by the user with msat_free(). For each term at index i in out_terms, the corresponding annotation is stored as a key, value pair at indices 2*i and 2*i+1 in out_annots.

Returns

zero on success, nonzero on error.

Converts the given list of annotated terms to SMT-LIB v2 format.

Parameters

e	The environment in which the terms are defined
n	The number of terms to dump
terms	The terms to convert
annots	An array of annotations for the terms. For each term at index i in terms, the corresponding (key, value) annotation is stored at indices 2*i and 2*i+1 in annots. Terms with multiple annotations should be listed multiple times in terms (once for each annotation).

Returns

a string in SMT-LIB v2 format storing all the annotated input terms, or NULL in case of errors. If not NULL, the returned string must be deallocated by the user with msat_free().

Like msat_annotated_list_to_smtlib2(), but writes to a FILE instead of returning a string.

Parameters

e	The environment in which the terms are defined
n	The number of terms to dump
terms	The terms to convert
annots	An array of annotations for the terms. For each term at index i in terms, the corresponding (key, value) annotation is stored at indices 2*i and 2*i+1 in annots. Terms with multiple annotations should be listed multiple times in terms (once for each annotation).
out	The output file

Returns

zero on success, nonzero on error.

substitutes the terms in to_subst with values in t

Parameters

e	The environment in which to operate
t	The term to apply the substitution to
n	The number of terms to substitute
to_subst	The terms to substitute
values	The values to substitute

Returns

The result of the substitution, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.

Adds a logical formula to an environment.

Parameters

e	The environment in which the formula is asserted
formula	The formula to assert. Must have been created in e, otherwise bad things will happen (probably a crash)

Returns

zero on success, nonzero on error

Clears the list of preferred variables for branching.

Parameters

e	The environment in which to operate

Returns

zero on success, nonzero on error

Creates a new MathSAT configuration.

Returns

A new configuration.

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

Parameters

logic

An SMT-LIB logic name

Returns

A new configuration. In case of errors, a cfg s.t. MSAT_ERROR_CONFIG(cfg) is true is returned

Creates a new MathSAT environment from the given configuration.

Parameters

cfg	The configuration to use.

Returns

A new environment. Use MSAT_ERROR_ENV to check for errors

Creates a new group for interpolation.

When computing an interpolant, formulas are organized into several groups, which are partitioned into two sets GA and GB. The conjuction of formulas in GA will play the role of A, and that of formulas in GB will play the role of B (see msat_set_itp_group, msat_get_interpolant).

Parameters

e	The environment in which to operate.

Returns

an identifier for the new group, or -1 in case of error.

Creates a model iterator.

Parameters

e	The environment in use

Returns

an iterator for the current model

Creates an environment that can share terms with its sibling.

Parameters

cfg	The configuration to use.
sibling	The environment with which to share terms.

Returns

A new environment. Use MSAT_ERROR_ENV to check for errors

Returns the type of the given argument for the input declaration.

Parameters

d	A declaration
n	The index of the argument for which the type is needed

Returns

The type of the given argument, or MSAT_U on error.

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

Parameters

d	A declaration

Returns

The arity of the declaration.

Returns the name corresponding to the given declaration.

Parameters

d	A 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.

Returns the return type of the given declaration.

The return type for a constant is simply the constant's type.

Parameters

d	A declaration

Returns

The return type. In case of error, MSAT_U is returned.

Returns the symbol tag associated to the given declaration.

Parameters

e	The environment in which to operate
d	A declaration

Returns

the tag of the declaration

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

d	A declaration.

Returns

a unique (within the defining env) numeric identifier

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

d	A declaration.

Returns

a string reprsentation of d, or NULL in case of errors. The string must be dellocated by the caller with msat_free().

Declares a new uninterpreted function/constant.

Parameters

e	The environment of the declaration.
name	A name for the function. It must be unique in the environment.
type	The type of the function.

Returns

A constant declaration, or a val s.t. MSAT_ERROR_DECL(val) is true in case of errors.

Destroys a configuration.

It is an error to destroy a configuration that is still being used by an environment.

Parameters

cfg	The configuration to destroy.

Destroys an environment.

Parameters

e	The environment to destroy.

Destroys the given model object.

Parameters

m	A model object.

Destroys a model iterator.

Parameters

i	The iterator to destroy.

Destroys a proof manager.

Destroying a proof manager will also destroy all the proofs associated with it.

Parameters

m	The proof manager to destroy.

Callback function that the external SAT solver must call for asking MathSAT the reason for a theory-deduced literal, during conflict analysis.

Parameters

cb	The callback object to use.
level	The literal whose reason needs to be computed.
reason	Pointer to the zero-terminated reason clause for lit, with the first element being lit itself.

Returns

zero on success, nonzero on error.

Callback function that the external SAT solver must call when a Boolean model has been found.

The code value set by callback function tells the SAT solver what to do.

• if it is MSAT_TRUE, the model is theory satisfiable, so the formula is satisfiable.
• if it is MSAT_FALSE, MathSAT found a theory conflict, which is stored in conflict. The SAT solver is expected to perform conflict analysis on it and backjump.
• if it is MSAT_UNDEF, MathSAT created some new variables that need to be assigned by the SAT solver, so the search should continue.

Parameters

cb	The callback object to use.
code	Pointer to a variable set by the callback function.
conflict	Pointer for retrieving the theory conflict, when the code value is set to MSAT_FALSE.

Returns

zero on success, nonzero on error.

Callback function that the external SAT solver must call when a round of BCP has been completed without finding a Boolean conflict.

The code value set by callback function tells the SAT solver what to do.

• if it is MSAT_TRUE, the SAT solver can go on.
• if it is MSAT_FALSE, MathSAT found a theory conflict, which is stored in conflict. The SAT solver is expected to perform conflict analysis on it and backjump.
• if it is MSAT_UNDEF, the SAT solver needs to perform another round of BCP, because MathSAT enqueued some new literals on the trail.

Parameters

cb	The callback object to use.
code	Pointer to a variable set by the callback function.
conflict	Pointer for retrieving the theory conflict, when the code value is set to MSAT_FALSE.

Returns

zero on success, nonzero on error.

Callback function that the external SAT solver must call whenever a literal is added to the trail.

Parameters

cb	The callback object to use.
lit	The assigned literal in DIMACS format.

Returns

zero on success, nonzero on error.

Callback function that the external SAT solver must call whenever it backtracks.

Parameters

cb	The callback object to use.
level	The target decision level for backtracking.

Returns

zero on success, nonzero on error.

Callback function that the external SAT solver must call whenever a new decision level is opened.

Parameters

cb	The callback object to use.

Returns

zero on success, nonzero on error.

Returns a term resulting from existentially quantifying the given constants in the given term.

Parameters

e	The environment of the definition
t	The term whose constants should be existentially quantified.
args	The list of constants to quantify.
n	The size of the list of constants.

Returns

The term exists constants body, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.

Returns the declaration of the given symbol in the given environment (if any)

If symbol is not declared in e, the returned value ret will be s.t. MSAT_ERROR_DECL(ret) is true

Parameters

e	The environment in which to operate

Returns

The declaration of symbol in e, or a ret s.t. MSAT_ERROR_DECL(ret) is true

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

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

Parameters

e	The environment in which to create the term.
data	The string representation in SMT-LIB v1 format.

Returns

The created term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.

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

Parameters

e	The environment in which to create the term.
f	The file in SMT-LIB v1 format.

Returns

The created term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.

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

Parameters

e	The environment in which to create the term.
data	The string representation in SMT-LIB v2 format. It can't contain commands other than functions and type declarations, definitions, and assertions

Returns

The created term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.

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

Parameters

e	The environment in which to create the term.
f	The file in SMT-LIB v2 format. It can't contain commands other than functions and type declarations, definitions, and assertions

Returns

The created term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.

Creates a term from its string representation.

The syntax of repr is that of the SMT-LIB v2. All the variables and functions must have been previously declared in e.

Parameters

e	The environment of the definition
repr	The string to parse, in SMT-LIB v2 syntax

Returns

The created term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.

Performs garbage collection on the given environment.

This function will perform garbage collection on the given environment. All the internal caches of the environment will be cleared (including those in the active solvers and preprocessors). If the environment is not shared, all the terms that are not either in tokeep or in the current asserted formulas will be deleted.

Parameters

env	The environment in which to operate.
tokeep	List of terms to not delete.
num_tokeep	Size of the tokeep array.

Returns

zero on success, nonzero on error.

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

Returns the list of formulas in the assertion stack.

The return value is a dynamically-allocated array of *num_asserted elements, which must be deallocated by the user. NULL is returned in case of errors. The array elements are formulas that are logically equivalent to the one asserted using msat_assert_formula

Parameters

e	The environment in which to operate.
num_asserted	Pointer to a valid address for storing the number of formulas currently in the assertion stack.

Returns

An array with the asserted formulas, or NULL in case of errors. The array is must be deallocated by allocated the user with msat_free().

returns the type for Booleans in the given env.

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

returns an enum type in the given env.

Parameters

env	The environment in which to operate
name	The name of the enum type
domain_size	The number of values of the enum
domain	The possible values of the enum

Returns

an enum type

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

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

returns a function type in the given env.

Parameters

env	The environment in which to operate
param_types	The types of the function arguments
num_params	The arity of the function type
return_type	The type of the return value

Returns

a function type

returns the type for integers in the given env.

Computes an interpolant for a pair (A, B) of formulas.

A is the conjucntion of all the assumed formulas in the groups_of_a groups (see msat_create_itp_group), and B is the rest of assumed formulas.

This function must be called only after msat_solve, and only if MSAT_UNSAT was returned. Moreover, interpolation must have been enabled in the configuration for the environment

Parameters

e	The environment in which to operate.
groups_of_a	An array of group identifiers.
n	The size of the groups_of_a array.

Returns

The interpolating term, or a t s.t. MSAT_ERROR_TERM(t) is true in case of errors.

Creates a model object.

Parameters

e	The environment in use.

Returns

A model object. Use MSAT_ERROR_MODEL() to check for errors.

Returns the value of the term term in the current model.

Preconditions:

• model computation was enabled in the configuration of the environment
• the last call to msat_solve returned a MSAT_SAT result
• no assert/push/pop/allsat commands have been issued in the meantime

Parameters

e	The environment in use
term	The term of interest.

Returns

The model value for term. If an error occurs, the return value ret is such that MSAT_ERROR_TERM(ret) is true

Returns a proof of unsatisfiability.

a proof is recursively defined as:

msat_proof ::= msat_term | name msat_proof*

i.e., it is either a term or a list of a name and children proofs. Proofs can be distinguished by their name, or by whether they are terms. Relevant proofs include:

"clause-hyp", which are the clauses of the (CNF conversion of the) input problem. They have a list of terms as children

"res-chain", representing Boolean resolution chains. The children are an interleaving of proofs and terms, where terms are the pivots for the resolution. For example: "res-chain p1 v p2" represents a resolution step between p1 and p2 on the pivot v

"theory-lemma", representing theory lemmas. They have as children a list of terms that consititute the lemma, plus an optional last element which is a more detailed proof produced by a theory solver.

Parameters

m	The proof manager in which to operate.

Returns

The proof of unsatisfiability associated to the latest msat_solve() call, or an object p s.t. MSAT_ERROR_PROOF(p) is true in case of errors.

Returns a proof manager for the given environment.

The manager must be destroyed by the user, with msat_destroy_proof_manager. In order to obtain a non-error result, the option "proof_generation" must be set to "true" in the configuration used for creating the environment.

Parameters

e	The environment in which to operate.

Returns

A proof manager for the environment. MSAT_ERROR_PROOF_MANAGER can be used to check whether an error occurred.

returns the type for rationals in the given env.

Returns a string with search statistics for the given environment.

The returned string will contain newline-separated statistics for the DPLL engine and the active theory solvers in the given environment.

Parameters

e	The environment in which to operate.

Returns

A string with search statistics, or NULL in case of errors. The string must be deallocated by the user with msat_free().

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

Retrieves the theory lemmas used in the last search (see msat_solve).

For the function to work, the option "dpll.store_tlemmas" must be set to "true" in the configuration object for the environment.

Parameters

e	The environment in which to operate.
num_tlemmas	Pointer to a valid address for storing the number of theory lemmas returned.

Returns

An array with the theory lemmas, or NULL in case of errors. The array must be deallocated by the user with msat_free().

Returns the list of assumptions resposible for the unsatisfiability detected by the last search (see msat_solve_with_assumptions).

Parameters

e	The environment in which to operate.
assumps_size	Pointer to a valid address for storing the number of formulas in the returned array.

Returns

An array with the list of inconsistent assumptions, or NULL in case of errors. The array must be deallocated by the user with msat_free().

Returns the unsatisfiable core of the last search (see msat_solve) as a subset of the asserted formulas, if the problem was unsatisfiable.

Parameters

e	The environment in which to operate.
core_size	Pointer to a valid address for storing the number of formulas in the unsat core.

Returns

An array with the unsat core, or NULL in case of errors. The array must be deallocated by the user with msat_free().

Returns the unsatisfiable core of the last search (see msat_solve) as a subset of the asserted formulas, computed using an external Boolean unsat core extractor (see msat_ext_unsat_core_extractor).

Parameters

e	The environment in which to operate.
core_size	Pointer to a valid address for storing the number of formulas in the unsat core.
extractor	The external Boolean core extractor.
user_data	Generic data pointer which will be passed to extractor. Can be anything, its value will not be interpreted.

Returns

An array with the unsat core, or NULL in case of errors. The array must be deallocated by the user with msat_free().

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().

checks whether the given type is an array.

Parameters

env	The environment in which to operate
tp	The type to check
out_itp	Pointer to a variable where to store the type of the array indices (can be NULL)
out_itp	Pointer to a variable where to store the type of the array elements (can be NULL)

Returns

1 if the type is an array, 0 otherwise

checks whether the given type is bool.

Parameters

env	The environment in which to operate
tp	The type to check

Returns

1 if the type is bool, 0 otherwise

checks whether the given type is a bit-vector.

Parameters

env	The environment in which to operate
tp	The type to check
out_width	Pointer to a variable where to store the width of the BV type in case of success (can be NULL)

Returns

1 if the type is a bit-vector, 0 otherwise

checks whether the given type is an enum

Parameters

env	The environment in which to operate
tp	The type to check
out_exp_width	Pointer to a variable where to store the number of values in the enum (can be NULL)
out_mant_width	Pointer to a variable where to store the list of values in the enum (can be NULL)

Returns

1 if the type is an enum, 0 otherwise

checks whether the given type is a float rounding mode type.

Parameters

env	The environment in which to operate
tp	The type to check

checks whether the given type is a float.

Parameters

env	The environment in which to operate
tp	The type to check
out_exp_width	Pointer to a variable where to store the width of the exponent of the float in case of success (can be NULL)
out_mant_width	Pointer to a variable where to store the width of the significand/mantissa of the float in case of success (can be NULL)

Returns

1 if the type is a float, 0 otherwise