FSM: Actions

murxla::Action::generate()

Function murxla::Action::generate() is responsible for checking an action’s preconditions and selecting (and, in execeptional cases, creating) the arguments for its execution. For this, it queries the solver manager (see murxla::SolverManager), which provides a rich interface to pick and manage sorts, terms and manage a solver’s current state.

For example, action murxla::ActionAssertFormula (from the the base set of actions) is responsible for asserting a random formula (SMT-LIB: assert). It asserts that the solver is initialized for Murxla-level debugging purposes, and checks the required precondition that Boolean terms already exist in the term database. It then generates the arguments to the action execution by picking a random Boolean term:

bool
ActionAssertFormula::generate()
{
  assert(d_solver.is_initialized());
  if (!d_smgr.has_term(SORT_BOOL, 0)) return false;
  Term assertion = d_smgr.pick_term(SORT_BOOL, 0);

  run(assertion);
  return true;
}

In general, murxla::Action::generate() should only pick existing sorts and terms as arguments. However, there exist some exceptional cases where it is beneficial to create arguments on demand. For example, it makes no sense to globally create patterns (murxla::Op::DT_MATCH_CASE, murxla::Op::DT_MATCH_BIND_CASE) for murxla::Op::DT_MATCH (SMT-LIB: match). If created globally, they would be added to the term database and could potentially be picked when selecting arguments for an operator other than murxla::Op::DT_MATCH, which shouldn’t be the case. Instead, we create these patterns on demand in murxla::ActionMkTerm::generate().

For example, for a patterns that matches a specific non-nullary datatype constructor (of kind murxla::Op::DT_MATCH_BIND_CASE), we need variables of a specific sort for each selector of the constructor, and a quantified term that possibly uses these variables. We thus create such patterns on demand as follows:

ActionMkVar mkvar(d_smgr);  // to create variables on demand

[ ... ]

for (const auto& sel : sel_names)
{
  /* Create variable of selector codomain sort for each selector. */
  auto var_id =
      mkvar.run(dt_sort->get_dt_sel_sort(dt_sort, ctor, sel),
                d_smgr.pick_symbol())[0];
  match_case_args.push_back(d_smgr.get_term(var_id));
}
/* Create some terms that (possibly) use these variables. */
uint32_t n_terms_created = 0;
while ((!d_smgr.has_quant_term(sort) && !d_smgr.has_term(sort))
       || n_terms_created < MURXLA_MIN_N_QUANT_TERMS)
{
  /* We only create op terms here (no consts, values, vars). The
   * former two wouldn't be quantified terms that use the created vars
   * anyways, and we have already picked a sort with terms, so we do
   * have terms of that sort in the term db. We may consider to create
   * vars here in the future. */
  Op::Kind op_kind = d_smgr.pick_op_kind(true, sort_kind);
  if (op_kind == Op::DT_MATCH) continue;
  /* Do not create quantifiers since this would bind the variables
   * created above. */
  if (op_kind == Op::FORALL || op_kind == Op::EXISTS) continue;
  // Skip set comprehension since it would also bind the variables
  // created above.
  if (op_kind == Op::SET_COMPREHENSION) continue;
  if (generate(op_kind)) n_terms_created += 1;
}
match_case_kind = Op::DT_MATCH_BIND_CASE;

murxla::Action<Name>::run(<args>)

The execution of an action is implemented in a (usually private) member function murxla::Action<Name>::run(<args>), which allows to use the same action execution code for both murxla::Action::generate() and murxla::Action::untrace(). This function is responsible for tracing, and is usually the only one to interact with the solver via the generic solver wrapper API (or directly via the solver API for solver-specific actions). It is further responsible for registering created sorts and terms with the solver manager (if to be used in the future).

For example, murxla::ActionAssertFormula::run() is implemented as follows:

void
ActionAssertFormula::run(Term assertion)
{
  MURXLA_TRACE << get_kind() << " " << assertion;
  reset_sat();
  d_solver.assert_formula(assertion);
}

In this example, we first trace the actioan via MURXLA_TRACE, then reset the solver state from sat to assert (see Fig. 4.1 of the SMT-LIB Standard 2.6), and then assert the formula via murxla::Solver::assert_formula().

Actions that create new sorts and terms must trace these return values via macro MURXLA_TRACE_RETURN (see tracing). Further, for testing assertions about the solver under test, we use macro MURXLA_TEST. For example, the action execution of action murxla::ActionMkSort is implemented as follows:

std::vector<uint64_t>
ActionMkSort::run(SortKind kind, uint32_t bw)
{
  MURXLA_TRACE << get_kind() << " " << kind << " " << bw;
  assert(kind == SORT_BV);
  Sort res = d_solver.mk_sort(kind, bw);
  MURXLA_TEST(res->get_bv_size() == bw);
  d_smgr.add_sort(res, kind);
  check_sort(res);
  MURXLA_TRACE_RETURN << res;
  return {res->get_id()};
}

