diff options
author | Tim King <taking@cs.nyu.edu> | 2011-03-03 16:34:48 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-03-03 16:34:48 +0000 |
commit | 3c8309cbf3f6549d9cc54fe45ccb5bb32a106d8e (patch) | |
tree | 8383e8e393ec7ec04c3cb1da02102e8876cc1adb /src/theory/arith/theory_arith.h | |
parent | 7cd7c850304caa12827c0deab1752293655d1248 (diff) |
Merged the tableau-copy branch into trunk. This adds a copy constructor and operator=(...) to Tableau.
Diffstat (limited to 'src/theory/arith/theory_arith.h')
-rw-r--r-- | src/theory/arith/theory_arith.h | 11 |
1 files changed, 1 insertions, 10 deletions
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index dc841170b..fb39eac09 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -71,15 +71,6 @@ private: */ std::map<ArithVar, Node> d_removedRows; - /** - * Priority Queue of the basic variables that may be inconsistent. - * - * This is required to contain at least 1 instance of every inconsistent - * basic variable. This is only required to be a superset though so its - * contents must be checked to still be basic and inconsistent. - */ - std::priority_queue<ArithVar> d_possiblyInconsistent; - /** Stores system wide constants to avoid unnessecary reconstruction. */ ArithConstants d_constants; @@ -157,7 +148,7 @@ public: void shutdown(){ } void presolve(); - + void notifyRestart(); void staticLearning(TNode in, NodeBuilder<>& learned); std::string identify() const { return std::string("TheoryArith"); } |