Object

ap.terfor

TerForConvenience

Related Doc: package terfor

Permalink

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

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. def arithConj(formulas: Formula*)(implicit order: TermOrder): ArithConj

    Permalink
  5. def arithConj(formulas: Iterable[Formula])(implicit order: TermOrder): ArithConj

    Permalink
  6. def arithConj(formulas: Iterator[Formula])(implicit order: TermOrder): ArithConj

    Permalink
  7. implicit def arithConj2Conj(ac: ArithConj): Conjunction

    Permalink
  8. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  9. implicit def atom2Conj(atom: Atom): Conjunction

    Permalink
  10. implicit def atom2PredConj(atom: Atom): PredConj

    Permalink
  11. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  12. def conj(formulas: Formula*)(implicit order: TermOrder): Conjunction

    Permalink
  13. def conj(formulas: Iterable[Formula])(implicit order: TermOrder): Conjunction

    Permalink
  14. def conj(formulas: Iterator[Formula])(implicit order: TermOrder): Conjunction

    Permalink
  15. def disj(formulas: Conjunction*)(implicit order: TermOrder): Conjunction

    Permalink
  16. def disj(formulas: Iterable[Conjunction])(implicit order: TermOrder): Conjunction

    Permalink
  17. def disj(formulas: Iterator[Conjunction])(implicit order: TermOrder): Conjunction

    Permalink
  18. def disjFor(formulas: Formula*)(implicit order: TermOrder): Conjunction

    Permalink
  19. def disjFor(formulas: Iterable[Formula])(implicit order: TermOrder): Conjunction

    Permalink
  20. def disjFor(formulas: Iterator[Formula])(implicit order: TermOrder): Conjunction

    Permalink
  21. final def eq(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  22. implicit def eqConj2ArithConj(eqs: EquationConj): ArithConj

    Permalink
  23. implicit def eqConj2Conj(eqs: EquationConj): Conjunction

    Permalink
  24. def eqZ(lcs: Iterator[LinearCombination])(implicit order: TermOrder): EquationConj

    Permalink
  25. def eqZ(lcs: Iterable[LinearCombination])(implicit order: TermOrder): EquationConj

    Permalink
  26. def equals(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  27. def exists(n: Int, f: Formula)(implicit order: TermOrder): Conjunction

    Permalink

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

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

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

    Permalink

    Quantify the variable with De Brujin-index 0

  29. def exists(constant: ConstantTerm, f: Formula)(implicit order: TermOrder): Conjunction

    Permalink
  30. def exists(constants: Seq[ConstantTerm], f: Formula)(implicit order: TermOrder): Conjunction

    Permalink
  31. def existsSorted(sorts: Seq[Sort], f: Formula)(implicit order: TermOrder): Conjunction

    Permalink

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

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

  32. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  33. def forall(n: Int, f: Formula)(implicit order: TermOrder): Conjunction

    Permalink

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

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

    Permalink

    Quantify the variable with De Brujin-index 0

  35. def forall(constant: ConstantTerm, f: Formula)(implicit order: TermOrder): Conjunction

    Permalink
  36. def forall(constants: Seq[ConstantTerm], f: Formula)(implicit order: TermOrder): Conjunction

    Permalink
  37. def forallSorted(sorts: Seq[Sort], f: Formula)(implicit order: TermOrder): Conjunction

    Permalink

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

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

  38. def geqZ(lcs: Iterator[LinearCombination])(implicit order: TermOrder): InEqConj

    Permalink
  39. def geqZ(lcs: Iterable[LinearCombination])(implicit order: TermOrder): InEqConj

    Permalink
  40. final def getClass(): Class[_]

    Permalink
    Definition Classes
    AnyRef → Any
  41. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  42. implicit def inEqConj2ArithConj(eqs: InEqConj): ArithConj

    Permalink
  43. implicit def inEqConj2Conj(eqs: InEqConj): Conjunction

    Permalink
  44. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  45. implicit def l(t: Term)(implicit order: TermOrder): LinearCombination

    Permalink
  46. implicit def l(i: IdealInt): LinearCombination

    Permalink
  47. implicit def l(i: Int): LinearCombination

    Permalink
  48. def lcSum(lcs: Iterator[LinearCombination])(implicit order: TermOrder): LinearCombination

    Permalink
  49. def lcSum(lcs: Iterable[LinearCombination])(implicit order: TermOrder): LinearCombination

    Permalink
  50. final def ne(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  51. implicit def negEqConj2ArithConj(eqs: NegEquationConj): ArithConj

    Permalink
  52. implicit def negEqConj2Conj(eqs: NegEquationConj): Conjunction

    Permalink
  53. implicit def negatedConjs2Conj(conjs: NegatedConjunctions): Conjunction

    Permalink
  54. final def notify(): Unit

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

    Permalink
    Definition Classes
    AnyRef
  56. implicit def pred2Conj(p: Predicate)(implicit order: TermOrder): Conjunction

    Permalink
  57. implicit def pred2PredConj(p: Predicate)(implicit order: TermOrder): PredConj

    Permalink
  58. implicit def pred2RichPred(pred: Predicate)(implicit order: TermOrder): RichPredicate

    Permalink
  59. implicit def predConj2Conj(pc: PredConj): Conjunction

    Permalink
  60. def quantify(quan: Quantifier, constants: Seq[ConstantTerm], f: Formula)(implicit order: TermOrder): Conjunction

    Permalink
  61. def sum(lcs: Iterator[(IdealInt, LinearCombination)])(implicit order: TermOrder): LinearCombination

    Permalink
  62. def sum(lcs: Seq[(IdealInt, LinearCombination)])(implicit order: TermOrder): LinearCombination

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

    Permalink
    Definition Classes
    AnyRef
  64. implicit def term2RichLC(lc: Term)(implicit order: TermOrder): RichLinearCombination

    Permalink
  65. implicit def termSeq2RichLCSeq(lcs: Seq[Term])(implicit order: TermOrder): RichLinearCombinationSeq

    Permalink
  66. def toString(): String

    Permalink
    Definition Classes
    AnyRef → Any
  67. def unEqZ(lcs: Iterator[LinearCombination])(implicit order: TermOrder): NegEquationConj

    Permalink
  68. def unEqZ(lcs: Iterable[LinearCombination])(implicit order: TermOrder): NegEquationConj

    Permalink
  69. def v(index: Int): VariableTerm

    Permalink
  70. final def wait(): Unit

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

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

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

Inherited from AnyRef

Inherited from Any

Ungrouped