diff options
author | Tim King <taking@cs.nyu.edu> | 2011-03-17 21:20:28 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-03-17 21:20:28 +0000 |
commit | 0e22528f5d249e301b2a5dc1f14849a7f8e25439 (patch) | |
tree | edca918e8722a75568e174f25a5af066daabe484 /src/theory/arith/simplex.h | |
parent | 232042b3e2e265dbfe9c693d018d48388be91018 (diff) |
SimplexDecisionProcedure no longer takes an OutputChannel as a parameter.
Diffstat (limited to 'src/theory/arith/simplex.h')
-rw-r--r-- | src/theory/arith/simplex.h | 23 |
1 files changed, 9 insertions, 14 deletions
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 6f3ff073f..968275ae5 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -10,7 +10,6 @@ #include "theory/arith/delta_rational.h" #include "theory/arith/tableau.h" #include "theory/arith/partial_model.h" -#include "theory/output_channel.h" #include "util/options.h" @@ -31,8 +30,6 @@ private: */ ArithPartialModel& d_partialModel; - OutputChannel* d_out; - Tableau& d_tableau; ArithPriorityQueue d_queue; @@ -45,10 +42,8 @@ private: public: SimplexDecisionProcedure(ArithPartialModel& pm, - OutputChannel* out, Tableau& tableau) : d_partialModel(pm), - d_out(out), d_tableau(tableau), d_queue(pm, tableau), d_numVariables(0), @@ -61,20 +56,20 @@ public: * Assert*(n, orig) takes an bound n that is implied by orig. * and asserts that as a new bound if it is tighter than the current bound * and updates the value of a basic variable if needed. - * If this new bound is in conflict with the other bound, - * a conflict is created and asserted to the output channel. * - * orig must be an atom in the SAT solver so that it can be used for + * orig must be a literal in the SAT solver so that it can be used for * conflict analysis. * - * n is of the form (x =?= c) where x is a variable, - * c is a constant and =?= is either LT, LEQ, EQ, GEQ, or GT. + * x is the variable getting the new bound, + * c is the value of the new bound. * - * returns true if a conflict was asserted. + * If this new bound is in conflict with the other bound, + * a node describing this conflict is returned. + * If this new bound is not in conflict, Node::null() is returned. */ - bool AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode orig); - bool AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode orig); - bool AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode orig); + Node AssertLower(ArithVar x, const DeltaRational& c, TNode orig); + Node AssertUpper(ArithVar x, const DeltaRational& c, TNode orig); + Node AssertEquality(ArithVar x, const DeltaRational& c, TNode orig); private: /** |