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

3. abstract class IndexedBVOp extends SortedIFunction

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

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

15. final def asInstanceOf[T0]: T0

Definition Classes
Any
16. 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

68. def cast2Int(t: ITerm): ITerm

Cast a term to an integer term.

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

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

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

Cast a term to a signed bit-vector term.

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

Cast a term to a modulo sort.

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

Cast a term to an unsigned bit-vector term.

73. def clone(): AnyRef

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

75. val debug: Boolean

Attributes
protected[ap.theories.bitvectors]
76. 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
77. val directlyEncodeExtract: Boolean

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

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

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

Evaluate `bv_extract` with concrete arguments

Evaluate `bv_extract` with concrete arguments

81. 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
82. def evalModCast(lower: IdealInt, upper: IdealInt, number: IdealInt): IdealInt

Evaluate `mod_cast` with concrete arguments

Evaluate `mod_cast` with concrete arguments

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

86. def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( classOf[java.lang.Throwable] )
87. 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

89. 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
90. val functions: List[SortedIFunction]

Interpreted functions of the theory

Interpreted functions of the theory

Definition Classes
ModuloArithmeticTheory
91. 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
92. final def getClass(): Class[_]

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

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

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

Definition Classes
AnyRef → Any
96. def iPostprocess(f: IFormula, signature: Signature): IFormula

Optionally, a post-processor that is applied to formulas output by the prover, for instance to interpolants or the result of quantifier elimination.

Optionally, a post-processor that is applied to formulas output by the prover, for instance to interpolants or the result of quantifier elimination. This method will be applied to the formula after calling `Internal2Inputabsy`.

Definition Classes
ModuloArithmeticTheory
97. 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
98. val int_cast: MonoSortedIFunction

Function to map the modulo-sorts back to integers.

Function to map the modulo-sorts back to integers. Semantically this is just the identify function

99. final def isInstanceOf[T0]: Boolean

Definition Classes
Any
100. 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
101. 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)`.

102. 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)`

103. val modelGenPredicates: Set[Predicate]

Optionally, a set of predicates used by the theory to tell the `PresburgerModelFinder` about terms that will be handled exclusively by this theory.

Optionally, a set of predicates used by the theory to tell the `PresburgerModelFinder` about terms that will be handled exclusively by this theory. If a proof goal in model generation mode contains an atom `p(x)`, for `p` in this set, then the `PresburgerModelFinder` will ignore `x` when assigning concrete values to symbols.

Definition Classes
Theory
104. final def ne(arg0: AnyRef): Boolean

Definition Classes
AnyRef
105. final def notify(): Unit

Definition Classes
AnyRef
106. final def notifyAll(): Unit

Definition Classes
AnyRef

109. 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
110. def postSimplifiers: Seq[(IExpression) ⇒ IExpression]

Optionally, simplifiers that are applied to formulas output by the prover, for instance to interpolants or the result of quantifier.

Optionally, simplifiers that are applied to formulas output by the prover, for instance to interpolants or the result of quantifier. Such simplifiers are invoked by with `ap.parser.Simplifier`.

Definition Classes
Theory
111. def postprocess(f: Conjunction, order: TermOrder): Conjunction

Optionally, a post-processor that is applied to formulas output by the prover, for instance to interpolants or the result of quantifier elimination.

Optionally, a post-processor that is applied to formulas output by the prover, for instance to interpolants or the result of quantifier elimination. This method will be applied to the raw formulas, before calling `Internal2Inputabsy`.

Definition Classes
Theory
112. def pow2(bits: IdealInt): IdealInt

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

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

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

Attributes
protected[ap.theories.bitvectors]

117. 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
118. val predicates: Seq[Predicate]

Interpreted predicates of the theory

Interpreted predicates of the theory

Definition Classes
ModuloArithmeticTheory
119. 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
120. 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)`.

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

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

125. 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
126. final def synchronized[T0](arg0: ⇒ T0): T0

Definition Classes
AnyRef
127. def toString(): String

Definition Classes
ModuloArithmetic → AnyRef → Any
128. 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
129. 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
130. final def wait(): Unit

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

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

Definition Classes
AnyRef
Annotations
@throws( ... )