This first traces the action, then asserts that the given sort kind is the bit-vector sort kind (Murxla-level debug assertion), then creates the sort via murxla::Solver::mk_sort(), tests if the created sort has the expected bit-width via MURXLA_TEST, adds the sort to the sort database via murxla::SolverManager::add_sort(), performs some checks on the sort via murxla::ActionMkSort::check_sort(), traces the sort as return value via MURXLA_TRACE_RETURN and returns its id (used for untracing only).

murxla::Action::untrace()

Actions are replayed via murxla::Action::untrace(), which takes a vector of tokens as arguments, converts those tokens into sort and term objects where necessary, and executes the action via murxla::Action::generate().

For example, action murxla::ActionAssertFormula is replayed via murxla::ActionAssertFormula::untrace() as follows:

std::vector<uint64_t>
ActionAssertFormula::untrace(const std::vector<std::string>& tokens)
{
  MURXLA_CHECK_TRACE_NTOKENS(1, tokens.size());
  Term t = get_untraced_term(untrace_str_to_id(tokens[0]));
  MURXLA_CHECK_TRACE_TERM(t, tokens[0]);
  run(t);
  return {};
}

Murxla provides a set of macros for checking expected properties of given action line trace tokens. In the example above, we use macro MURXLA_CHECK_TRACE_NTOKENS to check if tokens holds exactly one trace token (the id of the asserted term). We retrieve the term matched to the traced term id via murxla::Action::get_untraced_term() (similarly, traced sorts are retrieved from the sort database via murxla::Action::get_untraced_sort()), and check if we were able to match the term (or if the given id is unknown) via MURXLA_CHECK_TRACE_TERM (similarly, for sorts, via MURXLA_CHECK_TRACE_SORT).

Solver-specific Actions

Solver-specific actions derived from murxla::Action usually access the API of the solver under test directly, without going through the solver wrapper API.

For example, Bitwuzla defines a solver-specific action BitwuzlaActionIsUnsatAssumption for comparing the sort of two terms, and its execution BitwuzlaActionIsUnsatAssumption::run(Term) is implemented follows:

  void run(Term term)
  {
    MURXLA_TRACE << get_kind() << " " << term;
    BitwuzlaSolver& bzla_solver = dynamic_cast<BitwuzlaSolver&>(d_solver);
    (void) bzla_solver.get_solver()->is_unsat_assumption(
        BitwuzlaTerm::get_bitwuzla_term(term));
  }

Tracing

In order to be able to replay a sequence of actions that triggered an issue in the solver under test, we trace each action execution in a simple, easy-to-parse output format.

Each action trace line follows the pattern

<solver RNG seed> <action kind> [<args ...>]

optionally followed by a return statement if the action creates new sorts or terms:

return <values ...>

Additionally, in the first line of a trace, Murxla records the command line options provided to generate this trace.

For example, the following trace triggered an issue in cvc5:

 1set-murxla-options --cvc5 -t 1 -m 10000 --fuzz-opts
 292880 new
 332252 set-logic BVFPNIA
 496760 set-option incremental false
 53046 set-option solve-int-as-bv 925956265872928556
 636189 mk-sort SORT_INT
 7return s14
 819629 mk-const s14 "_x35"
 9return t46
1081876 mk-term OP_INT_DIV SORT_INT 2 t46 t46
11return t125 s14
1250301 mk-term OP_INT_LTE SORT_BOOL 2 t125 t125
13return t127 s12
1488360 cvc5-simplify t127

As indicated in the first line, this trace was generated when running Murxla continuously for 1000 runs to test cvc5 with a one second time limit per run and with option fuzzing enabled. Line 2 creates a new solver instance, line 3 restricts the logic to BVFPNIA, lines 4-5 enable incremental solving and a cvc5-specific option that translates integers to bit-vectors, line 6 queries the integer sort from the solver, lines 8-9 create and return a constant of that sort, lines 10-11 create and return an integer division (murxla::Op::INT_DIV) and an integer less-than-or-equal (murxla::Op::INT_LTE) term, and line 14 executes a cvc5-specific action cvc5-simplify to simplify the integer division term t127.

As shown in lines 10-11, when creating terms, we trace argument lists while also providing the number of arguments, e.g., 2 t46 t46 in line 10. If an operator is indexed, we similarly provide the list of indices with its size, e.g., a bit-vector extract from index 4 to 3 on a term t99 of sort 9 we would trace as

<seed> mk-term OP_BV_EXTRACT SORT_BV 9 1 t99 2 4 3

Generally, also for solver-specific actions, it is recommended to also trace the size of argument lists to an action whenever they can be of arbitrary size.

