package bitvectors
- Alphabetic
- Public
- Protected
Type Members
- case class GaloisField(p: IdealInt) extends ModRing with Field with Product with Serializable
Galois fields of cardinality
p, for some prime numberp. - class ModRing extends Ring with RingWithOrder with CommutativeRing with RingWithIntConversions
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
Value Members
- 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]. - 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.