The OptiMathSAT OMT Solver

OptiMathSAT (>= 1.6.0) C API Reference

API specific to the OptiMathSAT OMT solver. More...

Reference to remaining OptiMathSAT API in common with MathSAT 5 is available at MathSAT 5 API.

NEW (1.3.8): functions pushing an objective on the formula stack now return a handler to the objective instance.
NEW (1.5.0): pareto optimization, optimization result is now distinct from search result, minor improvement.

Data types and special values
struct	msat_env
	MathSAT environment.
struct	msat_objective
	OptiMathSAT objective.
struct	msat_objective_iterator
	OptiMathSAT objective iterator.
struct	msat_pareto_model_handler
	MathSAT Model Handler.
enum	msat_objective_value { MSAT_OPTIMUM = 0, MSAT_FINAL_LOWER = 1, MSAT_FINAL_UPPER = 2, MSAT_FINAL_ERROR = 3 }
enum	msat_objective_type { MSAT_OBJECTIVE_MINIMIZE = -1, MSAT_OBJECTIVE_MAXIMIZE = 1 }
enum	msat_opt_result { MSAT_OPT_UNKNOWN = -1, MSAT_OPT_UNSAT = 0, MSAT_OPT_SAT_PARTIAL = 1, MSAT_OPT_SAT_APPROX = 2, MSAT_OPT_SAT_OPTIMAL = 3 }

Optimization Functions
Objectives creation
msat_objective	msat_make_minimize (msat_env e, msat_term term)
	Create the new objective 'min(term)'.
msat_objective	msat_make_minimize_signed (msat_env e, msat_term term)
	Create the new objective 'min(term)'. The goal is interpreted as signed if it is of BV type.
msat_objective	msat_make_maximize (msat_env e, msat_term term)
	Create the new objective 'max(term)'.
msat_objective	msat_make_maximize_signed (msat_env e, msat_term term)
	Create the new objective 'max(term)'. The goal is interpreted as signed if it is of BV type.
msat_objective	msat_make_minmax (msat_env e, size_t len, msat_term terms[])
	Create the new objective 'min(max(term0), ..., max(termN))'.
msat_objective	msat_make_minmax_signed (msat_env e, size_t len, msat_term terms[])
	Create the new objective 'min(max(term0), ..., max(termN))'. The goal is interpreted as signed if it is of BV type.
msat_objective	msat_make_maxmin (msat_env e, size_t len, msat_term terms[])
	Create the new objective 'max(min(term0), ..., min(termN))'.
msat_objective	msat_make_maxmin_signed (msat_env e, size_t len, msat_term terms[])
	Create the new objective 'max(min(term0), ..., min(termN))'. The goal is interpreted as signed if it is of BV type.
int	msat_assert_objective (msat_env e, msat_objective o)
	Push an objective on the internal stack of objectives
int	msat_destroy_objective (msat_env e, msat_objective o)
	Destroy an objective.
int	msat_assert_soft_formula (msat_env e, msat_term term, msat_term weight, const char *id)
	Associate a weight to a term declaration with respect to a MaxSMT group identified by a common id label. Assert-soft constraints are ineffective unless the id label is used by an objective that is pushed on the stack.
int	msat_load_objective_model (msat_env e, msat_objective obj)
	Load into memory the model associated with the objective, provided that there exists a solution.
Objectives iteration
msat_objective_iterator	msat_create_objective_iterator (msat_env e)
	Create an objective iterator. Allowed only after an ::msat_solve call.
int	msat_objective_iterator_has_next (msat_objective_iterator i)
	Checks whether i can be incremented.
int	msat_objective_iterator_next (msat_objective_iterator i, msat_objective *o)
	Returns the next objective on the stack, and increments the given iterator.
void	msat_destroy_objective_iterator (msat_objective_iterator i)
	Destroys an objective iterator.
Functions for objective state inspection
msat_opt_result	msat_objective_result (msat_env e, msat_objective o)
	Returns the optimization search state of the given objective.
msat_term	msat_objective_get_term (msat_env e, msat_objective o)
	Returns the term which is optimized by the objective.
msat_objective_type	msat_objective_get_type (msat_env e, msat_objective o)
	Returns the objective optimization type (min or max).
msat_model	msat_get_model (msat_env e, msat_objective obj)
	Returns the model associated with a given objective (if any).
char *	msat_objective_get_search_stats (msat_env e, msat_objective o)
	Returns optimization search statistics.
