diff options
Diffstat (limited to 'src/theory/arith/linear_equality.h')
-rw-r--r-- | src/theory/arith/linear_equality.h | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index 4d1d917b3..b5d439769 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -36,6 +36,7 @@ #include "theory/arith/arithvar.h" #include "theory/arith/partial_model.h" #include "theory/arith/tableau.h" +#include "theory/arith/constraint.h" #include "util/stats.h" @@ -101,14 +102,16 @@ private: * of the basic variable basic, using the non-basic variables in the row. */ template <bool upperBound> - void explainNonbasics(ArithVar basic, NodeBuilder<>& output); + void propagateNonbasics(ArithVar basic, Constraint c); public: - void explainNonbasicsLowerBound(ArithVar basic, NodeBuilder<>& output){ - explainNonbasics<false>(basic, output); + void propagateNonbasicsLowerBound(ArithVar basic, Constraint c){ + Assert(c->isLowerBound()); + propagateNonbasics<false>(basic, c); } - void explainNonbasicsUpperBound(ArithVar basic, NodeBuilder<>& output){ - explainNonbasics<true>(basic, output); + void propagateNonbasicsUpperBound(ArithVar basic, Constraint c){ + Assert(c->isUpperBound()); + propagateNonbasics<true>(basic, c); } /** |