Solver Wrapper Interface: Solver

class Solver

The abstract base class for the solver implementation.

A solver wrapper must implement a solver-specific solver wrapper class derived from this class.

Subclassed by murxla::shadow::ShadowSolver, murxla::smt2::Smt2Solver

Public Types

enum Result

The result of a satisfiability check.

Values:

enumerator UNKNOWN

enumerator SAT

enumerator UNSAT

enum Base

The numerical base of a string representing a number.

Values:

enumerator BIN: binary

enumerator DEC: decimal

enumerator HEX: hexa-decimal

using OpKindSortKindMap = std::unordered_map<Op::Kind, SortKindSet>: Map operator kind to a set of sort kinds.

Public Functions

Solver(SolverSeedGenerator &sng)

Constructor.

Parameters:: sng – The associated solver seed generator.

Solver() = delete: Default constructor is deleted.

virtual ~Solver() = default: Default destructor is deleted.

virtual void new_solver() = 0: Create and initialize wrapped solver.

virtual void delete_solver() = 0: Delete wrapped solver.

virtual bool is_initialized() const = 0

Determine if the wrapped solver is initialized.

Returns:: True if wrapped solver is initialized.

virtual const std::string get_name() const = 0

Get the name of the wrapped solver.

Returns:: The solver name.

virtual Term mk_var(Sort sort, const std::string &name) = 0

Create variable.

Parameters:

sort – The sort of the variable.
name – The name of the variable.

Returns:

The variable.

virtual Term mk_const(Sort sort, const std::string &name) = 0

Create first order constant.

Parameters:

sort – The sort of the constant.
name – The name of the constant.

Returns:

The constant.

virtual Term mk_fun(const std::string &name, const std::vector<Term> &args, Term body) = 0

Create function.

Parameters:

name – The name of the function.
args – The function arguments.
body – The function body.

Returns:

The function.

virtual Sort mk_sort(SortKind kind) = 0

Create sort with no additional arguments.

Examples are sorts of kind SORT_BOOL, SORT_INT, SORT_REAL, SORT_RM, SORT_REGLAN, and SORT_STRING.

Parameters:: kind – The kind of the sort.
Returns:: The created sort.

virtual Sort mk_sort(SortKind kind, const std::vector<Sort> &sorts) = 0

Create sort with given sort arguments.

The sort arguments are given as:

SORT_ARRAY: {<index sort>, <element sort>}
SORT_BAG: {<element sort>}
SORT_FUN: {<domain sort_1>, ..., <domain sort_n>, <codomain sort>}
SORT_SET: {<element sort>}
SORT_SEQ: {<element sort>}

Parameters:

kind – The kind of the sort.
sorts – The sort arguments.

Returns:

The created sort.

virtual Term mk_term(const Op::Kind &kind, const std::vector<Term> &args, const std::vector<uint32_t> &indices) = 0

Create term with given term arguments and indices.

Parameters:

kind – The kind of the term (Op::Kind).
args – The argument terms.
indices – The index arguments.

Returns:

The created term.

virtual Term mk_term(const Op::Kind &kind, const std::vector<std::string> &str_args, const std::vector<Term> &args)

Create term with given string and term arguments.

This is mainly intended for Op::DT_APPLY_SEL, Op::DT_APPLY_TESTER and Op::DT_APPLY_UPDATER.

The string arguments identify constructors and selectors by name and are given for the following kinds as follows:

Op::DT_APPLY_SEL: {<constructor name>, <selector name>}
Op::DT_APPLY_TESTER: {<constructor name>}
Op::DT_APPLY_UPDATER: {<constructor name>, <selector name>}

Parameters:

kind – The kind of the term (Op::Kind).
str_args – The names of constructors/selectors as indicated above.
args – The argument terms.

virtual Term mk_term(const Op::Kind &kind, Sort sort, const std::vector<std::string> &str_args, const std::vector<Term> &args)

Create term with given Sort, string and term arguments.

This is mainly intended for Op::DT_APPLY_CONS, Op::DT_MATCH_BIND_CASE and Op::DT_MATCH_CASE.

The string arguments identify constructors and selectors by name and are given for the following kinds as follows:

Op::DT_APPLY_CONS: {<constructor name>}
Op::DT_MATCH_BIND_CASE: {<constructor name>}
Op::DT_MATCH_CASE: {<constructor name>}

Parameters:

kind – The kind of the term (Op::Kind).
sort – The datatype sort to apply the given kind on.
str_args – The names of constructors/selectors as indicated above.
args – The argument terms.

