diff options
| -rw-r--r-- | src/theory/arith/Makefile.am | 1 | ||||
| -rw-r--r-- | src/theory/arith/arithvar_set.h | 134 | ||||
| -rw-r--r-- | src/theory/arith/normal_form.h | 1 | ||||
| -rw-r--r-- | src/theory/arith/simplex.cpp | 132 | ||||
| -rw-r--r-- | src/theory/arith/simplex.h | 19 | ||||
| -rw-r--r-- | src/theory/arith/tableau.cpp | 6 | ||||
| -rw-r--r-- | src/theory/arith/tableau.h | 62 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith.cpp | 221 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith.h | 37 | ||||
| -rw-r--r-- | src/theory/arith/unate_propagator.cpp | 9 | ||||
| -rw-r--r-- | src/theory/arith/unate_propagator.h | 3 |
11 files changed, 427 insertions, 198 deletions
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index 6cb35e518..31867c4cf 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -20,6 +20,7 @@ libarith_la_SOURCES = \ ordered_bounds_list.h \ ordered_set.h \ arithvar_dense_set.h \ + arithvar_set.h \ tableau.h \ tableau.cpp \ simplex.h \ diff --git a/src/theory/arith/arithvar_set.h b/src/theory/arith/arithvar_set.h new file mode 100644 index 000000000..95617c5a0 --- /dev/null +++ b/src/theory/arith/arithvar_set.h @@ -0,0 +1,134 @@ +/********************* */ +/*! \file arithvar_set.h + ** \verbatim + ** Original author: taking + ** Major contributors: mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include <vector> +#include "theory/arith/arith_utilities.h" + + +#ifndef __CVC4__THEORY__ARITH__ARTIHVAR_SET_H +#define __CVC4__THEORY__ARITH__ARTIHVAR_SET_H + +namespace CVC4 { +namespace theory { +namespace arith { + +/** + * This is an abstraction of a set of ArithVars. + * This class is designed to provide constant time insertion, deletion, and element_of + * and fast iteration. + * The cost of doing this is that it takes O(M) where M is the total number + * of ArithVars in memory. + */ + +class ArithVarSet { +private: + typedef std::vector<ArithVar> VarList; + //List of the ArithVars in the set. + VarList d_list; + + //Each ArithVar in the set is mapped to its position in d_list. + //Each ArithVar not in the set is mapped to ARITHVAR_SENTINEL + std::vector<unsigned> d_posVector; + +public: + typedef VarList::const_iterator iterator; + + ArithVarSet() : d_list(), d_posVector() {} + + size_t size() const { + return d_list.size(); + } + + size_t allocated() const { + return d_posVector.size(); + } + + void increaseSize(ArithVar max){ + Assert(max >= allocated()); + d_posVector.resize(max+1, ARITHVAR_SENTINEL); + } + + void increaseSize(){ + increaseSize(allocated()); + } + + bool isMember(ArithVar x) const{ + Assert(x < allocated()); + return d_posVector[x] != ARITHVAR_SENTINEL; + } + + /** Invalidates iterators */ + void init(ArithVar x, bool val) { + Assert(x >= size()); + increaseSize(x); + if(val){ + add(x); + } + } + + /** Invalidates iterators */ + void add(ArithVar x){ + Assert(!isMember(x)); + d_posVector[x] = size(); + d_list.push_back(x); + } + + iterator begin() const{ return d_list.begin(); } + iterator end() const{ return d_list.end(); } + + + /** Invalidates iterators */ + void remove(ArithVar x){ + Assert(isMember(x)); + swapToBack(x); + d_posVector[x] = ARITHVAR_SENTINEL; + d_list.pop_back(); + } + + private: + + /** This should be true of all x < allocated() after every operation. */ + bool wellFormed(ArithVar x){ + if(d_posVector[x] == ARITHVAR_SENTINEL){ + return true; + }else{ + return d_list[d_posVector[x]] == x; + } + } + + /** Swaps a member x to the back of d_list. */ + void swapToBack(ArithVar x){ + Assert(isMember(x)); + + unsigned currentPos = d_posVector[x]; + ArithVar atBack = d_list.back(); + + d_list[currentPos] = atBack; + d_posVector[atBack] = currentPos; + + d_list[size() - 1] = x; + d_posVector[x] = size() - 1; + } +}; + +}; /* namespace arith */ +}; /* namespace theory */ +}; /* namespace CVC4 */ + +#endif /* __CVC4__THEORY__ARITH__ARTIHVAR_SET_H */ diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index 29db6cdb9..aa4e8bc13 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -188,6 +188,7 @@ public: static bool isMember(Node n) { if (n.getKind() == kind::CONST_INTEGER) return false; if (n.getKind() == kind::CONST_RATIONAL) return false; + if (isRelationOperator(n.getKind())) return false; return Theory::isLeafOf(n, theory::THEORY_ARITH); } diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 2e9fb7352..f7e3c112c 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -21,7 +21,10 @@ SimplexDecisionProcedure::Statistics::Statistics(): d_statUnEjections("theory::arith::UnEjections", 0), d_statEarlyConflicts("theory::arith::EarlyConflicts", 0), d_statEarlyConflictImprovements("theory::arith::EarlyConflictImprovements", 0), - d_selectInitialConflictTime("theory::arith::selectInitialConflictTime") + d_selectInitialConflictTime("theory::arith::selectInitialConflictTime"), + d_pivotsAfterConflict("theory::arith::pivotsAfterConflict", 0), + d_checksWithWastefulPivots("theory::arith::checksWithWastefulPivots", 0), + d_pivotTime("theory::arith::pivotTime") { StatisticsRegistry::registerStat(&d_statPivots); StatisticsRegistry::registerStat(&d_statUpdates); @@ -33,6 +36,10 @@ SimplexDecisionProcedure::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_statEarlyConflicts); StatisticsRegistry::registerStat(&d_statEarlyConflictImprovements); StatisticsRegistry::registerStat(&d_selectInitialConflictTime); + + StatisticsRegistry::registerStat(&d_pivotsAfterConflict); + StatisticsRegistry::registerStat(&d_checksWithWastefulPivots); + StatisticsRegistry::registerStat(&d_pivotTime); } SimplexDecisionProcedure::Statistics::~Statistics(){ @@ -46,10 +53,15 @@ SimplexDecisionProcedure::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_statEarlyConflicts); StatisticsRegistry::unregisterStat(&d_statEarlyConflictImprovements); StatisticsRegistry::unregisterStat(&d_selectInitialConflictTime); + + StatisticsRegistry::unregisterStat(&d_pivotsAfterConflict); + StatisticsRegistry::unregisterStat(&d_checksWithWastefulPivots); + StatisticsRegistry::unregisterStat(&d_pivotTime); } void SimplexDecisionProcedure::ejectInactiveVariables(){ + return; //die die die for(ArithVarSet::iterator i = d_tableau.begin(), end = d_tableau.end(); i != end;){ ArithVar variable = *i; @@ -247,6 +259,32 @@ void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){ Assert(x_i != x_j); + TimerStat::CodeTimer codeTimer(d_statistics.d_pivotTime); + + if(Debug.isOn("arith::pivotAndUpdate")){ + Debug("arith::pivotAndUpdate") << "x_i " << "|->" << x_j << endl; + ReducedRowVector* row_k = d_tableau.lookup(x_i); + for(ReducedRowVector::NonZeroIterator varIter = row_k->beginNonZero(); + varIter != row_k->endNonZero(); + ++varIter){ + + ArithVar var = varIter->first; + const Rational& coeff = varIter->second; + DeltaRational beta = d_partialModel.getAssignment(var); + Debug("arith::pivotAndUpdate") << var << beta << coeff; + if(d_partialModel.hasLowerBound(var)){ + Debug("arith::pivotAndUpdate") << "(lb " << d_partialModel.getLowerBound(var) << ")"; + } + if(d_partialModel.hasUpperBound(var)){ + Debug("arith::pivotAndUpdate") << "(up " << d_partialModel.getUpperBound(var) + << ")"; + } + Debug("arith::pivotAndUpdate") << endl; + } + Debug("arith::pivotAndUpdate") << "end row"<< endl; + } + + ReducedRowVector* row_i = d_tableau.lookup(x_i); const Rational& a_ij = row_i->lookup(x_j); @@ -279,11 +317,35 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR } } + // Pivots ++(d_statistics.d_statPivots); + if( d_foundAConflict ){ + ++d_pivotsSinceConflict; + if(d_pivotsSinceConflict == 1){ + ++(d_statistics.d_checksWithWastefulPivots); + } + ++(d_statistics.d_pivotsAfterConflict); + } + d_tableau.pivot(x_i, x_j); checkBasicVariable(x_j); + // Debug found conflict + if( !d_foundAConflict ){ + DeltaRational beta_j = d_partialModel.getAssignment(x_j); + + if(d_partialModel.belowLowerBound(x_j, beta_j, true)){ + if(selectSlackBelow(x_j) == ARITHVAR_SENTINEL ){ + d_foundAConflict = true; + } + }else if(d_partialModel.aboveUpperBound(x_j, beta_j, true)){ + if(selectSlackAbove(x_j) == ARITHVAR_SENTINEL ){ + d_foundAConflict = true; + } + } + } + if(Debug.isOn("tableau")){ d_tableau.printTableau(); } @@ -364,7 +426,8 @@ ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){ }else{ slack = nonbasic; break; } - }else if(cmp < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){if(d_pivotStage){ + }else if(cmp < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){ + if(d_pivotStage){ if(d_tableau.getRowCount(nonbasic) < numRows){ slack = nonbasic; numRows = d_tableau.getRowCount(nonbasic); @@ -409,26 +472,15 @@ Node SimplexDecisionProcedure::selectInitialConflict() { ArithVar x_i = (*i).first; d_griggioRuleQueue.push(*i); - DeltaRational beta_i = d_partialModel.getAssignment(x_i); + Node possibleConflict = checkBasicForConflict(x_i); + if(!possibleConflict.isNull()){ + Node better = betterConflict(bestConflict, possibleConflict); - if(d_partialModel.belowLowerBound(x_i, beta_i, true)){ - DeltaRational l_i = d_partialModel.getLowerBound(x_i); - ArithVar x_j = selectSlackBelow(x_i); - if(x_j == ARITHVAR_SENTINEL ){ - Node better = betterConflict(bestConflict, generateConflictBelow(x_i)); - if(better != bestConflict) ++conflictChanges; - bestConflict = better; - ++(d_statistics.d_statEarlyConflicts); - } - }else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){ - DeltaRational u_i = d_partialModel.getUpperBound(x_i); - ArithVar x_j = selectSlackAbove(x_i); - if(x_j == ARITHVAR_SENTINEL ){ - Node better = betterConflict(bestConflict, generateConflictAbove(x_i)); - if(better != bestConflict) ++conflictChanges; - bestConflict = better; - ++(d_statistics.d_statEarlyConflicts); + if(better != bestConflict){ + ++conflictChanges; } + bestConflict = better; + ++(d_statistics.d_statEarlyConflicts); } } if(conflictChanges > 1) ++(d_statistics.d_statEarlyConflictImprovements); @@ -438,7 +490,13 @@ Node SimplexDecisionProcedure::selectInitialConflict() { Node SimplexDecisionProcedure::updateInconsistentVars(){ if(d_griggioRuleQueue.empty()) return Node::null(); - Node possibleConflict = selectInitialConflict(); + d_foundAConflict = false; + d_pivotsSinceConflict = 0; + + Node possibleConflict = Node::null(); + if(d_griggioRuleQueue.size() > 1){ + possibleConflict = selectInitialConflict(); + } if(possibleConflict.isNull()){ possibleConflict = privateUpdateInconsistentVars(); } @@ -457,6 +515,25 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){ return possibleConflict; } +Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){ + + Assert(d_basicManager.isMember(basic)); + const DeltaRational& beta = d_partialModel.getAssignment(basic); + + if(d_partialModel.belowLowerBound(basic, beta, true)){ + ArithVar x_j = selectSlackBelow(basic); + if(x_j == ARITHVAR_SENTINEL ){ + return generateConflictBelow(basic); + } + }else if(d_partialModel.aboveUpperBound(basic, beta, true)){ + ArithVar x_j = selectSlackAbove(basic); + if(x_j == ARITHVAR_SENTINEL ){ + return generateConflictAbove(basic); + } + } + return Node::null(); +} + //corresponds to Check() in dM06 Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){ Assert(d_pivotStage || d_griggioRuleQueue.empty()); @@ -470,7 +547,7 @@ Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){ if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); } ArithVar x_i = selectSmallestInconsistentVar(); - Debug("arith_update") << "selectSmallestInconsistentVar()=" << x_i << endl; + Debug("arith::update::select") << "selectSmallestInconsistentVar()=" << x_i << endl; if(x_i == ARITHVAR_SENTINEL){ Debug("arith_update") << "No inconsistent variables" << endl; return Node::null(); //sat @@ -481,10 +558,11 @@ Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){ ejectInactiveVariables(); DeltaRational beta_i = d_partialModel.getAssignment(x_i); + ArithVar x_j = ARITHVAR_SENTINEL; if(d_partialModel.belowLowerBound(x_i, beta_i, true)){ DeltaRational l_i = d_partialModel.getLowerBound(x_i); - ArithVar x_j = selectSlackBelow(x_i); + x_j = selectSlackBelow(x_i); if(x_j == ARITHVAR_SENTINEL ){ ++(d_statistics.d_statUpdateConflicts); return generateConflictBelow(x_i); //unsat @@ -493,13 +571,19 @@ Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){ }else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){ DeltaRational u_i = d_partialModel.getUpperBound(x_i); - ArithVar x_j = selectSlackAbove(x_i); + x_j = selectSlackAbove(x_i); if(x_j == ARITHVAR_SENTINEL ){ ++(d_statistics.d_statUpdateConflicts); return generateConflictAbove(x_i); //unsat } pivotAndUpdate(x_i, x_j, u_i); } + Assert(x_j != ARITHVAR_SENTINEL); + //Check to see if we already have a conflict with x_j to prevent wasteful work + Node earlyConflict = checkBasicForConflict(x_j); + if(!earlyConflict.isNull()){ + return earlyConflict; + } } if(d_pivotStage && iteratationNum >= d_numVariables){ diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 2ae6b091d..587f468e0 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -5,7 +5,7 @@ #define __CVC4__THEORY__ARITH__SIMPLEX_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/partial_model.h" @@ -55,7 +55,7 @@ private: */ ArithPartialModel& d_partialModel; - ArithVarDenseSet& d_basicManager; + ArithVarSet& d_basicManager; ActivityMonitor& d_activityMonitor; OutputChannel* d_out; @@ -70,7 +70,7 @@ private: public: SimplexDecisionProcedure(const ArithConstants& constants, ArithPartialModel& pm, - ArithVarDenseSet& bm, + ArithVarSet& bm, OutputChannel* out, ActivityMonitor& am, Tableau& tableau) : @@ -197,6 +197,15 @@ private: /** Check to make sure all of the basic variables are within their bounds. */ void checkBasicVariable(ArithVar basic); + /** + * Checks a basic variable, b, to see if it is in conflict. + * If a conflict is discovered a node summarizing the conflict is returned. + * Otherwise, Node::null() is returned. + */ + Node checkBasicForConflict(ArithVar b); + + bool d_foundAConflict; + unsigned d_pivotsSinceConflict; /** These fields are designed to be accessable to TheoryArith methods. */ class Statistics { @@ -207,7 +216,11 @@ private: IntStat d_statEjections, d_statUnEjections; IntStat d_statEarlyConflicts, d_statEarlyConflictImprovements; + TimerStat d_selectInitialConflictTime; + + IntStat d_pivotsAfterConflict, d_checksWithWastefulPivots; + TimerStat d_pivotTime; Statistics(); ~Statistics(); }; diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index 1d58c5e1d..1cf6d07cd 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -33,7 +33,7 @@ void Tableau::addRow(ArithVar basicVar, //The new basic variable cannot already be a basic variable Assert(!isActiveBasicVariable(basicVar)); - d_activeBasicVars.insert(basicVar); + d_activeBasicVars.add(basicVar); ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs,d_rowCount); d_rowsTable[basicVar] = row_current; @@ -73,10 +73,10 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){ d_rowsTable[x_s] = row_s; d_rowsTable[x_r] = NULL; - d_activeBasicVars.erase(x_r); + d_activeBasicVars.remove(x_r); d_basicManager.remove(x_r); - d_activeBasicVars.insert(x_s); + d_activeBasicVars.add(x_s); d_basicManager.add(x_s); row_s->pivot(x_s); diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 5e34ac1a2..05fcf6cf8 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -22,7 +22,7 @@ #include "expr/attribute.h" #include "theory/arith/arith_utilities.h" -#include "theory/arith/arithvar_dense_set.h" +#include "theory/arith/arithvar_set.h" #include "theory/arith/normal_form.h" #include "theory/arith/row_vector.h" @@ -37,54 +37,6 @@ namespace CVC4 { namespace theory { namespace arith { -class ArithVarSet { -private: - typedef std::list<ArithVar> VarList; - -public: - typedef VarList::const_iterator iterator; - -private: - VarList d_list; - std::vector< VarList::iterator > d_posVector; - -public: - ArithVarSet() : d_list(), d_posVector() {} - - iterator begin() const{ return d_list.begin(); } - iterator end() const{ return d_list.end(); } - - void insert(ArithVar av){ - Assert(inRange(av) ); - Assert(!inSet(av) ); - - d_posVector[av] = d_list.insert(d_list.end(), av); - } - - void erase(ArithVar var){ - Assert( inRange(var) ); - Assert( inSet(var) ); - - d_list.erase(d_posVector[var]); - d_posVector[var] = d_list.end(); - } - - void increaseSize(){ - d_posVector.push_back(d_list.end()); - } - - bool inSet(ArithVar v) const{ - Assert(inRange(v) ); - - return d_posVector[v] != d_list.end(); - } - -private: - bool inRange(ArithVar v) const{ - return v < d_posVector.size(); - } -}; - class Tableau { private: @@ -95,7 +47,7 @@ private: ActivityMonitor& d_activityMonitor; - ArithVarDenseSet& d_basicManager; + ArithVarSet& d_basicManager; std::vector<uint32_t> d_rowCount; @@ -103,7 +55,7 @@ public: /** * Constructs an empty tableau. */ - Tableau(ActivityMonitor &am, ArithVarDenseSet& bm) : + Tableau(ActivityMonitor &am, ArithVarSet& bm) : d_activeBasicVars(), d_rowsTable(), d_activityMonitor(am), @@ -163,20 +115,22 @@ public: Assert(d_basicManager.isMember(basic)); Assert(isActiveBasicVariable(basic)); - d_activeBasicVars.erase(basic); + d_activeBasicVars.remove(basic); } void reinjectBasic(ArithVar basic){ + AlwaysAssert(false); + Assert(d_basicManager.isMember(basic)); Assert(isEjected(basic)); ReducedRowVector* row = lookupEjected(basic); - d_activeBasicVars.insert(basic); + d_activeBasicVars.add(basic); updateRow(row); } private: inline bool isActiveBasicVariable(ArithVar var){ - return d_activeBasicVars.inSet(var); + return d_activeBasicVars.isMember(var); } void updateRow(ReducedRowVector* row); diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index ff79c18e6..1e1ac03ba 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -31,7 +31,7 @@ #include "theory/arith/delta_rational.h" #include "theory/arith/partial_model.h" #include "theory/arith/tableau.h" -#include "theory/arith/arithvar_dense_set.h" +#include "theory/arith/arithvar_set.h" #include "theory/arith/arith_rewriter.h" #include "theory/arith/unate_propagator.h" @@ -58,6 +58,7 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) : d_constants(NodeManager::currentNM()), d_partialModel(c), d_basicManager(), + d_userVariables(), d_activityMonitor(), d_diseq(c), d_tableau(d_activityMonitor, d_basicManager), @@ -73,13 +74,18 @@ TheoryArith::Statistics::Statistics(): d_statSlackVariables("theory::arith::SlackVariables", 0), d_statDisequalitySplits("theory::arith::DisequalitySplits", 0), d_statDisequalityConflicts("theory::arith::DisequalityConflicts", 0), - d_staticLearningTimer("theory::arith::staticLearningTimer") + d_staticLearningTimer("theory::arith::staticLearningTimer"), + d_permanentlyRemovedVariables("theory::arith::permanentlyRemovedVariables", 0), + d_presolveTime("theory::arith::presolveTime") { StatisticsRegistry::registerStat(&d_statUserVariables); StatisticsRegistry::registerStat(&d_statSlackVariables); StatisticsRegistry::registerStat(&d_statDisequalitySplits); StatisticsRegistry::registerStat(&d_statDisequalityConflicts); StatisticsRegistry::registerStat(&d_staticLearningTimer); + + StatisticsRegistry::registerStat(&d_permanentlyRemovedVariables); + StatisticsRegistry::registerStat(&d_presolveTime); } TheoryArith::Statistics::~Statistics(){ @@ -88,6 +94,9 @@ TheoryArith::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_statDisequalitySplits); StatisticsRegistry::unregisterStat(&d_statDisequalityConflicts); StatisticsRegistry::unregisterStat(&d_staticLearningTimer); + + StatisticsRegistry::unregisterStat(&d_permanentlyRemovedVariables); + StatisticsRegistry::unregisterStat(&d_presolveTime); } void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) { @@ -132,34 +141,34 @@ void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) { TNode cright = (c.getKind() == NOT) ? c[0][1] : c[1]; if((t == cright) && (e == cleft)){ - TNode tmp = t; - t = e; - e = tmp; - k = reverseRelationKind(k); + TNode tmp = t; + t = e; + e = tmp; + k = reverseRelationKind(k); } if(t == cleft && e == cright){ - // t == cleft && e == cright - Assert( t == cleft ); - Assert( e == cright ); - switch(k){ - case LT: // (ite (< x y) x y) - case LEQ: { // (ite (<= x y) x y) - Node nLeqX = NodeBuilder<2>(LEQ) << n << t; - Node nLeqY = NodeBuilder<2>(LEQ) << n << e; - Debug("arith::mins") << n << "is a min =>" << nLeqX << nLeqY << endl; - learned << nLeqX << nLeqY; - break; - } - case GT: // (ite (> x y) x y) - case GEQ: { // (ite (>= x y) x y) - Node nGeqX = NodeBuilder<2>(GEQ) << n << t; - Node nGeqY = NodeBuilder<2>(GEQ) << n << e; - Debug("arith::mins") << n << "is a max =>" << nGeqX << nGeqY << endl; - learned << nGeqX << nGeqY; - break; - } - default: Unreachable(); - } + // t == cleft && e == cright + Assert( t == cleft ); + Assert( e == cright ); + switch(k){ + case LT: // (ite (< x y) x y) + case LEQ: { // (ite (<= x y) x y) + Node nLeqX = NodeBuilder<2>(LEQ) << n << t; + Node nLeqY = NodeBuilder<2>(LEQ) << n << e; + Debug("arith::mins") << n << "is a min =>" << nLeqX << nLeqY << endl; + learned << nLeqX << nLeqY; + break; + } + case GT: // (ite (> x y) x y) + case GEQ: { // (ite (>= x y) x y) + Node nGeqX = NodeBuilder<2>(GEQ) << n << t; + Node nGeqY = NodeBuilder<2>(GEQ) << n << e; + Debug("arith::mins") << n << "is a max =>" << nGeqX << nGeqY << endl; + learned << nGeqX << nGeqY; + break; + } + default: Unreachable(); + } } } // == 2-CONSTANTS == @@ -177,84 +186,15 @@ void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) { Debug("arith::mins") << n << " is a constant sandwich" << nGeqMin << nLeqMax << endl; learned << nGeqMin << nLeqMax; } - - // // binary OR of binary ANDs of EQUALities - // if(n.getKind() == kind::OR && n.getNumChildren() == 2 && - // n[0].getKind() == kind::AND && n[0].getNumChildren() == 2 && - // n[1].getKind() == kind::AND && n[1].getNumChildren() == 2 && - // (n[0][0].getKind() == kind::EQUAL || n[0][0].getKind() == kind::IFF) && - // (n[0][1].getKind() == kind::EQUAL || n[0][1].getKind() == kind::IFF) && - // (n[1][0].getKind() == kind::EQUAL || n[1][0].getKind() == kind::IFF) && - // (n[1][1].getKind() == kind::EQUAL || n[1][1].getKind() == kind::IFF)) { - // // now we have (a = b && c = d) || (e = f && g = h) - - // Debug("diamonds") << "has form of a diamond!" << endl; - - // TNode - // a = n[0][0][0], b = n[0][0][1], - // c = n[0][1][0], d = n[0][1][1], - // e = n[1][0][0], f = n[1][0][1], - // g = n[1][1][0], h = n[1][1][1]; - - // // test that one of {a, b} = one of {c, d}, and make "b" the - // // shared node (i.e. put in the form (a = b && b = d)) - // // note we don't actually care about the shared ones, so the - // // "swaps" below are one-sided, ignoring b and c - // if(a == c) { - // a = b; - // } else if(a == d) { - // a = b; - // d = c; - // } else if(b == c) { - // // nothing to do - // } else if(b == d) { - // d = c; - // } else { - // // condition not satisfied - // Debug("diamonds") << "+ A fails" << endl; - // continue; - // } - - // Debug("diamonds") << "+ A holds" << endl; - - // // same: one of {e, f} = one of {g, h}, and make "f" the - // // shared node (i.e. put in the form (e = f && f = h)) - // if(e == g) { - // e = f; - // } else if(e == h) { - // e = f; - // h = g; - // } else if(f == g) { - // // nothing to do - // } else if(f == h) { - // h = g; - // } else { - // // condition not satisfied - // Debug("diamonds") << "+ B fails" << endl; - // continue; - // } - - // Debug("diamonds") << "+ B holds" << endl; - - // // now we have (a = b && b = d) || (e = f && f = h) - // // test that {a, d} == {e, h} - // if( (a == e && d == h) || - // (a == h && d == e) ) { - // // learn: n implies a == d - // Debug("diamonds") << "+ C holds" << endl; - // Node newEquality = a.getType().isBoolean() ? a.iffNode(d) : a.eqNode(d); - // Debug("diamonds") << " ==> " << newEquality << endl; - // learned << n.impNode(newEquality); - // } else { - // Debug("diamonds") << "+ C fails" << endl; - // } - // } } } -ArithVar TheoryArith::findBasicRow(ArithVar variable){ +ArithVar TheoryArith::findShortestBasicRow(ArithVar variable){ + ArithVar bestBasic = ARITHVAR_SENTINEL; + unsigned rowLength = 0; + for(ArithVarSet::iterator basicIter = d_tableau.begin(); basicIter != d_tableau.end(); ++basicIter){ @@ -262,10 +202,14 @@ ArithVar TheoryArith::findBasicRow(ArithVar variable){ ReducedRowVector* row_j = d_tableau.lookup(x_j); if(row_j->has(variable)){ - return x_j; + if((bestBasic == ARITHVAR_SENTINEL) || + (bestBasic != ARITHVAR_SENTINEL && row_j->size() < rowLength)){ + bestBasic = x_j; + rowLength = row_j->size(); + } } } - return ARITHVAR_SENTINEL; + return bestBasic; } @@ -279,7 +223,7 @@ void TheoryArith::preRegisterTerm(TNode n) { d_out->setIncomplete(); } - if(isLeaf(n) || isStrictlyVarList){ + if(Variable::isMember(n) || isStrictlyVarList){ ++(d_statistics.d_statUserVariables); ArithVar varN = requestArithVar(n,false); setupInitialValue(varN); @@ -322,6 +266,7 @@ ArithVar TheoryArith::requestArithVar(TNode x, bool basic){ d_activityMonitor.push_back(0); d_basicManager.init(varX,basic); + d_userVariables.init(varX, !basic); d_tableau.increaseSize(); Debug("arith::arithvar") << x << " |-> " << varX << endl; @@ -710,3 +655,71 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) { void TheoryArith::notifyEq(TNode lhs, TNode rhs) { } + +bool TheoryArith::entireStateIsConsistent(){ + typedef std::vector<Node>::const_iterator VarIter; + for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){ + ArithVar var = asArithVar(*i); + if(!d_partialModel.assignmentIsConsistent(var)){ + d_partialModel.printModel(var); + cerr << "Assignment is not consistent for " << var << *i << endl; + return false; + } + } + return true; +} + +void TheoryArith::permanentlyRemoveVariable(ArithVar v){ + //There are 3 cases + // 1) v is non-basic and is contained in a row + // 2) v is basic + // 3) v is non-basic and is not contained in a row + // It appears that this can happen after other variables have been removed! + // Tread carefullty with this one. + + if(!d_basicManager.isMember(v)){ + ArithVar basic = findShortestBasicRow(v); + + if(basic == ARITHVAR_SENTINEL){ + //Case 3) do nothing else. + //TODO think hard about if this is okay... + return; + } + + AlwaysAssert(basic != ARITHVAR_SENTINEL); + d_tableau.pivot(basic, v); + } + + Assert(d_basicManager.isMember(v)); + + d_tableau.ejectBasic(v); + //remove the row from the tableau + //TODO: It would be better to remove the row from the tableau + //and store this row in another data structure + + + Debug("arith::permanentlyRemoveVariable") << v << " died an ignoble death."<< endl; + ++(d_statistics.d_permanentlyRemovedVariables); +} + +void TheoryArith::presolve(){ + TimerStat::CodeTimer codeTimer(d_statistics.d_presolveTime); + + typedef std::vector<Node>::const_iterator VarIter; + for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){ + Node variableNode = *i; + ArithVar var = asArithVar(variableNode); + if(d_userVariables.isMember(var) && !d_propagator.hasAnyAtoms(variableNode)){ + //The user variable is unconstrained. + //Remove this variable permanently + permanentlyRemoveVariable(var); + } + } + + //Assert(entireStateIsConsistent()); //Boy is this paranoid + if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); } + + static int callCount = 0; + Debug("arith::presolve") << "TheoryArith::presolve #" << (callCount++) << endl; + check(FULL_EFFORT); +} 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(); }; diff --git a/src/theory/arith/unate_propagator.cpp b/src/theory/arith/unate_propagator.cpp index 6e442ded9..e042e2320 100644 --- a/src/theory/arith/unate_propagator.cpp +++ b/src/theory/arith/unate_propagator.cpp @@ -47,6 +47,15 @@ bool ArithUnatePropagator::leftIsSetup(TNode left){ return left.hasAttribute(PropagatorEqSet()); } +bool ArithUnatePropagator::hasAnyAtoms(TNode v){ + Assert(!leftIsSetup(v) + || !v.getAttribute(PropagatorEqSet())->empty() + || !v.getAttribute(PropagatorLeqSet())->empty() + || !v.getAttribute(PropagatorGeqSet())->empty()); + + return leftIsSetup(v); +} + void ArithUnatePropagator::setupLefthand(TNode left){ Assert(!leftIsSetup(left)); diff --git a/src/theory/arith/unate_propagator.h b/src/theory/arith/unate_propagator.h index 1aab795cb..ca2135cf3 100644 --- a/src/theory/arith/unate_propagator.h +++ b/src/theory/arith/unate_propagator.h @@ -77,6 +77,9 @@ public: */ void addAtom(TNode atom); + /** Returns true if v has been added as a left hand side in an atom */ + bool hasAnyAtoms(TNode v); + private: /** Sends an implication (=> a b) to the PropEngine via d_arithOut. */ void addImplication(TNode a, TNode b); |