Further, as shown in lines 11 and 13, for actions that create new terms that should be added to the term database (and are thus traced in a return statement), we not only need to the trace the returned term but also its sort. This is due to the fact that some operators create new sorts (e.g., murxla::Op::BV_EXTRACT) that may not have been encountered in the trace yet, but are added to the sorts database and can thus occur later in the trace.

We use macro MURXLA_TRACE for tracing action executions, and macro MURXLA_TRACE_RETURN for tracing an action’s return values.

Furthermore, in order to be able to deterministically replay a given trace, even when minimized, solver wrappers maintain an independent RNG to decouple non-deterministic choices in the solver wrapper from Murxla’s main RNG. The solver wrapper RNG is seeded with a random seed at the beginning of an action’s execution, and this seed is traced as <solver RNG seed>. Each call to run() must first trace the Action’s execution via macro MURXLA_TRACE, and 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() << " "

MURXLA_TRACE

The macro to be used for tracing an exection of an action.

Seeds the solver wrapper RNG and prepends the current seed to the trace line. Add trace line contents via operator<<, e.g.,

MURXLA_TRACE << <action>.get_kind() << " " << <args...>;

MURXLA_TRACE_RETURN

The macro to be used for tracing the return value of an action’s execution.

Add trace return line contents via operator<<, e.g., for a sort return value with id 1,

MURXLA_TRACE_RETURN << <created sort>;

will be traced as

return s1;

Note

For actions that return newly created terms, it is required to not only trace the term, but also its sort. This is necessary because some operator kinds create terms of possibly yet unseen sorts (e.g., murxla::Op::BV_EXTRACT). Newly created terms are traced as

MURXLA_TRACE_RETURN << <created term> << " " << <sort of created term>;

FSM Configuration

Actions are added to states of the FSM via murxla::State::add_action() while optionally defining a next state to transition into (or remaining in the state it’s been added to). We further derive a class murxla::Transition from murxla::Action, which represents a transition from one state to the next without executing any solver API calls (an empty action).

Existing states are retrieved via murxla::FSM::get_state(), new states are created and added via murxla::FSM::new_state() (see FSM: States).

Each action added to a state via murxla::State::add_action() has a weight, which is defined via its priority, with 1 as the highest priority, UINT32_MAX the lowest priority, and 0 corresponding to disabling the action.

The Base Class for Actions

class Action

The base class for actions.

An action defines an interaction with the solver under test, . Actions are responsible for (1) randomly generating API call arguments (Action::generate()); (2) executing API calls with a given set of arguments (member run() of derived actions); and (3) replaying a traced copy of the action (Action::untrace()).

Subclassed by murxla::ActionAssertFormula, murxla::ActionCheckSat, murxla::ActionCheckSatAssuming, murxla::ActionDelete, murxla::ActionGetUnsatAssumptions, murxla::ActionGetUnsatCore, murxla::ActionGetValue, murxla::ActionInstantiateSort, murxla::ActionMkConst, murxla::ActionMkFun, murxla::ActionMkSort, murxla::ActionMkSpecialValue, murxla::ActionMkTerm, murxla::ActionMkValue, murxla::ActionMkVar, murxla::ActionNew, murxla::ActionPop, murxla::ActionPrintModel, murxla::ActionPush, murxla::ActionReset, murxla::ActionResetAssertions, murxla::ActionSetLogic, murxla::ActionSetOption, murxla::ActionSetOptionReq, murxla::ActionTermGetChildren, murxla::Transition

Public Types

enum ReturnValue

The kind of value this action is expected to return.

This indicates how the return value of this action is traced, which is mainly relevant for error checking when untracing.

Values:

enumerator NONE

enumerator ID

No return trace statement expected.

enumerator ID_LIST

Returns a single sort or term id.

using Kind = std::string

The kind of an action.

This is used as action identifier when tracing. We further use strings here to make FSM::d_actions easily extensible with solver-specific actions.

Public Functions

Action() = delete

Disallow default constructor.

Action(SolverManager &smgr, const Kind &kind, ReturnValue returns, bool empty = false)

Constructor.

Parameters:

• smgr – The associated solver manager.

• kind – The kind of the action. By convention, the static identifier s_name of a derived action should be passed as the kind.

• returns – The expected value this action traces as return statement.

• empty – True if this action does not execute any solver API calls. This is intended for transitions from one state to another that don’t perform an actual action.

virtual ~Action() = default

Destructor.

virtual bool generate() = 0

Generate API call arguments and execute the action.

Returns:

True if the generation and execution was successful. False if no arguments can be generated or the action cannot be executed in the current configuration or state of the solver under test.

inline bool disabled() const

Indicates whether an action should be disabled after generate() has returned false.

Returns:

True if the action should be disabled.