int	msat_objective_value_is_unbounded (msat_env e, msat_objective o, msat_objective_value i)
	Determines if the given objective value is unbounded.
int	msat_objective_value_is_plus_inf (msat_env e, msat_objective o, msat_objective_value i)
	Determines if the given objective value is +INF.
int	msat_objective_value_is_minus_inf (msat_env e, msat_objective o, msat_objective_value i)
	Determines if the given objective value is -INF.
int	msat_objective_value_is_strict (msat_env e, msat_objective o, msat_objective_value i)
	Determines if the given objective value is strict.
int	msat_objective_value_get_epsilon (msat_env e, msat_objective o, msat_objective_value i)
	Returns the value of epsilon of a strict objective value.
msat_term	msat_objective_value_term (msat_env e, msat_objective o, msat_objective_value i, msat_term inf, msat_term eps)
	Returns term representation of the given objective value.

Detailed Description

API specific to the OptiMathSAT OMT solver.

Define Documentation

#define MSAT_ERROR_OBJECTIVE ( obj ) ((obj).repr == NULL)

Error checking for objectives.

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

#define MSAT_ERROR_OBJECTIVE_ITERATOR ( objiter ) ((objiter).repr == NULL)

Error checking for objective iterators.

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

Data types and special values

enum msat_objective_value

OptiMathSAT codes for queries on values in objective items.

Enumerator:

MSAT_OPTIMUM	Query the state of the last candidate optimum value found.
MSAT_FINAL_LOWER	Query the state of the final lower bound value.
MSAT_FINAL_UPPER	Query the state of the final upper bound value.
MSAT_FINAL_ERROR	Query the state of the final error value.

enum msat_objective_type

OptiMathSAT objective type, either minimize or maximize.

Enumerator:

MSAT_OBJECTIVE_MINIMIZE	The term with which objective has been created is minimized.
MSAT_OBJECTIVE_MAXIMIZE	The term with which objective has been created is maximized.

enum msat_opt_result

Result of the optimization search for each objective.

Enumerator:

MSAT_OPT_UNKNOWN	Unknown.
MSAT_OPT_UNSAT	Unsat.
MSAT_OPT_SAT_PARTIAL	Sat, partially optimized.
MSAT_OPT_SAT_APPROX	Sat, approximates optimum value.
MSAT_OPT_OPTIMAL	Sat, certified optimal solution.

Optimization Functions

msat_objective msat_make_minimize	(	msat_env	e,
		msat_term	term,
	)

Create the new objective 'min(term)'.

Parameters:

	e	The environment in which to operate.
	term	A generic linear arithmetic term to be minimized.

Returns:: An objective, or a o s.t. ::MSAT_ERROR_OBJECTIVE(o) is true in case of errors.

msat_objective msat_make_minimize_signed	(	msat_env	e,
		msat_term	term,
	)

Create the new objective 'min(term)'. The goal is interpreted as signed if it is of BV type.

Parameters:

	e	The environment in which to operate.
	term	A generic linear arithmetic term to be minimized.

Returns:: An objective, or a o s.t. ::MSAT_ERROR_OBJECTIVE(o) is true in case of errors.

msat_objective msat_make_maximize	(	msat_env	e,
		msat_term	term,
	)

Create the new objective 'max(term)'.

Parameters:

	e	The environment in which to operate.
	term	A generic linear arithmetic term to be maximized.

Returns:: An objective, or a o s.t. ::MSAT_ERROR_OBJECTIVE(o) is true in case of errors.

msat_objective msat_make_maximize_signed	(	msat_env	e,
		msat_term	term,
	)

Create the new objective 'max(term)'. The goal is interpreted as signed if it is of BV type.

Parameters:

	e	The environment in which to operate.
	term	A generic linear arithmetic term to be maximized.

Returns:: An objective, or a o s.t. ::MSAT_ERROR_OBJECTIVE(o) is true in case of errors.

msat_objective msat_make_minmax	(	msat_env	e,
		size_t	len,
		msat_term	terms[],
	)

Create the new objective 'min(max(term0), ..., max(termN))'.

Parameters:

	e	The environment in which to operate.
	len	The size of terms.
	terms	The array of terms to be optimized.

Returns:: An objective, or a o s.t. ::MSAT_ERROR_OBJECTIVE(o) is true in case of errors.

