bitvectors

case class GaloisField(p: IdealInt) extends ModRing with Field with Product with Serializable

Galois fields of cardinality p, for some prime number p.
Galois fields of cardinality p, for some prime number p.
class ModRing extends Ring with RingWithOrder with CommutativeRing with RingWithIntConversions

Modular arithmetic in the interval [lower, upper].
Modular arithmetic in the interval [lower, upper].
case class SignedBVRing(bits: Int) extends ModRing with EuclidianRing with Product with Serializable

Ring of signed fixed-size bit-vectors
case class UnsignedBVRing(bits: Int) extends ModRing with EuclidianRing with Product with Serializable

Ring of unsigned fixed-size bit-vectors

object ExtractArithEncoder extends TheoryProcedure

ExtractArithEncoder translates bv_extract to an existentially quantified equation
object LShiftCastSplitter extends TheoryProcedure

Splitter handles the splitting of l_shift_cast-operations, when no other inference steps are possible anymore.
object ModCastSplitter extends TheoryProcedure

Splitter handles the splitting of mod_cast-operations, when no other inference steps are possible anymore.
object ModPlugin extends Plugin
object ModPostprocessor extends CollectingVisitor[Sort, IExpression]

Post-processing of bit-vector formulas to make them correctly typed.
object ModPreprocessor

Pre-processing of formulas
object ModReducer

Reducer for modular arithmetic
object ModRing

Modular arithmetic in the interval [lower, upper].
Modular arithmetic in the interval [lower, upper].
object ModuloArithmetic extends Theory

Theory for performing bounded modulo-arithmetic (arithmetic modulo some number N).
Theory for performing bounded modulo-arithmetic (arithmetic modulo some number N). This in particular includes bit-vector/machine arithmetic.
object RShiftCastSplitter extends TheoryProcedure

Splitter handles the splitting of r_shift_cast-operations, when no other inference steps are possible anymore.