virtual std::vector<uint64_t> untrace(const std::vector<std::string> &tokens) = 0

Replay an action.

Parameters:

tokens – The tokens of the trace statement to replay.

Returns:

A vector of ids of created objects, if objects have been created, and an empty vector otherwise. Needed to be able to compare ids of created objects to the traced ids in the trace’s return statement.

inline const Kind &get_kind() const

Get the string representing the kind of this action.

Returns:

The kind of this action.

inline const uint64_t get_id() const

Get the id of this action.

Returns:

The id of this action.

inline void set_id(uint64_t id)

Set the id of this action.

Parameters:

id – The id of this action to set.

inline ReturnValue returns() const

Get the kind of return value this action returns.

Returns:

The return value of this action.

inline bool empty() const

Determine if this action is empty.

Returns:

True if this action is empty, i.e., a transition without performing any API calls.

void seed_solver_rng() const

Generate next seed and seed solver RNG. This should never be called when untracing.

Term get_untraced_term(uint64_t id)

Get the untraced term with the given id. Checks that such a term exists.

Parameters:

id – The id of the untraced term.

Returns:

The untraced term.

Sort get_untraced_sort(uint64_t id)

Get the untraced sort with the given id. Checks that such a sort exists.

Parameters:

id – The id of the untraced sort.

Returns:

The untraced sort.

Public Static Functions

static uint64_t untrace_str_to_id(const std::string &s)

Convert traced sort id ("s<id>") or term id ("t<id>") string to id.

Throws a MurxlaUntraceIdException if given string does not represent a valid sort or term id.

Parameters:

s – The sort or term id string.

Returns:

The sort or term id.

static SortKind get_sort_kind_from_str(const std::string &s)

Convert a sort kind string to a SortKind.

Parameters:

s – The sort kind string.

Returns:

The sort kind.

Public Static Attributes

static const Kind UNDEFINED = "undefined"

The undefined action.

class TraceStream

The output stream wrapper for tracing actions.

Public Functions

TraceStream(SolverManager &smgr)

Constructor.

Parameters:

smgr – The associated solver manager.

~TraceStream()

Destructor.

TraceStream(const TraceStream &astream) = default

Copy constructor.

Parameters:

astream – The trace stream to copy.

std::ostream &stream()

Get the wrapped output stream.

Returns:

The output stream.

Default Transitions

A murxla::Transition is an empty action, i.e., an action that does not generate and execute solver API calls. It is used to simply transition from the current state to the next state.

class Transition : public murxla::Action

(Empty) transition from current state to next state without pre-conditions.

Subclassed by murxla::TransitionCreateInputs, murxla::TransitionCreateSorts, murxla::TransitionDefault

class TransitionDefault : public murxla::Transition

Default (generic) transition.

class TransitionCreateInputs : public murxla::Transition

Transition from creating inputs to the next state if there exists at least one input.

class TransitionCreateSorts : public murxla::Transition

Transition from creating sorts to the next state if there exists at least one sort.

The Base Set of Actions

class ActionNew : public murxla::Action

The action to create and initialize a solver instance of the solver under test.

Public Functions

inline ActionNew(SolverManager &smgr)

Constructor.

Parameters:

smgr – The associated solver manager.

virtual bool generate() override

Generate API call arguments and execute the action.

Returns:

True if the generation and execution was successful. False if no arguments can be generated or the action cannot be executed in the current configuration or state of the solver under test.

virtual std::vector<uint64_t> untrace(const std::vector<std::string> &tokens) override

Replay an action.

Parameters:

tokens – The tokens of the trace statement to replay.

Returns:

A vector of ids of created objects, if objects have been created, and an empty vector otherwise. Needed to be able to compare ids of created objects to the traced ids in the trace’s return statement.

Public Static Attributes

static const Kind s_name = "new"

The name of this action.

class ActionDelete : public murxla::Action

The action to delete the solver instance of the solver under test.

Public Functions

inline ActionDelete(SolverManager &smgr)

Constructor.

Parameters:

smgr – The associated solver manager.

virtual bool generate() override

Generate API call arguments and execute the action.

Returns:

True if the generation and execution was successful. False if no arguments can be generated or the action cannot be executed in the current configuration or state of the solver under test.

virtual std::vector<uint64_t> untrace(const std::vector<std::string> &tokens) override

Replay an action.

Parameters:

tokens – The tokens of the trace statement to replay.

Returns:

A vector of ids of created objects, if objects have been created, and an empty vector otherwise. Needed to be able to compare ids of created objects to the traced ids in the trace’s return statement.

Public Static Attributes

static const Kind s_name = "delete"

The name of this action.

class ActionSetLogic : public murxla::Action

The action to constrain the logic of created formulas.

Public Functions

inline ActionSetLogic(SolverManager &smgr)

