NegEquationConj

final def !=(arg0: Any): Boolean

final def ##(): Int

def ++[B >: LinearCombination, That](that: GenTraversableOnce[B])(implicit bf: CanBuildFrom[IndexedSeq[LinearCombination], B, That]): That

def ++:[B >: LinearCombination, That](that: Traversable[B])(implicit bf: CanBuildFrom[IndexedSeq[LinearCombination], B, That]): That

def ++:[B >: LinearCombination, That](that: TraversableOnce[B])(implicit bf: CanBuildFrom[IndexedSeq[LinearCombination], B, That]): That

def +:[B >: LinearCombination, That](elem: B)(implicit bf: CanBuildFrom[IndexedSeq[LinearCombination], B, That]): That

def --(that: NegEquationConj): NegEquationConj

def /:[B](z: B)(op: (B, LinearCombination) ⇒ B): B

def :+[B >: LinearCombination, That](elem: B)(implicit bf: CanBuildFrom[IndexedSeq[LinearCombination], B, That]): That

def :\[B](z: B)(op: (LinearCombination, B) ⇒ B): B

final def ==(arg0: Any): Boolean

def addString(b: StringBuilder): StringBuilder

def addString(b: StringBuilder, sep: String): StringBuilder

def addString(b: StringBuilder, start: String, sep: String, end: String): StringBuilder

def aggregate[B](z: ⇒ B)(seqop: (B, LinearCombination) ⇒ B, combop: (B, B) ⇒ B): B

def andThen[C](k: (LinearCombination) ⇒ C): PartialFunction[Int, C]

def apply(i: Int): LinearCombination

def applyOrElse[A1 <: Int, B1 >: LinearCombination](x: A1, default: (A1) ⇒ B1): B1

final def asInstanceOf[T0]: T0

def canEqual(that: Any): Boolean

def clone(): AnyRef

def collect[B, That](pf: PartialFunction[LinearCombination, B])(implicit bf: CanBuildFrom[IndexedSeq[LinearCombination], B, That]): That

def collectFirst[B](pf: PartialFunction[LinearCombination, B]): Option[B]

def combinations(n: Int): Iterator[IndexedSeq[LinearCombination]]

def companion: GenericCompanion[IndexedSeq]

def compose[A](g: (A) ⇒ Int): (A) ⇒ LinearCombination

lazy val constants: Set[ConstantTerm]

def contains(lc: LinearCombination): Boolean

def contains[A1 >: LinearCombination](elem: A1): Boolean

def containsSlice[B](that: GenSeq[B]): Boolean

def copyToArray[B >: LinearCombination](xs: Array[B], start: Int, len: Int): Unit

def copyToArray[B >: LinearCombination](xs: Array[B]): Unit

def copyToArray[B >: LinearCombination](xs: Array[B], start: Int): Unit

def copyToBuffer[B >: LinearCombination](dest: Buffer[B]): Unit

def corresponds[B](that: GenSeq[B])(p: (LinearCombination, B) ⇒ Boolean): Boolean

def count(p: (LinearCombination) ⇒ Boolean): Int

def diff[B >: LinearCombination](that: GenSeq[B]): IndexedSeq[LinearCombination]

def distinct: IndexedSeq[LinearCombination]

def drop(n: Int): IndexedSeq[LinearCombination]

def dropRight(n: Int): IndexedSeq[LinearCombination]

def dropWhile(p: (LinearCombination) ⇒ Boolean): IndexedSeq[LinearCombination]

def endsWith[B](that: GenSeq[B]): Boolean

final def eq(arg0: AnyRef): Boolean

def equals(that: Any): Boolean

def exists(p: (LinearCombination) ⇒ Boolean): Boolean

def filter(p: (LinearCombination) ⇒ Boolean): IndexedSeq[LinearCombination]

def filterNot(p: (LinearCombination) ⇒ Boolean): IndexedSeq[LinearCombination]

def find(p: (LinearCombination) ⇒ Boolean): Option[LinearCombination]

def flatMap[B, That](f: (LinearCombination) ⇒ GenTraversableOnce[B])(implicit bf: CanBuildFrom[IndexedSeq[LinearCombination], B, That]): That

def flatten[B](implicit asTraversable: (LinearCombination) ⇒ GenTraversableOnce[B]): IndexedSeq[B]

def fold[A1 >: LinearCombination](z: A1)(op: (A1, A1) ⇒ A1): A1

def foldLeft[B](z: B)(op: (B, LinearCombination) ⇒ B): B

def foldRight[B](z: B)(op: (LinearCombination, B) ⇒ B): B

def forall(p: (LinearCombination) ⇒ Boolean): Boolean

def foreach[U](f: (LinearCombination) ⇒ U): Unit

def genericBuilder[B]: Builder[B, IndexedSeq[B]]

final def getClass(): Class[_]

def groundAtoms: Set[Atom]

def groupBy[K](f: (LinearCombination) ⇒ K): Map[K, IndexedSeq[LinearCombination]]

def grouped(size: Int): Iterator[IndexedSeq[LinearCombination]]

def hasDefiniteSize: Boolean

def hashCode(): Int

def head: LinearCombination

def headOption: Option[LinearCombination]

def implies(that: EquationSet): Boolean

def indexOf[B >: LinearCombination](elem: B, from: Int): Int

def indexOf[B >: LinearCombination](elem: B): Int

def indexOfSlice[B >: LinearCombination](that: GenSeq[B], from: Int): Int

def indexOfSlice[B >: LinearCombination](that: GenSeq[B]): Int

def indexWhere(p: (LinearCombination) ⇒ Boolean, from: Int): Int

def indexWhere(p: (LinearCombination) ⇒ Boolean): Int

def indices: Range

def init: IndexedSeq[LinearCombination]

def inits: Iterator[IndexedSeq[LinearCombination]]

def intersect[B >: LinearCombination](that: GenSeq[B]): IndexedSeq[LinearCombination]

def isDefinedAt(idx: Int): Boolean

def isEmpty: Boolean

def isFalse: Boolean

The only allowed case of obviously unsatisfiable conjunctions of negated equations is the one of a single equation 0!=0

final def isInstanceOf[T0]: Boolean

def isSortedBy(otherOrder: TermOrder): Boolean

final def isTraversableAgain: Boolean

def isTrue: Boolean

Return true if this formula is obviously always true

def iterator: Iterator[LinearCombination]

def last: LinearCombination

def lastIndexOf[B >: LinearCombination](elem: B, end: Int): Int

def lastIndexOf[B >: LinearCombination](elem: B): Int

def lastIndexOfSlice[B >: LinearCombination](that: GenSeq[B], end: Int): Int

def lastIndexOfSlice[B >: LinearCombination](that: GenSeq[B]): Int

def lastIndexWhere(p: (LinearCombination) ⇒ Boolean, end: Int): Int

def lastIndexWhere(p: (LinearCombination) ⇒ Boolean): Int

def lastOption: Option[LinearCombination]

lazy val leadingTermSet: Set[Term]

def length: Int

def lengthCompare(len: Int): Int

val lhss: Array[LinearCombination]

def lift: (Int) ⇒ Option[LinearCombination]

def map[B, That](f: (LinearCombination) ⇒ B)(implicit bf: CanBuildFrom[IndexedSeq[LinearCombination], B, That]): That

def max[B >: LinearCombination](implicit cmp: Ordering[B]): LinearCombination

def maxBy[B](f: (LinearCombination) ⇒ B)(implicit cmp: Ordering[B]): LinearCombination

def min[B >: LinearCombination](implicit cmp: Ordering[B]): LinearCombination

def minBy[B](f: (LinearCombination) ⇒ B)(implicit cmp: Ordering[B]): LinearCombination

def mkString: String

def mkString(sep: String): String

def mkString(start: String, sep: String, end: String): String

final def ne(arg0: AnyRef): Boolean

def negate: EquationConj

Create the negation of at most one negated equation

