# ISortedQuantified

### Related Doc: package parser

#### 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

### 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.

Conjunction of two formulas.

Definition Classes
IFormula
4. #### def &&&(that: IFormula): IFormula

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

Exclusive-or of two formulas.

Exclusive-or of two formulas.

Definition Classes
IFormula
6. #### def <===>(that: IFormula): IFormula

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

Equivalence of two formulas.

Equivalence of two formulas.

Definition Classes
IFormula
8. #### final def ==(arg0: Any): Boolean

Definition Classes
AnyRef → Any
9. #### def ===>(that: IFormula): IFormula

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

Implication between two formulas.

Implication between two formulas.

Definition Classes
IFormula
11. #### def andSimplify(that: IFormula): IFormula

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

Return the `i`th sub-expression.

Return the `i`th sub-expression.

Definition Classes
ISortedQuantifiedIExpression
13. #### final def asInstanceOf[T0]: T0

Definition Classes
Any
14. #### def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( ... )
15. #### final def eq(arg0: AnyRef): Boolean

Definition Classes
AnyRef
16. #### def eqvSimplify(that: IFormula): IFormula

Equivalence operator that directly simplify expressions involving true/false.

Equivalence operator that directly simplify expressions involving true/false.

Definition Classes
IFormula
17. #### def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( classOf[java.lang.Throwable] )
18. #### final def getClass(): Class[_]

Definition Classes
AnyRef → Any
19. #### val hashCode: Int

Definition Classes
ISortedQuantified → AnyRef → Any
20. #### def impSimplify(that: IFormula): IFormula

Disjunction operator that directly simplify expressions involving true/false.

Disjunction operator that directly simplify expressions involving true/false.

Definition Classes
IFormula
21. #### def isFalse: Boolean

Incomplete check whether the given formula is unsatisfiable.

Incomplete check whether the given formula is unsatisfiable.

Definition Classes
IFormula
22. #### final def isInstanceOf[T0]: Boolean

Definition Classes
Any
23. #### def isTrue: Boolean

Incomplete check whether the given formula is valid.

Incomplete check whether the given formula is valid.

Definition Classes
IFormula
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
ISortedQuantifiedIExpression
26. #### final def ne(arg0: AnyRef): Boolean

Definition Classes
AnyRef
27. #### def notSimplify: IFormula

Negation of a formula, with direct simplification.

Negation of a formula, with direct simplification.

Definition Classes
IFormula
28. #### final def notify(): Unit

Definition Classes
AnyRef
29. #### final def notifyAll(): Unit

Definition Classes
AnyRef
30. #### def orSimplify(that: IFormula): IFormula

Disjunction operator that directly simplify expressions involving true/false.

Disjunction operator that directly simplify expressions involving true/false.

Definition Classes
IFormula
31. #### val quan: Quantifier

The quantifier.

The quantifier.

Definition Classes
ISortedQuantifiedIQuantified
32. #### val sort: Sort

The sort of the bound variable.

The sort of the bound variable.

Definition Classes
ISortedQuantifiedIQuantifiedIVariableBinder
33. #### def subExpressions: IndexedSeq[IExpression]

The sub-expressions of this expression.

The sub-expressions of this expression.

Definition Classes
IExpression
34. #### val subformula: IFormula

The body of the quantified formula.

The body of the quantified formula.

Definition Classes
ISortedQuantifiedIQuantified
35. #### final def synchronized[T0](arg0: ⇒ T0): T0

Definition Classes
AnyRef
36. #### def toString(): String

Definition Classes
ISortedQuantified → AnyRef → Any
37. #### def unary_!: IFormula

Negation of a formula.

Negation of a formula.

Definition Classes
IFormula
38. #### def unary_~: IFormula

Negation of a formula, with direct simplification.

Negation of a formula, with direct simplification.

Definition Classes
IFormula
39. #### def update(newSubExprs: Seq[IExpression]): ISortedQuantified

Replace the subexpressions of this node with new expressions

Replace the subexpressions of this node with new expressions

Definition Classes
ISortedQuantifiedIFormulaIExpression
40. #### final def wait(): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
41. #### final def wait(arg0: Long, arg1: Int): Unit

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

Definition Classes
AnyRef
Annotations
@throws( ... )
43. #### def |(that: IFormula): IFormula

Disjunction of two formulas.

Disjunction of two formulas.

Definition Classes
IFormula
44. #### def |||(that: IFormula): IFormula

Disjunction operator that directly simplify expressions involving true/false.

Disjunction operator that directly simplify expressions involving true/false.

Definition Classes
IFormula