Operators

Murxla globally defines a base set of operator kinds as static const members of type murxla::Op::Kind of class murxla::Op. Operator kinds are maintained by an operator kind manager (murxla::OpKindManager), and each kind is associated with an murxla::Op object, which maintains configuration data such as its associated theory, arity, number of indices, the sort kind of a term of that operator kind and the sort kinds of its arguments.

Solver-specific operator kinds are (by convention) defined as a static const member of type murxla::Op::Kind 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);

Configuration Macros

MURXLA_MK_TERM_N_ARGS

Arity of n-ary operators that expect at least one argument.

MURXLA_MK_TERM_N_ARGS_BIN

Arity of n-ary operators that expect at least two arguments.

Operator

struct Op

The struct representing an operator.

Public Types

using Kind = std::string

The kind of an operator.

Public Functions

Op(uint64_t id, const Kind &kind, int32_t arity, uint32_t nidxs, SortKindSet sort_kinds, const std::vector<SortKindSet> &sort_kinds_args, Theory theory)

Constructor.

Parameters:

  • id – The unique id of the operator.

  • kind – The kind of the operator.

  • arity – The arity of the operator. Use MURXLA_MK_TERM_N_ARGS for n-ary operators that expect at least one argument, and MURXLA_MK_TERM_N_ARGS_BIN for n-ary operators that expect at least two arguments.

  • nidxs – The number of indices of the operator.

  • sort_kinds – The sort kind of the operator.

  • sort_kinds_args – A vector of sorts of the operators’ arguments. If all or the remaining kinds are the same, it’s sufficient to only list it once.

  • theory – The associated theory.

bool operator==(const Op &other) const

Operator overload for equality over operators.

Parameters:

other – The operator to be compared with this operator.

Returns:

True if both operators are equal.

SortKindSet get_arg_sort_kind(size_t i) const

Get the argument sort kind at index i.

Parameters:

i – The index of the argument sort kinds vector to query.

Returns:

The sort kind of the operator argument at given index.

Public Members

uint64_t d_id = 0u

The operator id, assigned in the order operators have been created.

const Kind &d_kind = UNDEFINED

The operator kind.

int32_t d_arity

The arity (number of arguments) of this operator kind.

Is MURXLA_MK_TERM_N_ARGS for n-ary operators that expect at least one argument, and MURXLA_MK_TERM_N_ARGS_BIN for n-ary operators that expect at least two arguments.

uint32_t d_nidxs

The number of indices if indexed.

SortKindSet d_sort_kinds

The sort kind of a term of this kind.

Will contain more than one sort kind for operators that can be of SORT_ANY, which is expanded via get_all_sort_kinds_for_any() with all sort kinds supported by the solver when operators are added to the OpKindManager via OpKindManager::add_op_kind().

May not contain SORT_ANY.

Theory d_theory

The theory to which the operator belongs to.

Operator Kinds

Operator kinds are defined as static members of struct murxla::Op, see the list of pre-defined operator kinds.

Operator Kind Datastructures

using murxla::OpKindVector = std::vector<Op::Kind>

A std::vector of operator kinds.

using murxla::OpKindSet = std::unordered_set<Op::Kind>

A std::unordered_set of operator kinds.

using murxla::OpKindMap = std::unordered_map<Op::Kind, Op>

A std::unordered_map mapping operator kind to operator.

using murxla::OpKinds = std::unordered_map<SortKind, OpKindVector>

A std::unordered_map mapping sort kind of an operator to operator kinds of that sort kind.

Operator Management

class OpKindManager

The operator kinds manager.

Maintains the current set of operator kinds, based on enabled theories and unsupported operator kinds.

Public Functions

inline OpKindManager(const TheorySet &enabled_theories, const SortKindMap &enabled_sort_kinds, const OpKindSet &disabled_op_kinds, const std::unordered_map<Op::Kind, SortKindSet> &unsupported_op_kind_sorts, bool arith_linear, statistics::Statistics *stats)

Constructor.

Parameters:

  • enabled_theories – The set of enabled theories.

  • enabled_sort_kinds – The enabled sort kinds. Maps sort kind to sort kind data.

  • disabled_op_kinds – The set of disabled operator kinds.

  • unsupported_op_kind_sorts – The unsupported sorts for operator kinds. Maps operator kind to set of unsupported sort kinds.

  • arith_linear – True to restrict arithmetic operators to linear fragment.

  • stats – The associated statistics object.

Op &get_op(const Op::Kind &kind)

Get operator of given kind. Returns a reference to d_op_undefined if the op kind has not been added to the op database.

void add_op_kind(const Op::Kind &kind, int32_t arity, uint32_t nidxs, SortKind sort_kind, const std::vector<SortKind> &sort_kind_args, Theory theory)

Add operator kind to operator kinds database.

Parameters:

  • kind – The kind of the operator.

  • arity – The arity of the operator

  • nidxs – The number of indices of the operator.

  • sort_kind – The sort kind of the operator.

  • sort_kind_args – A vector of sorts of the operators’ arguments. If all or the remaining kinds are the same, it’s sufficient to only list it once.

  • theory – The associated theory.

inline const OpKindMap &get_op_kinds()

Get a map of enabled operator kinds to their corresponding operator.

Returns:

A map mapping enabled operator kinds to their corresponding Op.