class Reducer extends ReducerPlugin
- Alphabetic
- By Inheritance
- Reducer
- ReducerPlugin
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Instance Constructors
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(predConj: 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
- 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
Perform GC, remove literals that are no longer needed in a formula.
Perform GC, remove literals that are no longer needed in a formula.
- 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): ReducerPlugin
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
- 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)