Constructor.

Parameters:

smgr – The associated solver manager.

virtual bool generate() override

Generate API call arguments and execute the action.

Returns:

True if the generation and execution was successful. False if no arguments can be generated or the action cannot be executed in the current configuration or state of the solver under test.

virtual std::vector<uint64_t> untrace(const std::vector<std::string> &tokens) override

Replay an action.

Parameters:

tokens – The tokens of the trace statement to replay.

Returns:

A vector of ids of created objects, if objects have been created, and an empty vector otherwise. Needed to be able to compare ids of created objects to the traced ids in the trace’s return statement.

Public Static Attributes

static const Kind s_name = "set-logic"

The name of this action.

class ActionSetOption : public murxla::Action

The action to configure solver options.

Public Functions

inline ActionSetOption(SolverManager &smgr)

Constructor.

Parameters:

smgr – The associated solver manager.

virtual bool generate() override

Generate API call arguments and execute the action.

Returns:

True if the generation and execution was successful. False if no arguments can be generated or the action cannot be executed in the current configuration or state of the solver under test.

virtual std::vector<uint64_t> untrace(const std::vector<std::string> &tokens) override

Replay an action.

Parameters:

tokens – The tokens of the trace statement to replay.

Returns:

A vector of ids of created objects, if objects have been created, and an empty vector otherwise. Needed to be able to compare ids of created objects to the traced ids in the trace’s return statement.

Public Static Attributes

static const Kind s_name = "set-option"

The name this action.

class ActionSetOptionReq : public murxla::Action

The action to configure solver options that are required for the current solver configuration (see Solver::get_required_options()).

This further includes options enforced via command line option -o.

Public Functions

inline ActionSetOptionReq(SolverManager &smgr)

Constructor.

Parameters:

smgr – The associated solver manager.

virtual bool generate() override

Generate API call arguments and execute the action.

Returns:

True if the generation and execution was successful. False if no arguments can be generated or the action cannot be executed in the current configuration or state of the solver under test.

virtual std::vector<uint64_t> untrace(const std::vector<std::string> &tokens) override

Replay an action.

Parameters:

tokens – The tokens of the trace statement to replay.

Returns:

A vector of ids of created objects, if objects have been created, and an empty vector otherwise. Needed to be able to compare ids of created objects to the traced ids in the trace’s return statement.

void init(const std::vector<std::pair<std::string, std::string>> &solver_options, ActionSetOption *setoption)

Public Static Attributes

static const Kind s_name = "set-option-req"

The name of this action.

class ActionMkSort : public murxla::Action

The action to create a sort.

Public Functions

ActionMkSort(SolverManager &smgr)

Constructor.

Parameters:

smgr – The associated solver manager.

virtual bool generate() override

Generate API call arguments and execute the action.

Returns:

True if the generation and execution was successful. False if no arguments can be generated or the action cannot be executed in the current configuration or state of the solver under test.

virtual std::vector<uint64_t> untrace(const std::vector<std::string> &tokens) override

Replay an action.

Parameters:

tokens – The tokens of the trace statement to replay.

Returns:

A vector of ids of created objects, if objects have been created, and an empty vector otherwise. Needed to be able to compare ids of created objects to the traced ids in the trace’s return statement.

Public Static Attributes

static const Kind s_name = "mk-sort"

The name of this action.

class ActionMkTerm : public murxla::Action

The action to create a term.

Public Functions

ActionMkTerm(SolverManager &smgr)

Constructor.

Parameters:

smgr – The associated solver manager.

virtual bool generate() override

Generate API call arguments and execute the action.

Returns:

True if the generation and execution was successful. False if no arguments can be generated or the action cannot be executed in the current configuration or state of the solver under test.

virtual std::vector<uint64_t> untrace(const std::vector<std::string> &tokens) override

Replay an action.

Parameters:

tokens – The tokens of the trace statement to replay.

Returns:

A vector of ids of created objects, if objects have been created, and an empty vector otherwise. Needed to be able to compare ids of created objects to the traced ids in the trace’s return statement.

void check_term(Term term)

Perform checks on the created term.

bool generate(Op::Kind kind)

Create term of given operator kind.

bool generate(SortKind sort_kind)

Create term of a given sort kind.

Public Static Attributes

static const Kind s_name = "mk-term"

The name of this action.

class ActionMkConst : public murxla::Action

The action to create a first-order constant.

Public Functions

inline ActionMkConst(SolverManager &smgr)

Constructor.

Parameters:

smgr – The associated solver manager.

virtual bool generate() override

Generate API call arguments and execute the action.

Returns:

True if the generation and execution was successful. False if no arguments can be generated or the action cannot be executed in the current configuration or state of the solver under test.

virtual std::vector<uint64_t> untrace(const std::vector<std::string> &tokens) override

