Solver Manager

class murxla::SolverManager

Public Functions

void clear(): Clear all data.

Solver &get_solver()

Get solver.

Returns: A reference to the solver (wrapper) instance.

RNGenerator &get_rng() const

Get the associated global random number generator.

Returns: A reference to the RNG instance.

SolverSeedGenerator &get_sng()

Get the associated solver seed generator.

Returns: A reference to the solver seed generator instance.

const TheorySet &get_enabled_theories() const

Get set of enabled theories.

Returns: The set of currently enabled theories.

std::ostream &get_trace()

Get a reference to the trace stream.

Returns: A reference to the trace stream.

void mark_option_used(const std::string &opt)

Mark given option as already configured.

Parameters: opt – The option to mark.

uint64_t get_num_terms_max_level() const

Get the number of created terms in the top scope.

Returns: the number of created terms in the current top scope.

size_t get_num_vars() const

Get the number of available variables.

Returns: The number of available variables.

void add_sort(Sort &sort, SortKind sort_kind, bool parametric = false, bool well_founded = true)

Add sort to sort database.

Parametric sorts are not added to the main database (the database that we pick sorts from), but to a separate database that we only pick from when we explicitly need parametric sorts (see pick_sort_dt_param()).

We only add well founded sorts. A sort that is not well founded gets an id to trace the return statement of mk-sort, but is otherwise discarded.

Parameters

sort – The sort to add to the databse.
sort_kind – The kind of the sort.
parametric – True if given sort has parameter sorts.
well_founded – True if fiven sort is well founded.

void add_value(Term &term, Sort &sort, SortKind sort_kind, const AbsTerm::SpecialValueKind &value_kind = AbsTerm::SPECIAL_VALUE_NONE)

Add value to term database.

Parameters

term – The term to add to the database.
sort – The sort of the term to add.
sort_kind – The sort of the sort of the term to add.
value_kind – The kind of the special value, AbsTerm::SPECIAL_VALUE_NONE if given term is not a special value.

void add_string_char_value(Term &term)

Add string value of length 1.

Parameters: term – A term representing a string value of length 1.

void add_input(Term &term, Sort &sort, SortKind sort_kind)

Add input to term database.

Parameters

term – A term representing an input.
sort – The sort of the term.
sort_kind – The sort of the sort of the term.

void add_var(Term &term, Sort &sort, SortKind sort_kind)

Add var to term database.

Parameters

term – A term representing a variable.
sort – The sort of the term.

void add_const(Term &term, Sort &sort, SortKind sort_kind)

Add const to term database.

Parameters

term – A term representing a constant.
sort – The sort of the term.
sort_kind – The kind of the sort of the term.

void add_term(Term &term, SortKind sort_kind, const std::vector<Term> &args = {})

Add non-input term to term database.

Parameters

term – A term representing anything other than an input
sort_kind – The kind of the sort of the term.
args – The argument terms to the given term.

std::string pick_symbol(const std::string &prefix = "_x")

Pick arbitrary symbol (simple or piped). Simple symbols are generated as <prefix><id>.

Parameters: prefix – The prefix of the symbol.
Returns: An arbitrary symbol.

SortKind pick_sort_kind(bool with_terms = true)

Pick sort kind of existing (= created) sort.

Optionally restrict selection to sort kinds with terms only if with_terms is true.

Note

This excludes parametric datatype sorts.

Parameters: with_terms – True to only pick sort kinds of a sort for which we have already created terms.
Returns: The sort kind.

SortKind pick_sort_kind(const SortKindSet &sort_kinds, bool with_terms = true)

Pick sort kind of existing (= created) sort out of given set of sort kinds. Asserts that a sort of any of the given kinds exists.

Optionally restrict selection to sort kinds with terms only if with_terms is true.

Note

This excludes parametric datatype sorts.

Parameters

sort_kinds – The set of sort kinds to pick from.
with_terms – True to only pick sort kinds of a sort for which we have already created terms.

Returns

The sort kind.

SortKind pick_sort_kind_excluding(const SortKindSet &exclude_sort_kinds, bool with_terms = true) const

Pick a sort kind of existing (= created) sort, excluding the given sort kinds.

Optionally restrict selection to sort kinds with terms only if with_terms is true.

Note

This excludes parametric datatype sorts.

Parameters

exclude_sort_kinds – The sort kinds to exclude.
with_terms – True to only pick sort kinds of a sort for which we have already created terms.

Returns

The sort kind.

SortKind pick_sort_kind(uint32_t level, const SortKindSet &exclude_sort_kinds)

Pick sort kind of existing (= created) sort with terms at given level.

Optionally, exclude given sort kinds.

Note

This excludes parametric datatype sorts.

Parameters

