From b1200db566d19132a3f0861eeef35f3c0aaa0a08 Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 29 Jun 2010 22:01:30 +0000 Subject: [PATCH] This commit merges the decaying-rows branch into the main trunk. --- src/theory/arith/Makefile.am | 1 + src/theory/arith/arith_activity.h | 42 +++++++++++++ src/theory/arith/partial_model.cpp | 36 +++++++++++ src/theory/arith/partial_model.h | 11 ++++ src/theory/arith/tableau.h | 97 +++++++++++++++++++++++------- src/theory/arith/theory_arith.cpp | 84 +++++++++++++++++++++++++- src/theory/arith/theory_arith.h | 5 ++ 7 files changed, 253 insertions(+), 23 deletions(-) create mode 100644 src/theory/arith/arith_activity.h diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index 37df73edd..541426ac3 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -11,6 +11,7 @@ libarith_la_SOURCES = \ arith_rewriter.cpp \ arith_utilities.h \ arith_constants.h \ + arith_activity.h \ delta_rational.h \ delta_rational.cpp \ partial_model.h \ diff --git a/src/theory/arith/arith_activity.h b/src/theory/arith/arith_activity.h new file mode 100644 index 000000000..1dc0e900b --- /dev/null +++ b/src/theory/arith/arith_activity.h @@ -0,0 +1,42 @@ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__ARITH__ARITH_ACTIVITY_H +#define __CVC4__THEORY__ARITH__ARITH_ACTIVITY_H + +#include "expr/node.h" +#include "expr/attribute.h" + +namespace CVC4 { +namespace theory { +namespace arith { + + +struct ArithActivityID {}; +typedef expr::Attribute ArithActivity; + +inline void resetActivity(TNode var){ + var.setAttribute(ArithActivity(), 0); +} +inline void initActivity(TNode var){ + resetActivity(var); +} + +inline uint64_t getActivity(TNode var){ + return var.getAttribute(ArithActivity()); +} + +inline void increaseActivity(TNode var, uint64_t x){ + Assert(var.hasAttribute(ArithActivity())); + uint64_t newValue = x + getActivity(var); + var.setAttribute(ArithActivity(), newValue); +} + +const static uint64_t ACTIVITY_THRESHOLD = 100; + +}; /* namesapce arith */ +}; /* namespace theory */ +}; /* namespace CVC4 */ + + +#endif diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index e7e3f8bc2..bd2d5d61e 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -32,6 +32,7 @@ void ArithPartialModel::setUpperBound(TNode x, const DeltaRational& r){ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); Debug("partial_model") << "setUpperBound(" << x << "," << r << ")" << endl; + x.setAttribute(partial_model::HasHadABound(), true); d_UpperBoundMap[x] = r; } @@ -39,6 +40,8 @@ void ArithPartialModel::setUpperBound(TNode x, const DeltaRational& r){ void ArithPartialModel::setLowerBound(TNode x, const DeltaRational& r){ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); Debug("partial_model") << "setLowerBound(" << x << "," << r << ")" << endl; + x.setAttribute(partial_model::HasHadABound(), true); + d_LowerBoundMap[x] = r; } @@ -60,6 +63,33 @@ void ArithPartialModel::setAssignment(TNode x, const DeltaRational& r){ Debug("partial_model") << "pm: updating the assignment to" << x << " now " << r < UpperConstraint; struct TheoryArithPropagatedID {}; typedef expr::CDAttribute TheoryArithPropagated; +struct HasHadABoundID {}; +typedef expr::Attribute HasHadABound; + }; /*namespace partial_model*/ @@ -152,11 +155,14 @@ public: + void setUpperBound(TNode x, const DeltaRational& r); void setLowerBound(TNode x, const DeltaRational& r); /* Sets an unsafe variable assignment */ void setAssignment(TNode x, const DeltaRational& r); + void setAssignment(TNode x, const DeltaRational& safe, const DeltaRational& r); + /** Must know that the bound exists before calling this! */ DeltaRational getUpperBound(TNode x) const; @@ -182,6 +188,11 @@ public: void printModel(TNode x); + bool hasBounds(TNode x); + bool hasEverHadABound(TNode var){ + return var.getAttribute(partial_model::HasHadABound()); + } + private: /** diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 0cadc8d10..4e4088bb0 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -22,6 +22,8 @@ #include "expr/attribute.h" #include "theory/arith/basic.h" +#include "theory/arith/arith_activity.h" + #include #include @@ -170,28 +172,35 @@ public: private: typedef __gnu_cxx::hash_map RowsTable; - VarSet d_basicVars; - RowsTable d_rows; + VarSet d_activeBasicVars; + RowsTable d_activeRows, d_inactiveRows; public: /** * Constructs an empty tableau. */ - Tableau() : d_basicVars(), d_rows() {} + Tableau() : d_activeBasicVars(), d_activeRows(), d_inactiveRows() {} VarSet::iterator begin(){ - return d_basicVars.begin(); + return d_activeBasicVars.begin(); } VarSet::iterator end(){ - return d_basicVars.end(); + return d_activeBasicVars.end(); } Row* lookup(TNode var){ - Assert(contains(var)); - return d_rows[var]; + Assert(isActiveBasicVariable(var)); + return d_activeRows[var]; + } + +private: + Row* lookupEjected(TNode var){ + Assert(isEjected(var)); + return d_inactiveRows[var]; } +public: void addRow(TNode eq){ Assert(eq.getKind() == kind::EQUAL); @@ -203,10 +212,10 @@ public: Assert(var.getAttribute(IsBasic())); //The new basic variable cannot already be a basic variable - Assert(d_basicVars.find(var) == d_basicVars.end()); - d_basicVars.insert(var); + Assert(!isActiveBasicVariable(var)); + d_activeBasicVars.insert(var); Row* row_var = new Row(var,sum); - d_rows[var] = row_var; + d_activeRows[var] = row_var; //A variable in the row may have been made non-basic already. //If this is the case we fake pivoting this variable @@ -217,7 +226,7 @@ public: Assert(child[0].getKind() == kind::CONST_RATIONAL); TNode c = child[1]; Assert(var.getMetaKind() == kind::metakind::VARIABLE); - if(contains(c)){ + if(isActiveBasicVariable(c)){ Row* row_c = lookup(c); row_var->subsitute(*row_c); } @@ -231,42 +240,88 @@ public: * a_rs != 0. */ void pivot(TNode x_r, TNode x_s){ - RowsTable::iterator ptrRow_r = d_rows.find(x_r); - Assert(ptrRow_r != d_rows.end()); + RowsTable::iterator ptrRow_r = d_activeRows.find(x_r); + Assert(ptrRow_r != d_activeRows.end()); Row* row_s = (*ptrRow_r).second; Assert(row_s->has(x_s)); row_s->pivot(x_s); - d_rows.erase(ptrRow_r); - d_basicVars.erase(x_r); + d_activeRows.erase(ptrRow_r); + d_activeBasicVars.erase(x_r); makeNonbasic(x_r); - d_rows.insert(std::make_pair(x_s,row_s)); - d_basicVars.insert(x_s); + d_activeRows.insert(std::make_pair(x_s,row_s)); + d_activeBasicVars.insert(x_s); makeBasic(x_s); - for(VarSet::iterator basicIter = begin(); basicIter != end(); ++basicIter){ + for(VarSet::iterator basicIter = begin(), endIter = end(); + basicIter != endIter; ++basicIter){ TNode basic = *basicIter; Row* row_k = lookup(basic); if(row_k->basicVar() != x_s){ if(row_k->has(x_s)){ + increaseActivity(basic, 30); + row_k->subsitute(*row_s); } } } } void printTableau(){ - for(VarSet::iterator basicIter = begin(); basicIter != end(); ++basicIter){ + for(VarSet::iterator basicIter = begin(), endIter = end(); + basicIter != endIter; ++basicIter){ TNode basic = *basicIter; Row* row_k = lookup(basic); row_k->printRow(); } } + + bool isEjected(TNode var){ + return d_inactiveRows.find(var) != d_inactiveRows.end(); + } + + void ejectBasic(TNode basic){ + Assert(isActiveBasicVariable(basic)); + + Row* row = lookup(basic); + d_activeRows.erase(basic); + d_activeBasicVars.erase(basic); + + d_inactiveRows.insert(make_pair(basic, row)); + } + + void reinjectBasic(TNode basic){ + Assert(isEjected(basic)); + + Row* row = lookupEjected(basic); + + d_inactiveRows.erase(basic); + d_activeBasicVars.insert(basic); + d_activeRows.insert(make_pair(basic, row)); + + updateRow(row); + } private: - inline bool contains(TNode var){ - return d_basicVars.find(var) != d_basicVars.end(); + inline bool isActiveBasicVariable(TNode var){ + return d_activeBasicVars.find(var) != d_activeBasicVars.end(); + } + + void updateRow(Row* row){ + for(Row::iterator i=row->begin(), endIter = row->end(); i != endIter; ){ + TNode var = *i; + ++i; + if(isBasic(var)){ + Row* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var); + + Assert(row_var != row); + row->subsitute(*row_var); + + i = row->begin(); + endIter = row->end(); + } + } } }; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index bd35e0797..26d554356 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -26,12 +26,12 @@ #include "util/integer.h" #include "theory/arith/arith_utilities.h" -#include "theory/arith/theory_arith.h" #include "theory/arith/delta_rational.h" #include "theory/arith/partial_model.h" #include "theory/arith/tableau.h" #include "theory/arith/slack.h" #include "theory/arith/basic.h" +#include "theory/arith/arith_activity.h" #include "theory/arith/arith_rewriter.h" #include "theory/arith/arith_propagator.h" @@ -126,6 +126,58 @@ bool isNormalAtom(TNode n){ } } + + +bool TheoryArith::shouldEject(TNode var){ + if(d_partialModel.hasBounds(var)){ + return false; + }else if(d_tableau.isEjected(var)) { + return false; + }else if(!d_partialModel.hasEverHadABound(var)){ + return true; + }else if(getActivity(var) >= ACTIVITY_THRESHOLD){ + return true; + } + return false; +} + +TNode TheoryArith::findBasicRow(TNode variable){ + for(Tableau::VarSet::iterator basicIter = d_tableau.begin(); + basicIter != d_tableau.end(); + ++basicIter){ + TNode x_j = *basicIter; + Row* row_j = d_tableau.lookup(x_j); + + if(row_j->has(variable)){ + return x_j; + } + } + return TNode::null(); +} + +void TheoryArith::ejectInactiveVariables(){ + Debug("decay") << "begin ejectInactiveVariables()" << endl; + for(std::vector::iterator i = d_variables.begin(), + end = d_variables.end(); i != end; ++i){ + TNode variable = *i; + if(shouldEject(variable)){ + if(isBasic(variable)){ + Debug("decay") << "ejecting basic " << variable << endl;; + d_tableau.ejectBasic(variable); + } + } + } +} + +void TheoryArith::reinjectVariable(TNode x){ + d_tableau.reinjectBasic(x); + + + DeltaRational safeAssignment = computeRowValueUsingSavedAssignment(x); + DeltaRational assignment = computeRowValueUsingAssignment(x); + d_partialModel.setAssignment(x,safeAssignment,assignment); +} + void TheoryArith::preRegisterTerm(TNode n) { Debug("arith_preregister") <<"begin arith::preRegisterTerm("<< n <<")"<< endl; Kind k = n.getKind(); @@ -201,6 +253,8 @@ void TheoryArith::setupVariable(TNode x){ Assert(x.getMetaKind() == kind::metakind::VARIABLE); d_variables.push_back(Node(x)); + initActivity(x); + if(!isBasic(x)){ d_partialModel.initialize(x,d_constants.d_ZERO_DELTA); }else{ @@ -282,7 +336,9 @@ bool TheoryArith::AssertUpper(TNode n, TNode original){ Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl; - + if(isBasic(x_i) && d_tableau.isEjected(x_i)){ + reinjectVariable(x_i); + } if(d_partialModel.aboveUpperBound(x_i, c_i, false) ){ // \upperbound(x_i) <= c_i return false; //sat @@ -299,6 +355,8 @@ bool TheoryArith::AssertUpper(TNode n, TNode original){ d_partialModel.setUpperConstraint(x_i,original); d_partialModel.setUpperBound(x_i, c_i); + resetActivity(x_i); + if(!isBasic(x_i)){ if(d_partialModel.getAssignment(x_i) > c_i){ update(x_i, c_i); @@ -318,6 +376,10 @@ bool TheoryArith::AssertLower(TNode n, TNode original){ Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl; + if(isBasic(x_i) && d_tableau.isEjected(x_i)){ + reinjectVariable(x_i); + } + if(d_partialModel.belowLowerBound(x_i, c_i, false)){ return false; //sat } @@ -332,6 +394,7 @@ bool TheoryArith::AssertLower(TNode n, TNode original){ d_partialModel.setLowerConstraint(x_i,original); d_partialModel.setLowerBound(x_i, c_i); + resetActivity(x_i); if(!isBasic(x_i)){ if(d_partialModel.getAssignment(x_i) < c_i){ @@ -352,6 +415,9 @@ bool TheoryArith::AssertEquality(TNode n, TNode original){ Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl; + if(isBasic(x_i) && d_tableau.isEjected(x_i)){ + reinjectVariable(x_i); + } // u_i <= c_i <= l_i // This can happen if both c_i <= x_i and x_i <= c_i are in the system. @@ -381,6 +447,7 @@ bool TheoryArith::AssertEquality(TNode n, TNode original){ d_partialModel.setUpperConstraint(x_i,original); d_partialModel.setUpperBound(x_i, c_i); + resetActivity(x_i); if(!isBasic(x_i)){ if(!(d_partialModel.getAssignment(x_i) == c_i)){ @@ -413,6 +480,9 @@ void TheoryArith::update(TNode x_i, DeltaRational& v){ const DeltaRational& assignment = d_partialModel.getAssignment(x_j); DeltaRational nAssignment = assignment+(diff * a_ji); d_partialModel.setAssignment(x_j, nAssignment); + + increaseActivity(x_j, 1); + checkBasicVariable(x_j); } } @@ -452,6 +522,9 @@ void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){ const Rational& a_kj = row_k->lookup(x_j); DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj); d_partialModel.setAssignment(x_k, nextAssignment); + + increaseActivity(x_j, 1); + checkBasicVariable(x_k); } } @@ -527,6 +600,8 @@ TNode TheoryArith::selectSlack(TNode x_i){ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06 Debug("arith") << "updateInconsistentVars" << endl; + static int iteratationNum = 0; + static const int EJECT_FREQUENCY = 10; while(true){ if(debugTagIsOn("paranoid:check_tableau")){ checkTableau(); } @@ -536,6 +611,11 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06 Debug("arith_update") << "No inconsistent variables" << endl; return Node::null(); //sat } + + ++iteratationNum; + if(iteratationNum % EJECT_FREQUENCY == 0) + ejectInactiveVariables(); + DeltaRational beta_i = d_partialModel.getAssignment(x_i); if(d_partialModel.belowLowerBound(x_i, beta_i, true)){ diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index c76923bee..ba9b5329d 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -232,6 +232,10 @@ private: */ bool assertionCases(TNode original, TNode assertion); + TNode findBasicRow(TNode variable); + bool shouldEject(TNode var); + void ejectInactiveVariables(); + void reinjectVariable(TNode x); //TODO get rid of this! Node simulatePreprocessing(TNode n); @@ -249,6 +253,7 @@ private: Statistics d_statistics; + }; }/* CVC4::theory::arith namespace */ -- 2.30.2