ReduceWithAC

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

def apply(conj: PredConj, logger: ComputationLogger): PredConj

def apply(conj: EquationConj): EquationConj

def apply(conj: ArithConj): ArithConj

final def asInstanceOf[T0]: T0

def clone(): AnyRef

final def eq(arg0: AnyRef): Boolean

def equals(arg0: Any): Boolean

final def getClass(): Class[_]

def hashCode(): Int

final def isInstanceOf[T0]: Boolean

def lowerBound(t: Term): Option[IdealInt]

Check whether known inequalities imply a lower bound of the given term.

def lowerBoundWithAssumptions(t: Term): Option[(IdealInt, Seq[LinearCombination])]

Check whether the known inequalities imply a lower bound of the given term.

final def ne(arg0: AnyRef): Boolean

final def notify(): Unit

final def notifyAll(): Unit

def passQuantifiers(num: Int): ReduceWithAC

def plainReduce(conj: ArithConj): (ArithConj, ReduceWithAC)

Just reduce the components of the conjunction individually, do not do any internal propagation.

def reduceAndAdd(conj: ArithConj, logger: ComputationLogger): (ArithConj, ReduceWithAC)

Reduce an arithmetic conjunction using the information stored in this object.

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

def toString(): String

def upperBound(t: Term): Option[IdealInt]

Check whether known inequalities imply an upper bound of the given term.

def upperBoundWithAssumptions(t: Term): Option[(IdealInt, Seq[LinearCombination])]

Check whether the known inequalities imply an upper bound of the given term.

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

final def wait(arg0: Long): Unit

final def wait(): Unit

def finalize(): Unit