level – The scope level of existing terms to pick the sort kind from.
exclude_sort_kinds – The sort kinds to exclude.

Returns

The sort kind.

SortKindData &pick_sort_kind_data()

Pick enabled sort kind (and get its data).

Only sort kinds of enabled theories are picked. This function does not guarantee that a sort of this kind alreay exists.

Note

This excludes parametric datatype sorts.

Returns: The sort kind.

Op::Kind pick_op_kind(bool with_terms = true, SortKind sort_kind = SORT_ANY)

Pick enabled operator kind (and get its data).

Optionally restricted to operator kinds that create terms of given sort kind.

Only operator kinds of enabled theories are picked.

Parameters

with_terms – True to only pick operator kinds of already created terms.
The – sort kind of terms of the operator kind to select.

Returns

The operator kind.

Op &get_op(const Op::Kind &kind)

Get the Op data for given operator kind.

Parameters: kind – The operator kind.
Returns: The configuration data of the operator.

Term pick_value()

Pick a value of any sort.

Note

Requires that a value of any sort exists.

Returns: The value.

Term pick_value(Sort sort)

Pick a value of given sort.

Note

Requires that a value of given sort exists.

Parameters: sort – The sort of the value to pick.
Returns: The value.

Term pick_string_char_value()

Pick string value with length 1.

Returns: A term representing a string value of length 1.

Term pick_term(Sort sort)

Pick a term of given sort.

Note

Requires that terms of this sort exist.

Parameters: sort – The sort of the term to pick.
Returns: The term.

Term pick_term(SortKind sort_kind, size_t level)

Pick term of given sort kind and scope level.

Note

Requires that terms of this sort kind exist.

Parameters

sort_kind – The kind of the sort of the term to pick.
level – The scope level of the term to pick.

Returns

The term.

Term pick_term(SortKind sort_kind)

Pick term of given sort kind.

Note

Requires that terms of this sort kind exist.

Parameters: sort_kind – The kind of the sort of the term to pick.
Returns: The term.

Term pick_term()

Pick any term.

Note

Requires that terms of any sort kind exist.

Returns: The term.

Term pick_term(size_t level)

Pick any term from given level.

Note

Requires that terms of any sort kind exist.

Parameters: level – The scope level of the term to pick.
Returns: The term.

Term pick_term_min_level(Sort sort, size_t level)

Pick any term from any level from the given level to the max level.

Note

Requires that terms of any sort kind exist.

Parameters: level – The scope level of the term to pick.
Returns: The term.

Term pick_fun(const std::vector<Sort> &domain_sorts)

Pick function term with given domain sorts.

Note

Requires that such terms exist.

Parameters: domain_sorts – The sorts of the domain of the function to pick.
Returns: A term representing a function.

Term pick_var()

Pick variable from current scope level.

Note

Requires that a variable exists.

Returns: A term representing a variable.

std::vector<Term> pick_vars(size_t num_vars) const

Pick num_vars variables.

Note

Requires that at least num_vars variables exist.

Parameters: num_vars – The number of variables to pick.
Returns: A vector with the picked variables.

void remove_var(const Term &var)

Remove variable from current scope level.

Note

Must be called before calling add_term.

Parameters: var – The variable to remove.

Term pick_quant_body()

Pick Boolean term from current scope level.

Returns: The term.

Term pick_quant_term()

Pick term of any sort from current scope level.

Returns: The term.

Term pick_quant_term(Sort sort)

Pick term of given sort from current scope level.

Returns: The term.

void add_assumption(Term t)

Add given term to the set of currently assumed assumptions.

Parameters: t – The assumption to cache.

Term pick_assumed_assumption()

Pick assumption out of the set of currently assumed assumptions.

Note

Requires that d_assumptions is not empty.

Returns: A term representing an assumptions.

void reset(): Reset solver manager state into start mode.

void reset_sat()

Reset solver manager state into assert mode.

After this call, calling

get_unsat_assumptions()
get_unsat_core() and is not possible until after the next SAT call.

bool has_value() const

Determine if term database contains any value of any sort.

Returns: True if term database contains any value of any sort.

bool has_value(Sort sort) const

Determine if term database contains any value of given sort.

Returns: True if term database contains any value of given sort.

bool has_string_char_value() const

Determine if we already created string values with length 1.

Returns: True if we already created string values with length 1.

bool has_term() const

Determine if term database contains any term.

Returns: True if term database contains any term.

bool has_term(size_t level) const

Determine if term database contains any term on given level.

Parameters: level – The scope level to query for terms.
Returns: True if term database contains any term on given level.

bool has_term(SortKind sort_kind, size_t level) const

Determine if term database contains any term of given sort kind at given level.

Parameters

