diff options
author | Tim King <taking@cs.nyu.edu> | 2012-12-05 21:45:12 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-12-05 21:45:12 +0000 |
commit | bd0a6c39c56c6ad2bf12e7b9fd41db1772fed9cd (patch) | |
tree | 51f4bc5994a0716e6f4cfeed136360954ce505ac /src/theory/arith/theory_arith.cpp | |
parent | 356a8b6e5ea2622d0fef5cf209159caf08ba5297 (diff) |
Improved garbage collection for TheoryArith. The merges all of the code over from branches/arithmetic/converge except for the new code for simplex.
Diffstat (limited to 'src/theory/arith/theory_arith.cpp')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 168 |
1 files changed, 110 insertions, 58 deletions
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<Rational>& 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<Rational>& 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("<<x<<")"<<std::endl; } @@ -1254,8 +1300,8 @@ Node TheoryArith::dioCutting(){ context::Context::ScopedPush speculativePush(getSatContext()); //DO NOT TOUCH THE OUTPUTSTREAM - //TODO: Improve this - for(ArithVar v = 0, end = d_variables.size(); v != end; ++v){ + for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){ + ArithVar v = *vi; if(isInteger(v)){ const DeltaRational& dr = d_partialModel.getAssignment(v); if(d_partialModel.equalsUpperBound(v, dr) || d_partialModel.equalsLowerBound(v, dr)){ @@ -1485,7 +1531,8 @@ bool TheoryArith::assertionCases(Constraint constraint){ * If this returns true, all integer variables have an integer assignment. */ bool TheoryArith::hasIntegerModel(){ - if(d_variables.size() > 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<Node>::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<Node>::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)"; } |