From bd0a6c39c56c6ad2bf12e7b9fd41db1772fed9cd Mon Sep 17 00:00:00 2001 From: Tim King Date: Wed, 5 Dec 2012 21:45:12 +0000 Subject: [PATCH] Improved garbage collection for TheoryArith. The merges all of the code over from branches/arithmetic/converge except for the new code for simplex. --- src/theory/arith/Makefile.am | 1 + src/theory/arith/arithvar.cpp | 13 ++ src/theory/arith/arithvar.h | 7 +- src/theory/arith/arithvar_node_map.h | 31 +++- src/theory/arith/congruence_manager.cpp | 2 +- src/theory/arith/constraint.cpp | 48 ++++- src/theory/arith/constraint.h | 20 +++ src/theory/arith/linear_equality.cpp | 19 +- src/theory/arith/linear_equality.h | 7 +- src/theory/arith/matrix.cpp | 16 +- src/theory/arith/matrix.h | 76 ++++---- src/theory/arith/theory_arith.cpp | 168 ++++++++++++------ src/theory/arith/theory_arith.h | 27 ++- src/theory/quantifiers/inst_strategy_cbqi.cpp | 18 +- src/util/dense_map.h | 22 +++ 15 files changed, 347 insertions(+), 128 deletions(-) create mode 100644 src/theory/arith/arithvar.cpp diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index b2d1b9f09..76d8d9083 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -9,6 +9,7 @@ libarith_la_SOURCES = \ theory_arith_type_rules.h \ type_enumerator.h \ arithvar.h \ + arithvar.cpp \ arith_rewriter.h \ arith_rewriter.cpp \ arith_static_learner.h \ diff --git a/src/theory/arith/arithvar.cpp b/src/theory/arith/arithvar.cpp new file mode 100644 index 000000000..76b143fff --- /dev/null +++ b/src/theory/arith/arithvar.cpp @@ -0,0 +1,13 @@ + +#include "theory/arith/arithvar.h" +#include + +namespace CVC4 { +namespace theory { +namespace arith { + +const ArithVar ARITHVAR_SENTINEL = std::numeric_limits::max(); + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/arith/arithvar.h b/src/theory/arith/arithvar.h index eac238cba..95614a011 100644 --- a/src/theory/arith/arithvar.h +++ b/src/theory/arith/arithvar.h @@ -22,24 +22,23 @@ #ifndef __CVC4__THEORY__ARITH__ARITHVAR_H #define __CVC4__THEORY__ARITH__ARITHVAR_H -#include #include #include "expr/node.h" #include "context/cdhashset.h" -#include "context/cdhashset.h" #include "util/index.h" +#include "util/dense_map.h" namespace CVC4 { namespace theory { namespace arith { typedef Index ArithVar; -const ArithVar ARITHVAR_SENTINEL = std::numeric_limits::max(); +extern const ArithVar ARITHVAR_SENTINEL; //Maps from Nodes -> ArithVars, and vice versa typedef __gnu_cxx::hash_map NodeToArithVarMap; -typedef __gnu_cxx::hash_map ArithVarToNodeMap; +typedef DenseMap ArithVarToNodeMap; /** * ArithVarCallBack provides a mechanism for agreeing on callbacks while diff --git a/src/theory/arith/arithvar_node_map.h b/src/theory/arith/arithvar_node_map.h index 3a2cff236..e0e589e57 100644 --- a/src/theory/arith/arithvar_node_map.h +++ b/src/theory/arith/arithvar_node_map.h @@ -40,31 +40,50 @@ private: ArithVarToNodeMap d_arithVarToNodeMap; public: + + typedef ArithVarToNodeMap::const_iterator var_iterator; + ArithVarNodeMap() {} inline bool hasArithVar(TNode x) const { return d_nodeToArithVarMap.find(x) != d_nodeToArithVarMap.end(); } + inline bool hasNode(ArithVar a) const { + return d_arithVarToNodeMap.isKey(a); + } + 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; + Assert(hasNode(a)); + return d_arithVarToNodeMap[a]; } inline void setArithVar(TNode x, ArithVar a){ Assert(!hasArithVar(x)); - Assert(d_arithVarToNodeMap.find(a) == d_arithVarToNodeMap.end()); - d_arithVarToNodeMap[a] = x; + Assert(!d_arithVarToNodeMap.isKey(a)); + d_arithVarToNodeMap.set(a, x); d_nodeToArithVarMap[x] = a; } - const ArithVarToNodeMap& getArithVarToNodeMap() const { - return d_arithVarToNodeMap; + inline void remove(ArithVar x){ + Assert(hasNode(x)); + Node node = asNode(x); + + d_nodeToArithVarMap.erase(d_nodeToArithVarMap.find(node)); + d_arithVarToNodeMap.remove(x); + } + + var_iterator var_begin() const { + return d_arithVarToNodeMap.begin(); + } + var_iterator var_end() const { + return d_arithVarToNodeMap.end(); } };/* class ArithVarNodeMap */ diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 5ee250c09..de4c7eac3 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -272,7 +272,7 @@ void ArithCongruenceManager::addWatchedPair(ArithVar s, TNode x, TNode y){ d_watchedVariables.add(s); Node eq = x.eqNode(y); - d_watchedEqualities[s] = eq; + d_watchedEqualities.set(s, eq); } void ArithCongruenceManager::assertionToEqualityEngine(bool isEquality, ArithVar s, TNode reason){ diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index 392d04f6c..cf3aeafee 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -371,6 +371,10 @@ void ConstraintValue::setAssertedToTheTheory(TNode witness) { d_database->pushAssertionOrderWatch(this, witness); } +// bool ConstraintValue::isPsuedoConstraint() const { +// return d_proof == d_database->d_psuedoConstraintProof; +// } + bool ConstraintValue::isSelfExplaining() const { return d_proof == d_database->d_selfExplainingProof; } @@ -481,6 +485,9 @@ ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Co d_equalityEngineProof = d_proofs.size(); d_proofs.push_back(NullConstraint); + + // d_psuedoConstraintProof = d_proofs.size(); + // d_proofs.push_back(NullConstraint); } Constraint ConstraintDatabase::getConstraint(ArithVar v, ConstraintType t, const DeltaRational& r){ @@ -566,8 +573,32 @@ ConstraintDatabase::Statistics::~Statistics(){ } void ConstraintDatabase::addVariable(ArithVar v){ - Assert(v == d_varDatabases.size()); - d_varDatabases.push_back(new PerVariableDatabase(v)); + if(d_reclaimable.isMember(v)){ + SortedConstraintMap& scm = getVariableSCM(v); + + std::vector constraintList; + + for(SortedConstraintMapIterator i = scm.begin(), end = scm.end(); i != end; ++i){ + (i->second).push_into(constraintList); + } + while(!constraintList.empty()){ + Constraint c = constraintList.back(); + constraintList.pop_back(); + Assert(c->safeToGarbageCollect()); + delete c; + } + Assert(scm.empty()); + + d_reclaimable.remove(v); + }else{ + Assert(v == d_varDatabases.size()); + d_varDatabases.push_back(new PerVariableDatabase(v)); + } +} + +void ConstraintDatabase::removeVariable(ArithVar v){ + Assert(!d_reclaimable.isMember(v)); + d_reclaimable.add(v); } bool ConstraintValue::safeToGarbageCollect() const{ @@ -802,6 +833,13 @@ void ConstraintValue::impliedBy(const std::vector& b){ } } +// void ConstraintValue::setPsuedoConstraint(){ +// Assert(truthIsUnknown()); +// Assert(!hasLiteral()); + +// d_database->pushProofWatch(this, d_database->d_psuedoConstraintProof); +// } + void ConstraintValue::setEqualityEngineProof(){ Assert(truthIsUnknown()); Assert(hasLiteral()); @@ -818,6 +856,7 @@ void ConstraintValue::markAsTrue(){ void ConstraintValue::markAsTrue(Constraint imp){ Assert(truthIsUnknown()); Assert(imp->hasProof()); + //Assert(!imp->isPsuedoConstraint()); d_database->d_proofs.push_back(NullConstraint); d_database->d_proofs.push_back(imp); @@ -829,6 +868,8 @@ void ConstraintValue::markAsTrue(Constraint impA, Constraint impB){ Assert(truthIsUnknown()); Assert(impA->hasProof()); Assert(impB->hasProof()); + //Assert(!impA->isPsuedoConstraint()); + //Assert(!impB->isPsuedoConstraint()); d_database->d_proofs.push_back(NullConstraint); d_database->d_proofs.push_back(impA); @@ -845,6 +886,7 @@ void ConstraintValue::markAsTrue(const vector& a){ for(vector::const_iterator i = a.begin(), end = a.end(); i != end; ++i){ Constraint c_i = *i; Assert(c_i->hasProof()); + //Assert(!c_i->isPsuedoConstraint()); d_database->d_proofs.push_back(c_i); } @@ -861,6 +903,7 @@ SortedConstraintMap& ConstraintValue::constraintSet() const{ bool ConstraintValue::proofIsEmpty() const{ Assert(hasProof()); bool result = d_database->d_proofs[d_proof] == NullConstraint; + //Assert((!result) || isSelfExplaining() || hasEqualityEngineProof() || isPsuedoConstraint()); Assert((!result) || isSelfExplaining() || hasEqualityEngineProof()); return result; } @@ -869,6 +912,7 @@ void ConstraintValue::explainBefore(NodeBuilder<>& nb, AssertionOrder order) con Assert(hasProof()); Assert(!isSelfExplaining() || assertedToTheTheory()); + if(assertedBefore(order)){ nb << getWitness(); }else if(hasEqualityEngineProof()){ diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 331fd2bcb..52aa5a5ce 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -485,6 +485,15 @@ public: void setEqualityEngineProof(); bool hasEqualityEngineProof() const; + + /** + * There cannot be a literal associated with this constraint. + * The explanation is the constant true. + * explainInto() does nothing. + */ + //void setPsuedoConstraint(); + //bool isPsuedoConstraint() const; + /** * Returns a explanation of the constraint that is appropriate for conflicts. * @@ -694,6 +703,14 @@ private: */ ProofId d_equalityEngineProof; + /** + * Marks a node as being true always. + * This is only okay for purely internal things. + * + * This is a special proof that is always a member of the list. + */ + //ProofId d_psuedoConstraintProof; + typedef context::CDList ProofCleanupList; typedef context::CDList CBPList; typedef context::CDList AOList; @@ -817,6 +834,7 @@ public: void addVariable(ArithVar v); bool variableDatabaseIsSetup(ArithVar v) const; + void removeVariable(ArithVar v); Node eeExplain(ConstConstraint c) const; void eeExplain(ConstConstraint c, NodeBuilder<>& nb) const; @@ -881,6 +899,8 @@ public: private: void raiseUnateConflict(Constraint ant, Constraint cons); + DenseSet d_reclaimable; + class Statistics { public: IntStat d_unatePropagateCalls; diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index 360e45289..5063a05c7 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -80,7 +80,7 @@ void LinearEqualityModule::update(ArithVar x_i, const DeltaRational& v){ if(Debug.isOn("paranoid:check_tableau")){ debugCheckTableau(); } } -void LinearEqualityModule::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){ +void LinearEqualityModule::pivotAndUpdate(ArithVar x_i, ArithVar x_j, const DeltaRational& v){ Assert(x_i != x_j); TimerStat::CodeTimer codeTimer(d_statistics.d_pivotTime); @@ -188,6 +188,23 @@ void LinearEqualityModule::debugCheckTableau(){ Assert(sum == shouldBe); } } +bool LinearEqualityModule::debugEntireLinEqIsConsistent(const string& s){ + bool result = true; + for(ArithVar var = 0, end = d_tableau.getNumColumns(); var != end; ++var){ + // for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){ + //ArithVar var = d_arithvarNodeMap.asArithVar(*i); + if(!d_partialModel.assignmentIsConsistent(var)){ + d_partialModel.printModel(var); + Warning() << s << ":" << "Assignment is not consistent for " << var ; + if(d_tableau.isBasic(var)){ + Warning() << " (basic)"; + } + Warning() << endl; + result = false; + } + } + return result; +} DeltaRational LinearEqualityModule::computeBound(ArithVar basic, bool upperBound){ DeltaRational sum(0,0); diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index f337ef0db..7df5ee9c3 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -79,7 +79,7 @@ public: * and then pivots x_i with the nonbasic variable in its row x_j. * Updates the assignment of the other basic variables accordingly. */ - void pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v); + void pivotAndUpdate(ArithVar x_i, ArithVar x_j, const DeltaRational& v); ArithPartialModel& getPartialModel() const{ return d_partialModel; } @@ -141,6 +141,11 @@ public: /** Debugging information for a pivot. */ void debugPivot(ArithVar x_i, ArithVar x_j); + /** + * + */ + bool debugEntireLinEqIsConsistent(const std::string& s); + private: /** These fields are designed to be accessible to TheoryArith methods. */ diff --git a/src/theory/arith/matrix.cpp b/src/theory/arith/matrix.cpp index 8e7fe7894..cd7a8a9aa 100644 --- a/src/theory/arith/matrix.cpp +++ b/src/theory/arith/matrix.cpp @@ -247,7 +247,7 @@ void Tableau::rowPivot(ArithVar basicOld, ArithVar basicNew){ d_basic2RowIndex.remove(basicOld); d_basic2RowIndex.set(basicNew, rid); - d_rowIndex2basic[rid] = basicNew; + d_rowIndex2basic.set(rid, basicNew); } // void Tableau::addEntry(ArithVar row, ArithVar col, const Rational& coeff){ @@ -397,10 +397,11 @@ void Tableau::addRow(ArithVar basic, RowIndex newRow = Matrix::addRow(coefficients, variables); addEntry(newRow, basic, Rational(-1)); - Assert(d_rowIndex2basic.size() == newRow); + Assert(!d_basic2RowIndex.isKey(basic)); + Assert(!d_rowIndex2basic.isKey(newRow)); d_basic2RowIndex.set(basic, newRow); - d_rowIndex2basic.push_back(basic); + d_rowIndex2basic.set(newRow, basic); if(Debug.isOn("matrix")){ printMatrix(); } @@ -558,6 +559,15 @@ void ReducedRowVector::enqueueNonBasicVariablesAndCoefficients(std::vector< Arit // return newId; // } +void Tableau::removeBasicRow(ArithVar basic){ + RowIndex rid = basicToRowIndex(basic); + + removeRow(rid); + d_basic2RowIndex.remove(basic); + d_rowIndex2basic.remove(rid); + +} + }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h index ea6c389b9..027397b6a 100644 --- a/src/theory/arith/matrix.h +++ b/src/theory/arith/matrix.h @@ -25,6 +25,7 @@ #include "util/dense_map.h" #include "theory/arith/arithvar.h" +#include "theory/arith/arithvar_node_map.h" #include "theory/arith/normal_form.h" #include @@ -377,6 +378,8 @@ protected: uint32_t d_entriesInUse; MatrixEntryVector d_entries; + std::vector d_pool; + T d_zero; public: @@ -446,6 +449,23 @@ protected: d_entries.freeEntry(id); } + private: + RowIndex requestRowIndex(){ + if(d_pool.empty()){ + RowIndex ridx = d_rows.size(); + d_rows.push_back(RowVectorT(&d_entries)); + return ridx; + }else{ + RowIndex rid = d_pool.back(); + d_pool.pop_back(); + return rid; + } + } + + void releaseRowIndex(RowIndex rid){ + d_pool.push_back(rid); + } + public: size_t getNumRows() const { @@ -485,8 +505,11 @@ public: */ RowIndex addRow(const std::vector& coeffs, const std::vector& variables){ - RowIndex ridx = d_rows.size(); - d_rows.push_back(RowVectorT(&d_entries)); + + RowIndex ridx = requestRowIndex(); + + //RowIndex ridx = d_rows.size(); + //d_rows.push_back(RowVectorT(&d_entries)); std::vector::const_iterator coeffIter = coeffs.begin(); std::vector::const_iterator varsIter = variables.begin(); @@ -701,36 +724,7 @@ public: EntryID id = i.getID(); removeEntry(id); } - } - - - Node rowAsEquality(RowIndex rid, const ArithVarToNodeMap& map){ - using namespace CVC4::kind; - - Assert(getRowLength(rid) >= 2); - - std::vector pairs; - for(RowIterator i = getRow(rid); !i.atEnd(); ++i){ - const Entry& entry = *i; - ArithVar colVar = entry.getColVar(); - - Node var = (map.find(colVar))->second; - Node coeff = mkRationalNode(entry.getCoefficient()); - - Node mult = NodeBuilder<2>(MULT) << coeff << var; - pairs.push_back(mult); - } - - Node sum = Node::null(); - if(pairs.size() == 1 ){ - sum = pairs.front(); - }else{ - Assert(pairs.size() >= 2); - NodeBuilder<> sumBuilder(PLUS); - sumBuilder.append(pairs); - sum = sumBuilder; - } - return NodeBuilder<2>(EQUAL) << sum << mkRationalNode(d_zero); + releaseRowIndex(rid); } double densityMeasure() const{ @@ -754,6 +748,15 @@ public: } } + void loadSignQueries(RowIndex rid, DenseMap& target) const{ + + RowIterator i = getRow(rid).begin(), i_end = getRow(rid).end(); + for(; i != i_end; ++i){ + const MatrixEntry& entry = *i; + target.set(entry.getColVar(), entry.getCoefficient().sgn()); + } + } + protected: uint32_t numNonZeroEntries() const { return size(); } @@ -833,8 +836,10 @@ private: // Set of all of the basic variables in the tableau. // ArithVarMap : ArithVar |-> RowIndex BasicToRowMap d_basic2RowIndex; + // RowIndex |-> Basic Variable - std::vector d_rowIndex2basic; + typedef DenseMap RowIndexToBasicMap; + RowIndexToBasicMap d_rowIndex2basic; public: @@ -882,10 +887,6 @@ public: return getRow(basicToRowIndex(basic)).begin(); } - // RowIterator rowIterator(RowIndex r) const { - // return getRow(r).begin(); - // } - /** * Adds a row to the tableau. * The new row is equivalent to: @@ -911,7 +912,6 @@ public: void removeBasicRow(ArithVar basic); - private: /* Changes the basic variable on the row for basicOld to basicNew. */ void rowPivot(ArithVar basicOld, ArithVar basicNew); diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index d2814348a..f036e20fd 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -62,6 +62,8 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha d_unknownsInARow(0), d_hasDoneWorkSinceCut(false), d_learner(u), + d_numberOfVariables(0), + d_pool(), d_setupLiteralCallback(this), d_assertionsThatDoNotMatchTheirLiterals(c), d_nextIntegerCheckVar(0), @@ -79,6 +81,7 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha d_tableauResetPeriod(10), d_conflicts(c), d_raiseConflict(d_conflicts), + d_tempVarMalloc(*this), d_congruenceManager(c, d_constraintDatabase, d_setupLiteralCallback, d_arithvarNodeMap, d_raiseConflict), d_simplex(d_linEq, d_raiseConflict), d_constraintDatabase(c, u, d_arithvarNodeMap, d_congruenceManager, d_raiseConflict), @@ -822,8 +825,9 @@ void TheoryArith::setupVariable(const Variable& x){ Assert(!isSetup(n)); ++(d_statistics.d_statUserVariables); - ArithVar varN = requestArithVar(n,false); - setupInitialValue(varN); + requestArithVar(n,false); + //ArithVar varN = requestArithVar(n,false); + //setupInitialValue(varN); markSetup(n); @@ -860,8 +864,9 @@ void TheoryArith::setupVariableList(const VarList& vl){ d_nlIncomplete = true; ++(d_statistics.d_statUserVariables); - ArithVar av = requestArithVar(vlNode, false); - setupInitialValue(av); + requestArithVar(vlNode, false); + //ArithVar av = requestArithVar(vlNode, false); + //setupInitialValue(av); markSetup(vlNode); } @@ -1054,7 +1059,7 @@ void TheoryArith::setupPolynomial(const Polynomial& poly) { ArithVar varSlack = requestArithVar(polyNode, true); d_tableau.addRow(varSlack, coefficients, variables); - setupInitialValue(varSlack); + setupBasicValue(varSlack); //Add differences to the difference manager Polynomial::iterator i = poly.begin(), end = poly.end(); @@ -1125,6 +1130,14 @@ void TheoryArith::preRegisterTerm(TNode n) { Debug("arith::preregister") << "end arith::preRegisterTerm("<< n <<")" << endl; } +void TheoryArith::releaseArithVar(ArithVar v){ + Assert(d_arithvarNodeMap.hasNode(v)); + + d_constraintDatabase.removeVariable(v); + d_arithvarNodeMap.remove(v); + + d_pool.push_back(v); +} ArithVar TheoryArith::requestArithVar(TNode x, bool slack){ //TODO : The VarList trick is good enough? @@ -1135,32 +1148,73 @@ ArithVar TheoryArith::requestArithVar(TNode x, bool slack){ Assert(!d_arithvarNodeMap.hasArithVar(x)); Assert(x.getType().isReal());// real or integer - ArithVar varX = d_variables.size(); - d_variables.push_back(Node(x)); - Debug("integers") << "isInteger[[" << x << "]]: " << x.getType().isInteger() << endl; + // ArithVar varX = d_variables.size(); + // d_variables.push_back(Node(x)); + + bool reclaim = !d_pool.empty(); + ArithVar varX; + + if(reclaim){ + varX = d_pool.back(); + d_pool.pop_back(); + + d_partialModel.setAssignment(varX, d_DELTA_ZERO, d_DELTA_ZERO); + }else{ + varX = d_numberOfVariables; + ++d_numberOfVariables; + + d_slackVars.push_back(true); + d_variableTypes.push_back(ATReal); + d_simplex.increaseMax(); + + d_tableau.increaseSize(); + d_tableauSizeHasBeenModified = true; + + d_partialModel.initialize(varX, d_DELTA_ZERO); + } + + ArithType type; if(slack){ //The type computation is not quite accurate for Rationals that are integral. //We'll use the isIntegral check from the polynomial package instead. Polynomial p = Polynomial::parsePolynomial(x); - d_variableTypes.push_back(p.isIntegral() ? ATInteger : ATReal); + type = p.isIntegral() ? ATInteger : ATReal; }else{ - d_variableTypes.push_back(nodeToArithType(x)); + type = nodeToArithType(x); } + d_variableTypes[varX] = type; + d_slackVars[varX] = slack; - d_slackVars.push_back(slack); - - d_simplex.increaseMax(); + d_constraintDatabase.addVariable(varX); d_arithvarNodeMap.setArithVar(x,varX); - d_tableau.increaseSize(); - d_tableauSizeHasBeenModified = true; + // Debug("integers") << "isInteger[[" << x << "]]: " << x.getType().isInteger() << endl; - d_constraintDatabase.addVariable(varX); + // if(slack){ + // //The type computation is not quite accurate for Rationals that are integral. + // //We'll use the isIntegral check from the polynomial package instead. + // Polynomial p = Polynomial::parsePolynomial(x); + // d_variableTypes.push_back(p.isIntegral() ? ATInteger : ATReal); + // }else{ + // d_variableTypes.push_back(nodeToArithType(x)); + // } + + // d_slackVars.push_back(slack); + + // d_simplex.increaseMax(); + + // d_tableau.increaseSize(); + // d_tableauSizeHasBeenModified = true; + + // d_constraintDatabase.addVariable(varX); Debug("arith::arithvar") << x << " |-> " << varX << endl; + Assert(!d_partialModel.hasUpperBound(varX)); + Assert(!d_partialModel.hasLowerBound(varX)); + return varX; } @@ -1179,18 +1233,7 @@ void TheoryArith::asVectors(const Polynomial& p, std::vector& coeffs, Assert(theoryOf(n) != THEORY_ARITH || d_arithvarNodeMap.hasArithVar(n)); Assert(d_arithvarNodeMap.hasArithVar(n)); - ArithVar av; - // The first if is likely dead is likely dead code: - // if (theoryOf(n) != THEORY_ARITH && !d_arithvarNodeMap.hasArithVar(n)) { - // // The only way not to get it through pre-register is if it's a foreign term - // ++(d_statistics.d_statUserVariables); - // av = requestArithVar(n,false); - // setupInitialValue(av); - // } else { - // // Otherwise, we already have it's variable - // av = d_arithvarNodeMap.asArithVar(n); - // } - av = d_arithvarNodeMap.asArithVar(n); + ArithVar av = d_arithvarNodeMap.asArithVar(n); coeffs.push_back(constant.getValue()); variables.push_back(av); @@ -1200,11 +1243,12 @@ void TheoryArith::asVectors(const Polynomial& p, std::vector& coeffs, /* Requirements: * For basic variables the row must have been added to the tableau. */ -void TheoryArith::setupInitialValue(ArithVar x){ +void TheoryArith::setupBasicValue(ArithVar x){ + Assert(d_tableau.isBasic(x)); - if(!d_tableau.isBasic(x)){ - d_partialModel.initialize(x, d_DELTA_ZERO); - }else{ + // if(!d_tableau.isBasic(x)){ + // d_partialModel.setAssignment(x, d_DELTA_ZERO, d_DELTA_ZERO); + // }else{ //If the variable is basic, assertions may have already happened and updates //may have occured before setting this variable up. @@ -1212,9 +1256,11 @@ void TheoryArith::setupInitialValue(ArithVar x){ //time instead of register DeltaRational safeAssignment = d_linEq.computeRowValue(x, true); DeltaRational assignment = d_linEq.computeRowValue(x, false); - d_partialModel.initialize(x,safeAssignment); - d_partialModel.setAssignment(x,assignment); - } + //d_partialModel.initialize(x,safeAssignment); + //d_partialModel.setAssignment(x,assignment); + d_partialModel.setAssignment(x,safeAssignment,assignment); + + // } Debug("arith") << "setupVariable("< 0){ + //if(d_variables.size() > 0){ + if(getNumberOfVariables()){ const ArithVar rrEnd = d_nextIntegerCheckVar; do { //Do not include slack variables @@ -1495,7 +1542,7 @@ bool TheoryArith::hasIntegerModel(){ return false; } } - } while((d_nextIntegerCheckVar = (1 + d_nextIntegerCheckVar == d_variables.size() ? 0 : 1 + d_nextIntegerCheckVar)) != rrEnd); + } while((d_nextIntegerCheckVar = (1 + d_nextIntegerCheckVar == getNumberOfVariables() ? 0 : 1 + d_nextIntegerCheckVar)) != rrEnd); } return true; } @@ -1576,6 +1623,7 @@ void TheoryArith::check(Effort effortLevel){ Assert(d_conflicts.empty()); d_qflraStatus = d_simplex.findModel(fullEffort(effortLevel)); + switch(d_qflraStatus){ case Result::SAT: if(newFacts){ @@ -1822,7 +1870,8 @@ bool TheoryArith::splitDisequalities(){ */ void TheoryArith::debugPrintAssertions() { Debug("arith::print_assertions") << "Assertions:" << endl; - for (ArithVar i = 0; i < d_variables.size(); ++ i) { + for (var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){ + ArithVar i = *vi; if (d_partialModel.hasLowerBound(i)) { Constraint lConstr = d_partialModel.getLowerBoundConstraint(i); Debug("arith::print_assertions") << lConstr << endl; @@ -1842,13 +1891,15 @@ void TheoryArith::debugPrintAssertions() { void TheoryArith::debugPrintModel(){ Debug("arith::print_model") << "Model:" << endl; - - for (ArithVar i = 0; i < d_variables.size(); ++ i) { - Debug("arith::print_model") << d_variables[i] << " : " << - d_partialModel.getAssignment(i); - if(d_tableau.isBasic(i)) - Debug("arith::print_model") << " (basic)"; - Debug("arith::print_model") << endl; + for (var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){ + ArithVar i = *vi; + if(d_arithvarNodeMap.hasNode(i)){ + Debug("arith::print_model") << d_arithvarNodeMap.asNode(i) << " : " << + d_partialModel.getAssignment(i); + if(d_tableau.isBasic(i)) + Debug("arith::print_model") << " (basic)"; + Debug("arith::print_model") << endl; + } } } @@ -2057,7 +2108,8 @@ Rational TheoryArith::deltaValueForTotalOrder() const{ relevantDeltaValues.insert(val); } - for(ArithVar v = 0; v < d_variables.size(); ++v){ + for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){ + ArithVar v = *vi; const DeltaRational& value = d_partialModel.getAssignment(v); relevantDeltaValues.insert(value); if( d_partialModel.hasLowerBound(v)){ @@ -2108,7 +2160,8 @@ void TheoryArith::collectModelInfo( TheoryModel* m, bool fullModel ){ // TODO: // This is not very good for user push/pop.... // Revisit when implementing push/pop - for(ArithVar v = 0; v < d_variables.size(); ++v){ + for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){ + ArithVar v = *vi; if(!isSlackVariable(v)){ Node term = d_arithvarNodeMap.asNode(v); @@ -2187,13 +2240,13 @@ void TheoryArith::notifyRestart(){ } bool TheoryArith::entireStateIsConsistent(const string& s){ - typedef std::vector::const_iterator VarIter; bool result = true; - for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){ - ArithVar var = d_arithvarNodeMap.asArithVar(*i); + for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){ + ArithVar var = *vi; + //ArithVar var = d_arithvarNodeMap.asArithVar(*i); if(!d_partialModel.assignmentIsConsistent(var)){ d_partialModel.printModel(var); - Warning() << s << ":" << "Assignment is not consistent for " << var << *i; + Warning() << s << ":" << "Assignment is not consistent for " << var << d_arithvarNodeMap.asNode(var); if(d_tableau.isBasic(var)){ Warning() << " (basic)"; } @@ -2205,15 +2258,14 @@ bool TheoryArith::entireStateIsConsistent(const string& s){ } bool TheoryArith::unenqueuedVariablesAreConsistent(){ - typedef std::vector::const_iterator VarIter; bool result = true; - for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){ - ArithVar var = d_arithvarNodeMap.asArithVar(*i); + for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){ + ArithVar var = *vi; if(!d_partialModel.assignmentIsConsistent(var)){ if(!d_simplex.debugIsInCollectionQueue(var)){ d_partialModel.printModel(var); - Warning() << "Unenqueued var is not consistent for " << var << *i; + Warning() << "Unenqueued var is not consistent for " << var << d_arithvarNodeMap.asNode(var); if(d_tableau.isBasic(var)){ Warning() << " (basic)"; } @@ -2221,7 +2273,7 @@ bool TheoryArith::unenqueuedVariablesAreConsistent(){ result = false; } else if(Debug.isOn("arith::consistency::initial")){ d_partialModel.printModel(var); - Warning() << "Initial var is not consistent for " << var << *i; + Warning() << "Initial var is not consistent for " << var << d_arithvarNodeMap.asNode(var); if(d_tableau.isBasic(var)){ Warning() << " (basic)"; } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index b791186cf..7d1150fb1 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -89,17 +89,20 @@ private: /** Static learner. */ ArithStaticLearner d_learner; - /** - * List of the variables in the system. - * This is needed to keep a positive ref count on slack variables. - */ - std::vector d_variables; + + ArithVar d_numberOfVariables; + inline ArithVar getNumberOfVariables() const { return d_numberOfVariables; } + std::vector d_pool; + void releaseArithVar(ArithVar v); /** * The map between arith variables to nodes. */ ArithVarNodeMap d_arithvarNodeMap; + typedef ArithVarNodeMap::var_iterator var_iterator; + var_iterator var_begin() const { return d_arithvarNodeMap.var_begin(); } + var_iterator var_end() const { return d_arithvarNodeMap.var_end(); } NodeSet d_setupNodes; bool isSetup(Node n) const { @@ -273,6 +276,18 @@ private: void outputConflicts(); + class TempVarMalloc : public ArithVarMalloc { + private: + TheoryArith& d_ta; + public: + TempVarMalloc(TheoryArith& ta) : d_ta(ta) {} + ArithVar request(){ + Node skolem = mkRealSkolem("tmpVar"); + return d_ta.requestArithVar(skolem, false); + } + void release(ArithVar v){ d_ta.releaseArithVar(v); } + } d_tempVarMalloc; + /** * A copy of the tableau. * This is equivalent to the original tableau if d_tableauSizeHasBeenModified @@ -433,7 +448,7 @@ private: ArithVar requestArithVar(TNode x, bool slack); /** Initial (not context dependent) sets up for a variable.*/ - void setupInitialValue(ArithVar x); + void setupBasicValue(ArithVar x); /** Initial (not context dependent) sets up for a new slack variable.*/ void setupSlack(TNode left); diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index d79ddee31..ddf763b73 100755 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -46,11 +46,12 @@ void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort d_tableaux.clear(); d_ceTableaux.clear(); //search for instantiation rows in simplex tableaux - ArithVarToNodeMap avtnm = d_th->d_arithvarNodeMap.getArithVarToNodeMap(); - for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){ - ArithVar x = (*it).first; + ArithVarNodeMap& avnm = d_th->d_arithvarNodeMap; + ArithVarNodeMap::var_iterator vi, vend; + for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){ + ArithVar x = *vi; if( d_th->d_partialModel.hasEitherBound( x ) ){ - Node n = (*it).second; + Node n = avnm.asNode(x); Node f; NodeBuilder<> t(kind::PLUS); if( n.getKind()==PLUS ){ @@ -167,10 +168,11 @@ void InstStrategySimplex::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder } void InstStrategySimplex::debugPrint( const char* c ){ - ArithVarToNodeMap avtnm = d_th->d_arithvarNodeMap.getArithVarToNodeMap(); - for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){ - ArithVar x = (*it).first; - Node n = (*it).second; + const ArithVarNodeMap& avnm = d_th->d_arithvarNodeMap; + ArithVarNodeMap::var_iterator vi, vend; + for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){ + ArithVar x = *vi; + Node n = avnm.asNode(x); //if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){ Debug(c) << x << " : " << n << ", bounds = "; if( d_th->d_partialModel.hasLowerBound( x ) ){ diff --git a/src/util/dense_map.h b/src/util/dense_map.h index fa78e6787..222a761c3 100644 --- a/src/util/dense_map.h +++ b/src/util/dense_map.h @@ -151,6 +151,7 @@ public: pop_back(); } + /** Returns the key at the back of a non-empty list.*/ Key back() const { return d_list.back(); } @@ -164,6 +165,27 @@ public: d_list.pop_back(); } + + /** Adds at least a constant fraction of the elements in the current map to another map. */ + void splitInto(DenseMap& target){ + uint32_t targetSize = size()/2; + while(size() > targetSize){ + Key key = back(); + target.set(key, get(key)); + pop_back(); + } + } + + /** Adds the current target map to the current map.*/ + void addAll(const DenseMap& target){ + for(const_iterator i = target.begin(), e = target.end(); i != e; ++i){ + Key k = *i; + set(k, target[k]); + } + } + + + private: size_t allocated() const { -- 2.30.2