sort_kind – The sort kind of the terms to query for.
level – The scope level to query for terms.

Returns

True if term database contains any term of given sort kind at given level.

bool has_term(SortKind sort_kind) const

Determine if term database contains any term of given sort kind.

Parameters: sort_kind – The sort kind of the terms to query for.
Returns: true if term database contains any term of given sort kind.

bool has_term(const SortKindSet &sort_kinds) const

Determine if term database contains any term of one of the given sort kinds.

Parameters: sort_kind – The sort kind of the terms to query for.
Returns: True if term database contains any term of one of the given sort kinds.

bool has_term(Sort sort) const

Determine if term database contains any term of given sort.

Parameters: sort – The sort of the terms to query for.
Returns: true if term database contains any term of given sort.

bool has_assumed() const

Determine if d_assumptions is not empty.

Returns: True if d_assumptions is not empty.

bool has_fun(const std::vector<Sort> &domain_sorts) const

Determine if term database contains a function term with given domain sorts.

Parameters: domain_sorts – The domain sorts of the function to query for.
Returns: True if term database contains a function term with given domain sorts.

bool has_var() const

Determine if term database contains a variable.

Returns: true if term database contains a variable.

bool has_quant_body() const

Determine if term database contains a variable and a Boolean term in the current scope level.

Returns: True if term database contains a variable and a Boolean term in the current scope level.

bool has_quant_term() const

Determine if term database contains a variable and a term of any sort in the current scope level.

Returns: True if term database contains a variable and a term of any sort in the current scope level.

bool has_quant_term(Sort sort) const

Determine if term database contains a variable and a term of given sort in the current scope level.

Returns: True if term database contains a variable and a term of given sort in the current scope level.

Term find_term(Term term, Sort sort, SortKind sort_kind)

Find the Term in the Term database that wraps the same solver term with the given sort and sort kind.

Note

We need this for Terms returned by the solver that are only wrapped solver terms without sort information.

Returns: A nullptr if given Term is not in the term database.

Term get_term(uint64_t id) const

Get the term with the given id.

Parameters: id – The id of the term.
Returns: The term with the given id.

Term get_untraced_term(uint64_t id) const

Get the untraced term with the given id.

Parameters: id – The id of the term.
Returns: The untraced term with the given id.

Sort pick_sort()

Pick sort.

It is not guaranteed that there exist terms of the returned sort.

Note

This excludes parametric datatype sorts.

Returns: The sort.

Sort pick_sort_with_sort_params()

Pick sort that has sort parameters.

It is not guaranteed that there exist terms of the returned sort.

Note

This includes (parametric) datatype sorts.

Returns: The sort.

Sort pick_sort(SortKind sort_kind, bool with_terms = true)

Pick sort of given sort kind.

Optionally restrict selection to sorts with terms only if with_terms is true.

Note

This excludes parametric datatype sorts.

Parameters

sort_kind – The sort_kind of the sort to pick.
with_terms – True to restrict to sorts with already created terms.

Returns

The sort.

Sort pick_sort(const SortKindSet &sort_kinds, bool with_terms = true)

Pick sort of any of the given sort kinds.

Optionally restrict selection to sorts with terms only if with_terms is true.

Parameters

sort_kinds – The set of sort kinds to pick from.
with_terms – True to restrict to sorts with already created terms.

Returns

This excludes parametric datatype sorts.

Sort pick_sort_excluding(const SortKindSet &exclude_sort_kinds, bool with_terms = true)

Pick sort, excluding sorts of kinds included in exclude_sort_kinds.

It is not guaranteed that there exist terms of the returned sort.

Parameters

exclude_sort_kinds – The sort kinds to exclude.
with_terms – True to restrict to sorts with already created terms.

Returns

This excludes parametric datatype sorts.

Sort pick_sort_bv(uint32_t bw, bool with_terms = true)

Pick bit-vector sort with given bit-width.

Optionally restrict selection to sorts with terms only if with_terms is true.

Parameters

bw – The bit-width of the bit-vector sort to pick.
with_terms – True to restrict to sorts with already created terms.

Returns

The sort.

Sort pick_sort_bv_max(uint32_t bw_max, bool with_terms = true)

Pick bit-vector sort with given maximum bit-width.

Optionally restrict selection to sorts with terms only if with_terms is true.

Parameters

bw_max – The maximum bit-width (incl.) of the bit-vector sort to pick.
with_terms – True to restrict to sorts with already created terms.

Returns

The sort.

Sort pick_sort_dt_param()

Pick parametric datatypes sort.

Returns: The sort.

bool has_sort() const

Determine if any sort has been created.

This does not guarantee that any terms have been created.

Note

This excludes parametric datatype sorts.

Returns: True if any sort has been created.