virtual Sort get_sort(Term term, SortKind sort_kind) = 0

Get a freshly wrapped solver sort of the given term.

This is used for querying the sort of a freshly created term while delegating sort inference to the solver. The returned sort will have sort kind SORT_ANY and id 0 (will be assigned in the FSM, before adding the sort to the sort database). Given sort kind is typically unused, but needed by the Smt2Solver.

Parameters:

term – The term to query for its sort.
sort_kind – The kind of the term’s sort.

Returns:

The sort of the given term.

virtual std::string get_option_name_incremental() const = 0

Get the string representation that identifies the solver configuration option for enabling/disabling incremental solving.

Returns:: Return the string representation of the solver option for enabling/disabling incremental solving.

virtual std::string get_option_name_model_gen() const = 0

Get the string representation that identifies the solver configuration option for enabling/disabling model production.

Returns:: Return the string representation of the solver option for enabling/disabling model production.

virtual std::string get_option_name_unsat_assumptions() const = 0

Get the string representation that identifies the solver configuration option for enabling/disabling unsat assumptions production.

Returns:: Return the string representation of the solver option for enabling/disabling unsat assumption production.

virtual std::string get_option_name_unsat_cores() const = 0

Get the string representation that identifies the solver configuration option for enabling/disabling unsat cores production.

Returns:: Return the string representation of the solver option for enabling/disabling unsat core production.

virtual bool option_incremental_enabled() const = 0

Determine if incremental solving is currently enabled.

Returns:: True if incremental solving is currently enabled.

virtual bool option_model_gen_enabled() const = 0

Determine if model production is currently enabled.

Returns:: True if model production is currently enabled.

virtual bool option_unsat_assumptions_enabled() const = 0

Determine if unsat assumptions production is currently enabled.

Returns:: True if unsat assumptions production is currently enabled.

virtual bool option_unsat_cores_enabled() const = 0

Determine if unsat cores production is currently enabled.

Returns:: True if unsat cores production is currently enabled.

virtual bool is_unsat_assumption(const Term &t) const = 0

Determine if given term is an unsat assumption.

Returns:: True if given term is an unsat assumption.

virtual void assert_formula(const Term &t) = 0

Assert given formula.

SMT-LIB:

(assert <term>)

Parameters:: t – The formula to assert.

virtual Result check_sat() = 0

Check satisfiability of currently asserted formulas.

SMT-LIB:

(check-sat)

Returns:: The satisfiability Result.

virtual Result check_sat_assuming(const std::vector<Term> &assumptions) = 0

Check satisfiability of currently asserted formulas under the given set of assumptions.

SMT-LIB:

(check-sat-assuming)

Parameters:: assumptions – The set of assumptions.
Returns:: The satisfiability Result.

virtual std::vector<Term> get_unsat_assumptions() = 0

Get the current set of unsat assumptions.

SMT-LIB:

(get-unsat-assumptions)

Returns:: The current set of unsat assumptions.

virtual void push(uint32_t n_levels) = 0

Push the given number of assertion levels.

SMT-LIB:

(push <n>)

Parameters:: n_levels – The number of assertion levels to push.

virtual void pop(uint32_t n_levels) = 0

Pop the given number of assertion levels.

SMT-LIB:

(pop <n>)

Parameters:: n_levels – The number of assertion levels to pop.

virtual void print_model() = 0

Print model after a sat check-sat call.

SMT-LIB:

(get-unsat-core)

virtual void reset() = 0

Reset solver.

SMT-LIB:

(reset)

virtual void reset_assertions() = 0

Reset assertion stack.

SMT-LIB:

(reset-assertions)

virtual void set_opt(const std::string &opt, const std::string &value) = 0

Configure solver option.

Should throw a MurxlaSolverOptionException if opt=value is not valid with the currently configured options.

SMT-LIB:

(set-option :<option> <value>)

Parameters:

opt – A string identifying the solver configuration option.
value – A string representation of the option value to configure.

virtual std::vector<Term> get_value(const std::vector<Term> &terms) = 0

Get a term representation of the values of the given terms after a sat check-sat query.

SMT-LIB:

(get-value (<term_1>... <term_n>)

Parameters:: terms – The terms to query the value for.
Returns:: A set of terms representing the values of the given terms.

inline virtual const std::string get_profile() const: Return solver profile JSON string.

inline virtual void configure_fsm(FSM *fsm) const

Configure the FSM with solver-specific extensions.

This is for adding solver-specific actions, states and transitions. Override for solver-specific configuration of the FSM.

Does nothing by default.

Parameters:: fsm – The fsm to configure with extensions.

inline virtual void disable_unsupported_actions(FSM *fsm) const

Disable unsupported actions of the base FSM configuration.

Does nothing by default.

Parameters:: fsm – The fsm to disable actions in.

inline virtual void configure_opmgr(OpKindManager *opmgr) const

Configure the operator kind manager with solver-specific extensions.

This is for adding and configuring solver-specific operator kinds.

Does nothing by default.

Parameters:: opmgr – The operator kind manager to configure.

inline virtual void configure_options(SolverManager *smgr) const

Configure solver configuration options.

This is for adding and configuring solver options (see SolverManager::add_option()).

Does nothing by default.

Parameters:: smgr – The solver manager maintaining the solver options to configure.

virtual void reset_sat()

Reset solver state into assert mode.

After this call, calling

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

virtual Term mk_value(Sort sort, bool value) = 0

Create value from Boolean value.

This is mainly used for creating Boolean values.

Parameters:

sort – The sort of the value.
value – The value.

Returns:

A term representing the value of given sort.

virtual Term mk_value(Sort sort, const std::string &value)

Create value from string.

This is mainly used for floating-point, integer, real, regular language and string values.

Parameters:

sort – The sort of the value.
value – The string representation of the value.

Returns:

A term representing the value of given sort.

virtual Term mk_value(Sort sort, const std::string &num, const std::string &den)

Create rational value.

Parameters:

sort – The sort of the value.
num – A decimal string representing the numerator.
den – A decimal string representing the denominator.

Returns:

A term representing the rational value.

virtual Term mk_value(Sort sort, const std::string &value, Base base)

Create value from string given in a specific base.

This is mainly used for creating bit-vector values.

Parameters:

sort – The sort of the value.
value – The string representation of the value.
base – The numerical base the value string is given in.

Returns:

A term representing the value.

virtual Term mk_special_value(Sort sort, const AbsTerm::SpecialValueKind &value)

Create a special value (as defined in SMT-LIB, or as added as solver-specific special values).

Parameters:

sort – The sort of the special value.
value – The kind of the special value.

Returns:

A term representing the special value.

inline virtual Sort mk_sort(const std::string &name)

Create uninterpreted sort.

Parameters:: name – The name of the uninterpreted sort.
Returns:: An uninterpreted sort.

virtual Sort mk_sort(SortKind kind, const std::string &size)

Create sort with one string argument.

This is mainly for creating finite-field sorts.

Parameters:

kind – The kind of the sort.
size – The size of the finite-field sort.

Returns:

The created sort.

virtual Sort mk_sort(SortKind kind, uint32_t size)

Create sort with one unsigned integer argument.

This is mainly for creating bit-vector sorts.

Parameters:

kind – The kind of the sort.
size – The size of the bit-vector sort.

Returns:

The created sort.

virtual Sort mk_sort(SortKind kind, uint32_t esize, uint32_t ssize)

Create sort with two unsigned integer arguments.

This is mainly for creating floating-point sorts.

Parameters:

kind – The kind of the sort.
esize – The size of the exponent.
ssize – The size of the significand.

Returns:

The created sort.

virtual std::vector<Sort> mk_sort(SortKind kind, const std::vector<std::string> &dt_names, const std::vector<std::vector<Sort>> &param_sorts, const std::vector<AbsSort::DatatypeConstructorMap> &constructors)

Create one or more datatype sorts.

Selectors may return a term of

a regular Sort
a parameter sort (ParamSort)
a yet unresolved dataype sort (UnresolvedSort)
the sort that is currently being created, indicated by passing a nullptr for the selector codomain sort

ParamSort and UnresolvedSort do not wrap actual sorts but are sort placeholders. Thus, solvers must special case cases 1-3 accordingly.

ParamSort keeps a back reference to the associated datatype sort in ParamSort::d_sorts (inherited from AbsSort, see AbsSort::get_sorts()).

For mutually recursive datatypes, we use instances of UnresolvedSort as place holders. These instances are not unique, we create a new instance of UnresolvedSort for every occurence of an unresolved sort. Solvers must distinguish these sorts via their names (see UnresolvedSort::get_symbol()).

If the mutually recursive datatypes are parametric, then we specify sorts for instantiating these parameters, and store them in UnresolvedSort::d_sorts (inherited from AbsSort). These sorts can be retrieved via UnresolvedSort::get_sorts() (inherited).

Parameters:

kind – The kind of the sort.
dt_names – A vector with the names of the datatypes.
param_sorts – A vector with the lists of parameter sorts in case of parametric datatype sorts. The list of parameter sorts for a datatype may be empty.
constructors – A vector with the lists of datatype constructors, wich are given as maps of constructor name to vector of selectors (which are given as a pair of name and sort).

Returns:

The created sort.

virtual Sort instantiate_sort(Sort param_sort, const std::vector<Sort> &sorts)

Instantiate parametric sort param_sort with given sorts

Parameters:

param_sort – The parametric sort to be instantiated.
sorts – The sorts to instantiate the sort parameters of param_sort with.

Returns:

The instantiated sort.

inline virtual void set_logic(const std::string &logic)

Set the logic.

SMT-LIB:

(set-logic <logic>)

Does nothing by default.

Parameters:: logic – A string representing the logic to configure, as defined in the SMT-LIB standard.

virtual std::vector<Term> get_unsat_core()

Retrieve the unsat core after an unsat check-sat call.

SMT-LIB:

(get-unsat-core)

Note

Do not override if solver does not support unsat cores.

Returns:: A set of terms representing the unsat core. Returns an empty vector by default.

inline virtual void check_term(Term term)

Solver-specific term checks.

Parameters:: term – The term to perform solver-specific checks for.

inline virtual void check_term(Term term, const std::vector<std::string> &str_args)

Solver-specific term checks.

Parameters:

term – The term to perform solver-specific checks for.
str_args – The string arguments used to create term (see Solver::mk_term(const Op::Kind&,Sort,const std::vector<std::string>&,const std::vector<Term>&) and Solver::mk_term(const Op::Kind& kind,const std::vector<std::string>& str_args,const std::vector<Term>& args).

inline virtual void check_value(Term term)

Solver-specific value checks.

Parameters:: term – The value term to perform solver-specific checks for.

inline virtual void check_sort(Sort sort)

Solver-specific sort checks.

Parameters:: sort – The sort to perform solver-specific checks for.

inline virtual std::unordered_map<std::string, std::string> get_required_options(Theory theory) const

Query solver options that need to be enabled for a given theory.

Parameters:: theory – The theory for which to query solver options for.
Returns:: A map from option string to option value string of enabled options for a given theory.

inline RNGenerator &get_rng()

Get the random number generator of this solver.

Returns:: The RNG of this solver.

void add_special_value(SortKind sort_kind, const AbsTerm::SpecialValueKind &kind)

Add solver-specific special value kind.

Note

As a style convention, solver-specific special value kinds should be defined in the solver-specific implementation of AbsTerm.

Parameters:

sort_kind – The sort kind of a term of given special value kind.
kind – The solver-specific special value kind to add.

const std::unordered_set<AbsTerm::SpecialValueKind> &get_special_values(SortKind sort_kind) const

Get the set of special value kinds registered with this solver for a given sort kind.

Returns:: The special values for given sort kind. If no special values are defined, return an empty set.

const SortKindSet &get_special_values_sort_kinds() const

Get the sort kinds for which special value kinds are registered with this solver.

Returns:: The set of sort kinds for which this solver has special value kinds defined.

Protected Attributes

RNGenerator d_rng

The random number generator instance of this solver.

This RNG is independent from the main RNG (FSM::d_rng, the RNG associated with the FSM). It is seeded in each action by a seed from a dedicated SolverSeedGenerator (SolverManager::d_sng, the SolverSeedGenerator associated with the SolverManager).

This RNG is seeded when the action is executed (Action::run()) via macro MURXLA_TRACE, which must always be called first in Action::run().

std::unordered_map<SortKind, std::unordered_set<AbsTerm::SpecialValueKind>> d_special_values

Map sort kind to special value kinds.

By default, this includes special values defined in SMT-LIB, and common special values for BV (which don’t have an SMT-LIB equivalent). The entry for SORT_ANY is a dummy entry for sort kinds with no special values.

This map can be extended with solver-specific special values.

Note

Special values for BV must be converted to binary, decimal or hexadecimal strings or integer values if the solver does not provide dedicated API functions to generate these values. Utility functions for these conversions are provided in src/util.hpp.

SortKindSet d_special_values_sort_kinds: Contains all sort kinds for have special value kinds have been registered.