msat_objective msat_make_minmax_signed	(	msat_env	e,
		size_t	len,
		msat_term	terms[],
	)

Create the new objective 'min(max(term0), ..., max(termN))'. The goal is interpreted as signed if it is of BV type.

Parameters:

	e	The environment in which to operate.
	len	The size of terms.
	terms	The array of terms to be optimized.

Returns:: An objective, or a o s.t. ::MSAT_ERROR_OBJECTIVE(o) is true in case of errors.

msat_objective msat_make_maxmin	(	msat_env	e,
		size_t	len,
		msat_term	terms[],
	)

Create the new objective 'max(min(term0), ..., min(termN))'.

Parameters:

	e	The environment in which to operate.
	len	The size of terms.
	terms	The array of terms to be optimized.

Returns:: An objective, or a o s.t. ::MSAT_ERROR_OBJECTIVE(o) is true in case of errors.

msat_objective msat_make_maxmin_signed	(	msat_env	e,
		size_t	len,
		msat_term	terms[],
	)

Create the new objective 'max(min(term0), ..., min(termN))'. The goal is interpreted as signed if it is of BV type.

Parameters:

	e	The environment in which to operate.
	len	The size of terms.
	terms	The array of terms to be optimized.

Returns:: An objective, or a o s.t. ::MSAT_ERROR_OBJECTIVE(o) is true in case of errors.

int msat_assert_objective	(	msat_env	e,
		msat_objective	o
	)

Push an objective on the internal stack of objectives.

Parameters:

	e	The environment in which to operate.
	o	The objective to be pushed.

Returns:: zero on success, nonzero on error.

int msat_destroy_objective	(	msat_env	e,
		msat_objective	o
	)

Destroys an objective.

Parameters:

	e	The environment in which to operate.
	o	The objective to be destroyed.

Returns:: zero on success, nonzero on error.

int msat_assert_soft_formula	(	msat_env	e,
		msat_term	term,
		msat_term	weight,
		const char *	id
	)

Associate a weight to a term declaration with respect to a MaxSMT group identified by a common id label. Assert-soft constraints are ineffective unless the id label is used by an objective that is pushed on the stack.

Parameters:

	e	The environment in which to operate.
	term	The term to which a weight is attached.
	weight	The weight of not satisfying this soft-clause, must be of a Real or Integer number.
	id	The MaxSMT sum onto which the weight contribution is added.

Returns:: zero on success, nonzero on error.

msat_objective_iterator msat_create_objective_iterator	(	msat_env	e
	)

Creates an objective iterator. It can only be used after an ::msat_solve call and prior to any further call to msat_assert_formula/msat_push/msat_pop or other functions for creating objectives.

Parameters:

The environment in which to operate.

Returns:: an iterator for the current stack of objectives.

int msat_objective_iterator_has_next	(	msat_objective_iterator	i
	)

Checks whether i can be incremented.

Parameters:

An objective stack iterator.

Returns:: nonzero if i can be incremented, zero otherwise.

int msat_objective_iterator_next	(	msat_objective_iterator	i,
		msat_objective *	o
	)

Returns the next objective on the stack, and increments the given iterator.

Parameters:

	i	The objective iterator to increment.
	o	Output value for the next objective on the stack.

Returns:: zero on success, nonzero on error.

void msat_destroy_objective_iterator	(	msat_objective_iterator	i
	)

Destroys an objective iterator.

Parameters:

The objective iterator to destroy.

msat_opt_result msat_objective_result	(	msat_env	e,
		msat_objective	o
	)

Returns the optimization search state of the given objective.

Possible values:

MSAT_OPT_UNKNOWN: the objective was not optimized, or the optimization search was interrupted before it could find a solution.
MSAT_OPT_UNSAT: the objective is unsatisfiable.
MSAT_OPT_SAT_PARTIAL: the optimization search was not completed, but a partially optimized solution was found.
MSAT_OPT_SAT_APPROX: the optimization search completed with an approximate solution.
MSAT_OPT_SAT_OPTIMAL: the optimization search completed with a certified optimum value.

Parameters:

	e	The environment in which to operate.
	o	The objective.

Returns:: a msat_opt_result value.

msat_term msat_objective_get_term	(	msat_env	e,
		msat_objective	o
	)

Returns the term which is optimized by the objective.

Parameters:

	e	The environment in which to operate.
	o	The objective.

Returns:: msat_term representation of the objective function.