def newBuilder: Builder[LinearCombination, IndexedSeq[LinearCombination]]

def nonEmpty: Boolean

final def notify(): Unit

final def notifyAll(): Unit

def orElse[A1 <: Int, B1 >: LinearCombination](that: PartialFunction[A1, B1]): PartialFunction[A1, B1]

val order: TermOrder

def padTo[B >: LinearCombination, That](len: Int, elem: B)(implicit bf: CanBuildFrom[IndexedSeq[LinearCombination], B, That]): That

def par: ParSeq[LinearCombination]

def parCombiner: Combiner[LinearCombination, ParSeq[LinearCombination]]

def partition(p: (LinearCombination) ⇒ Boolean): (IndexedSeq[LinearCombination], IndexedSeq[LinearCombination])

def patch[B >: LinearCombination, That](from: Int, patch: GenSeq[B], replaced: Int)(implicit bf: CanBuildFrom[IndexedSeq[LinearCombination], B, That]): That

def permutations: Iterator[IndexedSeq[LinearCombination]]

def predicates: Set[Predicate]

def prefixLength(p: (LinearCombination) ⇒ Boolean): Int

def product[B >: LinearCombination](implicit num: Numeric[B]): B

def reduce[A1 >: LinearCombination](op: (A1, A1) ⇒ A1): A1

def reduceLeft[B >: LinearCombination](op: (B, LinearCombination) ⇒ B): B

def reduceLeftOption[B >: LinearCombination](op: (B, LinearCombination) ⇒ B): Option[B]

def reduceOption[A1 >: LinearCombination](op: (A1, A1) ⇒ A1): Option[A1]

def reduceRight[B >: LinearCombination](op: (LinearCombination, B) ⇒ B): B

def reduceRightOption[B >: LinearCombination](op: (LinearCombination, B) ⇒ B): Option[B]

val relationString: String

def repr: IndexedSeq[LinearCombination]

def reverse: IndexedSeq[LinearCombination]

def reverseIterator: Iterator[LinearCombination]

def reverseMap[B, That](f: (LinearCombination) ⇒ B)(implicit bf: CanBuildFrom[IndexedSeq[LinearCombination], B, That]): That

def reversed: List[LinearCombination]

def runWith[U](action: (LinearCombination) ⇒ U): (Int) ⇒ Boolean

def sameElements[B >: LinearCombination](that: GenIterable[B]): Boolean

def scan[B >: LinearCombination, That](z: B)(op: (B, B) ⇒ B)(implicit cbf: CanBuildFrom[IndexedSeq[LinearCombination], B, That]): That

def scanLeft[B, That](z: B)(op: (B, LinearCombination) ⇒ B)(implicit bf: CanBuildFrom[IndexedSeq[LinearCombination], B, That]): That

def scanRight[B, That](z: B)(op: (LinearCombination, B) ⇒ B)(implicit bf: CanBuildFrom[IndexedSeq[LinearCombination], B, That]): That

def segmentLength(p: (LinearCombination) ⇒ Boolean, from: Int): Int

def seq: IndexedSeq[LinearCombination]

def size: Int

def slice(from: Int, until: Int): IndexedSeq[LinearCombination]

def sliding(size: Int, step: Int): Iterator[IndexedSeq[LinearCombination]]

def sliding(size: Int): Iterator[IndexedSeq[LinearCombination]]

def sortBy(newOrder: TermOrder): NegEquationConj

Re-sort an object with a new TermOrder.

def sortBy[B](f: (LinearCombination) ⇒ B)(implicit ord: Ordering[B]): IndexedSeq[LinearCombination]

def sortWith(lt: (LinearCombination, LinearCombination) ⇒ Boolean): IndexedSeq[LinearCombination]

def sorted[B >: LinearCombination](implicit ord: Ordering[B]): IndexedSeq[LinearCombination]

def span(p: (LinearCombination) ⇒ Boolean): (IndexedSeq[LinearCombination], IndexedSeq[LinearCombination])

def splitAt(n: Int): (IndexedSeq[LinearCombination], IndexedSeq[LinearCombination])

