IterativeClauseMatcher

Related Docs: class IterativeClauseMatcher | package conjunctions

object IterativeClauseMatcher

Linear Supertypes
AnyRef, Any
Ordering
1. Alphabetic
2. By Inheritance
Inherited
1. IterativeClauseMatcher
2. AnyRef
3. Any
1. Hide All
2. Show All
Visibility
1. Public
2. All

Value Members

1. final def !=(arg0: Any): Boolean

Definition Classes
AnyRef → Any
2. final def ##(): Int

Definition Classes
AnyRef → Any
3. final def ==(arg0: Any): Boolean

Definition Classes
AnyRef → Any

5. final def asInstanceOf[T0]: T0

Definition Classes
Any
6. def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( ... )
7. def convertQuantifiers(c: Conjunction, config: PredicateMatchConfig): Conjunction

Convert all quantifiers that cannot be handled using e-matching to existential quantifiers (for which Skolem symbols can be introduced)

9. final def eq(arg0: AnyRef): Boolean

Definition Classes
AnyRef
10. def equals(arg0: Any): Boolean

Definition Classes
AnyRef → Any
11. def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( classOf[java.lang.Throwable] )
12. final def getClass(): Class[_]

Definition Classes
AnyRef → Any
13. def hashCode(): Int

Definition Classes
AnyRef → Any
14. final def isInstanceOf[T0]: Boolean

Definition Classes
Any

16. def isMatchableRec(c: Conjunction, config: PredicateMatchConfig): Boolean

Determine whether all quantifiers in the given formula can be handled using matching or using Skolemisation.

Determine whether all quantifiers in the given formula can be handled using matching or using Skolemisation. This is relevant, because then the formula can be treated without using free variables at all, i.e., a more efficient way of proof construction (`ModelSearchProver`) can be used

17. def matchedPredicatesRec(c: Conjunction, config: PredicateMatchConfig): Set[Predicate]

Determine the set of predicates that are matched in some quantified expression

18. final def ne(arg0: AnyRef): Boolean

Definition Classes
AnyRef
19. final def notify(): Unit

Definition Classes
AnyRef
20. final def notifyAll(): Unit

Definition Classes
AnyRef
21. def pullOutTriggers(c: Conjunction, config: PredicateMatchConfig): Conjunction

Make sure that, when applying e-matching, either all or none of the quantifiers in a quantified expressions are instantiated.

22. final def synchronized[T0](arg0: ⇒ T0): T0

Definition Classes
AnyRef
23. def toString(): String

Definition Classes
AnyRef → Any
24. final def wait(): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
25. final def wait(arg0: Long, arg1: Int): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
26. final def wait(arg0: Long): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )