abstract class ReducerPlugin extends AnyRef
Interface for plugins that can be added to the
ReduceWithConjunction class.
Linear Supertypes
Known Subclasses
Ordering
- Alphabetic
- By Inheritance
Inherited
- ReducerPlugin
- AnyRef
- Any
- Hide All
- Show All
Visibility
- Public
- Protected
Instance Constructors
- new ReducerPlugin()
Abstract Value Members
- abstract def addAssumptions(predConj: PredConj, mode: ReducerPlugin.ReductionMode.Value): ReducerPlugin
Add further assumptions to this reducer.
- abstract def addAssumptions(arithConj: ArithConj, mode: ReducerPlugin.ReductionMode.Value): ReducerPlugin
Add further assumptions to this reducer.
- abstract val factory: ReducerPluginFactory
Factory to generate further instances of this plugin.
- abstract 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.
- abstract def passQuantifiers(num: Int): ReducerPlugin
Construct a new reducer to work underneath
numquantifiers. - abstract def reduce(predConj: PredConj, baseReducer: ReduceWithConjunction, logger: ComputationLogger, mode: 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.
Concrete 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
- 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
- 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()
- 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)