class Reducer extends ReducerPlugin
- Alphabetic
- By Inheritance
- Reducer
- ReducerPlugin
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Instance Constructors
- new Reducer(state: ReducerState, baseAssumptions: Conjunction, baseOrder: TermOrder)
Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- def addAssumptions(preds: PredConj, mode: terfor.conjunctions.ReducerPlugin.ReductionMode.Value): ReducerPlugin
Add further assumptions to this reducer.
Add further assumptions to this reducer.
- Definition Classes
- Reducer → ReducerPlugin
- def addAssumptions(arithConj: ArithConj, mode: terfor.conjunctions.ReducerPlugin.ReductionMode.Value): Reducer
Add further assumptions to this reducer.
Add further assumptions to this reducer.
- Definition Classes
- Reducer → ReducerPlugin
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- lazy val baseReducer: ReduceWithConjunction
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- val factory: ReducerFactory.type
Factory to generate further instances of this plugin.
Factory to generate further instances of this plugin.
- Definition Classes
- Reducer → ReducerPlugin
- def finalReduce(conj: Conjunction): Conjunction
Do a final check whether a complete conjunction can be reduced.
Do a final check whether a complete conjunction can be reduced. All sub-formulas are already fully reduced at this point.
- Definition Classes
- Reducer → ReducerPlugin
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def passQuantifiers(num: Int): Reducer
Construct a new reducer to work underneath
numquantifiers.Construct a new reducer to work underneath
numquantifiers.- Definition Classes
- Reducer → ReducerPlugin
- def reduce(predConj: PredConj, reducer: ReduceWithConjunction, logger: ComputationLogger, mode: terfor.conjunctions.ReducerPlugin.ReductionMode.Value): ReductionResult
Reduce the given predicate formulas.
Reduce the given predicate formulas. The result indicates whether nothing changed, or whether the formulas were updated, possibly generating additional arithmetic constraints or negated constraints. Reduction is not required to be idempotent.
- Definition Classes
- Reducer → ReducerPlugin
- def reduceSelects(predConj: PredConj, logger: ComputationLogger, mode: terfor.conjunctions.ReducerPlugin.ReductionMode.Value): ReductionResult
- def reduceStores(predConj: PredConj, logger: ComputationLogger, mode: terfor.conjunctions.ReducerPlugin.ReductionMode.Value): ReductionResult
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toString(): String
- Definition Classes
- AnyRef → Any
- final def wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- final def wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException]) @native()
- final def wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
(Since version 9)