bitvectors
Interface for handling different kinds of bit-vector atoms in the
ModCastSplitter.
Galois fields of cardinality p, for some prime
number p.
Galois fields of cardinality p, for some prime
number p.
Modular arithmetic in the interval [lower, upper].
Modular arithmetic in the interval [lower, upper].
Ring of signed fixed-size bit-vectors
Ring of unsigned fixed-size bit-vectors
BitwiseOpIntervalPropagator handles interval constraint propagation between the arguments and results of bit-wise operators, currently bv_and.
Class responsible for splitting bit-wise operators, moving gradually towards a fully bit-blasted representation of the operator.
Splitter handles the splitting of mod_cast,
l_shift_cast, r_shift_cast.
Splitter handles the splitting of mod_cast,
l_shift_cast, r_shift_cast.
ExtractArithEncoder translates bv_extract to an existentially quantified equation
ExtractIntervalPropagator handles interval constraint propagation between the arguments and results of extract atoms.
Partition extract-atoms for given terms to eliminate overlapping extracts.
Class implementing some bit-vector-specific simplification rules for
inequalities over zero-one variables:
s >= 2*t - 1 --> s >= t and
2*s >= t --> s >= t.
Class implementing some bit-vector-specific simplification rules for
inequalities over zero-one variables:
s >= 2*t - 1 --> s >= t and
2*s >= t --> s >= t.
TODO: can those rules be implemented within the ModReducer?
Splitter handles the splitting of l_shift_cast-operations, when no other inference steps are possible anymore.
Splitter handles the splitting of mod_cast-operations, when no other inference steps are possible anymore.
Post-processing of bit-vector formulas to make them correctly typed.
Pre-processing of formulas
Reducer for modular arithmetic
Modular arithmetic in the interval [lower, upper].
Modular arithmetic in the interval [lower, upper].
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.
Splitter handles the splitting of r_shift_cast-operations, when no other inference steps are possible anymore.
Interface for handling different kinds of bit-vector atoms in the
ModCastSplitter.