class IterativeClauseMatcher extends Sorted[IterativeClauseMatcher]
Linear Supertypes
Ordering
- Alphabetic
- By Inheritance
Inherited
- IterativeClauseMatcher
- Sorted
- AnyRef
- Any
- Hide All
- Show All
Visibility
- 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 addClauses(newFacts: PredConj, addedClauses: Iterable[Conjunction], mayAlias: AliasChecker, contextReducer: ReduceWithConjunction, isIrrelevantMatch: (Conjunction, Set[ConstantTerm]) => Boolean, allowConditionalInstances: Boolean, logger: ComputationLogger, order: TermOrder): (Iterable[Conjunction], IterativeClauseMatcher)
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- val clauses: NegatedConjunctions
- 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
- def factsAreOutdated(actualFacts: PredConj): Boolean
Only used for assertion purposes
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def isEmpty: Boolean
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- def isSortedBy(order: TermOrder): Boolean
- Definition Classes
- IterativeClauseMatcher → Sorted
- 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 reduceClauses(clauseReducer: (Conjunction) => Conjunction, instanceReducer: (Conjunction) => Conjunction, order: TermOrder): (NegatedConjunctions, IterativeClauseMatcher)
Reduce the clauses of this matcher.
Reduce the clauses of this matcher. All reducible clauses are removed from the matcher and the reductions are returned
- def remove(removePred: (Formula) => Boolean): (Seq[Conjunction], IterativeClauseMatcher)
Remove clauses and cached literals from this matcher that are identified by the given predicate.
Remove clauses and cached literals from this matcher that are identified by the given predicate. The removed clauses are returned as the first result component.
- def sortBy(order: TermOrder): IterativeClauseMatcher
Re-sort an object with a new
TermOrder
.Re-sort an object with a new
TermOrder
. It is guaranteed that the resultisSortedBy(order)
- Definition Classes
- IterativeClauseMatcher → Sorted
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toString(): String
- Definition Classes
- IterativeClauseMatcher → AnyRef → Any
- def updateFacts(newFacts: PredConj, mayAlias: AliasChecker, contextReducer: ReduceWithConjunction, isIrrelevantMatch: (Conjunction, Set[ConstantTerm]) => Boolean, allowConditionalInstances: Boolean, logger: ComputationLogger, order: TermOrder): (Iterable[Conjunction], IterativeClauseMatcher)
- 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)