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
    @HotSpotIntrinsicCandidate() @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 forall(n: Int, f: Formula)(implicit order: TermOrder): Conjunction

    Permalink

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

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

    Permalink

    Quantify the variable with De Brujin-index 0

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

    Permalink

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

    Permalink

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

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

    Permalink

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

    Permalink

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

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()

  40. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()

  41. implicit def inEqConj2ArithConj(eqs: InEqConj): ArithConj

    Permalink

  42. implicit def inEqConj2Conj(eqs: InEqConj): Conjunction

    Permalink

  43. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any

  44. implicit def l(t: Term)(implicit order: TermOrder): LinearCombination

    Permalink

  45. implicit def l(i: IdealInt): LinearCombination

    Permalink

  46. implicit def l(i: Int): LinearCombination

    Permalink

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

    Permalink

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

    Permalink

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

    Permalink
    Definition Classes
    AnyRef

  50. implicit def negEqConj2ArithConj(eqs: NegEquationConj): ArithConj

    Permalink

  51. implicit def negEqConj2Conj(eqs: NegEquationConj): Conjunction

    Permalink

  52. implicit def negatedConjs2Conj(conjs: NegatedConjunctions): Conjunction

    Permalink

  53. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()

  54. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()

  55. implicit def pred2Conj(p: Predicate)(implicit order: TermOrder): Conjunction

    Permalink

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

    Permalink

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

    Permalink

  58. implicit def predConj2Conj(pc: PredConj): Conjunction

    Permalink

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

    Permalink

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

    Permalink

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

    Permalink

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

    Permalink
    Definition Classes
    AnyRef

  63. implicit def term2RichLC(lc: Term)(implicit order: TermOrder): RichLinearCombination

    Permalink

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

    Permalink

  65. def toString(): String

    Permalink
    Definition Classes
    AnyRef → Any

  66. def unEqZ(lcs: Iterator[LinearCombination])(implicit order: TermOrder): NegEquationConj

    Permalink

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

    Permalink

  68. def v(index: Int): VariableTerm

    Permalink

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

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

  70. final def wait(arg0: Long): Unit

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

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