msat_objective_type msat_objective_get_type	(	msat_env	e,
		msat_objective	o
	)

Returns the objective optimization type (min or max).

Parameters:

	e	The environment in which to operate.
	o	The objective.

Returns:: MSAT_OBJECTIVE_MINIMIZE or MSAT_OBJECTIVE_MAXIMIZE.

int msat_load_objective_model	(	msat_env	e,
		msat_objective	o
	)

Load into memory the model associated with the given objective, provided that there exists a solution.

Notes:

The option produce-models must be set to true to enable model generation.
A model is associated with an objective by calling msat_solve() and is destroyed with subsequent calls to msat_push/msat_pop/msat_assert_formula/msat_assert_soft_formula

Parameters:

	e	The environment in which to operate.
	o	The objective.

Returns:: zero on success, nonzero on error.

msat_model msat_get_model	(	msat_env	e,
		msat_objective	o
	)

Returns the model associated with the given objective (if any).

Parameters:

	e	The environment in which to operate.
	o	The objective.

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

char * msat_objective_get_search_stats	(	msat_env	e,
		msat_objective	o
	)

Returns optimization search statistics.

Parameters:

	e	The environment in which to operate.
	term	The cost function to match.
	select	The rule to be used to match the model, defaults to MSAT_ANY_MODEL.

Returns:: A string which provides some search statistics information on the optimization search of the given objective, or NULL on error. The string must be deallocated by the user with msat_free().

int msat_objective_value_is_unbounded	(	msat_env	e,
		msat_objective	o,
		msat_objective_value	i
	)

Determines if the given objective value is unbounded.

Parameters:

	e	The environment in which to operate.
	o	The objective providing the value.
	i	The objective field to be tested.

Returns:: 1 if unbounded, 0 if not, -1 on error.

int msat_objective_value_is_plus_inf	(	msat_env	e,
		msat_objective	o,
		msat_objective_value	i
	)

Determines if the given objective value is +INF.

Parameters:

	e	The environment in which to operate.
	o	The objective providing the value.
	i	The objective field to be tested.

Returns:: 1 if +INF, 0 if not, -1 on error.

int msat_objective_value_is_minus_inf	(	msat_env	e,
		msat_objective	o,
		msat_objective_value	i
	)

Determines if the given objective value is -INF.

Parameters:

	e	The environment in which to operate.
	o	The objective providing the value.
	i	The objective field to be tested.

Returns:: 1 if -INF, 0 if not, -1 on error.

int msat_objective_value_is_strict	(	msat_env	e,
		msat_objective	o,
		msat_objective_value	i,
	)

Determines if the given objective value is strict.

Example:

if term(o,i) = k and strict(o,i) = TRUE, then the actual value of 'i' is k+epsilon, where epsilon is any small positive value.

Parameters:

	e	The environment in which to operate.
	o	The objective providing the value.
	i	The objective field to be tested.

Returns:: 1 if strict, 0 if not, -1 on error.

int msat_objective_value_get_epsilon	(	msat_env	e,
		msat_objective	o,
		msat_objective_value	i,
	)

Returns the value of epsilon of a strict objective value.

Example:

if term(o,i) = k and strict(o,i) = TRUE, then the actual value of 'i' is k+epsilon, where epsilon is any small positive value.

Parameters:

	e	The environment in which to operate.
	o	The objective providing the value.
	i	The objective field to be tested.

Returns:: 1 if value equal to k + epsilon, -1 if value equal to k - epsilon and 0 otherwise.

int msat_objective_value_term	(	msat_env	e,
		msat_objective	o,
		msat_objective_value	i,
		msat_term	fin,
		msat_term	eps
	)

Returns the term representation of the given objective value.

Parameters:

	e	The environment in which to operate.
	o	The objective providing the value.
	i	The objective field to retrieve.
	fin	The symbol / positive value representing infinity. If equal to MSAT_ERROR_TERM, OptiMathSAT picks his own value.
	eps	The symbol / positive value representing epsilon. If equal to MSAT_ERROR_TERM, OptiMathSAT picks his own value.

Returns:: a term represanting the objective value, or msat_error_term on error.

OptiMathSAT

An Optimization Modulo Theories (OMT) tool

OptiMathSAT (>= 1.6.0) C API Reference

Data types and special values

Optimization Functions

Detailed Description

Define Documentation

Data types and special values

Optimization Functions