 # ModuloArithmetic

### Related Doc: package bitvectors

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

2. #### abstract class IndexedBVOp extends SortedIFunction

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

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

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

### Value Members

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

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

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

Definition Classes
AnyRef → Any

8. #### object SignedBVSort

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

9. #### object UnsignedBVSort

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

14. #### final def asInstanceOf[T0]: T0

Definition Classes
Any
15. #### val axioms: Conjunction

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

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

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

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

Cast a term to a signed bit-vector term.

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

Cast a term to a modulo sort.

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

Cast a term to an unsigned bit-vector term.

71. #### def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( ... )

73. #### val debug: Boolean

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

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

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

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

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

Evaluate `bv_extract` with concrete arguments

Evaluate `bv_extract` with concrete arguments

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

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

Evaluate `mod_cast` with concrete arguments

Evaluate `mod_cast` with concrete arguments

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

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

Add the symbols defined by this theory to the `order`

Add the symbols defined by this theory to the `order`

Definition Classes
Theory

84. #### def finalize(): Unit

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

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

87. #### val functionalPredicates: Set[Predicate]

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]

Interpreted functions of the theory

Interpreted functions of the theory

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

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[_]

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

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

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

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

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

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

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

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

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

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

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

Definition Classes
AnyRef

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

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

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

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

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

Attributes
protected[ap.theories.bitvectors]

110. #### val predicateMatchConfig: PredicateMatchConfig

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]

Interpreted predicates of the theory

Interpreted predicates of the theory

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

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

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

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

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

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.

118. #### val singleInstantiationPredicates: Set[Predicate]

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

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

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

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]

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

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

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

Definition Classes
AnyRef
Annotations
@throws( ... )