OmegaCertificate

Certificate corresponding to an application of the Omega rule, which has the same effect as repeated application of Strengthen to the inequalities boundsA in a goal.

For each of the inequalities in boundsA, strengthenCases tells how often Strengthen is applied. The counting works just like in StrengthenCertificate, i.e., 1 means that Strenghten is applied once (and there are two cases).

Linear Supertypes

Serializable, Serializable, Product, Equals, Certificate, AnyRef, Any

Instance Constructors

new OmegaCertificate(elimConst: ConstantTerm, boundsA: Seq[CertInequality], boundsB: Seq[CertInequality], children: Seq[Certificate], 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
def apply(i: Int): Certificate

Definition Classes
OmegaCertificate → Certificate
final def asInstanceOf[T0]: T0

Definition Classes
Any
lazy val assumedFormulas: Set[CertFormula]

Formulae that the proof assumes to be present on this branch (i.e., premisses of rules applied in the proof).
Formulae that the proof assumes to be present on this branch (i.e., premisses of rules applied in the proof). We assume that all formulae live in the antecedent.

Definition Classes
Certificate
val boundsA: Seq[CertInequality]
val boundsB: Seq[CertInequality]
val children: Seq[Certificate]
def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate() @throws( ... )
val closingConstraint: Conjunction

The constraint resulting from this proof
The constraint resulting from this proof

Definition Classes
OmegaCertificate → Certificate
lazy val constants: Set[ConstantTerm]

Set of constants occurring in this certificate.
Set of constants occurring in this certificate. By default this will contain the set of all constants in sub-certificates, as well as constants in assumed formulas.

Definition Classes
Certificate
val elimConst: ConstantTerm
final def eq(arg0: AnyRef): Boolean

Definition Classes
AnyRef
final def getClass(): Class[_]

Definition Classes
AnyRef → Any
Annotations
@HotSpotIntrinsicCandidate()
val hashCode: Int

Definition Classes
OmegaCertificate → AnyRef → Any
lazy val inferenceCount: Int

Definition Classes
Certificate
final def isInstanceOf[T0]: Boolean

Definition Classes
Any
def iterator: Iterator[Certificate]

Definition Classes
OmegaCertificate → Certificate
def length: Int

Definition Classes
OmegaCertificate → Certificate
val localAssumedFormulas: Set[CertFormula]

Definition Classes
OmegaCertificate → Certificate
val localBoundConstants: Set[ConstantTerm]

Constants bound by the root operator of the certificate.
Constants bound by the root operator of the certificate.

Definition Classes
Certificate
val localProvidedFormulas: Seq[Set[CertFormula]]

Formulae that are introduced into the antecedent by this rule application (one set for each subproof).
Formulae that are introduced into the antecedent by this rule application (one set for each subproof). This will implicitly simplify formulae (all simplifications that are built into the datastructures are carried out).

Definition Classes
OmegaCertificate → Certificate
final def ne(arg0: AnyRef): Boolean

Definition Classes
AnyRef
final def notify(): Unit

Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate()
final def notifyAll(): Unit

Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate()
val order: TermOrder

Definition Classes
OmegaCertificate → Certificate
def size: Int

Definition Classes
Certificate
val strengthenCases: Seq[IdealInt]
def subCertificates: IndexedSeq[Certificate]

Definition Classes
Certificate
final def synchronized[T0](arg0: ⇒ T0): T0

Definition Classes
AnyRef
lazy val theoryAxioms: Set[CertFormula]

Definition Classes
Certificate
def toString(): String

Definition Classes
OmegaCertificate → AnyRef → Any
def update(newSubCerts: Seq[Certificate]): Certificate

Definition Classes
OmegaCertificate → Certificate
final def wait(arg0: Long, arg1: Int): Unit

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

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

Definition Classes
AnyRef
Annotations
@throws( ... )

Deprecated Value Members

def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@Deprecated @deprecated @throws( classOf[java.lang.Throwable] )
Deprecated
(Since version ) see corresponding Javadoc for more information.

Related Docs: object OmegaCertificate | package certificates

case class OmegaCertificate(elimConst: ConstantTerm, boundsA: Seq[CertInequality], boundsB: Seq[CertInequality], children: Seq[Certificate], order: TermOrder) extends Certificate with Product with Serializable

Instance Constructors

new OmegaCertificate(elimConst: ConstantTerm, boundsA: Seq[CertInequality], boundsB: Seq[CertInequality], children: Seq[Certificate], order: TermOrder)

Value Members

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

def apply(i: Int): Certificate

final def asInstanceOf[T0]: T0

lazy val assumedFormulas: Set[CertFormula]

val boundsA: Seq[CertInequality]

val boundsB: Seq[CertInequality]

val children: Seq[Certificate]

def clone(): AnyRef

val closingConstraint: Conjunction

lazy val constants: Set[ConstantTerm]

val elimConst: ConstantTerm

final def eq(arg0: AnyRef): Boolean

final def getClass(): Class[_]

val hashCode: Int

lazy val inferenceCount: Int

final def isInstanceOf[T0]: Boolean

def iterator: Iterator[Certificate]

def length: Int

val localAssumedFormulas: Set[CertFormula]

val localBoundConstants: Set[ConstantTerm]

val localProvidedFormulas: Seq[Set[CertFormula]]

final def ne(arg0: AnyRef): Boolean

final def notify(): Unit

final def notifyAll(): Unit

val order: TermOrder

def size: Int

val strengthenCases: Seq[IdealInt]

def subCertificates: IndexedSeq[Certificate]

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

lazy val theoryAxioms: Set[CertFormula]

def toString(): String

def update(newSubCerts: Seq[Certificate]): Certificate

final def wait(arg0: Long, arg1: Int): Unit

final def wait(arg0: Long): Unit

final def wait(): Unit

Deprecated Value Members

def finalize(): Unit

Inherited from Serializable

Inherited from Serializable

Inherited from Product

Inherited from Equals

Inherited from Certificate

Inherited from AnyRef

Inherited from Any

Ungrouped