From 08df44e6b61999a14dd24a7a134146694dcb3596 Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 18 Apr 2011 20:19:29 +0000 Subject: [PATCH] Removing dead code that came in on commit r1740. --- src/theory/arith/arith_prop_manager.cpp | 8 -- src/theory/arith/arith_prop_manager.h | 7 - src/theory/arith/simplex.cpp | 183 +----------------------- src/theory/arith/theory_arith.cpp | 129 +---------------- 4 files changed, 3 insertions(+), 324 deletions(-) diff --git a/src/theory/arith/arith_prop_manager.cpp b/src/theory/arith/arith_prop_manager.cpp index a09bed8e8..151421b31 100644 --- a/src/theory/arith/arith_prop_manager.cpp +++ b/src/theory/arith/arith_prop_manager.cpp @@ -90,14 +90,6 @@ Node ArithPropManager::getBestImpliedUpperBound(ArithVar v, const DeltaRational& return d_propagator.getBestImpliedUpperBound(bound); } -bool ArithPropManager::hasStrongerLowerBound(TNode n) const{ - bool haveAcompilerWarning; - return true; -} -bool ArithPropManager::hasStrongerUpperBound(TNode n) const{ - return true; -} - Node ArithPropManager::boundAsNode(bool upperbound, ArithVar var, const DeltaRational& b) const { Assert((!upperbound) || (b.getInfinitesimalPart() <= 0) ); Assert(upperbound || (b.getInfinitesimalPart() >= 0) ); diff --git a/src/theory/arith/arith_prop_manager.h b/src/theory/arith/arith_prop_manager.h index 1fd23dd62..55d8ae635 100644 --- a/src/theory/arith/arith_prop_manager.h +++ b/src/theory/arith/arith_prop_manager.h @@ -105,10 +105,6 @@ public: return d_propagator.getWeakerImpliedUpperBound(n); } - - //Node strictlyWeakerAssertedUpperBound(TNode n) const; - //Node strictlyWeakerAssertedLowerBound(TNode n) const; - Node strictlyWeakerAssertedUpperBound(ArithVar v, const DeltaRational& b) const; Node strictlyWeakerAssertedLowerBound(ArithVar v, const DeltaRational& b) const; @@ -116,9 +112,6 @@ public: Node getBestImpliedLowerBound(ArithVar v, const DeltaRational& b) const; Node getBestImpliedUpperBound(ArithVar v, const DeltaRational& b) const; - bool hasStrongerLowerBound(TNode current) const; - bool hasStrongerUpperBound(TNode current) const; - bool containsLiteral(TNode n) const { return d_propagator.containsLiteral(n); } diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index b804cb1aa..113e80c27 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -149,17 +149,6 @@ Node SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_ if(d_partialModel.belowLowerBound(x_i, c_i, true)){ return Node::null(); } - // if(d_partialModel.equalsLowerBound(x_i, c_i) && original.getKind() != AND){ - // TNode prevConstraint = d_partialModel.getLowerConstraint(x_i); - // if(prevConstraint.getKind() == EQUAL){ - // return Node::null(); - // }else{ - // Debug("beat::ya") << x_i << " "<< c_i << original << prevConstraint << endl; - // Assert(prevConstraint.getKind() == AND); - // d_partialModel.setLowerConstraint(x_i,original); - // return Node::null(); - // } - // } if(d_partialModel.aboveUpperBound(x_i, c_i, true)){ Node ubc = d_partialModel.getUpperConstraint(x_i); @@ -197,17 +186,6 @@ Node SimplexDecisionProcedure::AssertUpper(ArithVar x_i, const DeltaRational& c_ return Node::null(); //sat } - // if(d_partialModel.equalsUpperBound(x_i, c_i) && original.getKind() != AND){ - // TNode prevConstraint = d_partialModel.getUpperConstraint(x_i); - // if(prevConstraint.getKind() == EQUAL){ - // return Node::null(); - // }else{ - // Debug("beat::ya") << x_i << " "<< c_i << original << prevConstraint << endl; - // Assert(prevConstraint.getKind() == AND); - // d_partialModel.setUpperConstraint(x_i,original); - // return Node::null(); - // } - // } if(d_partialModel.belowLowerBound(x_i, c_i, true)){// \lowerbound(x_i) > c_i Node lbc = d_partialModel.getLowerConstraint(x_i); Node conflict = NodeManager::currentNM()->mkNode(AND, lbc, original); @@ -375,15 +353,11 @@ bool SimplexDecisionProcedure::hasBounds(ArithVar basic, bool upperBound){ } void SimplexDecisionProcedure::propagateCandidate(ArithVar basic){ bool success = false; - if(d_partialModel.strictlyAboveLowerBound(basic) && - (!d_partialModel.hasLowerBound(basic) || d_propManager.hasStrongerLowerBound(d_partialModel.getLowerConstraint(basic))) && - hasLowerBounds(basic)){ + if(d_partialModel.strictlyAboveLowerBound(basic) && hasLowerBounds(basic)){ ++d_statistics.d_boundComputations; success |= propagateCandidateLowerBound(basic); } - if(d_partialModel.strictlyBelowUpperBound(basic) && - (!d_partialModel.hasUpperBound(basic) || d_propManager.hasStrongerUpperBound(d_partialModel.getUpperConstraint(basic))) && - hasUpperBounds(basic)){ + if(d_partialModel.strictlyBelowUpperBound(basic) && hasUpperBounds(basic)){ ++d_statistics.d_boundComputations; success |= propagateCandidateUpperBound(basic); } @@ -752,18 +726,6 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera if(!possibleConflict.isNull()){ return possibleConflict; } - // if(selectSlackUpperBound(x_j) == ARITHVAR_SENTINEL){ - // Node possibleConflict = deduceUpperBound(x_j); - // if(!possibleConflict.isNull()){ - // return possibleConflict; - // } - // } - // if(selectSlackLowerBound(x_j) == ARITHVAR_SENTINEL){ - // Node possibleConflict = deduceLowerBound(x_j); - // if(!possibleConflict.isNull()){ - // return possibleConflict; - // } - // } } } Assert(remainingIterations == 0); @@ -905,147 +867,6 @@ Node SimplexDecisionProcedure::weakenConflict(bool aboveUpper, ArithVar basicVar } -// Node SimplexDecisionProcedure::weakenLowerBoundConflict(ArithVar basicVar){ -// TimerStat::CodeTimer codeTimer(d_statistics.d_weakenTime); - -// bool anyWeakenings = false; -// const DeltaRational& assignment = d_partialModel.getAssignment(basicVar); -// Assert(d_partialModel.hasLowerBound(basicVar)); -// Assert(assignment < d_partialModel.getLowerBound(basicVar)); - -// DeltaRational surplus = d_partialModel.getLowerBound(basicVar) - assignment; - -// vector weakeningElements; -// queue potentialWeakingings; -// for(Tableau::RowIterator i = d_tableau.rowIterator(basicVar); !i.atEnd(); ++i){ -// const TableauEntry& entry = *i; -// ArithVar v = entry.getColVar(); -// const Rational& coeff = entry.getCoefficient(); - -// int sgn = coeff.sgn(); -// bool ub = (sgn > 0); -// Node exp = ub ? -// d_partialModel.getUpperConstraint(v) : -// d_partialModel.getLowerConstraint(v); -// DeltaRational bound = ub? -// d_partialModel.getUpperBound(v) : -// d_partialModel.getLowerBound(v); -// potentialWeakingings.push(weakeningElements.size()); -// weakeningElements.push_back(WeakeningElem(v, &coeff, ub, bound, exp)); -// } - -// vector conflict; - -// Debug("weak") << "weakenLowerBoundConflict" << endl; -// while(!potentialWeakingings.empty()){ -// uint32_t pos = potentialWeakingings.front(); -// potentialWeakingings.pop(); - -// WeakeningElem& curr = weakeningElements[pos]; - -// Node weaker = curr.upperBound? -// d_propManager.strictlyWeakerAssertedUpperBound(curr.var, curr.bound): -// d_propManager.strictlyWeakerAssertedLowerBound(curr.var, curr.bound); - -// bool weakened = false; -// if(!weaker.isNull()){ -// DeltaRational weakerBound = asDeltaRational(weaker); -// DeltaRational diff = weakerBound - curr.bound; -// //if var == basic, weakerBound < curr.bound -// // multiply by -1 -// diff = diff * (*curr.coeff); - -// if(surplus > diff){ -// ++d_statistics.d_weakenings; -// anyWeakenings = true; -// weakened = true; -// surplus = surplus - diff; - -// Debug("weak") << "found:" << endl; -// if(curr.var == basicVar){ -// Debug("weak") << " basic: "; -// } -// Debug("weak") << " " << surplus << " "<< diff << endl -// << " " << curr.bound << weakerBound << endl -// << " " << curr.explanation << weaker << endl; - -// if(curr.explanation.getKind() == AND){ -// Debug("weak") << "VICTORY" << endl; -// } - -// Assert(diff > d_DELTA_ZERO); -// curr.explanation = weaker; -// curr.bound = weakerBound; -// } -// } - -// if(weakened){ -// potentialWeakingings.push(pos); -// }else{ -// if(curr.explanation.getKind() == AND){ -// Debug("weak") << "boo: " << curr.explanation << endl; -// } -// conflict.push_back(curr.explanation); -// } -// } - -// ++d_statistics.d_weakeningAttempts; -// if(anyWeakenings){ -// ++d_statistics.d_weakeningSuccesses; -// } - -// NodeBuilder<> nb(AND); -// nb.append(conflict); -// return nb; -// } - -// Node SimplexDecisionProcedure::deduceUpperBound(ArithVar basicVar){ -// Assert(d_tableau.isBasic(basicVar)); -// Assert(selectSlackUpperBound(basicVar) == ARITHVAR_SENTINEL); - -// const DeltaRational& assignment = d_partialModel.getAssignment(basicVar); - -// Assert(assignment.getInfinitesimalPart() <= 0); - -// if(d_partialModel.strictlyBelowUpperBound(basicVar, assignment)){ -// NodeBuilder<> nb(kind::AND); -// explainNonbasicsUpperBound(basicVar, nb); -// Node explanation = maybeUnaryConvert(nb); -// Debug("waka-waka") << basicVar << " ub " << assignment << " "<< explanation << endl; -// Node res = AssertUpper(basicVar, assignment, explanation); -// if(res.isNull()){ -// d_propManager.propagateArithVar(true, basicVar, assignment, explanation); -// } -// return res; -// }else{ -// return Node::null(); -// } -// } - -// Node SimplexDecisionProcedure::deduceLowerBound(ArithVar basicVar){ -// Assert(d_tableau.isBasic(basicVar)); -// Assert(selectSlackLowerBound(basicVar) == ARITHVAR_SENTINEL); -// const DeltaRational& assignment = d_partialModel.getAssignment(basicVar); - -// if(Debug.isOn("paranoid:check_tableau")){ debugCheckTableau(); } - -// Assert(assignment.getInfinitesimalPart() >= 0); - -// if(d_partialModel.strictlyAboveLowerBound(basicVar, assignment)){ -// NodeBuilder<> nb(kind::AND); -// explainNonbasicsLowerBound(basicVar, nb); -// Node explanation = maybeUnaryConvert(nb); -// Debug("waka-waka") << basicVar << " lb " << assignment << " "<< explanation << endl; -// Node res = AssertLower(basicVar, assignment, explanation); -// if(res.isNull()){ -// d_propManager.propagateArithVar(false, basicVar, assignment, explanation); -// } -// return res; -// }else{ -// return Node::null(); -// } -// } - Node SimplexDecisionProcedure::generateConflictAboveUpperBound(ArithVar conflictVar){ return weakenConflict(true, conflictVar); } diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 3c275fae0..e724312fa 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -368,10 +368,7 @@ void TheoryArith::check(Effort effortLevel){ if(!possibleConflict.isNull()){ d_partialModel.revertAssignmentChanges(); - //Node simpleConflict = BooleanSimplification::simplifyConflict(possibleConflict); - Debug("arith::conflict") << "conflict " << possibleConflict << endl; - d_simplex.clearUpdates(); d_out->conflict(possibleConflict); return; @@ -386,9 +383,6 @@ void TheoryArith::check(Effort effortLevel){ if(possibleConflict != Node::null()){ d_partialModel.revertAssignmentChanges(); d_simplex.clearUpdates(); - - //Node simpleConflict = BooleanSimplification::simplifyConflict(possibleConflict); - Debug("arith::conflict") << "conflict " << possibleConflict << endl; d_out->conflict(possibleConflict); @@ -424,16 +418,6 @@ void TheoryArith::splitDisequalities(){ Node ltNode = NodeBuilder<2>(kind::LT) << lhs << rhs; Node gtNode = NodeBuilder<2>(kind::GT) << lhs << rhs; Node lemma = NodeBuilder<3>(OR) << eq << ltNode << gtNode; - - // // < => !> - // Node imp1 = NodeBuilder<2>(kind::IMPLIES) << ltNode << gtNode.notNode(); - // // < => != - // Node imp2 = NodeBuilder<2>(kind::IMPLIES) << ltNode << eq.notNode(); - // // > => != - // Node imp3 = NodeBuilder<2>(kind::IMPLIES) << gtNode << eq.notNode(); - // // All the implication - // Node impClosure = NodeBuilder<3>(kind::AND) << imp1 << imp2 << imp3; - ++(d_statistics.d_statDisequalitySplits); d_out->lemma(lemma); } @@ -476,112 +460,13 @@ void TheoryArith::debugPrintModel(){ } } -/* -bool TheoryArith::isImpliedUpperBound(ArithVar var, Node exp){ - Node varAsNode = asNode(var); - const DeltaRational& ub = d_partialModel.getUpperBound(var); - Assert(ub.getInfinitesimalPart() <= 0 ); - Kind kind = ub.getInfinitesimalPart() < 0 ? LT : LEQ; - Node ubAsNode = NodeBuilder<2>(kind) << varAsNode << mkRationalNode(ub.getNoninfinitesimalPart()); - Node bestImplied = d_propagator.getBestImpliedUpperBound(ubAsNode); - - return bestImplied == exp; -} - -bool TheoryArith::isImpliedLowerBound(ArithVar var, Node exp){ - Node varAsNode = asNode(var); - const DeltaRational& lb = d_partialModel.getLowerBound(var); - Assert(lb.getInfinitesimalPart() >= 0 ); - Kind kind = lb.getInfinitesimalPart() > 0 ? GT : GEQ; - Node lbAsIneq = NodeBuilder<2>(kind) << varAsNode << mkRationalNode(lb.getNoninfinitesimalPart()); - Node bestImplied = d_propagator.getBestImpliedLowerBound(lbAsIneq); - return bestImplied == exp; -} -*/ - void TheoryArith::explain(TNode n) { Debug("explain") << "explain @" << getContext()->getLevel() << ": " << n << endl; - //Assert(n.hasAttribute(Propagated())); - //NodeBuilder<> explainBuilder(AND); - //internalExplain(n,explainBuilder); Assert(d_propManager.isPropagated(n)); Node explanation = d_propManager.explain(n); - //Node flatExplanation = BooleanSimplification::simplifyConflict(explanation); - d_out->explanation(explanation, true); } -/* -void TheoryArith::internalExplain(TNode n, NodeBuilder<>& explainBuilder){ - Assert(n.hasAttribute(Propagated())); - Node bound = n.getAttribute(Propagated()); - - AlwaysAssert(bound.getKind() == kind::AND); - - for(Node::iterator i = bound.begin(), end = bound.end(); i != end; ++i){ - Node lit = *i; - if(lit.hasAttribute(Propagated())){ - cout << "hoop the sadjklasdj" << endl; - internalExplain(lit, explainBuilder); - }else{ - explainBuilder << lit; - } - } -} -*/ -/* -static const bool EXPORT_LEMMA_INSTEAD_OF_PROPAGATE = false; -void TheoryArith::propagateArithVar(bool upperbound, ArithVar var ){ - Node varAsNode = asNode(var); - const DeltaRational& b = upperbound ? - d_partialModel.getUpperBound(var) : d_partialModel.getLowerBound(var); - - Assert((!upperbound) || (b.getInfinitesimalPart() <= 0) ); - Assert(upperbound || (b.getInfinitesimalPart() >= 0) ); - Kind kind; - if(upperbound){ - kind = b.getInfinitesimalPart() < 0 ? LT : LEQ; - } else{ - kind = b.getInfinitesimalPart() > 0 ? GT : GEQ; - } - - Node bAsNode = NodeBuilder<2>(kind) << varAsNode - << mkRationalNode(b.getNoninfinitesimalPart()); - - Node bestImplied = upperbound ? - d_propagator.getBestImpliedUpperBound(bAsNode): - d_propagator.getBestImpliedLowerBound(bAsNode); - - if(!bestImplied.isNull()){ - Node satValue = d_valuation.getSatValue(bestImplied); - if(satValue.isNull()){ - - Node reason = upperbound ? - d_partialModel.getUpperConstraint(var) : - d_partialModel.getLowerConstraint(var); - - //cout << getContext()->getLevel() << " " << bestImplied << " " << reason << endl; - if(EXPORT_LEMMA_INSTEAD_OF_PROPAGATE){ - Node lemma = NodeBuilder<2>(IMPLIES) << reason - << bestImplied; - - //Temporary - Node clause = BooleanSimplification::simplifyHornClause(lemma); - d_out->lemma(clause); - }else{ - Assert(!bestImplied.hasAttribute(Propagated())); - bestImplied.setAttribute(Propagated(), reason); - d_reasons.push_back(reason); - d_out->propagate(bestImplied); - } - }else{ - Assert(!satValue.isNull()); - Assert(satValue.getKind() == CONST_BOOLEAN); - Assert(satValue.getConst()); - } - } -} -*/ void TheoryArith::propagate(Effort e) { if(quickCheckOrMore(e)){ @@ -701,19 +586,7 @@ void TheoryArith::notifyRestart(){ if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); } ++d_restartsCounter; - /* - if(d_restartsCounter % d_tableauResetPeriod == 0){ - double currentDensity = d_tableau.densityMeasure(); - d_statistics.d_avgTableauDensityAtRestart.addEntry(currentDensity); - if(currentDensity >= d_tableauResetDensity * d_initialDensity){ - - ++d_statistics.d_tableauResets; - d_tableauResetPeriod += s_TABLEAU_RESET_INCREMENT; - d_tableauResetDensity += .2; - d_tableau = d_initialTableau; - } - } - */ + static const bool debugResetPolicy = false; uint32_t currSize = d_tableau.size(); -- 2.30.2