OptiMathSAT

An Optimization Modulo Theories (OMT) tool

OptiMathSAT (>= 1.5.1) 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.
enum  msat_objective_value { MSAT_OPTIMUM = 0, MSAT_INITIAL_LOWER = 1, MSAT_INITIAL_UPPER = 2, MSAT_FINAL_LOWER = 3, MSAT_FINAL_UPPER = 4, MSAT_FINAL_ERROR = 5 }
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_push_minimize (msat_env e, msat_term term, msat_term lower, msat_term upper, bool bvsigned = false)
 Push on the stack the new objective 'min(term)' with optional optimization local interval [lower, upper[.
msat_objective msat_push_maximize (msat_env e, msat_term term, msat_term lower, msat_term upper, bool bvsigned = false)
 Push on the stack the new objective 'max(term)' with optional optimization local interval ]lower, upper].
msat_objective msat_push_minmax (msat_env e, size_t len, msat_term terms[], msat_term lower, msat_term upper, bool bvsigned = false)
 Push on the stack the new objective 'min(max(term0), ..., max(termN))' with optional optimization local interval ]lower, upper].
msat_objective msat_push_maxmin (msat_env e, size_t len, msat_term terms[], msat_term lower, msat_term upper, bool bvsigned = false)
 Push on the stack the new objective 'max(min(term0), ..., min(termN))' with optional optimization local interval [lower, upper[.
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_set_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, int &d)
 Determines if the given objective value is stric..
msat_term msat_objective_value_term (msat_env e, msat_objective o, msat_objective_value i, bool fin = false, bool eps = false)
 Returns term representation of the given objective value.
char * msat_objective_value_repr (msat_env e, msat_objective o, msat_objective_value i)
 Returns a string 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

OptiMathSAT codes for queries on values in objective items.

Enumerator:
MSAT_OPTIMUM 

Query the state of the last candidate optimum value found.

MSAT_INITIAL_LOWER 

Query the state of the initial lower bound value.

MSAT_INITIAL_UPPER 

Query the state of the initial upper bound value.

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.

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.

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_push_minimize ( msat_env  e,
msat_term term,
msat_term lower,
msat_term upper,
bool bvsigned = false
 ) 

Push on the stack the new objective 'min(term)' with optional optimization local interval [lower, upper[.

Parameters:
e The environment in which to operate.
term A generic linear arithmetic term to be minimized.
lower A constant-valued term corresponding to the local search interval lower bound. An error term is interpreted as -inf.
upper A constant-valued term corresponding to the local search interval upper bound. An error term is interpreted as +inf.
bvsigned Optional parameter, true iff term is a signed BV objective.
Returns:
An objective, or a o s.t. ::MSAT_ERROR_OBJECTIVE(o) is true in case of errors.
msat_objective msat_push_maximize ( msat_env  e,
msat_term term,
msat_term lower,
msat_term upper,
bool bvsigned = false
 ) 

Push on the stack the new objective 'max(term)' with optional optimization local interval ]lower, upper].

Parameters:
e The environment in which to operate.
term A generic linear arithmetic term to be maximized.
lower A constant-valued term corresponding to the local search interval lower bound. An error term is interpreted as -inf.
upper A constant-valued term corresponding to the local search interval upper bound. An error term is interpreted as +inf.
bvsigned Optional parameter, true iff term is a signed BV objective.
Returns:
An objective, or a o s.t. ::MSAT_ERROR_OBJECTIVE(o) is true in case of errors.
msat_objective msat_push_minmax ( msat_env  e,
size_t len,
msat_term terms[],
msat_term lower,
msat_term upper,
bool bvsigned = false
 ) 

Push on the stack the new objective 'min(max(term0), ..., max(termN))' with optional optimization local interval ]lower, upper].

Parameters:
e The environment in which to operate.
len The size of terms.
terms The array of terms to be optimized.
lower A constant-valued term corresponding to the local search interval lower bound. An error term is interpreted as -inf.
upper A constant-valued term corresponding to the local search interval upper bound. An error term is interpreted as +inf.
bvsigned Optional parameter, true iff term is a signed BV objective.
Returns:
An objective, or a o s.t. ::MSAT_ERROR_OBJECTIVE(o) is true in case of errors.
msat_objective msat_push_maxmin ( msat_env  e,
size_t len,
msat_term terms[],
msat_term lower,
msat_term upper,
bool bvsigned = false
 ) 

Push on the stack the new objective 'max(min(term0), ..., min(termN))' with optional optimization local interval [lower, upper[.

Parameters:
e The environment in which to operate.
len The size of terms.
terms The array of terms to be optimized.
lower A constant-valued term corresponding to the local search interval lower bound. An error term is interpreted as -inf.
upper A constant-valued term corresponding to the local search interval upper bound. An error term is interpreted as +inf.
bvsigned Optional parameter, true iff term is a signed BV objective.
Returns:
An objective, or a o s.t. ::MSAT_ERROR_OBJECTIVE(o) is true in case of errors.
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:
e 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:
i 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:
i 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_set_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,
int &d
 ) 

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.
d Output parameter, it contains the delta component associated with the objective.
Returns:
1 if strict, 0 if not, -1 on error.
int msat_objective_value_term ( msat_env  e,
msat_objective o,
msat_objective_value i,
bool fin = false,
bool eps = false
 ) 

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 If true, a finite representation is returned for any infintie value instead of MSAT_ERROR_TERM.
eps If true, a finite representation of the epsilon component is added to any strict value before returning it instead of being ignored.
Returns:
a term represanting the objective value, or msat_error_term on error.
int msat_objective_value_repr ( msat_env  e,
msat_objective o,
msat_objective_value i
 ) 

Returns a string 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.
Returns:
a string which represent the given objective value, or NULL on error. The string must be deallocated by the user with msat_free().