Object

ap.theories.bitvectors

ModuloArithmetic

Related Doc: package bitvectors

Permalink

object ModuloArithmetic extends Theory

Theory for performing bounded modulo-arithmetic (arithmetic modulo some number N). This in particular includes bit-vector/machine arithmetic.

Class under construction ...

Linear Supertypes
Theory, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. ModuloArithmetic
  2. Theory
  3. AnyRef
  4. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. class BVNAryOp extends IndexedBVOp

    Permalink
  2. abstract class IndexedBVOp extends SortedIFunction

    Permalink

    Generic class to represent families of functions, indexed by a vector of bit-widths.

  3. case class ModSort(lower: IdealInt, upper: IdealInt) extends ProxySort with Product with Serializable

    Permalink

    Modulo sorts, representing the interval [lower, upper] with wrap-around arithmetic.

    Modulo sorts, representing the interval [lower, upper] with wrap-around arithmetic.

  4. class ShiftFunction extends SortedIFunction

    Permalink
  5. class ShiftPredicate extends SortedPredicate

    Permalink

Value Members

  1. final def !=(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  4. object BVComp extends IndexedBVOp

    Permalink
  5. object BVConcat extends IndexedBVOp

    Permalink
  6. object BVExtract extends IndexedBVOp

    Permalink
  7. val MultTheory: nia.GroebnerMultiplication.type

    Permalink
  8. object SignedBVSort

    Permalink

    Object to create and recognise modulo sorts representing signed bit-vectors.

  9. object UnsignedBVSort

    Permalink

    Object to create and recognise modulo sorts representing unsigned bit-vectors.

  10. val _bv_extract: Predicate

    Permalink
  11. val _l_shift_cast: ShiftPredicate

    Permalink
  12. val _mod_cast: SortedPredicate

    Permalink
  13. val _r_shift_cast: ShiftPredicate

    Permalink
  14. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  15. val axioms: Conjunction

    Permalink

    Axioms defining the theory; such axioms are simply added as formulae to the problem to be proven, and thus handled using the standard reasoning techniques (including e-matching).

    Axioms defining the theory; such axioms are simply added as formulae to the problem to be proven, and thus handled using the standard reasoning techniques (including e-matching).

    Definition Classes
    ModuloArithmeticTheory
  16. def bv(width: Int, num: IdealInt): ITerm

    Permalink
  17. val bv_add: BVNAryOp

    Permalink
  18. val bv_and: BVNAryOp

    Permalink
  19. val bv_ashr: BVNAryOp

    Permalink
  20. val bv_comp: BVComp.type

    Permalink
  21. val bv_concat: BVConcat.type

    Permalink
  22. val bv_extract: BVExtract.type

    Permalink
  23. val bv_lshr: BVNAryOp

    Permalink
  24. val bv_mul: BVNAryOp

    Permalink
  25. val bv_neg: BVNAryOp

    Permalink
  26. val bv_not: BVNAryOp

    Permalink
  27. val bv_or: BVNAryOp

    Permalink
  28. val bv_sdiv: BVNAryOp

    Permalink
  29. val bv_shl: BVNAryOp

    Permalink
  30. val bv_sle: Predicate

    Permalink
  31. val bv_slt: Predicate

    Permalink
  32. val bv_smod: BVNAryOp

    Permalink
  33. val bv_srem: BVNAryOp

    Permalink
  34. val bv_sub: BVNAryOp

    Permalink
  35. val bv_udiv: BVNAryOp

    Permalink
  36. val bv_ule: Predicate

    Permalink
  37. val bv_ult: Predicate

    Permalink
  38. val bv_urem: BVNAryOp

    Permalink
  39. val bv_xnor: BVNAryOp

    Permalink
  40. val bv_xor: BVNAryOp

    Permalink
  41. def bvadd(t1: ITerm, t2: ITerm): ITerm

    Permalink
  42. def bvand(t1: ITerm, t2: ITerm): ITerm

    Permalink
  43. def bvashr(t1: ITerm, t2: ITerm): ITerm

    Permalink
  44. def bvcomp(t1: ITerm, t2: ITerm): ITerm

    Permalink
  45. def bvlshr(t1: ITerm, t2: ITerm): ITerm

    Permalink
  46. def bvmul(t1: ITerm, t2: ITerm): ITerm

    Permalink
  47. def bvneg(t: ITerm): ITerm

    Permalink
  48. def bvnot(t: ITerm): ITerm

    Permalink
  49. def bvor(t1: ITerm, t2: ITerm): ITerm

    Permalink
  50. def bvsdiv(t1: ITerm, t2: ITerm): ITerm

    Permalink
  51. def bvsge(t1: ITerm, t2: ITerm): IFormula

    Permalink
  52. def bvsgt(t1: ITerm, t2: ITerm): IFormula

    Permalink
  53. def bvshl(t1: ITerm, t2: ITerm): ITerm

    Permalink
  54. def bvsle(t1: ITerm, t2: ITerm): IFormula

    Permalink
  55. def bvslt(t1: ITerm, t2: ITerm): IFormula

    Permalink
  56. def bvsmod(t1: ITerm, t2: ITerm): ITerm

    Permalink
  57. def bvsrem(t1: ITerm, t2: ITerm): ITerm

    Permalink
  58. def bvsub(t1: ITerm, t2: ITerm): ITerm

    Permalink
  59. def bvudiv(t1: ITerm, t2: ITerm): ITerm

    Permalink
  60. def bvuge(t1: ITerm, t2: ITerm): IFormula

    Permalink
  61. def bvugt(t1: ITerm, t2: ITerm): IFormula

    Permalink
  62. def bvule(t1: ITerm, t2: ITerm): IFormula

    Permalink
  63. def bvult(t1: ITerm, t2: ITerm): IFormula

    Permalink
  64. def bvurem(t1: ITerm, t2: ITerm): ITerm

    Permalink
  65. def bvxnor(t1: ITerm, t2: ITerm): ITerm

    Permalink
  66. def bvxor(t1: ITerm, t2: ITerm): ITerm

    Permalink
  67. def cast2Interval(lower: IdealInt, upper: IdealInt, t: ITerm): ITerm

    Permalink

    Cast a term to an integer interval, with modulo semantics.

  68. def cast2SignedBV(bits: Int, t: ITerm): ITerm

    Permalink

    Cast a term to a signed bit-vector term.

  69. def cast2Sort(sort: ModSort, t: ITerm): ITerm

    Permalink

    Cast a term to a modulo sort.

  70. def cast2UnsignedBV(bits: Int, t: ITerm): ITerm

    Permalink

    Cast a term to an unsigned bit-vector term.

  71. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  72. def concat(t1: ITerm, t2: ITerm): ITerm

    Permalink
  73. val debug: Boolean

    Permalink
    Attributes
    protected[ap.theories.bitvectors]
  74. val dependencies: Iterable[Theory]

    Permalink

    Optionally, other theories that this theory depends on.

    Optionally, other theories that this theory depends on. Specified dependencies will be loaded before this theory, but the preprocessors of the dependencies will be called after the preprocessor of this theory.

    Definition Classes
    ModuloArithmeticTheory
  75. val directlyEncodeExtract: Boolean

    Permalink
    Attributes
    protected[ap.theories.bitvectors]
  76. final def eq(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  77. def equals(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  78. def evalExtract(start: Int, end: Int, number: IdealInt): IdealInt

    Permalink

    Evaluate bv_extract with concrete arguments

    Evaluate bv_extract with concrete arguments

  79. def evalFun(f: IFunApp): Option[ITerm]

    Permalink

    Optionally, a function evaluating theory functions applied to concrete arguments, represented as constructor terms.

    Optionally, a function evaluating theory functions applied to concrete arguments, represented as constructor terms.

    Definition Classes
    ModuloArithmeticTheory
  80. def evalModCast(lower: IdealInt, upper: IdealInt, number: IdealInt): IdealInt

    Permalink

    Evaluate mod_cast with concrete arguments

    Evaluate mod_cast with concrete arguments

  81. def evalPred(a: IAtom): Option[Boolean]

    Permalink

    Optionally, a function evaluating theory predicates applied to concrete arguments, represented as constructor terms.

    Optionally, a function evaluating theory predicates applied to concrete arguments, represented as constructor terms.

    Definition Classes
    ModuloArithmeticTheory
  82. def extend(order: TermOrder): TermOrder

    Permalink

    Add the symbols defined by this theory to the order

    Add the symbols defined by this theory to the order

    Definition Classes
    Theory
  83. def extract(begin: Int, end: Int, t: ITerm): ITerm

    Permalink
  84. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  85. val functionPredicateMapping: List[(SortedIFunction, Predicate)]

    Permalink

    Mapping of interpreted functions to interpreted predicates, used translating input ASTs to internal ASTs (the latter only containing predicates).

    Mapping of interpreted functions to interpreted predicates, used translating input ASTs to internal ASTs (the latter only containing predicates).

    Definition Classes
    ModuloArithmeticTheory
  86. val functionTranslation: Map[IFunction, Predicate]

    Permalink
  87. val functionalPredicates: Set[Predicate]

    Permalink

    Information which of the predicates satisfy the functionality axiom; at some internal points, such predicates can be handled more efficiently

    Information which of the predicates satisfy the functionality axiom; at some internal points, such predicates can be handled more efficiently

    Definition Classes
    ModuloArithmeticTheory
  88. val functions: List[SortedIFunction]

    Permalink

    Interpreted functions of the theory

    Interpreted functions of the theory

    Definition Classes
    ModuloArithmeticTheory
  89. def generateDecoderData(model: Conjunction): Option[TheoryDecoderData]

    Permalink

    If this theory defines any Theory.Decoder, which can translate model data into some theory-specific representation, this function can be overridden to pre-compute required data from a model.

    If this theory defines any Theory.Decoder, which can translate model data into some theory-specific representation, this function can be overridden to pre-compute required data from a model.

    Definition Classes
    Theory
  90. final def getClass(): Class[_]

    Permalink
    Definition Classes
    AnyRef → Any
  91. def getLowerUpper(arguments: Seq[Term]): (IdealInt, IdealInt)

    Permalink
    Attributes
    protected[ap.theories.bitvectors]
  92. def getModulus(a: Atom): IdealInt

    Permalink
    Attributes
    protected[ap.theories.bitvectors]
  93. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  94. def iPreprocess(f: IFormula, signature: Signature): (IFormula, Signature)

    Permalink

    Optionally, a pre-processor that is applied to formulas over this theory, prior to sending the formula to a prover.

    Optionally, a pre-processor that is applied to formulas over this theory, prior to sending the formula to a prover. This method will be applied very early in the translation process.

    Definition Classes
    ModuloArithmeticTheory
  95. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  96. def isSoundForSat(theories: Seq[Theory], config: Theory.SatSoundnessConfig.Value): Boolean

    Permalink

    Check whether we can tell that the given combination of theories is sound for checking satisfiability of a problem, i.e., if proof construction ends up in a dead end, can it be concluded that a problem is satisfiable.

    Check whether we can tell that the given combination of theories is sound for checking satisfiability of a problem, i.e., if proof construction ends up in a dead end, can it be concluded that a problem is satisfiable.

    Definition Classes
    ModuloArithmeticTheory
  97. val l_shift_cast: ShiftFunction

    Permalink

    Function for multiplying any number t with 2^n and mapping to an interval [lower, upper].

    Function for multiplying any number t with 2^n and mapping to an interval [lower, upper]. The function is applied as l_shift_cast(lower, upper, t, n).

  98. val mod_cast: SortedIFunction

    Permalink

    Function for mapping any number to an interval [lower, upper].

    Function for mapping any number to an interval [lower, upper]. The function is applied as mod_cast(lower, upper, number)

  99. final def ne(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  100. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
  101. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
  102. val order: TermOrder

    Permalink
  103. val otherPreds: List[Predicate]

    Permalink
  104. val plugin: Some[ModPlugin.type]

    Permalink

    Optionally, a plug-in implementing reasoning in this theory

    Optionally, a plug-in implementing reasoning in this theory

    Definition Classes
    ModuloArithmeticTheory
  105. def pow2(bits: IdealInt): IdealInt

    Permalink
    Attributes
    protected[ap.theories.bitvectors]
  106. def pow2(bits: Int): IdealInt

    Permalink
    Attributes
    protected[ap.theories.bitvectors]
  107. def pow2MinusOne(bits: Int): IdealInt

    Permalink
    Attributes
    protected[ap.theories.bitvectors]
  108. def pow2Mod(bits: IdealInt, modulus: IdealInt): IdealInt

    Permalink
    Attributes
    protected[ap.theories.bitvectors]
  109. val preAxioms: Formula

    Permalink
  110. val predicateMatchConfig: PredicateMatchConfig

    Permalink

    Information how interpreted predicates should be handled for e-matching.

    Information how interpreted predicates should be handled for e-matching.

    Definition Classes
    ModuloArithmeticTheory
  111. val predicates: Seq[Predicate]

    Permalink

    Interpreted predicates of the theory

    Interpreted predicates of the theory

    Definition Classes
    ModuloArithmeticTheory
  112. def preprocess(f: Conjunction, order: TermOrder): Conjunction

    Permalink

    Optionally, a pre-processor that is applied to formulas over this theory, prior to sending the formula to a prover.

    Optionally, a pre-processor that is applied to formulas over this theory, prior to sending the formula to a prover.

    Definition Classes
    ModuloArithmeticTheory
  113. val r_shift_cast: ShiftFunction

    Permalink

    Function for dividing any number t by 2^n, rounding towards negative, and mapping to an interval [lower, upper].

    Function for dividing any number t by 2^n, rounding towards negative, and mapping to an interval [lower, upper]. The function is applied as r_shift_cast(lower, upper, t, n).

  114. val reducerPlugin: ReducerPluginFactory

    Permalink

    Optionally, a plugin for the reducer applied to formulas both before and during proving.

    Optionally, a plugin for the reducer applied to formulas both before and during proving.

    Definition Classes
    ModuloArithmeticTheory
  115. def shiftLeft(sort: ModSort, shifted: ITerm, bits: ITerm): ITerm

    Permalink

    Shift the term shifted a number of bits to the left, staying within the given sort.

    Shift the term shifted a number of bits to the left, staying within the given sort.

  116. def shiftRight(sort: ModSort, shifted: ITerm, bits: ITerm): ITerm

    Permalink

    Shift the term shifted a number of bits to the right, staying within the given sort.

    Shift the term shifted a number of bits to the right, staying within the given sort.

  117. def sign_extend(addWidth: Int, t: ITerm): ITerm

    Permalink
  118. val singleInstantiationPredicates: Set[Predicate]

    Permalink

    When instantiating existentially quantifier formulas, EX phi, at most one instantiation is necessary provided that all predicates in phi are contained in this set.

    When instantiating existentially quantifier formulas, EX phi, at most one instantiation is necessary provided that all predicates in phi are contained in this set.

    Definition Classes
    ModuloArithmeticTheory
  119. final def synchronized[T0](arg0: ⇒ T0): T0

    Permalink
    Definition Classes
    AnyRef
  120. def toString(): String

    Permalink
    Definition Classes
    ModuloArithmetic → AnyRef → Any
  121. val totalityAxioms: Conjunction

    Permalink

    Additional axioms that are included if the option +genTotalityAxioms is given to Princess.

    Additional axioms that are included if the option +genTotalityAxioms is given to Princess.

    Definition Classes
    ModuloArithmeticTheory
  122. val triggerRelevantFunctions: Set[IFunction]

    Permalink

    A list of functions that should be considered in automatic trigger generation

    A list of functions that should be considered in automatic trigger generation

    Definition Classes
    ModuloArithmeticTheory
  123. final def wait(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  124. final def wait(arg0: Long, arg1: Int): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  125. final def wait(arg0: Long): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  126. def zero_extend(addWidth: Int, t: ITerm): ITerm

    Permalink

Inherited from Theory

Inherited from AnyRef

Inherited from Any

Ungrouped