Solver Wrapper Implementation for Solver

Solver wrappers derive a solver class from murxla::Solver, which manages construction and destruction of an instance of the solver under test. It further implements required and optional member function overrides.

Murxla uses naming convention <solver name (short)>Solver for solver wrapper solver implementations, e.g., the cvc5 implementation is called Cvc5Solver and the Bitwuzla implementation is called BzlaSolver.

Note that the constructor of murxla::Solver is not to be overriden. A solver instance is created and deleted via the required member function overrides of functions murxla::Solver::new_solver() and murxla::Solver::delete_solver(). For example, in the solver wrapper for cvc5 (using its C++ API) these are implemented as follows:

void
Cvc5Solver::new_solver()
{
  assert(d_solver == nullptr);
  d_solver = new ::cvc5::Solver();
  d_tracer.init();
}

void
Cvc5Solver::delete_solver()
{
  assert(d_solver != nullptr);
  delete d_solver;
  d_solver = nullptr;
}

Another example for a required override is member function murxla::Solver::get_name(), which returns the name of the solver under test. It is implemented for cvc5 as follows:

const std::string
Cvc5Solver::get_name() const
{
  return "cvc5";
}

An example for an optional override is member function murxla::Solver::get_unsat_core(), which returns a vector of terms representing the unsat core of the currently asserted formula. It is implemented in the solver wrapper for Bitwuzla (using its C API) as follows:

std::vector<Term>
BzlaSolver::get_unsat_core()
{
  size_t size;
  std::vector<Term> res;
  const BitwuzlaTerm** bzla_res = bitwuzla_get_unsat_core(d_solver, &size);
  for (uint32_t i = 0; i < size; ++i)
  {
    res.push_back(
        std::shared_ptr<BzlaTerm>(new BzlaTerm((BitwuzlaTerm*) bzla_res[i])));
  }
  return res;
}

The following list provides all the member functions of class murxla::Solver that are required or optional to be overriden by a solver wrapper.

Note

Optional overrides have default implementations, but should be overriden if supported by the solver.

Solver: Functions Required to be Overriden

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.

Solver: Functions to be Overriden Optionally

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

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.