case class CertNegEquation(_lhs: LinearCombination) extends CertArithLiteral with SortedWithOrder[CertNegEquation] with Product with Serializable
Formula expressing a negated equation lhs != 0
- Alphabetic
- By Inheritance
- CertNegEquation
- Serializable
- Product
- Equals
- SortedWithOrder
- Sorted
- CertArithLiteral
- CertFormula
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Instance Constructors
- new CertNegEquation(_lhs: LinearCombination)
Value Members
- val _lhs: LinearCombination
- def constants: Set[ConstantTerm]
- Definition Classes
- CertFormula
- def isFalse: Boolean
Return
true
if this formula is obviously always falseReturn
true
if this formula is obviously always false- Definition Classes
- CertNegEquation → CertFormula
- def isSortedBy(otherOrder: TermOrder): Boolean
- Definition Classes
- SortedWithOrder → Sorted
- def isTrue: Boolean
Return
true
if this formula is obviously always trueReturn
true
if this formula is obviously always true- Definition Classes
- CertNegEquation → CertFormula
- val lhs: LinearCombination
- Definition Classes
- CertArithLiteral
- val order: TermOrder
- Definition Classes
- CertFormula
- def predicates: Set[Predicate]
- Definition Classes
- CertFormula
- def productElementNames: Iterator[String]
- Definition Classes
- Product
- def sortBy(otherOrder: TermOrder): CertNegEquation
Re-sort an object with a new
TermOrder
.Re-sort an object with a new
TermOrder
. It is guaranteed that the resultisSortedBy(order)
- Definition Classes
- CertNegEquation → Sorted
- def toConj: Conjunction
Convert this formula to the corresponding formula in internal representation
Convert this formula to the corresponding formula in internal representation
- Definition Classes
- CertNegEquation → CertFormula
- def toFormula: NegEquationConj
Convert this formula to the corresponding formula in internal representation
Convert this formula to the corresponding formula in internal representation
- Definition Classes
- CertNegEquation → CertFormula
- def toString(): String
- Definition Classes
- CertNegEquation → AnyRef → Any
- def unary_!: CertEquation
Negate this formula
Negate this formula
- Definition Classes
- CertNegEquation → CertFormula
- def update(newLhs: LinearCombination): CertNegEquation
- Definition Classes
- CertNegEquation → CertArithLiteral