 # IQuantified

### Related Docs: object IQuantified | package parser

#### abstract class IQuantified extends IFormula with IVariableBinder

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

Linear Supertypes
Known Subclasses
Ordering
1. Alphabetic
2. By inheritance
Inherited
1. IQuantified
2. IVariableBinder
3. IFormula
4. IExpression
5. AnyRef
6. Any
1. Hide All
2. Show all
Visibility
1. Public
2. All

### Abstract Value Members

1. #### abstract def quan: Quantifier

The quantifier.

2. #### abstract def sort: Sort

The sort of the bound variable.

The sort of the bound variable.

Definition Classes
IQuantifiedIVariableBinder
3. #### abstract def subformula: IFormula

The body of the quantified formula.

### Concrete 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): IExpression

Return the `i`th sub-expression.

Return the `i`th sub-expression.

Definition Classes
IExpression
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 equals(arg0: Any): Boolean

Definition Classes
AnyRef → Any
17. #### 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
18. #### def finalize(): Unit

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

Definition Classes
AnyRef → Any
20. #### def hashCode(): Int

Definition Classes
AnyRef → Any
21. #### 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
22. #### def isFalse: Boolean

Incomplete check whether the given formula is unsatisfiable.

Incomplete check whether the given formula is unsatisfiable.

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

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

Incomplete check whether the given formula is valid.

Incomplete check whether the given formula is valid.

Definition Classes
IFormula
25. #### def iterator: Iterator[IExpression]

Iterator over the sub-expressions of this expression.

Iterator over the sub-expressions of this expression.

Definition Classes
IExpression
26. #### def length: Int

Number of sub-expressions.

Number of sub-expressions.

Definition Classes
IExpression
27. #### final def ne(arg0: AnyRef): Boolean

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

Negation of a formula, with direct simplification.

Negation of a formula, with direct simplification.

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

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

Definition Classes
AnyRef
31. #### 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
32. #### def subExpressions: IndexedSeq[IExpression]

The sub-expressions of this expression.

The sub-expressions of this expression.

Definition Classes
IExpression
33. #### final def synchronized[T0](arg0: ⇒ T0): T0

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

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

Negation of a formula.

Negation of a formula.

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

Negation of a formula, with direct simplification.

Negation of a formula, with direct simplification.

Definition Classes
IFormula
37. #### 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
IFormulaIExpression
38. #### final def wait(): Unit

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

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

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

Disjunction of two formulas.

Disjunction of two formulas.

Definition Classes
IFormula
42. #### 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