Packages

c

ap.parser

IFormula

abstract class IFormula extends IExpression

Abstract class representing formulae in input-syntax.

Linear Supertypes
IExpression, AnyRef, Any
Known Subclasses
IAtom, IBinFormula, IBoolLit, IEquation, IFormulaITE, IIntFormula, INamedPart, INot, IQuantified, ISortedQuantified, ITrigger
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. IFormula
  2. IExpression
  3. AnyRef
  4. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Instance Constructors

  1. new IFormula()

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##: Int
    Definition Classes
    AnyRef → Any
  3. def &(that: IFormula): IFormula

    Conjunction of two formulas.

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

    Conjunction operator that directly simplify expressions involving true/false.

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

    Exclusive-or of two formulas.

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

    Equivalence operator that directly simplify expressions involving true/false.

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

    Equivalence of two formulas.

  8. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  9. def ===>(that: IFormula): IFormula

    Implication operator that directly simplify expressions involving true/false.

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

    Implication between two formulas.

  11. def andSimplify(that: IFormula): IFormula

    Conjunction operator that directly simplify expressions involving true/false.

  12. def apply(i: Int): IExpression

    Return the ith sub-expression.

    Return the ith sub-expression.

    Definition Classes
    IExpression
  13. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  14. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
  15. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  16. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  17. def eqvSimplify(that: IFormula): IFormula

    Equivalence operator that directly simplify expressions involving true/false.

  18. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  19. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  20. def impSimplify(that: IFormula): IFormula

    Disjunction operator that directly simplify expressions involving true/false.

  21. def isFalse: Boolean

    Incomplete check whether the given formula is unsatisfiable.

  22. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  23. def isTrue: Boolean

    Incomplete check whether the given formula is valid.

  24. def iterator: Iterator[IExpression]

    Iterator over the sub-expressions of this expression.

    Iterator over the sub-expressions of this expression.

    Definition Classes
    IExpression
  25. def length: Int

    Number of sub-expressions.

    Number of sub-expressions.

    Definition Classes
    IExpression
  26. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  27. def notSimplify: IFormula

    Negation of a formula, with direct simplification.

  28. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  29. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  30. def orSimplify(that: IFormula): IFormula

    Disjunction operator that directly simplify expressions involving true/false.

  31. def subExpressions: IndexedSeq[IExpression]

    The sub-expressions of this expression.

    The sub-expressions of this expression.

    Definition Classes
    IExpression
  32. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  33. def toString(): String
    Definition Classes
    AnyRef → Any
  34. def unary_!: IFormula

    Negation of a formula.

  35. def unary_~: IFormula

    Negation of a formula, with direct simplification.

  36. def update(newSubExprs: Seq[IExpression]): IFormula

    Replace the subexpressions of this node with new expressions

    Replace the subexpressions of this node with new expressions

    Definition Classes
    IFormula → IExpression
  37. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  38. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  39. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  40. def |(that: IFormula): IFormula

    Disjunction of two formulas.

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

    Disjunction operator that directly simplify expressions involving true/false.

Deprecated Value Members

  1. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.Throwable]) @Deprecated
    Deprecated

    (Since version 9)

Inherited from IExpression

Inherited from AnyRef

Inherited from Any

Ungrouped