OptiMathSAT

An Optimization Modulo Theories (OMT) tool

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_INITIAL_LOWER = 1, MSAT_INITIAL_UPPER = 2, MSAT_FINAL_LOWER = 3, MSAT_FINAL_UPPER = 4, MSAT_FINAL_ERROR = 5, MSAT_FINAL_TOLERANCE = 6 }
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, msat_term lower, msat_term upper)
 Create the new objective 'min(term)' with optional optimization local interval [lower, upper[.
msat_objective msat_make_minimize_signed (msat_env e, msat_term term, msat_term lower, msat_term upper)
 Create the new objective 'min(term)' with optional optimization local interval [lower, upper[. The goal is interpreted as signed if it is of BV type.
msat_objective msat_make_maximize (msat_env e, msat_term term, msat_term lower, msat_term upper)
 Create the new objective 'max(term)' with optional optimization local interval ]lower, upper].
msat_objective msat_make_maximize_signed (msat_env e, msat_term term, msat_term lower, msat_term upper)
 Create the new objective 'max(term)' with optional optimization local interval ]lower, upper]. 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[], msat_term lower, msat_term upper)
 Create the new objective 'min(max(term0), ..., max(termN))' with optional optimization local interval ]lower, upper].
msat_objective msat_make_minmax_signed (msat_env e, size_t len, msat_term terms[], msat_term lower, msat_term upper)
 Create the new objective 'min(max(term0), ..., max(termN))' with optional optimization local interval ]lower, upper]. 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[], msat_term lower, msat_term upper)
 Create the new objective 'max(min(term0), ..., min(termN))' with optional optimization local interval [lower, upper[.
msat_objective msat_make_maxmin_signed (msat_env e, size_t len, msat_term terms[], msat_term lower, msat_term upper)
 Create the new objective 'max(min(term0), ..., min(termN))' with optional optimization local interval [lower, upper[. 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

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.

MSAT_FINAL_TOLERANCE 

Query the state of the final tolerance 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_make_minimize ( msat_env  e,
msat_term term,
msat_term lower,
msat_term upper,
 ) 

Create 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.
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,
msat_term lower,
msat_term upper,
 ) 

Create the new objective 'min(term)' with optional optimization local interval [lower, upper[. 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.
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.
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,
msat_term lower,
msat_term upper,
 ) 

Create 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.
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,
msat_term lower,
msat_term upper,
 ) 

Create the new objective 'max(term)' with optional optimization local interval ]lower, upper]. 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.
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.
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[],
msat_term lower,
msat_term upper,
 ) 

Create 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.
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[],
msat_term lower,
msat_term upper,
 ) 

Create the new objective 'min(max(term0), ..., max(termN))' with optional optimization local interval ]lower, upper]. 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.
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.
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[],
msat_term lower,
msat_term upper,
 ) 

Create 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.
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[],
msat_term lower,
msat_term upper,
 ) 

Create the new objective 'max(min(term0), ..., min(termN))' with optional optimization local interval [lower, upper[. 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.
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.
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:
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_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.