Theories

enum murxla::Theory

Values:

enumerator THEORY_ARRAY: Theory of arrays with extensionality as defined in SMT-LIB.

enumerator THEORY_BAG

The not yet standardized theory of bags, mostly based on cvc5’s theory definition for bags.

A bag (or multiset) \(m\) is a function from the domain \(D\) of its elements to the set of natural numbers (i.e., \(m : D \longrightarrow \mathbb{N}\)) where \(m(e)\) represents the multiplicity of element \(e\) in bag \(m\).

enumerator THEORY_BOOL: Theory of Booleans as defined in SMT-LIB as Core theory.

enumerator THEORY_BV

Theory of fixed-size bit-vectors as defined in SMT-LIB.

Includes extensions defined in the SMT-LIB logic of quantifier-free bit-vectors (QF_BV) .

enumerator THEORY_DT

The meta theory of algebraic datatypes.

In SMT-LIB, support for algebraic datatypes is part of the language definition rather than a theory definition. We introduce a meta theory for datatypes in order to simplify handling solver-specific support for it (most solvers don’t support algebraic datatypes).

enumerator THEORY_FF: Theory of finite-field arithmetic, as defined in this paper .

enumerator THEORY_FP: Theory of floating-point arithmetic as defined in SMT-LIB.

enumerator THEORY_INT

Theory of Ints as defined in SMT-LIB.

Includes extensions defined in the SMT-LIB theory of Reals_Ints .

enumerator THEORY_QUANT

The meta theory of quantifiers.

We only create quantified formulas when this theory is enabled. Introducing quantifiers as a meta theory further simplifies the configuration on solver-specific restrictions specific to quantifiers.

enumerator THEORY_REAL: Theory of Reals as defined in SMT-LIB. Includes extensions defined in the SMT-LIB theory of Reals_Ints .

enumerator THEORY_SEQ

The not yet standardized theory of sequences, mostly based on cvc5’s theory definition for sequences.

A sequence is a finite list of elements that supports common operations such as the extraction of subsequences, the concatenation of sequences, the replacement of subsequences, and matching against regular expressions.

enumerator THEORY_SET: The not yet standardized theory of bags, mostly based on cvc5’s theory definition for bags .

enumerator THEORY_STRING: Theory of strings as defined in SMT-LIB.

enumerator THEORY_TRANSCENDENTAL: The not yet standardized theory of transcendentals, mostly based on cvc5’s theory definition for transcendentals .

enumerator THEORY_UF

The meta theory of uninterpreted functions.

This theory introduces free sort and function symbols. Introducing these as a meta theory simplifies the configuration on solver-specific restrictions specific to uninterpreted sorts and functions.

enumerator THEORY_ALL: The meta theory representing all enabled theories.

using murxla::TheoryVector = std::vector<Theory>: A std::vector of theories.

using murxla::TheorySet = std::unordered_set<Theory>: A std::unordered_set of theories.

std::ostream &murxla::operator<<(std::ostream &out, Theory theory)

Serialize a theory to given stream.

Parameters:

out – The output stream.
theory – The theory to be serialized.

Returns:

The output stream.