From: Tim King Date: Sat, 19 Feb 2011 00:22:34 +0000 (+0000) Subject: Changes: X-Git-Tag: cvc5-1.0.0~8699 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0db4ec99a2f289b66878d0ca3be9d43492eff3ad;p=cvc5.git Changes: - The Tableau is now in charge of managing what variables are basic in a unified manner. Specifically, TheoryArith::d_basicManager was merged into Tableau::d_basicVariables. --- diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 4d417659e..0f4f27a76 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -72,7 +72,7 @@ bool SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_ d_partialModel.setLowerConstraint(x_i,original); d_partialModel.setLowerBound(x_i, c_i); - if(!d_basicManager.isMember(x_i)){ + if(!d_tableau.isBasic(x_i)){ if(d_partialModel.getAssignment(x_i) < c_i){ update(x_i, c_i); } @@ -103,7 +103,7 @@ bool SimplexDecisionProcedure::AssertUpper(ArithVar x_i, const DeltaRational& c_ d_partialModel.setUpperConstraint(x_i,original); d_partialModel.setUpperBound(x_i, c_i); - if(!d_basicManager.isMember(x_i)){ + if(!d_tableau.isBasic(x_i)){ if(d_partialModel.getAssignment(x_i) > c_i){ update(x_i, c_i); } @@ -149,7 +149,7 @@ bool SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational& d_partialModel.setUpperConstraint(x_i,original); d_partialModel.setUpperBound(x_i, c_i); - if(!d_basicManager.isMember(x_i)){ + if(!d_tableau.isBasic(x_i)){ if(!(d_partialModel.getAssignment(x_i) == c_i)){ update(x_i, c_i); } @@ -161,7 +161,7 @@ bool SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational& } void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){ - Assert(!d_basicManager.isMember(x_i)); + Assert(!d_tableau.isBasic(x_i)); DeltaRational assignment_x_i = d_partialModel.getAssignment(x_i); ++(d_statistics.d_statUpdates); @@ -294,7 +294,7 @@ ArithVar SimplexDecisionProcedure::selectSmallestInconsistentVar(){ while(!d_griggioRuleQueue.empty()){ ArithVar var = d_griggioRuleQueue.top().first; Debug("arith_update") << "possiblyInconsistentGriggio var" << var << endl; - if(d_basicManager.isMember(var)){ + if(d_tableau.isBasic(var)){ if(!d_partialModel.assignmentIsConsistent(var)){ return var; } @@ -305,7 +305,7 @@ ArithVar SimplexDecisionProcedure::selectSmallestInconsistentVar(){ while(!d_possiblyInconsistent.empty()){ ArithVar var = d_possiblyInconsistent.top(); Debug("arith_update") << "possiblyInconsistent var" << var << endl; - if(d_basicManager.isMember(var)){ + if(d_tableau.isBasic(var)){ if(!d_partialModel.assignmentIsConsistent(var)){ return var; } @@ -392,7 +392,7 @@ Node SimplexDecisionProcedure::selectInitialConflict() { while( !d_griggioRuleQueue.empty()){ ArithVar var = d_griggioRuleQueue.top().first; - if(d_basicManager.isMember(var)){ + if(d_tableau.isBasic(var)){ if(!d_partialModel.assignmentIsConsistent(var)){ init.push_back( d_griggioRuleQueue.top()); } @@ -451,7 +451,7 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){ Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){ - Assert(d_basicManager.isMember(basic)); + Assert(d_tableau.isBasic(basic)); const DeltaRational& beta = d_partialModel.getAssignment(basic); if(d_partialModel.belowLowerBound(basic, beta, true)){ @@ -520,7 +520,7 @@ Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){ if(d_pivotStage && iteratationNum >= d_numVariables){ while(!d_griggioRuleQueue.empty()){ ArithVar var = d_griggioRuleQueue.top().first; - if(d_basicManager.isMember(var)){ + if(d_tableau.isBasic(var)){ d_possiblyInconsistent.push(var); } d_griggioRuleQueue.pop(); @@ -623,7 +623,7 @@ Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){ * Computes the value of a basic variable using the current assignment. */ DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe){ - Assert(d_basicManager.isMember(x)); + Assert(d_tableau.isBasic(x)); DeltaRational sum = d_constants.d_ZERO_DELTA; ReducedRowVector& row = d_tableau.lookup(x); @@ -641,7 +641,7 @@ DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe void SimplexDecisionProcedure::checkBasicVariable(ArithVar basic){ - Assert(d_basicManager.isMember(basic)); + Assert(d_tableau.isBasic(basic)); if(!d_partialModel.assignmentIsConsistent(basic)){ if(d_pivotStage){ const DeltaRational& beta = d_partialModel.getAssignment(basic); diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index abd5cb5e6..84d7cdcbb 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -55,8 +55,6 @@ private: */ ArithPartialModel& d_partialModel; - ArithVarSet& d_basicManager; - OutputChannel* d_out; Tableau& d_tableau; @@ -68,13 +66,11 @@ private: public: SimplexDecisionProcedure(const ArithConstants& constants, ArithPartialModel& pm, - ArithVarSet& bm, OutputChannel* out, Tableau& tableau) : d_possiblyInconsistent(), d_constants(constants), d_partialModel(pm), - d_basicManager(bm), d_out(out), d_tableau(tableau), d_numVariables(0), diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index 5ba173eb6..d318a70e6 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -25,8 +25,8 @@ using namespace CVC4::theory; using namespace CVC4::theory::arith; Tableau::~Tableau(){ - while(!d_activeBasicVars.empty()){ - ArithVar curr = *(d_activeBasicVars.begin()); + while(!d_basicVariables.empty()){ + ArithVar curr = *(d_basicVariables.begin()); ReducedRowVector* vec = removeRow(curr); delete vec; } @@ -37,11 +37,10 @@ void Tableau::addRow(ArithVar basicVar, const std::vector& variables){ Assert(coeffs.size() == variables.size()); - Assert(d_basicManager.isMember(basicVar)); //The new basic variable cannot already be a basic variable - Assert(!d_activeBasicVars.isMember(basicVar)); - d_activeBasicVars.add(basicVar); + Assert(!d_basicVariables.isMember(basicVar)); + d_basicVariables.add(basicVar); ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs,d_rowCount); d_rowsTable[basicVar] = row_current; @@ -53,9 +52,7 @@ void Tableau::addRow(ArithVar basicVar, for( ; varsIter != varsEnd; ++varsIter){ ArithVar var = *varsIter; - if(d_basicManager.isMember(var)){ - Assert(d_activeBasicVars.isMember(var)); - + if(d_basicVariables.isMember(var)){ ReducedRowVector& row_var = lookup(var); row_current->substitute(row_var); } @@ -63,20 +60,19 @@ void Tableau::addRow(ArithVar basicVar, } ReducedRowVector* Tableau::removeRow(ArithVar basic){ - Assert(d_basicManager.isMember(basic)); - Assert(d_activeBasicVars.isMember(basic)); + Assert(d_basicVariables.isMember(basic)); ReducedRowVector* row = d_rowsTable[basic]; - d_activeBasicVars.remove(basic); + d_basicVariables.remove(basic); d_rowsTable[basic] = NULL; return row; } void Tableau::pivot(ArithVar x_r, ArithVar x_s){ - Assert(d_basicManager.isMember(x_r)); - Assert(!d_basicManager.isMember(x_s)); + Assert(d_basicVariables.isMember(x_r)); + Assert(!d_basicVariables.isMember(x_s)); Debug("tableau") << "Tableau::pivot(" << x_r <<", " <pivot(x_s); diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 433f6472f..32c2986e3 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -42,10 +42,9 @@ private: typedef std::vector< ReducedRowVector* > RowsTable; - ArithVarSet d_activeBasicVars; RowsTable d_rowsTable; - ArithVarSet& d_basicManager; + ArithVarSet d_basicVariables; std::vector d_rowCount; @@ -53,29 +52,33 @@ public: /** * Constructs an empty tableau. */ - Tableau(ArithVarSet& bm) : - d_activeBasicVars(), + Tableau() : d_rowsTable(), - d_basicManager(bm) + d_basicVariables(), + d_rowCount() {} ~Tableau(); void increaseSize(){ - d_activeBasicVars.increaseSize(); + d_basicVariables.increaseSize(); d_rowsTable.push_back(NULL); d_rowCount.push_back(0); } + bool isBasic(ArithVar v) const { + return d_basicVariables.isMember(v); + } + ArithVarSet::iterator begin(){ - return d_activeBasicVars.begin(); + return d_basicVariables.begin(); } ArithVarSet::iterator end(){ - return d_activeBasicVars.end(); + return d_basicVariables.end(); } ReducedRowVector& lookup(ArithVar var){ - Assert(d_activeBasicVars.isMember(var)); + Assert(d_basicVariables.isMember(var)); Assert(d_rowsTable[var] != NULL); return *(d_rowsTable[var]); } diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 9fbec23ac..4e84c85db 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -57,12 +57,11 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) : Theory(THEORY_ARITH, c, out), d_constants(NodeManager::currentNM()), d_partialModel(c), - d_basicManager(), d_userVariables(), d_diseq(c), - d_tableau(d_basicManager), + d_tableau(), d_propagator(c, out), - d_simplex(d_constants, d_partialModel, d_basicManager, d_out, d_tableau), + d_simplex(d_constants, d_partialModel, d_out, d_tableau), d_statistics() {} @@ -261,7 +260,7 @@ ArithVar TheoryArith::requestArithVar(TNode x, bool basic){ setArithVar(x,varX); - d_basicManager.init(varX,basic); + //d_basicManager.init(varX,basic); d_userVariables.init(varX, !basic); d_tableau.increaseSize(); @@ -316,7 +315,7 @@ void TheoryArith::setupSlack(TNode left){ */ void TheoryArith::setupInitialValue(ArithVar x){ - if(!d_basicManager.isMember(x)){ + if(!d_tableau.isBasic(x)){ d_partialModel.initialize(x,d_constants.d_ZERO_DELTA); }else{ //If the variable is basic, assertions may have already happened and updates @@ -542,7 +541,7 @@ void TheoryArith::check(Effort effortLevel){ for (ArithVar i = 0; i < d_variables.size(); ++ i) { Debug("arith::print_model") << d_variables[i] << " : " << d_partialModel.getAssignment(i); - if(d_basicManager.isMember(i)) + if(d_tableau.isBasic(i)) Debug("arith::print_model") << " (basic)"; Debug("arith::print_model") << endl; } @@ -676,7 +675,7 @@ void TheoryArith::permanentlyRemoveVariable(ArithVar v){ bool noRow = false; - if(!d_basicManager.isMember(v)){ + if(!d_tableau.isBasic(v)){ ArithVar basic = findShortestBasicRow(v); if(basic == ARITHVAR_SENTINEL){ @@ -687,9 +686,8 @@ void TheoryArith::permanentlyRemoveVariable(ArithVar v){ } } - if(d_basicManager.isMember(v)){ + if(d_tableau.isBasic(v)){ Assert(!noRow); - Assert(d_basicManager.isMember(v)); //remove the row from the tableau ReducedRowVector* row = d_tableau.removeRow(v); diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index efd1adde4..60d24708c 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -89,7 +89,9 @@ private: */ ArithPartialModel d_partialModel; - ArithVarSet d_basicManager; + /** + * Set of ArithVars that were introduced via preregisteration. + */ ArithVarSet d_userVariables; /** @@ -100,7 +102,6 @@ private: inline bool hasArithVar(TNode x) const { return d_nodeToArithVarMap.find(x) != d_nodeToArithVarMap.end(); - //return x.hasAttribute(ArithVarAttr()); } inline ArithVar asArithVar(TNode x) const{