Solver Wrapper Interface: Solver

class murxla::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, 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

1. a regular Sort

2. a parameter sort (ParamSort)

3. a yet unresolved dataype sort (UnresolvedSort)

4. 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.