OptiMathSAT

An Optimization Modulo Theories (OMT) tool

OptiMathSAT (>= 1.3.8) 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.

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 }

Optimization Functions

Objectives creation
msat_objective msat_push_minimize (msat_env e, msat_term term, const char *lower, const char *upper)
 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, const char *lower, const char *upper)
 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[], const char *lower, const char *upper)
 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[], const char *lower, const char *upper)
 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_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).
int msat_set_model (msat_env e, msat_objective o)
 Load into memory the model associated with the given objective.
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.
msat_term msat_objective_value_term (msat_env e, msat_objective o, msat_objective_value i)
 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.


Optimization Functions

msat_objective msat_push_minimize ( msat_env  e,
msat_term term,
const char * lower,
const char * upper
 ) 

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 string-encoded number corresponding to the local search interval lower bound. If it is an empty string or NULL then its value defaults to -inf.
upper A string-encoded number corresponding to the local search interval upper bound. If it is an empty string or NULL then its value defaults to +inf.
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,
const char * lower,
const char * upper
 ) 

Push on the stack the new objective 'min(-1 * 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 string-encoded number corresponding to the local search interval lower bound. If it is an empty string or NULL then its value defaults to -inf.
upper A string-encoded number corresponding to the local search interval upper bound. If it is an empty string or NULL then its value defaults to +inf.
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[],
const char * lower,
const char * upper
 ) 

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 string-encoded number corresponding to the local search interval lower bound. If it is an empty string or NULL then its value defaults to -inf.
upper A string-encoded number corresponding to the local search interval upper bound. If it is an empty string or NULL then its value defaults to +inf.
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[],
const char * lower,
const char * upper
 ) 

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 string-encoded number corresponding to the local search interval lower bound. If it is an empty string or NULL then its value defaults to -inf.
upper A string-encoded number corresponding to the local search interval upper bound. If it is an empty string or NULL then its value defaults to +inf.
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, assumed to be a positive 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_result msat_objective_result ( msat_env  e,
msat_objective o
 ) 

Returns the optimization search state of the given objective.

Possible values:

  • MSAT_SAT: the optimization search is complete and the optimum value certified.
  • MSAT_UNKNOWN: the optimization search has been interrupted due to some event (e.g. error, timed search) or the objective has not yet been optimized. The optimum value and its associated model can be sub-optimal.
  • MSAT_UNSAT: the objective is unsatisfiable.

Parameters:
e The environment in which to operate.
o The objective.
Returns:
a msat_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.
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_term ( msat_env  e,
msat_objective o,
msat_objective_value i
 ) 

Returns the term representation of the given objective value.

Notes:

  • The representation is a not-included lower bound if msat_objective_value is MSAT_OPTIMUM, the objective was minimized and such value is strict.
  • The representation is a not-included upper bound if msat_objective_value is MSAT_OPTIMUM, the objective was maximized and such value is strict.
  • For any other objective value, the representation is always precise.

Parameters:
e The environment in which to operate.
o The objective providing the value.
i The objective field to retrieve.
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().