package bitvectors
- Alphabetic
- Public
- Protected
Type Members
- trait AtomSplitHandler extends AnyRef
Interface for handling different kinds of bit-vector atoms in the
ModCastSplitter. - 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 BitwiseOpIntervalPropagator
BitwiseOpIntervalPropagator handles interval constraint propagation between the arguments and results of bit-wise operators, currently bv_and.
- object BitwiseOpSplitter extends TermBasedSaturationProcedure
Class responsible for splitting bit-wise operators, moving gradually towards a fully bit-blasted representation of the operator.
- object CastAtomSplitter extends TermBasedSaturationProcedure
Splitter handles the splitting of
mod_cast,l_shift_cast,r_shift_cast. - object ExtractArithEncoder extends TheoryProcedure
ExtractArithEncoder translates bv_extract to an existentially quantified equation
- object ExtractIntervalPropagator
ExtractIntervalPropagator handles interval constraint propagation between the arguments and results of extract atoms.
- object ExtractPartitioner extends TheoryProcedure
Partition extract-atoms for given terms to eliminate overlapping extracts.
- object InEqSimplifier
Class implementing some bit-vector-specific simplification rules for inequalities over zero-one variables:
s >= 2*t - 1 --> s >= tand2*s >= t --> s >= t.Class implementing some bit-vector-specific simplification rules for inequalities over zero-one variables:
s >= 2*t - 1 --> s >= tand2*s >= t --> s >= t.TODO: can those rules be implemented within the ModReducer?
- object LShiftCastSplitHandler extends AtomSplitHandler
Splitter handles the splitting of l_shift_cast-operations, when no other inference steps are possible anymore.
- object ModCastSplitHandler extends AtomSplitHandler
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 ModuloArithmeticConstants
- object RShiftCastSplitHandler extends AtomSplitHandler
Splitter handles the splitting of r_shift_cast-operations, when no other inference steps are possible anymore.