Packages

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

Type Members

  1. class BooleanFunApplier extends AnyRef

    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

    Imported type from the terfor package

  3. class FunApplier extends AnyRef

    Class implementing prefix-notation for functions

  4. class PredApplier extends AnyRef

    Class implementing prefix-notation for predicates

  5. type Predicate = terfor.preds.Predicate

    Imported type from the terfor package

  6. type Quantifier = terfor.conjunctions.Quantifier

    Imported type from the terfor package

  7. class RichITerm extends AnyRef
  8. class RichITermSeq extends AnyRef

    Various functions to work with vectors of terms

  9. type Sort = types.Sort

    Imported type from the types package

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

    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

    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
    Definition Classes
    AnyRef → Any
  2. final def ##: Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. val AC: AC_INPUT_ABSY.type
    Attributes
    protected[parser]
  5. implicit def Boolean2IFormula(value: Boolean): IFormula

    Implicit conversion from Booleans to formulas

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

    Implicit conversion from constants to terms

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

    Implicit conversion from integers to terms

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

    Implicit conversion from integers to terms

  9. val Quantifier: terfor.conjunctions.Quantifier.type

    Imported companion object from the terfor package

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

    Implicit conversion from Scala ranges to interval sorts

  11. val Sort: types.Sort.type

    Imported companion object from the types package

  12. def abs(t: ITerm): ITerm

    Absolute value

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

    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.

  14. def all(f: (ITerm, ITerm, ITerm, ITerm, ITerm) => IFormula): IFormula

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

  15. def all(f: (ITerm, ITerm, ITerm, ITerm) => IFormula): IFormula

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

  16. def all(f: (ITerm, ITerm, ITerm) => IFormula): IFormula

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

  17. def all(f: (ITerm, ITerm) => IFormula): IFormula

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

  18. def all(f: (ITerm) => IFormula): IFormula

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

  19. def all(f: IFormula): IQuantified

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

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

    Generate the conjunction of the given formulas.

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

    Generate the conjunction of the given formulas.

  22. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  23. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
  24. def connect(fors: Iterator[IFormula], op: IBinJunctor.Value): IFormula
  25. def connect(fors: Iterable[IFormula], op: IBinJunctor.Value): IFormula
  26. def connectSimplify(fors: Iterator[IFormula], op: IBinJunctor.Value): IFormula
  27. def connectSimplify(fors: Iterable[IFormula], op: IBinJunctor.Value): IFormula
  28. implicit def constantSeq2ITermSeq(lcs: Seq[ConstantTerm]): Seq[ITerm]
  29. implicit def constantSeq2RichITermSeq(lcs: Seq[ConstantTerm]): RichITermSeq
  30. def containFunctionApplications(f: IFormula): IFormula

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

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

    Generate a formula expressing that the given terms are pairwise distinct

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

    Generate a formula expressing that the given terms are pairwise distinct

  33. def eps(f: (ITerm) => IFormula): IEpsilon

    Higher-order syntax for epsilon-expressions.

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

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

    Generate an epsilon-expression with the given sort.

  35. def eps(f: IFormula): IEpsilon

    Generate an epsilon-expression with sort Sort.Integer.

  36. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  37. def eqZero(t: ITerm): IFormula

    Generate the equation t = 0.

  38. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  39. def ex(sorts: Seq[Sort], f: IFormula): IFormula

    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.

  40. def ex(f: (ITerm, ITerm, ITerm, ITerm, ITerm) => IFormula): IFormula

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

  41. def ex(f: (ITerm, ITerm, ITerm, ITerm) => IFormula): IFormula

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

  42. def ex(f: (ITerm, ITerm, ITerm) => IFormula): IFormula

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

  43. def ex(f: (ITerm, ITerm) => IFormula): IFormula

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

  44. def ex(f: (ITerm) => IFormula): IFormula

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

  45. def ex(f: IFormula): IQuantified

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

  46. def geqZero(t: ITerm): IFormula

    Generate the inequality t >= 0.

  47. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  48. def guardAll(f: IFormula, guard: IFormula): IFormula

    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.

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

    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.

  50. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  51. def i(value: Boolean): IFormula

    Conversion from Booleans to formulas

  52. def i(c: ConstantTerm): ITerm

    Conversion from constants to terms

  53. def i(value: IdealInt): ITerm

    Conversion from integers to terms

  54. def i(value: Int): ITerm

    Conversion from integers to terms

  55. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  56. def isSimpleTerm(t: ITerm): Boolean

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

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

    Generate a conditional formula.

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

    Generate a conditional term.

  59. implicit def iterm2RichITerm(lc: ITerm): RichITerm
  60. implicit def itermSeq2RichITermSeq(lcs: Seq[ITerm]): RichITermSeq
  61. def max(terms: Iterable[ITerm]): ITerm

    Maximum value of a sequence of terms

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

    Minimum value of a sequence of terms

  63. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  64. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  65. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  66. def or(fors: Iterable[IFormula]): IFormula

    Generate the disjunction of the given formulas.

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

    Generate the disjunction of the given formulas.

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

    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.

  69. def quan(q: Quantifier, f: (ITerm, ITerm, ITerm, ITerm, ITerm) => IFormula): IFormula

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

  70. def quan(q: Quantifier, f: (ITerm, ITerm, ITerm, ITerm) => IFormula): IFormula

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

  71. def quan(q: Quantifier, f: (ITerm, ITerm, ITerm) => IFormula): IFormula

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

  72. def quan(q: Quantifier, f: (ITerm, ITerm) => IFormula): IFormula

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

  73. def quan(q: Quantifier, f: (ITerm) => IFormula): IFormula

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

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

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

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

    Replace consts with bound variables, and quantify them.

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

    Quantify some of the variables occurring in a formula.

  77. def quanWithSorts(quans: Seq[(Quantifier, Sort)], f: IFormula): IFormula

    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.

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

    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.

  79. def removePartName(t: IFormula): IFormula
  80. def shiftVars(t: ITerm, shift: Int): ITerm

    Shift all variables by shift.

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

    Shift all variables with index >= offset by shift.

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

    Shift all variables by shift.

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

    Shift all variables with index >= offset by shift.

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

    Shift all variables by shift.

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

    Shift all variables with index >= offset by shift.

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

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

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

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

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

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

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

    Generate the sum of the given terms.

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

    Generate the sum of the given terms.

  91. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  92. implicit def toFunApplier(fun: IFunction): FunApplier

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

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

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

  94. def toString(): String
    Definition Classes
    AnyRef → Any
  95. def toTermSeq(newExprs: Seq[IExpression], oldExprs: Seq[ITerm]): Option[Seq[ITerm]]
    Attributes
    protected[parser]
  96. def trig(f: IFormula, patterns: IExpression*): ITrigger

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  104. def v(index: Int): IVariable

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

  105. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  106. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  107. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  108. object Conj

    Generate or match a binary conjunction phi & psi.

  109. object Const

    Extract the value of constant terms.

  110. object Difference

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

  111. object Disj

    Generate or match a binary disjunction phi | psi.

  112. object Divisibility

    Generate or match a divisibility expression ex x.

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

  113. object Eq

    Generate or match an equation s === t.

  114. object EqLit

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

  115. object EqZ

    Generate or match the equation t = 0.

  116. object Geq

    Generate or match an inequality s >= t.

  117. object GeqZ

    Generate or match the inequality t >= 0.

  118. object LeafFormula

    Identify formulae that do not have direct subformulae.

  119. object NonDivisibility

    Generate or match a non-divisibility expression forall x.

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

  120. object SignConst

    Extract the value and sign of constant terms.

  121. object SimpleTerm

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

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 AnyRef

Inherited from Any

Ungrouped