From: Tim King Date: Thu, 3 Mar 2011 16:34:48 +0000 (+0000) Subject: Merged the tableau-copy branch into trunk. This adds a copy constructor and operator... X-Git-Tag: cvc5-1.0.0~8675 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3c8309cbf3f6549d9cc54fe45ccb5bb32a106d8e;p=cvc5.git Merged the tableau-copy branch into trunk. This adds a copy constructor and operator=(...) to Tableau. --- diff --git a/src/theory/arith/arithvar_set.h b/src/theory/arith/arithvar_set.h index ff75b373a..08bc905e0 100644 --- a/src/theory/arith/arithvar_set.h +++ b/src/theory/arith/arithvar_set.h @@ -63,6 +63,11 @@ public: return d_posVector.size(); } + void clear(){ + d_list.clear(); + d_posVector.clear(); + } + void increaseSize(ArithVar max){ Assert(max >= allocated()); d_posVector.resize(max+1, ARITHVAR_SENTINEL); diff --git a/src/theory/arith/row_vector.cpp b/src/theory/arith/row_vector.cpp index 090938f28..9159d3d6f 100644 --- a/src/theory/arith/row_vector.cpp +++ b/src/theory/arith/row_vector.cpp @@ -304,3 +304,13 @@ Node ReducedRowVector::asEquality(const ArithVarToNodeMap& map) const{ */ } +void ReducedRowVector::enqueueNonBasicVariablesAndCoefficients(std::vector< ArithVar >& variables,std::vector< Rational >& coefficients) const{ + for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){ + ArithVar var = (*i).getArithVar(); + const Rational& q = (*i).getCoefficient(); + if(var != basic()){ + variables.push_back(var); + coefficients.push_back(q); + } + } +} diff --git a/src/theory/arith/row_vector.h b/src/theory/arith/row_vector.h index 0fdfd7f0c..45412ad3e 100644 --- a/src/theory/arith/row_vector.h +++ b/src/theory/arith/row_vector.h @@ -86,9 +86,11 @@ public: const std::vector< Rational >& coefficients, std::vector& count, std::vector& columnMatrix); - ~ReducedRowVector(); + void enqueueNonBasicVariablesAndCoefficients(std::vector< ArithVar >& variables, + std::vector< Rational >& coefficients) const; + /** Returns the basic variable.*/ ArithVar basic() const{ Assert(basicIsSet()); diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index a85765303..9769c628d 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -20,18 +20,81 @@ #include "theory/arith/tableau.h" +using namespace std; using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::arith; -using namespace std; + +Tableau::Tableau(const Tableau& tab){ + internalCopy(tab); +} + +void Tableau::internalCopy(const Tableau& tab){ + uint32_t N = tab.d_rowsTable.size(); + + Debug("tableau::copy") << "tableau copy "<< N << endl; + + if(N > 1){ + d_columnMatrix.insert(d_columnMatrix.end(), N, ArithVarSet()); + d_rowsTable.insert(d_rowsTable.end(), N, NULL); + d_basicVariables.increaseSize(N-1); + + Assert(d_basicVariables.allocated() == tab.d_basicVariables.allocated()); + + d_rowCount.insert(d_rowCount.end(), N, 0); + } + + ColumnMatrix::iterator i_colIter = d_columnMatrix.begin(); + ColumnMatrix::iterator end_colIter = d_columnMatrix.end(); + for(; i_colIter != end_colIter; ++i_colIter){ + Column& col = *i_colIter; + col.increaseSize(d_columnMatrix.size()); + } + + ArithVarSet::iterator i_basicIter = tab.d_basicVariables.begin(); + ArithVarSet::iterator i_basicEnd = tab.d_basicVariables.end(); + for(; i_basicIter != i_basicEnd; ++i_basicIter){ + ArithVar basicVar = *i_basicIter; + const ReducedRowVector* otherRow = tab.d_rowsTable[basicVar]; + + Assert(otherRow != NULL); + + std::vector< ArithVar > variables; + std::vector< Rational > coefficients; + otherRow->enqueueNonBasicVariablesAndCoefficients(variables, coefficients); + + ReducedRowVector* copy = new ReducedRowVector(basicVar, variables, coefficients, d_rowCount, d_columnMatrix); + + Debug("tableau::copy") << "copying " << basicVar << endl; + copy->printRow(); + + d_basicVariables.add(basicVar); + d_rowsTable[basicVar] = copy; + } +} + +Tableau& Tableau::operator=(const Tableau& other){ + clear(); + internalCopy(other); + return (*this); +} Tableau::~Tableau(){ + clear(); +} + +void Tableau::clear(){ while(!d_basicVariables.empty()){ ArithVar curr = *(d_basicVariables.begin()); ReducedRowVector* vec = removeRow(curr); delete vec; } + + d_rowsTable.clear(); + d_basicVariables.clear(); + d_rowCount.clear(); + d_columnMatrix.clear(); } void Tableau::addRow(ArithVar basicVar, diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 27aa1305c..6fe245285 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -63,8 +63,13 @@ public: d_rowCount(), d_columnMatrix() {} + + /** Copy constructor. */ + Tableau(const Tableau& tab); ~Tableau(); + Tableau& operator=(const Tableau& tab); + size_t getNumRows() const { return d_basicVariables.size(); } @@ -116,7 +121,6 @@ public: return *(d_rowsTable[var]); } -public: uint32_t getRowCount(ArithVar x){ Assert(x < d_rowCount.size()); AlwaysAssert(d_rowCount[x] == getColumn(x).size()); @@ -150,6 +154,14 @@ public: void printTableau(); ReducedRowVector* removeRow(ArithVar basic); + + +private: + /** Copies the datastructures in tab to this.*/ + void internalCopy(const Tableau& tab); + + /** Clears the structures in the tableau. */ + void clear(); }; }; /* namespace arith */ diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 2100e0b38..3899e5e80 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -652,6 +652,10 @@ void TheoryArith::notifyEq(TNode lhs, TNode rhs) { } +void TheoryArith::notifyRestart(){ + if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); } +} + bool TheoryArith::entireStateIsConsistent(){ typedef std::vector::const_iterator VarIter; for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){ @@ -727,5 +731,6 @@ void TheoryArith::presolve(){ 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 dc841170b..fb39eac09 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -71,15 +71,6 @@ private: */ std::map 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 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"); }