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
ExtractArithEncoder translates bv_extract to an existentially quantified equation
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.
Class under construction ...
Splitter handles the splitting of r_shift_cast-operations, when no other inference steps are possible anymore.
Galois fields of cardinality
p
, for some prime numberp
.