bool has_sort(SortKind sort_kind) const

Determine if a sort of given kind exists.

This does not guarantee that any terms of this sort have been created.

Note

This excludes parametric datatype sorts.

Parameters: sort_kind – The sort kind to check for created sorts.
Returns: True if a sort of given kind exists.

bool has_sort(const SortKindSet &sort_kinds) const

Determine if a sort of any of the given kinds exists.

This does not guarantee that any terms of these sorts have been created.

Note

This excludes parametric datatype sorts.

Parameters: sort_kinds – The sort kinds to check for created sorts.
Returns: True if a sort of any of the given kinds exists.

bool has_sort(Sort sort) const

Determine if given sort already exists.

This does not guarantee that any terms of this sort have been created.

Returns: sort The sort to query for.
Returns: True if given sort already exists.

bool has_sort_excluding(const std::unordered_set<SortKind> &exclude_sort_kinds, bool with_terms = true) const

Determine if sorts of a kind other than the kinds given in exclude_sort_kinds have been created.

Optionally restrict selection to sorts with terms only if with_terms is true.

Note

This excludes parametric datatype sorts.

Parameters

exclude_sort_kinds – The sort kinds to exclude.
with_terms – True to restrict to sorts with already created terms.

Returns

True if sort of a kind other than the given kinds have been created.

bool has_sort_excluding(uint32_t level, const std::unordered_set<SortKind> &exclude_sort_kinds) const

Determine if terms with sorts of a kind other than the kinds given in exclude_sort_kinds at the given scope level have been created.

Parameters

level – The scope level.
exclude_sort_kinds – The sort kinds to exclude.

Returns

True if terms with sorts of a kind other than the kinds given in exclude_sort_kinds have been created.

bool has_sort_with_sort_params() const

Determine if sorts that have sort parameters have been created.

Note

This includes non-parametric datatypes.

Returns: True if sorts that have sort parameters have been created.

bool has_sort_bv(uint32_t bw, bool with_terms = true) const

Determine if a bit-vector sort with given bit-width exists.

Optionally restrict selection to sorts with terms only if with_terms is true.

Returns: True if a bit-vector sort with given bit-width exists.

bool has_sort_bv_max(uint32_t bw_max, bool with_terms = true) const

Determine if a bit-vector sort up to given maximum bit-width exists.

Optionally restrict selection to sorts with terms only if with_terms is true.

Returns: True if a bit-vector sort up to given maximum bit-width exists.

bool has_sort_dt_parametric() const

Determine if a parametric datatypes sort exists.

Returns: True if a parametric datatypes sort exists.

Sort get_untraced_sort(uint64_t id) const

Get the untraced sort with the given id.

Returns: The untraced sort with the given id.

Sort find_sort(Sort sort) const

Find a matching sort for the given sort in the sort database d_sorts.

Parameters: sort – The sort to find.
Returns: The sort cached in d_sorts, if found, else the given sort.

std::pair<std::string, std::string> pick_option(std::string name = "", std::string value = "")

Pick an option and an option value.

If either are given, enforce option or value. If no option or the given option / value can be set, return empty pair.

Parameters

name – The option name.
value – The option value.

Returns

A pair of picked option name and value.

void clear_assumptions(): Clear cached set of assumptions.

void add_option(SolverOption *opt)

Add solver option.

Parameters: opt – The solver option to add.

void report_result(Solver::Result res)

Report solver result to solver manager.

Parameters: res – The solver result.

SolverProfile &get_profile()

Get the currently configured solver profile.

Returns: The solver profile.

Public Members

Stats d_stats: Statistics.

bool d_arith_linear = false: True to restrict arithmetic operators to linear fragment.

bool d_simple_symbols = false: True if all symbols for terms should be of the form ‘_sX’ rather than a random string.

bool d_incremental = false: True if incremental solving is enabled. (SMT-LIB: option :incremental).

bool d_model_gen = false: True if model generation is enabled. (SMT-LIB: option :produce-models).

bool d_unsat_assumptions = false: True if producing unsat assumptions is enabled. (SMT-LIB: option :produce-unsat-assumptions).

bool d_unsat_cores = false: True if producing unsat cores is enabled. (SMT-LIB: option :produce-unsat-cores).

uint32_t d_n_push_levels = 0: The number of scope levels previously pushed.

bool d_sat_called = false: True if a previous check-sat call is still “active”, i.e., if no formulas have been asserted or assumed since. While true it is save to check failed assumptions and query model values.

Solver::Result d_sat_result = Solver::Result::UNKNOWN : The result of the previous sat call.

uint32_t d_n_sat_calls = 0: The number of check-sat calls issued.

statistics::Statistics *d_mbt_stats: A pointer to the murxla-level statistics object.

struct Stats