class ReduceWithPredLits extends AnyRef
Class for reducing a conjunction of predicate literals using a set of known literals (facts). This reduction can be done modulo the axiom of functionality (for predicates encoding functions or partial functions), and then potentially replaces predicate literals with simple equations.
- Alphabetic
- By Inheritance
- ReduceWithPredLits
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
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 addLits(furtherLits: PredConj): ReduceWithPredLits
- def apply(conj: PredConj): (PredConj, ArithConj)
Reduce a conjunction of predicate literals using known predicate literals.
Reduce a conjunction of predicate literals using known predicate literals. This function knows about functional predicates, and is able to apply the functionality axiom to replace predicate literals with equations.
- def apply(conj: PredConj, logger: ComputationLogger): (PredConj, ArithConj)
Reduce a conjunction of predicate literals using known predicate literals.
Reduce a conjunction of predicate literals using known predicate literals. This function knows about functional predicates, and is able to apply the functionality axiom to replace predicate literals with equations.
- 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()
- def passQuantifiers(num: Int): ReduceWithPredLits
Create a
ReduceWithPredLitsthat can be used underneathnumbinders.Create a
ReduceWithPredLitsthat can be used underneathnumbinders. The conversion of de Brujin-variables is done on the fly, which should give a good performance when the resultingReduceWithEqsis not applied too often (TODO: caching) - def reductionPossible(conj: PredConj): Boolean
Determine whether a formula that contains the given predicates might be reducible by this reducer
- 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])
- lazy val withoutFacts: ReduceWithPredLits
A reducer corresponding to this one, but without assuming any facts known a priori.
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
(Since version 9)