From 005066130a774c9e4aa838ca500d5fd3137909be Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 18 Feb 2011 23:28:19 +0000 Subject: [PATCH] Changes: - ArithVar is no longer an attribute - RowVector's destructor reduces the row count of its variables upon. - Tableau's destructor now free its rows instead of leaking memory. - Added ability to convert ReducedRowVectors into equivalent Nodes. - getValue() should work again. --- src/theory/arith/arith_utilities.h | 20 +++---------- src/theory/arith/arithvar_set.h | 3 ++ src/theory/arith/row_vector.cpp | 48 ++++++++++++++++++++++++++++-- src/theory/arith/row_vector.h | 8 +++++ src/theory/arith/tableau.cpp | 8 +++++ src/theory/arith/tableau.h | 1 + src/theory/arith/theory_arith.cpp | 42 ++++++++++++++++++-------- src/theory/arith/theory_arith.h | 35 +++++++++++++++++++++- 8 files changed, 133 insertions(+), 32 deletions(-) diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 6a9102a19..2053379d9 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -28,6 +28,7 @@ #include #include #include +#include namespace CVC4 { namespace theory { @@ -38,23 +39,10 @@ typedef uint32_t ArithVar; //static const ArithVar ARITHVAR_SENTINEL = std::numeric_limits::max(); #define ARITHVAR_SENTINEL std::numeric_limits::max() -struct ArithVarAttrID{}; -typedef expr::Attribute ArithVarAttr; +//Maps from Nodes -> ArithVars, and vice versa +typedef __gnu_cxx::hash_map NodeToArithVarMap; +typedef __gnu_cxx::hash_map ArithVarToNodeMap; -inline bool hasArithVar(TNode x){ - return x.hasAttribute(ArithVarAttr()); -} - -inline ArithVar asArithVar(TNode x){ - Assert(hasArithVar(x)); - Assert(x.getAttribute(ArithVarAttr()) <= ARITHVAR_SENTINEL); - return x.getAttribute(ArithVarAttr()); -} - -inline void setArithVar(TNode x, ArithVar a){ - Assert(!hasArithVar(x)); - return x.setAttribute(ArithVarAttr(), (uint64_t)a); -} inline Node mkRationalNode(const Rational& q){ return NodeManager::currentNM()->mkConst(q); diff --git a/src/theory/arith/arithvar_set.h b/src/theory/arith/arithvar_set.h index 95617c5a0..de215696e 100644 --- a/src/theory/arith/arithvar_set.h +++ b/src/theory/arith/arithvar_set.h @@ -54,6 +54,9 @@ public: size_t size() const { return d_list.size(); } + bool empty() const { + return d_list.empty(); + } size_t allocated() const { return d_posVector.size(); diff --git a/src/theory/arith/row_vector.cpp b/src/theory/arith/row_vector.cpp index 6486077fb..07fc0186d 100644 --- a/src/theory/arith/row_vector.cpp +++ b/src/theory/arith/row_vector.cpp @@ -21,6 +21,16 @@ bool RowVector::isSorted(const VarCoeffArray& arr, bool strictlySorted) { return true; } +RowVector::~RowVector(){ + NonZeroIterator curr = beginNonZero(); + NonZeroIterator end = endNonZero(); + for(;curr != end; ++curr){ + ArithVar v = getArithVar(*curr); + Assert(d_rowCount[v] >= 1); + --(d_rowCount[v]); + } +} + bool RowVector::noZeroCoefficients(const VarCoeffArray& arr){ for(NonZeroIterator curr = arr.begin(), end = arr.end(); curr != end; ++curr){ @@ -149,9 +159,9 @@ void RowVector::addRowTimesConstant(const Rational& c, const RowVector& other){ void RowVector::printRow(){ for(NonZeroIterator i = beginNonZero(); i != endNonZero(); ++i){ ArithVar nb = getArithVar(*i); - Debug("tableau") << "{" << nb << "," << getCoefficient(*i) << "}"; + Debug("row::print") << "{" << nb << "," << getCoefficient(*i) << "}"; } - Debug("tableau") << std::endl; + Debug("row::print") << std::endl; } ReducedRowVector::ReducedRowVector(ArithVar basic, @@ -193,3 +203,37 @@ void ReducedRowVector::pivot(ArithVar x_j){ Assert(wellFormed()); } + + +Node ReducedRowVector::asEquality(const ArithVarToNodeMap& map) const{ + using namespace CVC4::kind; + + Assert(size() >= 2); + Node sum = Node::null(); + if(size() > 2){ + NodeBuilder<> sumBuilder(PLUS); + + for(NonZeroIterator i = beginNonZero(); i != endNonZero(); ++i){ + ArithVar nb = getArithVar(*i); + if(nb == basic()) continue; + Node var = (map.find(nb))->second; + Node coeff = mkRationalNode(getCoefficient(*i)); + + Node mult = NodeBuilder<2>(MULT) << coeff << var; + sumBuilder << mult; + } + sum = sumBuilder; + }else{ + Assert(size() == 2); + NonZeroIterator i = beginNonZero(); + if(getArithVar(*i) == basic()){ + ++i; + } + Assert(getArithVar(*i) != basic()); + Node var = (map.find(getArithVar(*i)))->second; + Node coeff = mkRationalNode(getCoefficient(*i)); + sum = NodeBuilder<2>(MULT) << coeff << var; + } + Node basicVar = (map.find(basic()))->second; + return NodeBuilder<2>(EQUAL) << basicVar << sum; +} diff --git a/src/theory/arith/row_vector.h b/src/theory/arith/row_vector.h index 05ceeb986..2b48564a4 100644 --- a/src/theory/arith/row_vector.h +++ b/src/theory/arith/row_vector.h @@ -89,6 +89,7 @@ public: const std::vector< Rational >& coefficients, std::vector& counts); + ~RowVector(); /** Returns the number of nonzero variables in the vector. */ uint32_t size() const { @@ -195,6 +196,13 @@ public: void pivot(ArithVar x_j); void substitute(const ReducedRowVector& other); + + /** + * Returns the reduced row as an equality with + * the basic variable on the lhs equal to the sum of the non-basics variables. + * The mapped from ArithVars to Nodes is specificied by map. + */ + Node asEquality(const ArithVarToNodeMap& map) const; }; /* class ReducedRowVector */ diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index 5f142fe8a..5ba173eb6 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -24,6 +24,14 @@ using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::arith; +Tableau::~Tableau(){ + while(!d_activeBasicVars.empty()){ + ArithVar curr = *(d_activeBasicVars.begin()); + ReducedRowVector* vec = removeRow(curr); + delete vec; + } +} + void Tableau::addRow(ArithVar basicVar, const std::vector& coeffs, const std::vector& variables){ diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index bd30dc13e..433f6472f 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -58,6 +58,7 @@ public: d_rowsTable(), d_basicManager(bm) {} + ~Tableau(); void increaseSize(){ d_activeBasicVars.increaseSize(); diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index dbfa86a98..9fbec23ac 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -575,6 +575,13 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) { case kind::VARIABLE: { ArithVar var = asArithVar(n); + if(d_removedRows.find(var) != d_removedRows.end()){ + Node eq = d_removedRows.find(var)->second; + Assert(n == eq[0]); + Node rhs = eq[1]; + return getValue(rhs, engine); + } + DeltaRational drat = d_partialModel.getAssignment(var); const Rational& delta = d_partialModel.getDelta(); Debug("getValue") << n << " " << drat << " " << delta << endl; @@ -667,28 +674,37 @@ void TheoryArith::permanentlyRemoveVariable(ArithVar v){ // It appears that this can happen after other variables have been removed! // Tread carefullty with this one. + bool noRow = false; + 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... - //Probably wrecks havoc with model generation - //*feh* DO IT ANYWAYS! - return; + noRow = true; + }else{ + Assert(basic != ARITHVAR_SENTINEL); + d_tableau.pivot(basic, v); } - - AlwaysAssert(basic != ARITHVAR_SENTINEL); - d_tableau.pivot(basic, v); } - Assert(d_basicManager.isMember(v)); + if(d_basicManager.isMember(v)){ + Assert(!noRow); + Assert(d_basicManager.isMember(v)); + + //remove the row from the tableau + ReducedRowVector* row = d_tableau.removeRow(v); + Node eq = row->asEquality(d_arithVarToNodeMap); - //remove the row from the tableau - ReducedRowVector* row = d_tableau.removeRow(v); - d_removedRows[v] = row; + if(Debug.isOn("row::print")) row->printRow(); + Debug("arith::permanentlyRemoveVariable") << eq << endl; + delete row; + + Assert(d_removedRows.find(v) == d_removedRows.end()); + d_removedRows[v] = eq; + } - Debug("arith::permanentlyRemoveVariable") << v << " died an ignoble death."<< endl; + Debug("arith::permanentlyRemoveVariable") << "Permanently removed variable " + << v << ":" << asNode(v) << endl; ++(d_statistics.d_permanentlyRemovedVariables); } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index fd3cf0c45..efd1adde4 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -64,7 +64,12 @@ private: std::vector d_variables; - std::map d_removedRows; + /** + * If ArithVar v maps to the node n in d_removednode, + * then n = (= asNode(v) rhs) where rhs is a term that + * can be used to determine the value of n uysing getValue(). + */ + std::map d_removedRows; /** * Priority Queue of the basic variables that may be inconsistent. @@ -87,6 +92,34 @@ private: ArithVarSet d_basicManager; ArithVarSet d_userVariables; + /** + * Bidirectional map between Nodes and ArithVars. + */ + NodeToArithVarMap d_nodeToArithVarMap; + ArithVarToNodeMap d_arithVarToNodeMap; + + inline bool hasArithVar(TNode x) const { + return d_nodeToArithVarMap.find(x) != d_nodeToArithVarMap.end(); + //return x.hasAttribute(ArithVarAttr()); + } + + inline ArithVar asArithVar(TNode x) const{ + Assert(hasArithVar(x)); + Assert((d_nodeToArithVarMap.find(x))->second <= ARITHVAR_SENTINEL); + return (d_nodeToArithVarMap.find(x))->second; + } + inline Node asNode(ArithVar a) const{ + Assert(d_arithVarToNodeMap.find(a) != d_arithVarToNodeMap.end()); + return (d_arithVarToNodeMap.find(a))->second; + } + + inline void setArithVar(TNode x, ArithVar a){ + Assert(!hasArithVar(x)); + Assert(d_arithVarToNodeMap.find(a) == d_arithVarToNodeMap.end()); + d_arithVarToNodeMap[a] = x; + d_nodeToArithVarMap[x] = a; + } + /** * List of all of the inequalities asserted in the current context. */ -- 2.30.2