Object/Class

ap.parser

IExpression

Related Docs: class IExpression | package parser

Permalink

object IExpression

Companion object of IExpression, with various helper methods.

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 SymbolEquation(symbol: ITerm) extends Product with Serializable

    Permalink

    Rewrite an equation to the form coeff * symbol = remainder (where remainder does not contain the atomic term symbol) and determine the coefficient and the remainder

    Rewrite an equation to the form coeff * symbol = remainder (where remainder does not contain the atomic term symbol) and determine the coefficient and the remainder

  11. 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 Divisibility

    Permalink

    Generate or match a divisibility expression ex x.

    Generate or match a divisibility expression ex x. denom*x = t.

  12. object Eq

    Permalink

    Generate or match an equation s === t.

    Generate or match an equation s === t.

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

  14. object EqZ

    Permalink

    Generate or match the equation t = 0.

    Generate or match the equation t = 0.

  15. object Geq

    Permalink

    Generate or match an inequality s >= t.

    Generate or match an inequality s >= t.

  16. object GeqZ

    Permalink

    Generate or match the inequality t >= 0.

    Generate or match the inequality t >= 0.

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

    Permalink

    Implicit conversion from integers to terms

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

    Permalink

    Implicit conversion from integers to terms

  19. object LeafFormula

    Permalink

    Identify formulae that do not have direct subformulae.

  20. object NonDivisibility

    Permalink

    Generate or match a non-divisibility expression forall x.

    Generate or match a non-divisibility expression forall x. denom*x != t.

  21. val Quantifier: terfor.conjunctions.Quantifier.type

    Permalink

    Imported companion object from the terfor package

    Imported companion object from the terfor package

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

    Permalink

    Implicit conversion from Scala ranges to interval sorts

  23. object SignConst

    Permalink

    Extract the value and sign of constant terms.

  24. object SimpleTerm

    Permalink

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

  25. val Sort: types.Sort.type

    Permalink

    Imported companion object from the types package

    Imported companion object from the types package

  26. def abs(t: ITerm): ITerm

    Permalink

    Absolute value

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

  28. 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)).

  29. 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)).

  30. 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)).

  31. 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)).

  32. 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)).

  33. def all(f: IFormula): IQuantified

    Permalink

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

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

    Permalink

    Generate the conjunction of the given formulas.

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

    Permalink

    Generate the conjunction of the given formulas.

  36. final def asInstanceOf[T0]: T0

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

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

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

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

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

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

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

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

    Permalink

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

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

    Permalink

    Generate a formula expressing that the given terms are pairwise distinct

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

    Permalink

    Generate a formula expressing that the given terms are pairwise distinct

  47. 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)).

  48. def eps(sort: Sort, f: IFormula): IEpsilon

    Permalink

    Generate an epsilon-expression with the given sort.

  49. def eps(f: IFormula): IEpsilon

    Permalink

    Generate an epsilon-expression with sort Sort.Integer.

    Generate an epsilon-expression with sort Sort.Integer.

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

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

    Permalink

    Generate the equation t = 0.

    Generate the equation t = 0.

  52. def equals(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  53. 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.

  54. 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)).

  55. 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)).

  56. 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)).

  57. 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)).

  58. 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)).

  59. def ex(f: IFormula): IQuantified

    Permalink

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

  60. def geqZero(t: ITerm): IFormula

    Permalink

    Generate the inequality t >= 0.

    Generate the inequality t >= 0.

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

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()
  62. 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.

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

  64. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()
  65. def i(value: Boolean): IFormula

    Permalink

    Conversion from Booleans to formulas

  66. def i(c: ConstantTerm): ITerm

    Permalink

    Conversion from constants to terms

  67. def i(value: IdealInt): ITerm

    Permalink

    Conversion from integers to terms

  68. def i(value: Int): ITerm

    Permalink

    Conversion from integers to terms

  69. final def isInstanceOf[T0]: Boolean

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

    Permalink

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

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

    Permalink

    Generate a conditional formula.

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

    Permalink

    Generate a conditional term.

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

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

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

    Permalink

    Maximum value of a sequence of terms

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

    Permalink

    Minimum value of a sequence of terms

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

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

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()
  79. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()
  80. def or(fors: Iterable[IFormula]): IFormula

    Permalink

    Generate the disjunction of the given formulas.

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

    Permalink

    Generate the disjunction of the given formulas.

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

  83. 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)).

  84. 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)).

  85. 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)).

  86. 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)).

  87. 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)).

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

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

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

    Permalink

    Quantify some of the variables occurring in a formula.

  91. def quanWithSorts(quans: Seq[(Quantifier, Sort)], 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.

  92. def quanWithSorts(q: Quantifier, sorts: Seq[Sort], f: IFormula): IFormula

    Permalink

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

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

  93. def removePartName(t: IFormula): IFormula

    Permalink
  94. def shiftVars(t: ITerm, shift: Int): ITerm

    Permalink

    Shift all variables by shift.

    Shift all variables by shift.

  95. def shiftVars(t: ITerm, offset: Int, shift: Int): ITerm

    Permalink

    Shift all variables with index >= offset by shift.

    Shift all variables with index >= offset by shift.

  96. def shiftVars(t: IFormula, shift: Int): IFormula

    Permalink

    Shift all variables by shift.

    Shift all variables by shift.

  97. def shiftVars(t: IFormula, offset: Int, shift: Int): IFormula

    Permalink

    Shift all variables with index >= offset by shift.

    Shift all variables with index >= offset by shift.

  98. def shiftVars(t: IExpression, shift: Int): IExpression

    Permalink

    Shift all variables by shift.

    Shift all variables by shift.

  99. def shiftVars(t: IExpression, offset: Int, shift: Int): IExpression

    Permalink

    Shift all variables with index >= offset by shift.

    Shift all variables with index >= offset by shift.

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

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

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

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

    Permalink

    Generate the sum of the given terms.

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

    Permalink

    Generate the sum of the given terms.

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

    Permalink
    Definition Classes
    AnyRef
  106. 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).

  107. 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).

  108. def toString(): String

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

    Permalink
    Attributes
    protected[ap.parser]
  110. 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))).

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

    Permalink

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

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

    Permalink

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

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

    Permalink

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

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

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

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

  117. def v(index: Int, sort: Sort): IVariable

    Permalink

    Generate the variable with de Bruijn index index and the given sort.

    Generate the variable with de Bruijn index index and the given sort.

  118. def v(index: Int): IVariable

    Permalink

    Generate the variable with de Bruijn index index and sort Sort.Integer.

    Generate the variable with de Bruijn index index and sort Sort.Integer.

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

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

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  121. final def wait(): Unit

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

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 AnyRef

Inherited from Any

Ungrouped