Packages

o

ap.terfor

TerForConvenience

object TerForConvenience

Collection of functions that makes it easier to use the term/formula datastructures by adding lots of syntactic sugar

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

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. def arithConj(formulas: Formula*)(implicit order: TermOrder): ArithConj
  5. def arithConj(formulas: Iterable[Formula])(implicit order: TermOrder): ArithConj
  6. def arithConj(formulas: Iterator[Formula])(implicit order: TermOrder): ArithConj
  7. implicit def arithConj2Conj(ac: ArithConj): Conjunction
  8. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  9. implicit def atom2Conj(atom: Atom): Conjunction
  10. implicit def atom2PredConj(atom: Atom): PredConj
  11. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
  12. def conj(formulas: Formula*)(implicit order: TermOrder): Conjunction
  13. def conj(formulas: Iterable[Formula])(implicit order: TermOrder): Conjunction
  14. def conj(formulas: Iterator[Formula])(implicit order: TermOrder): Conjunction
  15. def disj(formulas: Conjunction*)(implicit order: TermOrder): Conjunction
  16. def disj(formulas: Iterable[Conjunction])(implicit order: TermOrder): Conjunction
  17. def disj(formulas: Iterator[Conjunction])(implicit order: TermOrder): Conjunction
  18. def disjFor(formulas: Formula*)(implicit order: TermOrder): Conjunction
  19. def disjFor(formulas: Iterable[Formula])(implicit order: TermOrder): Conjunction
  20. def disjFor(formulas: Iterator[Formula])(implicit order: TermOrder): Conjunction
  21. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  22. implicit def eqConj2ArithConj(eqs: EquationConj): ArithConj
  23. implicit def eqConj2Conj(eqs: EquationConj): Conjunction
  24. def eqZ(lcs: Iterator[LinearCombination])(implicit order: TermOrder): EquationConj
  25. def eqZ(lcs: Iterable[LinearCombination])(implicit order: TermOrder): EquationConj
  26. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  27. def exists(n: Int, f: Formula)(implicit order: TermOrder): Conjunction

    Quantify the variables with De Brujin-index [0, ..., n)

  28. def exists(f: Formula)(implicit order: TermOrder): Conjunction

    Quantify the variable with De Brujin-index 0

  29. def exists(constant: ConstantTerm, f: Formula)(implicit order: TermOrder): Conjunction
  30. def exists(constants: Seq[ConstantTerm], f: Formula)(implicit order: TermOrder): Conjunction
  31. def existsSorted(sorts: Seq[Sort], f: Formula)(implicit order: TermOrder): Conjunction

    Quantify the variables with De Brujin-index [0, ..., sorts.size), assuming they have the given sorts

  32. def forall(n: Int, f: Formula)(implicit order: TermOrder): Conjunction

    Quantify the variables with De Brujin-index [0, ..., n)

  33. def forall(f: Formula)(implicit order: TermOrder): Conjunction

    Quantify the variable with De Brujin-index 0

  34. def forall(constant: ConstantTerm, f: Formula)(implicit order: TermOrder): Conjunction
  35. def forall(constants: Seq[ConstantTerm], f: Formula)(implicit order: TermOrder): Conjunction
  36. def forallSorted(sorts: Seq[Sort], f: Formula)(implicit order: TermOrder): Conjunction

    Quantify the variables with De Brujin-index [0, ..., sorts.size), assuming they have the given sorts

  37. def geqZ(lcs: Iterator[LinearCombination])(implicit order: TermOrder): InEqConj
  38. def geqZ(lcs: Iterable[LinearCombination])(implicit order: TermOrder): InEqConj
  39. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  40. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  41. implicit def inEqConj2ArithConj(eqs: InEqConj): ArithConj
  42. implicit def inEqConj2Conj(eqs: InEqConj): Conjunction
  43. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  44. implicit def l(t: Term)(implicit order: TermOrder): LinearCombination
  45. implicit def l(i: IdealInt): LinearCombination
  46. implicit def l(i: Int): LinearCombination
  47. def lcSum(lcs: Iterator[LinearCombination])(implicit order: TermOrder): LinearCombination
  48. def lcSum(lcs: Iterable[LinearCombination])(implicit order: TermOrder): LinearCombination
  49. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  50. implicit def negEqConj2ArithConj(eqs: NegEquationConj): ArithConj
  51. implicit def negEqConj2Conj(eqs: NegEquationConj): Conjunction
  52. implicit def negatedConjs2Conj(conjs: NegatedConjunctions): Conjunction
  53. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  54. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  55. implicit def pred2Conj(p: Predicate)(implicit order: TermOrder): Conjunction
  56. implicit def pred2PredConj(p: Predicate)(implicit order: TermOrder): PredConj
  57. implicit def pred2RichPred(pred: Predicate)(implicit order: TermOrder): RichPredicate
  58. implicit def predConj2Conj(pc: PredConj): Conjunction
  59. def quantify(quan: Quantifier, constants: Seq[ConstantTerm], f: Formula)(implicit order: TermOrder): Conjunction
  60. def sum(lcs: Iterator[(IdealInt, LinearCombination)])(implicit order: TermOrder): LinearCombination
  61. def sum(lcs: Seq[(IdealInt, LinearCombination)])(implicit order: TermOrder): LinearCombination
  62. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  63. implicit def term2RichLC(lc: Term)(implicit order: TermOrder): RichLinearCombination
  64. implicit def termSeq2RichLCSeq(lcs: Seq[Term])(implicit order: TermOrder): RichLinearCombinationSeq
  65. def toString(): String
    Definition Classes
    AnyRef → Any
  66. def unEqZ(lcs: Iterator[LinearCombination])(implicit order: TermOrder): NegEquationConj
  67. def unEqZ(lcs: Iterable[LinearCombination])(implicit order: TermOrder): NegEquationConj
  68. def v(index: Int): VariableTerm
  69. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  70. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  71. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])

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