Object/Class

ap.parser

IExpression

Related Docs: class IExpression | package parser

Permalink

object IExpression

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. IExpression
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. class BooleanFunApplier extends AnyRef

    Permalink

    Class implementing prefix-notation for functions that are considered Boolean-valued.

    Class implementing prefix-notation for functions that are considered Boolean-valued. Booleans are encoded into integers, mapping true to 0 and false to 1.

  2. type ConstantTerm = terfor.ConstantTerm

    Permalink

    Imported type from the terfor package

    Imported type from the terfor package

  3. class FunApplier extends AnyRef

    Permalink

    Class implementing prefix-notation for functions

  4. class PredApplier extends AnyRef

    Permalink

    Class implementing prefix-notation for predicates

  5. type Predicate = terfor.preds.Predicate

    Permalink

    Imported type from the terfor package

    Imported type from the terfor package

  6. type Quantifier = terfor.conjunctions.Quantifier

    Permalink

    Imported type from the terfor package

    Imported type from the terfor package

  7. class RichITerm extends AnyRef

    Permalink
  8. class RichITermSeq extends AnyRef

    Permalink

    Various functions to work with vectors of terms

  9. type Sort = types.Sort

    Permalink

    Imported type from the types package

    Imported type from the types package

  10. case class SymbolSum(symbol: ITerm) extends Product with Serializable

    Permalink

    Rewrite a term to the form coeff * symbol + remainder (where remainder does not contain the atomic term symbol) and determine the coefficient and the remainder

    Rewrite a term to the form coeff * symbol + remainder (where remainder does not contain the atomic term symbol) and determine the coefficient and the remainder

