Conjunction

final def !=(arg0: Any): Boolean

final def ##(): Int

def &(that: Conjunction)(implicit newOrder: TermOrder): Conjunction

def --(that: Conjunction): Conjunction

def <=>(that: Conjunction)(implicit newOrder: TermOrder): Conjunction

final def ==(arg0: Any): Boolean

def ==>(that: Conjunction)(implicit newOrder: TermOrder): Conjunction

val arithConj: ArithConj

final def asInstanceOf[T0]: T0

lazy val boundVariables: Set[VariableTerm]

def clone(): AnyRef

lazy val constants: Set[ConstantTerm]

final def eq(arg0: AnyRef): Boolean

def equals(that: Any): Boolean

final def getClass(): Class[_]

lazy val groundAtoms: Set[Atom]

def hashCode(): Int

def implies(that: Conjunction): Boolean

def instantiate(terms: Seq[Term])(implicit newOrder: TermOrder): Conjunction

Instantiate the outermost quantifiers with the given terms, starting with the innermost quantifier to be instantiated

def isArithLiteral: Boolean

Return whether this conjunction actually only is a single arithmetic literal (a single, unquantified (in)equation, inequality)

def isDivisibility: Boolean

Return whether this is a divisibility judgement EX (n*_0 + t = 0)

def isDivisionFormula: Option[(LinearCombination, LinearCombination, Conjunction)]

"Division quantifiers" of the form EX ( n*_0 + t >= 0 & -n*_0 - t - m >= 0 & phi ) where 0 <= m < n .

def isDivisionFormulaHelp: Option[(LinearCombination, LinearCombination, InEqConj)]

def isExactDivisionFormula: Option[(LinearCombination, Conjunction)]

"Exact division quantifiers" of the form EX ( n*_0 + t = 0 & phi) where 0 < n .

def isExactDivisionFormulaHelp: Option[(LinearCombination, EquationConj)]

def isFalse: Boolean

The only allow case of false is when arithConj is false and everything else is empty.

final def isInstanceOf[T0]: Boolean

def isLiteral: Boolean

Return whether this conjunction actually only is a single literal (a single, unquantified (in)equation, inequality or predicate literal)

def isNegatedConjunction: Boolean

Return whether this conjunction actually is the negation of a single conjunction

def isNonDivisibility: Boolean

Return whether this is a negated divisibility judgement ALL (n*_0 + t != 0)

def isProperDivisibility: Boolean

Assuming that this formula is a divisibility or non-divisibility statement, check whether the divisibility is proper (i.e., not of the form ALL (1*_0 + t != 0))

def isPurelyNegated: Boolean

Return whether this conjunction only contains negated sub-conjunctions

def isQuantifiedDivisibility: Boolean

Return whether this is a divisibility judgement EX (n*_0 + t = 0), possibly underneath quantifiers

def isQuantifiedDivisionFormula: Option[(LinearCombination, LinearCombination, Conjunction)]

def isQuantifiedExactDivisionFormula: Option[(LinearCombination, Conjunction)]

def isQuantifiedNegatedConjunction: Boolean

Return whether this conjunction actually is the negation of a single conjunction

def isQuantifiedNonDivisibility: Boolean

Return whether this is a negated divisibility judgement ALL (n*_0 + t != 0), possibly underneath quantifiers

def isSortedBy(otherOrder: TermOrder): Boolean

def isTrue: Boolean

Return true if this formula is obviously always true

def iterator: Iterator[Conjunction]

final def ne(arg0: AnyRef): Boolean

def negate: Conjunction

val negatedConjs: NegatedConjunctions

final def notify(): Unit

final def notifyAll(): Unit

def opCount: Int

val order: TermOrder

val predConj: PredConj

lazy val predicates: Set[Predicate]

val quans: Seq[Quantifier]

def remove(that: Conjunction, logger: ComputationLogger): Conjunction

def size: Int

def sortBy(newOrder: TermOrder): Conjunction

Re-sort an object with a new TermOrder.

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

def toString(): String

def unary_!: Conjunction

def unquantify(num: Int): Conjunction

Remove the num outermost quantifiers of this Conjunction, without changing the matrix of the formula

def updateArithConj(ac: ArithConj)(implicit newOrder: TermOrder): Conjunction

Update the arithmetic parts of this conjunction (without changing anything else apart from the TermOrder)

def updateInEqs(newEqs: InEqConj)(implicit newOrder: TermOrder): Conjunction

Update the inequalities of this conjunction (without changing anything else apart from the TermOrder)

def updateNegatedConjs(newNegConjs: NegatedConjunctions)(implicit newOrder: TermOrder): Conjunction

Update the inequalities of this conjunction (without changing anything else apart from the TermOrder)

def updateNegativeEqs(newEqs: NegEquationConj)(implicit newOrder: TermOrder): Conjunction

Update the negative equations of this conjunction (without changing anything else apart from the TermOrder)

def updatePositiveEqs(newEqs: EquationConj)(implicit newOrder: TermOrder): Conjunction

Update the positive equations of this conjunction (without changing anything else apart from the TermOrder)

def updatePredConj(pc: PredConj)(implicit newOrder: TermOrder): Conjunction

Update the predicate parts of this conjunction (without changing anything else apart from the TermOrder)

lazy val variables: Set[VariableTerm]

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

final def wait(arg0: Long): Unit

final def wait(): Unit

def |(that: Conjunction)(implicit newOrder: TermOrder): Conjunction

def finalize(): Unit