object TermOrder
Class for representing total orderings on constants (and variables), and their extension to arbitrary terms. For the time being, we do not consider arbitrary (non-nullary) functions apart from the pre-defined arithmetic operations.
constantSeq is the list of constants that are totally ordered by
this TermOrder, starting with the biggest constant. In
addition, variable terms are by default ordered as bigger as all constants.
We use the List datatype for the constant order, so that new
large constants can efficiently be added.
- Alphabetic
- By Inheritance
- TermOrder
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Type Members
- case class CoeffWeight(coefficient: IdealInt, baseWeight: NonCoeffWeight) extends Weight with Product with Serializable
- Attributes
- protected[terfor]
- case class ConstantWeight(value: Int) extends NonCoeffWeight with Product with Serializable
- Attributes
- protected[terfor]
- abstract class NonCoeffWeight extends Weight
- Attributes
- protected[terfor]
- case class VariableWeight(value: Int) extends NonCoeffWeight with Product with Serializable
- Attributes
- protected[terfor]
- abstract class Weight extends Ordered[Weight]
Weight objects that are used to abstract from the concrete terms.
Weight objects that are used to abstract from the concrete terms. There are three types of weights: for variables, and for constants, and for the literal 1. Variables are heavier that constants are heavier than literals.
- Attributes
- protected[terfor]
Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- val CONSTANT_NUM_SEP: Int
- val EMPTY: TermOrder
The term order that cannot sort anything apart from
Constant.ONEand variables - final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toString(): String
- Definition Classes
- AnyRef → Any
- final def wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- final def wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException]) @native()
- final def wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- case object OneWeight extends NonCoeffWeight with Product with Serializable
- Attributes
- protected[terfor]
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
(Since version 9)