Solver Wrappers

Random Number Generator (RNG)

Murxla’s generic solver API as implemented in the solver wrapper interface aims at providing an interface for the solver under test that allows to plug in any variants of API functions for specific SMT-LIB features. For example, murxla::Solver::mk_value() provides one interface for creating bit-vector values (murxla::Solver::mk_value(Sort sort, const std::string& value, Base base)), but most solvers provide API functions that take either a string or integer representation for the value as argument. For cases like this, it is useful to be able to randomly decide, for each call, which API function of the solver under test to use.

In order to be able to deterministically replay a given trace, even when minimized, it is necessary to decouple non-deterministic choices in the solver wrapper from Murxla’s main RNG. Thus, the solver wrapper base class maintains an independent RNG, which is seeded with a random seed at the beginning of each call to the execution function of an action (naming convention: <Action>::run(<args>)). This seed is traced, and since each call to run() must first trace the Action’s execution via macro MURXLA_TRACE, we automatically seed the solver wrapper’s RNG there and prepend the seed to the trace line:

#define MURXLA_TRACE                                                 \
  d_solver.get_rng().reseed(d_sng.seed()),                           \
      OstreamVoider()                                                \
          & Action::TraceStream(d_smgr).stream()                     \
                << std::setw(5) << d_sng.seed() << " "

The solver wrapper’s RNG can be directly accessed as the protected member murxla::Solver::d_rng, or via murxla::Solver::get_rng().

Operator Kinds

Murxla defines a base set of operator kinds as static const members of type murxla::Op::Kind of class murxla::Op. Solver-specific operator kinds are (by convention) defined as members of the solver wrapper implementation of murxla::AbsTerm. By convention, we prefix solver-specific operator kinds with the solver’s (short) name. For example, the solver wrapper for Bitwuzla defines a bit-vector decrement operator as member of murxla::BitwuzlaTerm as

  inline static const Op::Kind OP_BV_DEC = "bitwuzla-OP_BV_DEC";

Solver-specific operator kinds are added to the operator kind manager via overriding murxla::Solver::configure_opmgr(), e.g.,

  opmgr->add_op_kind(
      BitwuzlaTerm::OP_BV_DEC, 1, 0, SORT_BV, {SORT_BV}, THEORY_BV);

Special Value Kinds

Murxla introduces the notion of murxla::AbsTerm::SpecialValueKind for values that can be considered a special value in a theory, e.g., floating-point NaN (of a given floating-point format), or the minimum signed bit-vector value (of a given bit-width).

Terms representing special values are created via murxla::Solver::mk_special_value(). A list of all special value kinds defined in murxla::AbsTerm is provided below:

As with solver-specific operator kinds, solver-specific special value kinds are (by convention) defined as a static const member of type murxla::AbsTerm::SpecialValueKind of the solver wrapper implementation of murxla::AbsTerm. And again, by convention, we prefix solver-specific special value kinds with the solver’s (short) name.

Solver wrappers can extend the pre-defined list of special value kinds with solver-specific kinds via murxla::Solver::add_special_value().

Actions

Murxla defines a base API model implementing SMT-LIB semantics (as a finite state machine, see FSM) with a base set of actions. This base API model can be extended with solver-specific features that cannot be immediately plugged into the base API Model by adding transitions with associated solver-specific actions to the FSM via overriding murxla::Solver::configure_fsm().

Solver-specific actions directly interact with the API of the solver under test (see FSM: Actions). They are added to an existing (or new, solver-specific) state while defining its priority and (optionally) a next state via murxla::State::add_action() (see FSM Configuration).

Features Unsupported By The Solver Under Test

Murxla requires to define a solver profile (see Solver Profiles) to define the solver test configuration. The solver profile allows to define which theories to consider and to disable unsupported sort and operator kinds. Unsupported actions can be disabled via overriding murxla::Solver::disable_unsupported_actions().