Replay an action.

Parameters:

tokens – The tokens of the trace statement to replay.

Returns:

A vector of ids of created objects, if objects have been created, and an empty vector otherwise. Needed to be able to compare ids of created objects to the traced ids in the trace’s return statement.

bool generate(Sort sort)

Create const of given sort.

Public Static Attributes

static const Kind s_name = "mk-const"

The name of this action.

class ActionMkFun : public murxla::Action

The action to create a function.

Public Functions

ActionMkFun(SolverManager &smgr)

Constructor.

Parameters:

smgr – The associated solver manager.

virtual bool generate() override

Generate API call arguments and execute the action.

Returns:

True if the generation and execution was successful. False if no arguments can be generated or the action cannot be executed in the current configuration or state of the solver under test.

virtual std::vector<uint64_t> untrace(const std::vector<std::string> &tokens) override

Replay an action.

Parameters:

tokens – The tokens of the trace statement to replay.

Returns:

A vector of ids of created objects, if objects have been created, and an empty vector otherwise. Needed to be able to compare ids of created objects to the traced ids in the trace’s return statement.

Public Static Attributes

static const Kind s_name = "mk-fun"

The name of this action.

class ActionMkVar : public murxla::Action

The action to create a variable.

Public Functions

ActionMkVar(SolverManager &smgr)

Constructor.

Parameters:

smgr – The associated solver manager.

virtual bool generate() override

Generate API call arguments and execute the action.

Returns:

True if the generation and execution was successful. False if no arguments can be generated or the action cannot be executed in the current configuration or state of the solver under test.

virtual std::vector<uint64_t> untrace(const std::vector<std::string> &tokens) override

Replay an action.

Parameters:

tokens – The tokens of the trace statement to replay.

Returns:

A vector of ids of created objects, if objects have been created, and an empty vector otherwise. Needed to be able to compare ids of created objects to the traced ids in the trace’s return statement.

std::vector<uint64_t> run(Sort sort, const std::string &symbol)

Public Static Attributes

static const Kind s_name = "mk-var"

The name of this action.

class ActionMkValue : public murxla::Action

The action to create a value.

Public Functions

inline ActionMkValue(SolverManager &smgr)

Constructor.

Parameters:

smgr – The associated solver manager.

virtual bool generate() override

Generate API call arguments and execute the action.

Returns:

True if the generation and execution was successful. False if no arguments can be generated or the action cannot be executed in the current configuration or state of the solver under test.

virtual std::vector<uint64_t> untrace(const std::vector<std::string> &tokens) override

Replay an action.

Parameters:

tokens – The tokens of the trace statement to replay.

Returns:

A vector of ids of created objects, if objects have been created, and an empty vector otherwise. Needed to be able to compare ids of created objects to the traced ids in the trace’s return statement.

void check_value(Term term)

Perform checks on created value.

bool generate(Sort sort)

Create value of given sort.

Public Static Attributes

static const Kind s_name = "mk-value"

The name of this action.

class ActionMkSpecialValue : public murxla::Action

The action to create a special value.

Public Functions

inline ActionMkSpecialValue(SolverManager &smgr)

Constructor.

Parameters:

smgr – The associated solver manager.

virtual bool generate() override

Generate API call arguments and execute the action.

Returns:

True if the generation and execution was successful. False if no arguments can be generated or the action cannot be executed in the current configuration or state of the solver under test.

virtual std::vector<uint64_t> untrace(const std::vector<std::string> &tokens) override

Replay an action.

Parameters:

tokens – The tokens of the trace statement to replay.

Returns:

A vector of ids of created objects, if objects have been created, and an empty vector otherwise. Needed to be able to compare ids of created objects to the traced ids in the trace’s return statement.

bool generate(Sort sort)

Create special value of given sort.

Public Static Attributes

static const Kind s_name = "mk-special-value"

The name of this action.

class ActionInstantiateSort : public murxla::Action

The action to instanitate a parametric sort.

Public Functions

ActionInstantiateSort(SolverManager &smgr)

Constructor.

Parameters:

smgr – The associated solver manager.

virtual bool generate() override

Generate API call arguments and execute the action.

Returns:

True if the generation and execution was successful. False if no arguments can be generated or the action cannot be executed in the current configuration or state of the solver under test.

virtual std::vector<uint64_t> untrace(const std::vector<std::string> &tokens) override

Replay an action.

Parameters:

tokens – The tokens of the trace statement to replay.

Returns:

A vector of ids of created objects, if objects have been created, and an empty vector otherwise. Needed to be able to compare ids of created objects to the traced ids in the trace’s return statement.

Sort run(Sort param_sort, const std::vector<Sort> &inst_sorts)

Public Static Attributes

static const Kind s_name = "instantiate-sort"