def startsWith[B](that: GenSeq[B], offset: Int): Boolean

def startsWith[B](that: GenSeq[B]): Boolean

def stringPrefix: String

def sum[B >: LinearCombination](implicit num: Numeric[B]): B

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

def tail: IndexedSeq[LinearCombination]

def tails: Iterator[IndexedSeq[LinearCombination]]

def take(n: Int): IndexedSeq[LinearCombination]

def takeRight(n: Int): IndexedSeq[LinearCombination]

def takeWhile(p: (LinearCombination) ⇒ Boolean): IndexedSeq[LinearCombination]

def thisCollection: IndexedSeq[LinearCombination]

def to[Col[_]](implicit cbf: CanBuildFrom[Nothing, LinearCombination, Col[LinearCombination]]): Col[LinearCombination]

def toArray[B >: LinearCombination](implicit arg0: ClassTag[B]): Array[B]

def toBuffer[A1 >: LinearCombination]: Buffer[A1]

def toCollection(repr: IndexedSeq[LinearCombination]): IndexedSeq[LinearCombination]

def toIndexedSeq: IndexedSeq[LinearCombination]

def toIterable: Iterable[LinearCombination]

def toIterator: Iterator[LinearCombination]

def toList: List[LinearCombination]

def toMap[T, U](implicit ev: <:<[LinearCombination, (T, U)]): Map[T, U]

def toSeq: Seq[LinearCombination]

def toSet: Set[LinearCombination] { ... /* 2 definitions in type refinement */ }

def toSet[B >: LinearCombination]: Set[B]

def toStream: Stream[LinearCombination]

def toString(): String

def toTraversable: Traversable[LinearCombination]

def toVector: Vector[LinearCombination]

def transpose[B](implicit asTraversable: (LinearCombination) ⇒ GenTraversableOnce[B]): IndexedSeq[IndexedSeq[B]]

def union[B >: LinearCombination, That](that: GenSeq[B])(implicit bf: CanBuildFrom[IndexedSeq[LinearCombination], B, That]): That

def unzip[A1, A2](implicit asPair: (LinearCombination) ⇒ (A1, A2)): (IndexedSeq[A1], IndexedSeq[A2])

def unzip3[A1, A2, A3](implicit asTriple: (LinearCombination) ⇒ (A1, A2, A3)): (IndexedSeq[A1], IndexedSeq[A2], IndexedSeq[A3])

def updateEqs(newEqs: Seq[LinearCombination])(implicit newOrder: TermOrder): NegEquationConj

Update the equations of this conjunction; if nothing has changed, this is returned

def updateEqsSubset(newEqs: Seq[LinearCombination])(implicit newOrder: TermOrder): NegEquationConj

Update the equations of this conjunction under the assumption that the new equations form a subset of the old equations

def updated[B >: LinearCombination, That](index: Int, elem: B)(implicit bf: CanBuildFrom[IndexedSeq[LinearCombination], B, That]): That

lazy val variables: Set[VariableTerm]

def view(from: Int, until: Int): SeqView[LinearCombination, IndexedSeq[LinearCombination]]

def view: SeqView[LinearCombination, IndexedSeq[LinearCombination]]

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

final def wait(arg0: Long): Unit

final def wait(): Unit

def withFilter(p: (LinearCombination) ⇒ Boolean): FilterMonadic[LinearCombination, IndexedSeq[LinearCombination]]

def zip[A1 >: LinearCombination, B, That](that: GenIterable[B])(implicit bf: CanBuildFrom[IndexedSeq[LinearCombination], (A1, B), That]): That

def zipAll[B, A1 >: LinearCombination, That](that: GenIterable[B], thisElem: A1, thatElem: B)(implicit bf: CanBuildFrom[IndexedSeq[LinearCombination], (A1, B), That]): That

def zipWithIndex[A1 >: LinearCombination, That](implicit bf: CanBuildFrom[IndexedSeq[LinearCombination], (A1, Int), That]): That

def finalize(): Unit