Class

ap.parser

ISortedQuantified

Related Doc: package parser

Permalink

case class ISortedQuantified(quan: Quantifier, sort: Sort, subformula: IFormula) extends IQuantified with Product with Serializable

Application of a quantifier to a formula containing a free variable with de Bruijn index 0 and the given sort.

Linear Supertypes
Serializable, Serializable, Product, Equals, IQuantified, IVariableBinder, IFormula, IExpression, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. ISortedQuantified
  2. Serializable
  3. Serializable
  4. Product
  5. Equals
  6. IQuantified
  7. IVariableBinder
  8. IFormula
  9. IExpression
  10. AnyRef
  11. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new ISortedQuantified(quan: Quantifier, sort: Sort, subformula: IFormula)

    Permalink

Value Members

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

    Permalink
    Definition Classes
    AnyRef → Any

  2. final def ##(): Int

    Permalink
    Definition Classes
    AnyRef → Any

  3. def &(that: IFormula): IFormula

    Permalink

    Conjunction of two formulas.

    Conjunction of two formulas.

    Definition Classes
    IFormula

  4. def &&&(that: IFormula): IFormula

    Permalink

    Conjunction operator that directly simplify expressions involving true/false.

    Conjunction operator that directly simplify expressions involving true/false.

    Definition Classes
    IFormula

  5. def </>(that: IFormula): IFormula

    Permalink

    Exclusive-or of two formulas.

    Exclusive-or of two formulas.

    Definition Classes
    IFormula

  6. def <===>(that: IFormula): IFormula

    Permalink

    Equivalence operator that directly simplify expressions involving true/false.

    Equivalence operator that directly simplify expressions involving true/false.

    Definition Classes
    IFormula

  7. def <=>(that: IFormula): IFormula

    Permalink

    Equivalence of two formulas.

    Equivalence of two formulas.

    Definition Classes
    IFormula

  8. final def ==(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any

  9. def ===>(that: IFormula): IFormula

    Permalink

    Implication operator that directly simplify expressions involving true/false.

    Implication operator that directly simplify expressions involving true/false.

    Definition Classes
    IFormula

  10. def ==>(that: IFormula): IFormula

    Permalink

    Implication between two formulas.

    Implication between two formulas.

    Definition Classes
    IFormula

  11. def andSimplify(that: IFormula): IFormula

    Permalink

    Conjunction operator that directly simplify expressions involving true/false.

    Conjunction operator that directly simplify expressions involving true/false.

    Definition Classes
    IFormula

  12. def apply(i: Int): IFormula

    Permalink

    Return the ith sub-expression.

    Return the ith sub-expression.

    Definition Classes
    ISortedQuantified → IExpression

  13. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any

  14. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @throws( ... )

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

    Permalink
    Definition Classes
    AnyRef

  16. def eqvSimplify(that: IFormula): IFormula

    Permalink

    Equivalence operator that directly simplify expressions involving true/false.

    Equivalence operator that directly simplify expressions involving true/false.

    Definition Classes
    IFormula

  17. final def getClass(): Class[_]

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()

  18. val hashCode: Int

    Permalink
    Definition Classes
    ISortedQuantified → AnyRef → Any

  19. def impSimplify(that: IFormula): IFormula

    Permalink

    Disjunction operator that directly simplify expressions involving true/false.

    Disjunction operator that directly simplify expressions involving true/false.

    Definition Classes
    IFormula

  20. def isFalse: Boolean

    Permalink

    Incomplete check whether the given formula is unsatisfiable.

    Incomplete check whether the given formula is unsatisfiable.

    Definition Classes
    IFormula

  21. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any

  22. def isTrue: Boolean

    Permalink

    Incomplete check whether the given formula is valid.

    Incomplete check whether the given formula is valid.

    Definition Classes
    IFormula

  23. def iterator: Iterator[IExpression]

    Permalink

    Iterator over the sub-expressions of this expression.

    Iterator over the sub-expressions of this expression.

    Definition Classes
    IExpression

  24. def length: Int

    Permalink

    Number of sub-expressions.

    Number of sub-expressions.

    Definition Classes
    ISortedQuantified → IExpression

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

    Permalink
    Definition Classes
    AnyRef

  26. def notSimplify: IFormula

    Permalink

    Negation of a formula, with direct simplification.

    Negation of a formula, with direct simplification.

    Definition Classes
    IFormula

  27. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()

  28. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()

  29. def orSimplify(that: IFormula): IFormula

    Permalink

    Disjunction operator that directly simplify expressions involving true/false.

    Disjunction operator that directly simplify expressions involving true/false.

    Definition Classes
    IFormula

  30. val quan: Quantifier

    Permalink

    The quantifier.

    The quantifier.

    Definition Classes
    ISortedQuantified → IQuantified

  31. val sort: Sort

    Permalink

    The sort of the bound variable.

    The sort of the bound variable.

    Definition Classes
    ISortedQuantified → IQuantified → IVariableBinder

  32. def subExpressions: IndexedSeq[IExpression]

    Permalink

    The sub-expressions of this expression.

    The sub-expressions of this expression.

    Definition Classes
    IExpression

  33. val subformula: IFormula

    Permalink

    The body of the quantified formula.

    The body of the quantified formula.

    Definition Classes
    ISortedQuantified → IQuantified

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

    Permalink
    Definition Classes
    AnyRef

  35. def toString(): String

    Permalink
    Definition Classes
    ISortedQuantified → AnyRef → Any

  36. def unary_!: IFormula

    Permalink

    Negation of a formula.

    Negation of a formula.

    Definition Classes
    IFormula

  37. def unary_~: IFormula

    Permalink

    Negation of a formula, with direct simplification.

    Negation of a formula, with direct simplification.

    Definition Classes
    IFormula

  38. def update(newSubExprs: Seq[IExpression]): ISortedQuantified

    Permalink

    Replace the subexpressions of this node with new expressions

    Replace the subexpressions of this node with new expressions

    Definition Classes
    ISortedQuantified → IFormula → IExpression

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

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

  40. final def wait(arg0: Long): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

  41. final def wait(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

  42. def |(that: IFormula): IFormula

    Permalink

    Disjunction of two formulas.

    Disjunction of two formulas.

    Definition Classes
    IFormula

  43. def |||(that: IFormula): IFormula

    Permalink

    Disjunction operator that directly simplify expressions involving true/false.

    Disjunction operator that directly simplify expressions involving true/false.

    Definition Classes
    IFormula

Deprecated Value Members

  1. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @Deprecated @deprecated @throws( classOf[java.lang.Throwable] )
    Deprecated

    (Since version ) see corresponding Javadoc for more information.

Inherited from Serializable

Inherited from Serializable

Inherited from Product

Inherited from Equals

Inherited from IQuantified

Inherited from IVariableBinder

Inherited from IFormula

Inherited from IExpression

Inherited from AnyRef

Inherited from Any

Ungrouped