EquationConj
Related Docs:
object EquationConj
| package equations
The only allowed case of obviously unsatisfiable systems of equations is the one of a single equation that has a non-zero literal lhs
The only allowed case of obviously unsatisfiable systems of equations is the one of a single equation that has a non-zero literal lhs
Return true if this formula is obviously always true
Return true if this formula is obviously always true
Create the negation of at most one equation
(Changed in version 2.9.0) The behavior of scanRight has changed. The previous behavior can be reproduced with scanRight.reverse.
Re-sort an object with a new TermOrder.
Re-sort an object with a new TermOrder. It is guaranteed that
the result isSortedBy(order)
(Changed in version 2.9.0) transpose throws an IllegalArgumentException if collections are not uniformly sized.
Update the equations of this conjunction; if nothing has changed,
this is returned
Update the equations of this conjunction; if nothing has changed,
this is returned
Update the equations of this conjunction under the assumption that the new equations form a subset of the old equations
(Since version ) see corresponding Javadoc for more information.
The class for representing conjunctions of equations, i.e., of systems of equations. Systems of equations are always implicitly canonised and reduced by means of row operations, i.e., it is ensured that the leading terms of two equations are always distinct, and that no equation can be made smaller in the used
TermOrderby adding multiples of other equations. This is not a complete method for deciding the satisfiability of a system, it is also necessary to perform column operations. Column operations are not applied implicitly, however.