Value Members

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

    Permalink
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  4. val AC: AC_INPUT_ABSY.type

    Permalink
    Attributes
    protected[ap.parser]
  5. implicit def Boolean2IFormula(value: Boolean): IFormula

    Permalink

    Implicit conversion from Booleans to formulas

  6. object Conj

    Permalink

    Generate or match a binary conjunction phi & psi.

    Generate or match a binary conjunction phi & psi.

  7. object Const

    Permalink

    Extract the value of constant terms.

  8. implicit def ConstantTerm2ITerm(c: ConstantTerm): ITerm

    Permalink

    Implicit conversion from constants to terms

  9. object Difference

    Permalink

    Match on a difference IPlus(a, ITimes(IdealInt.MINUS_ONE, b)) or IPlus(ITimes(IdealInt.MINUS_ONE, b), a)

    Match on a difference IPlus(a, ITimes(IdealInt.MINUS_ONE, b)) or IPlus(ITimes(IdealInt.MINUS_ONE, b), a)

  10. object Disj

    Permalink

    Generate or match a binary disjunction phi | psi.

    Generate or match a binary disjunction phi | psi.

  11. object Eq

    Permalink

    Generate or match an equation s === t.

    Generate or match an equation s === t.

  12. object EqLit

    Permalink

    Generate or match an equation s === lit, where lit is an integer literal.

    Generate or match an equation s === lit, where lit is an integer literal.

  13. object EqZ

    Permalink

    Generate or match the equation t = 0.

    Generate or match the equation t = 0.

  14. object Geq

    Permalink

    Generate or match an inequality s >= t.

    Generate or match an inequality s >= t.

  15. object GeqZ

    Permalink

    Generate or match the inequality t >= 0.

    Generate or match the inequality t >= 0.

  16. implicit def IdealInt2ITerm(value: IdealInt): ITerm

    Permalink

    Implicit conversion from integers to terms

  17. implicit def Int2ITerm(value: Int): ITerm

    Permalink

    Implicit conversion from integers to terms

  18. object LeafFormula

    Permalink

    Identify formulae that do not have direct subformulae.

  19. val Quantifier: terfor.conjunctions.Quantifier.type

    Permalink

    Imported companion object from the terfor package

    Imported companion object from the terfor package

  20. implicit def Range2Interval(range: Range): Interval

    Permalink

    Implicit conversion from Scala ranges to interval sorts

  21. object SignConst

    Permalink

    Extract the value and sign of constant terms.

  22. object SimpleTerm

    Permalink

    Identify terms that only consist of variables, constants, and linear arithmetic operations.

  23. val Sort: types.Sort.type

    Permalink

    Imported companion object from the types package

    Imported companion object from the types package

  24. def abs(t: ITerm): ITerm

    Permalink

    Absolute value

  25. def all(sorts: Seq[Sort], f: IFormula): IFormula

    Permalink

    Add sorted universal quantifiers for the variables with de Bruijn index 0, ..., sorts.size - 1.

    Add sorted universal quantifiers for the variables with de Bruijn index 0, ..., sorts.size - 1. The first sort in sorts will be the innermost quantifier and corresponds to index 0.

  26. def all(f: (ITerm, ITerm, ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

    Permalink

    Higher-order syntax for universal quantifiers.

    Higher-order syntax for universal quantifiers. This makes it possible to write a quantifier as all((a, b, c, d, e) => phi(a, b, c, d, e)).

  27. def all(f: (ITerm, ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

    Permalink

    Higher-order syntax for universal quantifiers.

    Higher-order syntax for universal quantifiers. This makes it possible to write a quantifier as all((a, b, c, d) => phi(a, b, c, d)).

  28. def all(f: (ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

    Permalink

    Higher-order syntax for universal quantifiers.

    Higher-order syntax for universal quantifiers. This makes it possible to write a quantifier as all((a, b, c) => phi(a, b, c)).

  29. def all(f: (ITerm, ITerm) ⇒ IFormula): IFormula

    Permalink

    Higher-order syntax for universal quantifiers.

    Higher-order syntax for universal quantifiers. This makes it possible to write a quantifier as all((a, b) => phi(a, b)).

  30. def all(f: (ITerm) ⇒ IFormula): IFormula

    Permalink

    Higher-order syntax for universal quantifiers.

    Higher-order syntax for universal quantifiers. This makes it possible to write a quantifier as all(a => phi(a)).

  31. def all(f: IFormula): IQuantified

    Permalink

    Add an existential quantifier for the variable with de Bruijn index 0.

  32. def and(fors: Iterable[IFormula]): IFormula

    Permalink

    Generate the conjunction of the given formulas.

  33. def and(fors: Iterator[IFormula]): IFormula

    Permalink

    Generate the conjunction of the given formulas.

  34. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  35. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  36. def connect(fors: Iterator[IFormula], op: IBinJunctor.Value): IFormula

    Permalink
  37. def connect(fors: Iterable[IFormula], op: IBinJunctor.Value): IFormula

    Permalink
  38. def connectSimplify(fors: Iterator[IFormula], op: IBinJunctor.Value): IFormula

    Permalink
  39. def connectSimplify(fors: Iterable[IFormula], op: IBinJunctor.Value): IFormula

    Permalink
  40. implicit def constantSeq2ITermSeq(lcs: Seq[ConstantTerm]): Seq[ITerm]

    Permalink
  41. implicit def constantSeq2RichITermSeq(lcs: Seq[ConstantTerm]): RichITermSeq

    Permalink
  42. def containFunctionApplications(f: IFormula): IFormula

    Permalink

    When encoding functions using predicates, make sure that no functions escape.

  43. def distinct(terms: Iterable[ITerm]): IFormula

    Permalink

    Generate a formula expressing that the given terms are pairwise distinct

  44. def distinct(terms: Iterator[ITerm]): IFormula

    Permalink

    Generate a formula expressing that the given terms are pairwise distinct

  45. def eps(f: (ITerm) ⇒ IFormula): IEpsilon

    Permalink

    Higher-order syntax for epsilon-expressions.

    Higher-order syntax for epsilon-expressions. This makes it possible to write things like eps(a => phi(a)).

  46. def eps(f: IFormula): IEpsilon

    Permalink

    Generate an epsilon-expression.

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

    Permalink
    Definition Classes
    AnyRef
  48. def eqZero(t: ITerm): IFormula

    Permalink

    Generate the equation t = 0.

    Generate the equation t = 0.

  49. def equals(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  50. def ex(sorts: Seq[Sort], f: IFormula): IFormula

    Permalink

    Add sorted existential quantifiers for the variables with de Bruijn index 0, ..., sorts.size - 1.

    Add sorted existential quantifiers for the variables with de Bruijn index 0, ..., sorts.size - 1. The first sort in sorts will be the innermost quantifier and corresponds to index 0.

  51. def ex(f: (ITerm, ITerm, ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

    Permalink

    Higher-order syntax for existential quantifiers.

    Higher-order syntax for existential quantifiers. This makes it possible to write a quantifier as ex((a, b, c, d, e) => phi(a, b, c, d, e)).

  52. def ex(f: (ITerm, ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

    Permalink

    Higher-order syntax for existential quantifiers.

    Higher-order syntax for existential quantifiers. This makes it possible to write a quantifier as ex((a, b, c, d) => phi(a, b, c, d)).

  53. def ex(f: (ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

    Permalink

    Higher-order syntax for existential quantifiers.

    Higher-order syntax for existential quantifiers. This makes it possible to write a quantifier as ex((a, b, c) => phi(a, b, c)).

  54. def ex(f: (ITerm, ITerm) ⇒ IFormula): IFormula

    Permalink

    Higher-order syntax for existential quantifiers.

    Higher-order syntax for existential quantifiers. This makes it possible to write a quantifier as ex((a, b) => phi(a, b)).

  55. def ex(f: (ITerm) ⇒ IFormula): IFormula

    Permalink

    Higher-order syntax for existential quantifiers.

    Higher-order syntax for existential quantifiers. This makes it possible to write a quantifier as ex(a => phi(a)).

  56. def ex(f: IFormula): IQuantified

    Permalink

    Add an existential quantifier for the variable with de Bruijn index 0.

  57. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  58. def geqZero(t: ITerm): IFormula

    Permalink

    Generate the inequality t >= 0.

    Generate the inequality t >= 0.

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

    Permalink
    Definition Classes
    AnyRef → Any
  60. def guardAll(f: IFormula, guard: IFormula): IFormula

    Permalink

    Guard a formula, turning it into f ==> guard.

    Guard a formula, turning it into f ==> guard. The guard will be inserted underneath leading universal quantifiers.

  61. def guardEx(f: IFormula, guard: IFormula): IFormula

    Permalink

    Guard a formula, turning it into f & guard.

    Guard a formula, turning it into f & guard. The guard will be inserted underneath leading existential quantifiers.

  62. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  63. def i(value: Boolean): IFormula

    Permalink

    Implicit conversion from Booleans to formulas

  64. def i(c: ConstantTerm): ITerm

    Permalink

    Implicit conversion from constants to terms

  65. def i(value: IdealInt): ITerm

    Permalink

    Implicit conversion from integers to terms

  66. def i(value: Int): ITerm

    Permalink

    Implicit conversion from integers to terms

  67. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  68. def isSimpleTerm(t: ITerm): Boolean

    Permalink

    Identify terms that only consist of variables, constants, and linear arithmetic operations.

  69. def ite(cond: IFormula, left: IFormula, right: IFormula): IFormulaITE

    Permalink

    Generate a conditional formula.

  70. def ite(cond: IFormula, left: ITerm, right: ITerm): ITermITE

    Permalink

    Generate a conditional term.

  71. implicit def iterm2RichITerm(lc: ITerm): RichITerm

    Permalink
  72. implicit def itermSeq2RichITermSeq(lcs: Seq[ITerm]): RichITermSeq

    Permalink
  73. def max(terms: Iterable[ITerm]): ITerm

    Permalink

    Maximum value of a sequence of terms

  74. def min(terms: Iterable[ITerm]): ITerm

    Permalink

    Minimum value of a sequence of terms

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

    Permalink
    Definition Classes
    AnyRef
  76. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
  77. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
  78. def or(fors: Iterable[IFormula]): IFormula

    Permalink

    Generate the disjunction of the given formulas.

  79. def or(fors: Iterator[IFormula]): IFormula

    Permalink

    Generate the disjunction of the given formulas.

  80. def quan(quans: Seq[Quantifier], f: IFormula): IFormula

    Permalink

    Add quantifiers for the variables with de Bruijn index 0, ..., quans.size - 1.

    Add quantifiers for the variables with de Bruijn index 0, ..., quans.size - 1. The first quantifier in quans will be the innermost quantifier and corresponds to index 0.

  81. def quan(q: Quantifier, f: (ITerm, ITerm, ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

    Permalink

    Higher-order syntax for quantifiers.

    Higher-order syntax for quantifiers. This makes it possible to write a quantifier like in quan(Quantifier.ALL, (a, b, c, d, e) => phi(a, b, c, d, e)).

  82. def quan(q: Quantifier, f: (ITerm, ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

    Permalink

    Higher-order syntax for quantifiers.

    Higher-order syntax for quantifiers. This makes it possible to write a quantifier like in quan(Quantifier.ALL, (a, b, c, d) => phi(a, b, c, d)).

  83. def quan(q: Quantifier, f: (ITerm, ITerm, ITerm) ⇒ IFormula): IFormula

    Permalink

    Higher-order syntax for quantifiers.

    Higher-order syntax for quantifiers. This makes it possible to write a quantifier like in quan(Quantifier.ALL, (a, b, c) => phi(a, b, c)).

  84. def quan(q: Quantifier, f: (ITerm, ITerm) ⇒ IFormula): IFormula

    Permalink

    Higher-order syntax for quantifiers.

    Higher-order syntax for quantifiers. This makes it possible to write a quantifier like in quan(Quantifier.ALL, (a, b) => phi(a, b)).

  85. def quan(q: Quantifier, f: (ITerm) ⇒ IFormula): IFormula

    Permalink

    Higher-order syntax for quantifiers.

    Higher-order syntax for quantifiers. This makes it possible to write a quantifier like in quan(Quantifier.ALL, a => phi(a)).

  86. def quanConsts(quantifiedConstants: Seq[(Quantifier, ConstantTerm)], f: IFormula): IFormula

    Permalink

    Replace the constants in quantifiedConstants with bound variables, and quantify them.

    Replace the constants in quantifiedConstants with bound variables, and quantify them.

  87. def quanConsts(quan: Quantifier, consts: Iterable[ConstantTerm], f: IFormula): IFormula

    Permalink

    Replace consts with bound variables, and quantify them.

    Replace consts with bound variables, and quantify them.

  88. def quanVars(quan: Quantifier, vars: Iterable[IVariable], f: IFormula): IFormula

    Permalink

    Quantify some of the variables occurring in a formula.

  89. def removePartName(t: IFormula): IFormula

    Permalink
  90. def subst(t: IExpression, replacement: List[ITerm], shift: Int): IExpression

    Permalink

    Substitute terms for the variables with de Bruijn index 0, ..., replacement.size - 1, and increment all other variables by shift.

    Substitute terms for the variables with de Bruijn index 0, ..., replacement.size - 1, and increment all other variables by shift.

  91. def subst(t: IFormula, replacement: List[ITerm], shift: Int): IFormula

    Permalink

    Substitute terms for the variables with de Bruijn index 0, ..., replacement.size - 1, and increment all other variables by shift.

    Substitute terms for the variables with de Bruijn index 0, ..., replacement.size - 1, and increment all other variables by shift.

  92. def subst(t: ITerm, replacement: List[ITerm], shift: Int): ITerm

    Permalink

    Substitute terms for the variables with de Bruijn index 0, ..., replacement.size - 1, and increment all other variables by shift.

    Substitute terms for the variables with de Bruijn index 0, ..., replacement.size - 1, and increment all other variables by shift.

  93. def sum(terms: Iterator[ITerm]): ITerm

    Permalink

    Generate the sum of the given terms.

  94. def sum(terms: Iterable[ITerm]): ITerm

    Permalink

    Generate the sum of the given terms.

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

    Permalink
    Definition Classes
    AnyRef
  96. implicit def toFunApplier(fun: IFunction): FunApplier

    Permalink

    Implicit conversion, to enable the application of a function to a sequence of terms, like in f(s, t).

    Implicit conversion, to enable the application of a function to a sequence of terms, like in f(s, t).

  97. implicit def toPredApplier(pred: Predicate): PredApplier

    Permalink

    Implicit conversion, to enable the application of a predicate to a sequence of terms, like in p(s, t).

    Implicit conversion, to enable the application of a predicate to a sequence of terms, like in p(s, t).

  98. def toString(): String

    Permalink
    Definition Classes
    AnyRef → Any
  99. def toTermSeq(newExprs: Seq[IExpression], oldExprs: Seq[ITerm]): Option[Seq[ITerm]]

    Permalink
    Attributes
    protected[ap.parser]
  100. def trig(f: IFormula, patterns: IExpression*): ITrigger

    Permalink

    Trigger/patterns that are used to define in which way a quantified formula is supposed to be instantiated.

    Trigger/patterns that are used to define in which way a quantified formula is supposed to be instantiated. Triggers are only allowed to occur immediately after (inside) a quantifier. This class can both represent uni-triggers (for patterns.size == 1 and multi-triggers. Intended use is, for instance, all(x => trig(f(x) >= 0, f(x))).

  101. def updateAndSimplify(e: ITerm, newSubExpr: Seq[IExpression]): ITerm

    Permalink

    Update sub-expressions, and directly check whether simplifications are possible.

  102. def updateAndSimplify(t: IFormula, newSubExpr: Seq[IExpression]): IFormula

    Permalink

    Update sub-expressions, and directly check whether simplifications are possible.

  103. def updateAndSimplify(e: IExpression, newSubExpr: Seq[IExpression]): IExpression

    Permalink

    Update sub-expressions, and directly check whether simplifications are possible.

  104. def updateAndSimplifyLazily(e: ITerm, newSubExpr: Seq[IExpression]): ITerm

    Permalink

    Update sub-expressions; if the expression changed as a result of the update, check whether simplifications are possible.

  105. def updateAndSimplifyLazily(e: IFormula, newSubExpr: Seq[IExpression]): IFormula

    Permalink

    Update sub-expressions; if the expression changed as a result of the update, check whether simplifications are possible.

  106. def updateAndSimplifyLazily(e: IExpression, newSubExpr: Seq[IExpression]): IExpression

    Permalink

    Update sub-expressions; if the expression changed as a result of the update, check whether simplifications are possible.

  107. def v(index: Int): IVariable

    Permalink

    Generate the variable with de Bruijn index index

    Generate the variable with de Bruijn index index

  108. final def wait(): Unit

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

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

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

Inherited from AnyRef

Inherited from Any

Ungrouped