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