case class QuantifierInference(quantifiedFormula: CertCompoundFormula, newConstants: Seq[ConstantTerm], result: CertFormula, order: TermOrder) extends BranchInference with Product with Serializable
Inference corresponding to applications of the rules all-left,
ex-left, etc. A uniform prefix of quantifiers (only forall or
only exists) is instantiated with a single inference.
newConstants are the constants introduced to instantiate the
quantifiers, starting with the innermost instantiated quantifier.
- Alphabetic
- By Inheritance
- QuantifierInference
- Serializable
- Product
- Equals
- BranchInference
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Instance Constructors
- new QuantifierInference(quantifiedFormula: CertCompoundFormula, newConstants: Seq[ConstantTerm], result: CertFormula, order: TermOrder)
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
- val assumedFormulas: Set[CertFormula]
- Definition Classes
- QuantifierInference → BranchInference
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
- lazy val constants: Set[ConstantTerm]
Set of constants occurring in this inference.
Set of constants occurring in this inference.
- Definition Classes
- BranchInference
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- val localBoundConstants: Set[ConstantTerm]
- Definition Classes
- QuantifierInference → BranchInference
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- val newConstants: Seq[ConstantTerm]
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- val order: TermOrder
- def productElementNames: Iterator[String]
- Definition Classes
- Product
- def propagateConstraint(closingConstraint: Conjunction): Conjunction
Define the modification imposed by this rule application on the closing constraint.
Define the modification imposed by this rule application on the closing constraint.
- Definition Classes
- QuantifierInference → BranchInference
- val providedFormulas: Set[CertFormula]
Formulae that are introduced into the antecedent by this rule application.
Formulae that are introduced into the antecedent by this rule application. This will implicitly simplify formulae (all simplifications that are built into the datastructures are carried out).
- Definition Classes
- QuantifierInference → BranchInference
- val quantifiedFormula: CertCompoundFormula
- val result: CertFormula
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toString(): String
- Definition Classes
- QuantifierInference → 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)