TermOrder

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

final def asInstanceOf[T0]: T0

lazy val atomOrdering: Ordering[Atom]

Ordering on atoms that lists large atoms last

def clone(): AnyRef

def compare(a1: Atom, a2: Atom): Int

def compare(c1: ArithConj, c2: ArithConj): Int

def compare(c1: Seq[LinearCombination], c2: Seq[LinearCombination]): Int

def compare(t1: Term, t2: Term): Int

lazy val constOrdering: Ordering[ConstantTerm]

Ordering on terms that lists large terms last

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

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

final def eq(arg0: AnyRef): Boolean

def equals(that: Any): Boolean

def extend(newConsts: Seq[ConstantTerm]): TermOrder

def extend(newConst: ConstantTerm): TermOrder

def extend(newConst: ConstantTerm, biggerConstants: Set[ConstantTerm]): TermOrder

Extend this ordering by inserting a further constant newConst.

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

Extend this ordering by inserting further predicate newPreds.

def extendPred(newPred: Predicate): TermOrder

Extend this ordering by inserting a further predicate newPred.

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

final def getClass(): Class[_]

def hashCode(): Int

final def isInstanceOf[T0]: Boolean

def isSortingOf[A](x: A): Boolean

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

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.

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.

lazy val lcOrdering: Ordering[LinearCombination]

Ordering on linear combinations that lists large linear combinations last

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

final def ne(arg0: AnyRef): Boolean

final def notify(): Unit

final def notifyAll(): Unit

lazy val orderedConstants: Set[ConstantTerm]

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

lazy val orderedPredicates: Set[Predicate]

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

lazy val predOrdering: Ordering[Predicate]

Ordering on predicates that lists large predicates last

def resetPredicates: TermOrder

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

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

Restrict this ordering to the given symbols

lazy val reverseAtomOrdering: Ordering[Atom]

Ordering on atoms that lists large atoms first

lazy val reverseLCOrdering: Ordering[LinearCombination]

Ordering on linear combinations that lists large linear combinations first

lazy val reversePredOrdering: Ordering[Predicate]

Ordering on predicates that lists large predicates first

lazy val reverseTermOrdering: Ordering[Term]

Ordering on terms that lists large terms first

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

Sort the given constants in ascending order

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

Sort the given constants in ascending order

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

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

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

Sort the given predicates in ascending order

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

lazy val termOrdering: Ordering[Term]

Ordering on terms that lists large terms last

def toString(): String

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

final def wait(arg0: Long): Unit

final def wait(): Unit

def finalize(): Unit