diff options
Diffstat (limited to 'src/theory/arith/theory_arith.h')
-rw-r--r-- | src/theory/arith/theory_arith.h | 37 |
1 files changed, 27 insertions, 10 deletions
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 5d39f626c..fa60b5fcf 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -28,7 +28,7 @@ #include "expr/node.h" #include "theory/arith/arith_utilities.h" -#include "theory/arith/arithvar_dense_set.h" +#include "theory/arith/arithvar_set.h" #include "theory/arith/delta_rational.h" #include "theory/arith/tableau.h" #include "theory/arith/arith_rewriter.h" @@ -39,6 +39,7 @@ #include "util/stats.h" #include <vector> +#include <map> #include <queue> namespace CVC4 { @@ -63,6 +64,8 @@ private: std::vector<Node> d_variables; + std::map<ArithVar, ReducedRowVector*> d_removedRows; + /** * Priority Queue of the basic variables that may be inconsistent. * @@ -81,7 +84,8 @@ private: */ ArithPartialModel d_partialModel; - ArithVarDenseSet d_basicManager; + ArithVarSet d_basicManager; + ArithVarSet d_userVariables; ActivityMonitor d_activityMonitor; /** @@ -119,11 +123,7 @@ public: void shutdown(){ } - void presolve(){ - static int callCount = 0; - Debug("arith::presolve") << "TheoryArith::presolve #" << (callCount++) << endl; - check(FULL_EFFORT); - } + void presolve(); void staticLearning(TNode in, NodeBuilder<>& learned); @@ -148,15 +148,30 @@ private: void setupSlack(TNode left); - - /** * Handles the case splitting for check() for a new assertion. * returns true if their is a conflict. */ bool assertionCases(TNode assertion); - ArithVar findBasicRow(ArithVar variable); + /** + * Returns the basic variable with the shorted row containg a non-basic variable. + * If no such row exists, return ARITHVAR_SENTINEL. + */ + ArithVar findShortestBasicRow(ArithVar variable); + + /** + * Debugging only routine! + * Returns true iff every variable is consistent in the partial model. + */ + bool entireStateIsConsistent(); + + /** + * Permanently removes a variable from the problem. + * The caller guarentees the saftey of this removal! + */ + void permanentlyRemoveVariable(ArithVar v); + void asVectors(Polynomial& p, std::vector<Rational>& coeffs, @@ -171,6 +186,8 @@ private: IntStat d_statDisequalityConflicts; TimerStat d_staticLearningTimer; + IntStat d_permanentlyRemovedVariables; + TimerStat d_presolveTime; Statistics(); ~Statistics(); }; |