From: Tim King Date: Thu, 3 Mar 2011 18:00:35 +0000 (+0000) Subject: - Creates a queue for lemmas discovered during the simplex procedure. Lemmas are... X-Git-Tag: cvc5-1.0.0~8673 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=43bf1fc1ba1770715fbe9fa15fa0be2cf6fb164a;p=cvc5.git - Creates a queue for lemmas discovered during the simplex procedure. Lemmas are sent to the sat solver during theory propagation. The lemmas currently come from additional conflicts that are discovered by findConflictOnTheQueue(...). --- diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 2053379d9..59b4e9bef 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -224,6 +224,18 @@ struct RightHandRationalLT } }; +inline Node negateConjunctionAsClause(TNode conjunction){ + Assert(conjunction.getKind() == kind::AND); + NodeBuilder<> orBuilder(kind::OR); + + for(TNode::iterator i = conjunction.begin(), end=conjunction.end(); i != end; ++i){ + TNode child = *i; + Node negatedChild = NodeBuilder<1>(kind::NOT)<<(child); + orBuilder << negatedChild; + } + return orBuilder; +} + }; /* namesapce arith */ }; /* namespace theory */ }; /* namespace CVC4 */ diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 0809e0788..68ab429ca 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -22,6 +22,7 @@ SimplexDecisionProcedure::Statistics::Statistics(): d_successAfterDiffSearch("theory::arith::successAfterDiffSearch",0), d_attemptDuringVarOrderSearch("theory::arith::attemptDuringVarOrderSearch",0), d_successDuringVarOrderSearch("theory::arith::successDuringVarOrderSearch",0), + d_delayedConflicts("theory::arith::delayedConflicts",0), d_pivotTime("theory::arith::pivotTime"), d_avgNumRowsNotContainingOnUpdate("theory::arith::avgNumRowsNotContainingOnUpdate"), d_avgNumRowsNotContainingOnPivot("theory::arith::avgNumRowsNotContainingOnPivot") @@ -41,6 +42,8 @@ SimplexDecisionProcedure::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_attemptDuringVarOrderSearch); StatisticsRegistry::registerStat(&d_successDuringVarOrderSearch); + StatisticsRegistry::registerStat(&d_delayedConflicts); + StatisticsRegistry::registerStat(&d_pivotTime); StatisticsRegistry::registerStat(&d_avgNumRowsNotContainingOnUpdate); @@ -63,6 +66,7 @@ SimplexDecisionProcedure::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_attemptDuringVarOrderSearch); StatisticsRegistry::unregisterStat(&d_successDuringVarOrderSearch); + StatisticsRegistry::unregisterStat(&d_delayedConflicts); StatisticsRegistry::unregisterStat(&d_pivotTime); StatisticsRegistry::unregisterStat(&d_avgNumRowsNotContainingOnUpdate); @@ -401,7 +405,7 @@ Node SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type) { case DuringVarOrderSearch: ++(d_statistics.d_attemptDuringVarOrderSearch); break; } - Node bestConflict = Node::null(); + Node firstConflict = Node::null(); ArithPriorityQueue::const_iterator i = d_queue.begin(); ArithPriorityQueue::const_iterator end = d_queue.end(); for(; i != end; ++i){ @@ -410,19 +414,22 @@ Node SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type) { if(d_tableau.isBasic(x_i)){ Node possibleConflict = checkBasicForConflict(x_i); if(!possibleConflict.isNull()){ - - bestConflict = betterConflict(bestConflict, possibleConflict); + if(firstConflict.isNull()){ + firstConflict = possibleConflict; + }else{ + delayConflictAsLemma(possibleConflict); + } } } } - if(!bestConflict.isNull()){ + if(!firstConflict.isNull()){ switch(type){ case BeforeDiffSearch: ++(d_statistics.d_successBeforeDiffSearch); break; case AfterDiffSearch: ++(d_statistics.d_successAfterDiffSearch); break; case DuringVarOrderSearch: ++(d_statistics.d_successDuringVarOrderSearch); break; } } - return bestConflict; + return firstConflict; } Node SimplexDecisionProcedure::updateInconsistentVars(){ diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index a32a188b4..b847259a0 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -16,7 +16,7 @@ #include "util/stats.h" -#include +#include namespace CVC4 { namespace theory { @@ -42,6 +42,9 @@ private: ArithVar d_numVariables; + std::vector d_delayedLemmas; + uint32_t d_delayedLemmasPos; + public: SimplexDecisionProcedure(const ArithConstants& constants, ArithPartialModel& pm, @@ -52,10 +55,13 @@ public: d_out(out), d_tableau(tableau), d_queue(pm, tableau), - d_numVariables(0) + d_numVariables(0), + d_delayedLemmas(), + d_delayedLemmasPos(0) {} - void increaseMax() {d_numVariables++;} + +public: /** * Assert*(n, orig) takes an bound n that is implied by orig. @@ -183,7 +189,33 @@ public: */ DeltaRational computeRowValue(ArithVar x, bool useSafe); + + void increaseMax() {d_numVariables++;} + + /** Returns true if the simplex procedure has more delayed lemmas in its queue.*/ + bool hasMoreLemmas() const { + return d_delayedLemmasPos < d_delayedLemmas.size(); + } + /** Returns the next delayed lemmas on the queue.*/ + Node popLemma(){ + Assert(hasMoreLemmas()); + Node lemma = d_delayedLemmas[d_delayedLemmasPos]; + ++d_delayedLemmasPos; + return lemma; + } + private: + /** Adds a lemma to the queue. */ + void pushLemma(Node lemma){ + d_delayedLemmas.push_back(lemma); + ++(d_statistics.d_delayedConflicts); + } + + /** Adds a conflict as a lemma to the queue. */ + void delayConflictAsLemma(Node conflict){ + Node negatedConflict = negateConjunctionAsClause(conflict); + pushLemma(negatedConflict); + } /** * Checks a basic variable, b, to see if it is in conflict. @@ -206,6 +238,8 @@ private: IntStat d_attemptAfterDiffSearch, d_successAfterDiffSearch; IntStat d_attemptDuringVarOrderSearch, d_successDuringVarOrderSearch; + IntStat d_delayedConflicts; + TimerStat d_pivotTime; AverageStat d_avgNumRowsNotContainingOnUpdate; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 3899e5e80..60eed27d1 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -556,7 +556,12 @@ void TheoryArith::explain(TNode n) { } void TheoryArith::propagate(Effort e) { - + if(quickCheckOrMore(e)){ + while(d_simplex.hasMoreLemmas()){ + Node lemma = d_simplex.popLemma(); + d_out->lemma(lemma); + } + } // if(quickCheckOrMore(e)){ // std::vector implied = d_propagator.getImpliedLiterals(); // for(std::vector::iterator i = implied.begin();