The name of this action.

class ActionAssertFormula : public murxla::Action

The action to assert a formula.

Public Functions

inline ActionAssertFormula(SolverManager &smgr)

Constructor.

Parameters:

smgr – The associated solver manager.

virtual bool generate() override

[docs-action-assertformula-generate start]

virtual std::vector<uint64_t> untrace(const std::vector<std::string> &tokens) override

[docs-action-assertformula-generate end]

[docs-action-assertformula-untrace start]

Public Static Attributes

static const Kind s_name = "assert-formula"

The name of this action.

class ActionCheckSat : public murxla::Action

The action to check satisfiability of the currently asserted formulas.

Public Functions

inline ActionCheckSat(SolverManager &smgr)

Constructor.

Parameters:

smgr – The associated solver manager.

virtual bool generate() override

[docs-action-assertformula-run end]

virtual std::vector<uint64_t> untrace(const std::vector<std::string> &tokens) override

Replay an action.

Parameters:

tokens – The tokens of the trace statement to replay.

Returns:

A vector of ids of created objects, if objects have been created, and an empty vector otherwise. Needed to be able to compare ids of created objects to the traced ids in the trace’s return statement.

Public Static Attributes

static const Kind s_name = "check-sat"

The name of this action.

class ActionCheckSatAssuming : public murxla::Action

The action to check satisfiability of the currently asserted formulas under a set of assumptions.

Public Functions

inline ActionCheckSatAssuming(SolverManager &smgr)

Constructor.

Parameters:

smgr – The associated solver manager.

virtual bool generate() override

Generate API call arguments and execute the action.

Returns:

True if the generation and execution was successful. False if no arguments can be generated or the action cannot be executed in the current configuration or state of the solver under test.

virtual std::vector<uint64_t> untrace(const std::vector<std::string> &tokens) override

Replay an action.

Parameters:

tokens – The tokens of the trace statement to replay.

Returns:

A vector of ids of created objects, if objects have been created, and an empty vector otherwise. Needed to be able to compare ids of created objects to the traced ids in the trace’s return statement.

Public Static Attributes

static const Kind s_name = "check-sat-assuming"

The name of this action.

class ActionGetUnsatAssumptions : public murxla::Action

The action to get the set of unsat assumptions.

Public Functions

inline ActionGetUnsatAssumptions(SolverManager &smgr)

Constructor.

Parameters:

smgr – The associated solver manager.

virtual bool generate() override

Generate API call arguments and execute the action.

Returns:

True if the generation and execution was successful. False if no arguments can be generated or the action cannot be executed in the current configuration or state of the solver under test.

virtual std::vector<uint64_t> untrace(const std::vector<std::string> &tokens) override

Replay an action.

Parameters:

tokens – The tokens of the trace statement to replay.

Returns:

A vector of ids of created objects, if objects have been created, and an empty vector otherwise. Needed to be able to compare ids of created objects to the traced ids in the trace’s return statement.

Public Static Attributes

static const Kind s_name = "get-unsat-assumptions"

The name of this action.

class ActionGetUnsatCore : public murxla::Action

The action to get the unsat core.

Public Functions

inline ActionGetUnsatCore(SolverManager &smgr)

Constructor.

Parameters:

smgr – The associated solver manager.

virtual bool generate() override

Generate API call arguments and execute the action.

Returns:

True if the generation and execution was successful. False if no arguments can be generated or the action cannot be executed in the current configuration or state of the solver under test.

virtual std::vector<uint64_t> untrace(const std::vector<std::string> &tokens) override

Replay an action.

Parameters:

tokens – The tokens of the trace statement to replay.

Returns:

A vector of ids of created objects, if objects have been created, and an empty vector otherwise. Needed to be able to compare ids of created objects to the traced ids in the trace’s return statement.

Public Static Attributes

static const Kind s_name = "get-unsat-core"

The name of this action.

class ActionGetValue : public murxla::Action

The action to get the value of a set of terms.

Public Functions

ActionGetValue(SolverManager &smgr)

Constructor.

Parameters:

smgr – The associated solver manager.

virtual bool generate() override

Generate API call arguments and execute the action.

Returns:

True if the generation and execution was successful. False if no arguments can be generated or the action cannot be executed in the current configuration or state of the solver under test.

virtual std::vector<uint64_t> untrace(const std::vector<std::string> &tokens) override

Replay an action.

Parameters:

tokens – The tokens of the trace statement to replay.

Returns:

A vector of ids of created objects, if objects have been created, and an empty vector otherwise. Needed to be able to compare ids of created objects to the traced ids in the trace’s return statement.

Public Static Attributes

static const Kind s_name = "get-value"

The name of this action.

class ActionPush : public murxla::Action

The action to push one or more context levels.

Public Functions

