Package

ap.theories

bitvectors

Permalink

package bitvectors

Visibility
  1. Public
  2. All

Type Members

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

    Permalink

    Galois fields of cardinality p, for some prime number p.

    Galois fields of cardinality p, for some prime number p.

  2. class ModRing extends Ring with RingWithOrder with CommutativeRing with RingWithIntConversions

    Permalink

    Modular arithmetic in the interval [lower, upper].

    Modular arithmetic in the interval [lower, upper].

  3. case class SignedBVRing(bits: Int) extends ModRing with EuclidianRing with Product with Serializable

    Permalink

    Ring of signed fixed-size bit-vectors

  4. case class UnsignedBVRing(bits: Int) extends ModRing with EuclidianRing with Product with Serializable

    Permalink

    Ring of unsigned fixed-size bit-vectors

Value Members

  1. object ExtractArithEncoder extends TheoryProcedure

    Permalink

    ExtractArithEncoder translates bv_extract to an existentially quantified equation

  2. object LShiftCastSplitter extends TheoryProcedure

    Permalink

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

  3. object ModCastSplitter extends TheoryProcedure

    Permalink

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

  4. object ModPlugin extends Plugin

    Permalink
  5. object ModPreprocessor

    Permalink

    Pre-processing of formulas

  6. object ModReducer

    Permalink

    Reducer for modular arithmetic

  7. object ModRing

    Permalink

    Modular arithmetic in the interval [lower, upper].

    Modular arithmetic in the interval [lower, upper].

  8. object ModuloArithmetic extends Theory

    Permalink

    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 ...

  9. object RShiftCastSplitter extends TheoryProcedure

    Permalink

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

Ungrouped