object BetaCertificate extends Serializable
Linear Supertypes
Ordering
- Alphabetic
- By Inheritance
Inherited
- BetaCertificate
- Serializable
- 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
- val AC: AC_CERTIFICATES.type
- Attributes
- protected[certificates]
- def apply(children: Seq[(CertFormula, Certificate)], order: TermOrder): Certificate
Convenience method to handle splits with many children.
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- def betaIfNeeded(leftFormula: CertFormula, rightFormula: CertFormula, lemma: Boolean, leftChild: Certificate, rightChild: Certificate, order: TermOrder): Certificate
Create a beta certificate, but handle the case that one of the disjuncts subsumes the other; in this case, simply one of the child certificates will be returned.
- 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
- def naryWithDisjunction(children: Seq[(CertFormula, Certificate)], order: TermOrder): (CertFormula, Certificate)
Convenience method to handle splits with many children.
Convenience method to handle splits with many children. The method will return the new certificate, together with the final formula that was split (the disjunction of the cases provided).
- 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 providedFormulas(leftFormula: CertFormula, rightFormula: CertFormula, lemma: Boolean): Array[Set[CertFormula]]
- 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)