inline ActionPush(SolverManager &smgr)

Constructor.

Parameters:

smgr – The associated solver manager.

virtual bool generate() override

Generate API call arguments and execute the action.

Returns:

True if the generation and execution was successful. False if no arguments can be generated or the action cannot be executed in the current configuration or state of the solver under test.

virtual std::vector<uint64_t> untrace(const std::vector<std::string> &tokens) override

Replay an action.

Parameters:

tokens – The tokens of the trace statement to replay.

Returns:

A vector of ids of created objects, if objects have been created, and an empty vector otherwise. Needed to be able to compare ids of created objects to the traced ids in the trace’s return statement.

Public Static Attributes

static const Kind s_name = "push"

The name of this action.

class ActionPop : public murxla::Action

The action to pop one or more context levels.

Public Functions

inline ActionPop(SolverManager &smgr)

Constructor.

Parameters:

smgr – The associated solver manager.

virtual bool generate() override

Generate API call arguments and execute the action.

Returns:

True if the generation and execution was successful. False if no arguments can be generated or the action cannot be executed in the current configuration or state of the solver under test.

virtual std::vector<uint64_t> untrace(const std::vector<std::string> &tokens) override

Replay an action.

Parameters:

tokens – The tokens of the trace statement to replay.

Returns:

A vector of ids of created objects, if objects have been created, and an empty vector otherwise. Needed to be able to compare ids of created objects to the traced ids in the trace’s return statement.

Public Static Attributes

static const Kind s_name = "pop"

The name of this action.

class ActionReset : public murxla::Action

The action to reset the solver.

Public Functions

inline ActionReset(SolverManager &smgr)

Constructor.

Parameters:

smgr – The associated solver manager.

virtual bool generate() override

Generate API call arguments and execute the action.

Returns:

True if the generation and execution was successful. False if no arguments can be generated or the action cannot be executed in the current configuration or state of the solver under test.

virtual std::vector<uint64_t> untrace(const std::vector<std::string> &tokens) override

Replay an action.

Parameters:

tokens – The tokens of the trace statement to replay.

Returns:

A vector of ids of created objects, if objects have been created, and an empty vector otherwise. Needed to be able to compare ids of created objects to the traced ids in the trace’s return statement.

Public Static Attributes

static const Kind s_name = "reset"

The name of this action.

class ActionResetAssertions : public murxla::Action

The action to reset the set of currently asserted formulas.

Public Functions

inline ActionResetAssertions(SolverManager &smgr)

Constructor.

Parameters:

smgr – The associated solver manager.

virtual bool generate() override

Generate API call arguments and execute the action.

Returns:

True if the generation and execution was successful. False if no arguments can be generated or the action cannot be executed in the current configuration or state of the solver under test.

virtual std::vector<uint64_t> untrace(const std::vector<std::string> &tokens) override

Replay an action.

Parameters:

tokens – The tokens of the trace statement to replay.

Returns:

A vector of ids of created objects, if objects have been created, and an empty vector otherwise. Needed to be able to compare ids of created objects to the traced ids in the trace’s return statement.

Public Static Attributes

static const Kind s_name = "reset-assertions"

The name of this action.

class ActionPrintModel : public murxla::Action

The action to print model.

Public Functions

inline ActionPrintModel(SolverManager &smgr)

Constructor.

Parameters:

smgr – The associated solver manager.

virtual bool generate() override

Generate API call arguments and execute the action.

Returns:

True if the generation and execution was successful. False if no arguments can be generated or the action cannot be executed in the current configuration or state of the solver under test.

virtual std::vector<uint64_t> untrace(const std::vector<std::string> &tokens) override

Replay an action.

Parameters:

tokens – The tokens of the trace statement to replay.

Returns:

A vector of ids of created objects, if objects have been created, and an empty vector otherwise. Needed to be able to compare ids of created objects to the traced ids in the trace’s return statement.

Public Static Attributes

static const Kind s_name = "print-model"

The name of this action.

class ActionTermGetChildren : public murxla::Action

The action to get the children of a term.

Public Functions

inline ActionTermGetChildren(SolverManager &smgr)

Constructor.

Parameters:

smgr – The associated solver manager.

virtual bool generate() override

Generate API call arguments and execute the action.

Returns:

True if the generation and execution was successful. False if no arguments can be generated or the action cannot be executed in the current configuration or state of the solver under test.

virtual std::vector<uint64_t> untrace(const std::vector<std::string> &tokens) override

Replay an action.

Parameters:

tokens – The tokens of the trace statement to replay.

Returns:

A vector of ids of created objects, if objects have been created, and an empty vector otherwise. Needed to be able to compare ids of created objects to the traced ids in the trace’s return statement.

Public Static Attributes

static const Kind s_name = "term-get-children"

The name of this action.