Packages

class TermOrder extends AnyRef

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. TermOrder
  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. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  5. lazy val atomOrdering: Ordering[Atom]

    Ordering on atoms that lists large atoms last

  6. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
  7. def compare(a1: Atom, a2: Atom): Int
  8. def compare(c1: ArithConj, c2: ArithConj): Int
  9. def compare(c1: Seq[LinearCombination], c2: Seq[LinearCombination]): Int
  10. def compare(t1: Term, t2: Term): Int
  11. lazy val constOrdering: Ordering[ConstantTerm]

    Ordering on terms that lists large terms last

  12. def constantsAreMaximal(consts: Set[ConstantTerm]): Boolean

    Determine whether this term order does not consider any constants as bigger than the given constants

  13. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  14. def equals(that: Any): Boolean
    Definition Classes
    TermOrder → AnyRef → Any
  15. def extend(newConsts: Seq[ConstantTerm]): TermOrder
  16. def extend(newConst: ConstantTerm): TermOrder
  17. def extend(newConst: ConstantTerm, biggerConstants: Set[ConstantTerm]): TermOrder

    Extend this ordering by inserting a further constant newConst.

    Extend this ordering by inserting a further constant newConst. This constant is inserted so that it gets as big as possible, but such that it is smaller than all constants of the set biggerConstants

  18. def extendPred(newPreds: Seq[Predicate]): TermOrder

    Extend this ordering by inserting further predicate newPreds.

    Extend this ordering by inserting further predicate newPreds. The predicates are inserted so that they get as big as possible

  19. def extendPred(newPred: Predicate): TermOrder

    Extend this ordering by inserting a further predicate newPred.

    Extend this ordering by inserting a further predicate newPred. This predicate is inserted so that it gets as big as possible

  20. def findFirstIndex(lt: Term, seq: IndexedSeq[LinearCombination]): Int

    Assuming that seq is a sequence of linear combinations sorted in descending order according to this TermOrder, find the index of the first element whose leading term could be lt

  21. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  22. def hashCode(): Int
    Definition Classes
    TermOrder → AnyRef → Any
  23. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  24. def isSortingOf[A](x: A): Boolean

    Test whether x is sorting by this TermOrder, or return true if x is not a sorted entity

  25. def isSubOrderOf(that: TermOrder, consideredConstants: Set[ConstantTerm], consideredPredicates: Set[Predicate]): Boolean

    Return true iff the term order that is an extension of the order this considering only the constants consideredConstants.

    Return true iff the term order that is an extension of the order this considering only the constants consideredConstants. I.e., this restricted to the constants in consideredConstants is a suborder of that.

  26. def isSubOrderOf(that: TermOrder): Boolean

    Return true iff the term order that is an extension of the order this, i.e., when restricted to the constants that are ordered by this it describes the same order.

  27. lazy val lcOrdering: Ordering[LinearCombination]

    Ordering on linear combinations that lists large linear combinations last

  28. def makeMaximal(movedConst: ConstantTerm, biggerConstants: Set[ConstantTerm]): TermOrder

    Change this ordering by making the constant const as big as possible, but still smaller than all constants of the set biggerConstants

  29. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  30. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  31. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  32. lazy val orderedConstants: Set[ConstantTerm]

    Return the set of all constants that are sorted by this TermOrder

  33. lazy val orderedPredicates: Set[Predicate]

    Return the set of all predicates that are sorted by this TermOrder

  34. lazy val predOrdering: Ordering[Predicate]

    Ordering on predicates that lists large predicates last

  35. def resetPredicates: TermOrder

    Generate a new TermOrder that coincides with this one, except that all predicates have been removed

  36. def restrict(consts: Set[ConstantTerm]): TermOrder

    Restrict this ordering to the given symbols

  37. lazy val reverseAtomOrdering: Ordering[Atom]

    Ordering on atoms that lists large atoms first

  38. lazy val reverseLCOrdering: Ordering[LinearCombination]

    Ordering on linear combinations that lists large linear combinations first

  39. lazy val reversePredOrdering: Ordering[Predicate]

    Ordering on predicates that lists large predicates first

  40. lazy val reverseTermOrdering: Ordering[Term]

    Ordering on terms that lists large terms first

  41. def sort(constants: Iterator[ConstantTerm]): Seq[ConstantTerm]

    Sort the given constants in ascending order

  42. def sort(constants: Iterable[ConstantTerm]): Seq[ConstantTerm]

    Sort the given constants in ascending order

  43. def sort[A](x: A): A

    If x is a sorted entity, sort it by this TermOrder, or otherwise return the unchanged x

  44. def sortPreds(preds: Iterable[Predicate]): Seq[Predicate]

    Sort the given predicates in ascending order

  45. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  46. lazy val termOrdering: Ordering[Term]

    Ordering on terms that lists large terms last

  47. def toString(): String
    Definition Classes
    TermOrder → AnyRef → Any
  48. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  49. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  50. 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