From: Tim King Date: Sat, 2 Apr 2011 21:05:47 +0000 (+0000) Subject: Delayed the addition of unate propagation lemmas until propagation is called. The... X-Git-Tag: cvc5-1.0.0~8618 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a2cc0337aa53cfb686e26d68f98f2ae176ff1337;p=cvc5.git Delayed the addition of unate propagation lemmas until propagation is called. The OutputChannel is now untouched by TheoryArith during preregistration. --- diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index c22b0019d..524cdcafe 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -66,7 +66,7 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out, Valuation valu d_presolveHasBeenCalled(false), d_tableauResetDensity(1.6), d_tableauResetPeriod(10), - d_propagator(c, out), + d_propagator(c), d_simplex(d_partialModel, d_tableau), d_DELTA_ZERO(0), d_statistics() @@ -86,7 +86,9 @@ TheoryArith::Statistics::Statistics(): //d_tableauSizeHistory("theory::arith::tableauSizeHistory"), d_currSetToSmaller("theory::arith::currSetToSmaller", 0), d_smallerSetToCurr("theory::arith::smallerSetToCurr", 0), - d_restartTimer("theory::arith::restartTimer") + d_restartTimer("theory::arith::restartTimer"), + d_diseqSplitCalls("theory::arith::diseqSplitCalls", 0), + d_diseqSplitTimer("theory::arith::diseqSplitTimer") { StatisticsRegistry::registerStat(&d_statUserVariables); StatisticsRegistry::registerStat(&d_statSlackVariables); @@ -103,6 +105,9 @@ TheoryArith::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_currSetToSmaller); StatisticsRegistry::registerStat(&d_smallerSetToCurr); StatisticsRegistry::registerStat(&d_restartTimer); + + StatisticsRegistry::registerStat(&d_diseqSplitCalls); + StatisticsRegistry::registerStat(&d_diseqSplitTimer); } TheoryArith::Statistics::~Statistics(){ @@ -121,6 +126,9 @@ TheoryArith::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_currSetToSmaller); StatisticsRegistry::unregisterStat(&d_smallerSetToCurr); StatisticsRegistry::unregisterStat(&d_restartTimer); + + StatisticsRegistry::unregisterStat(&d_diseqSplitCalls); + StatisticsRegistry::unregisterStat(&d_diseqSplitTimer); } void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) { @@ -168,21 +176,15 @@ void TheoryArith::preRegisterTerm(TNode n) { setupInitialValue(varN); } + if(n.getKind() == PLUS){ + Assert(!n.hasAttribute(Slack())); + setupSlack(n); + } + if(isRelationOperator(k)){ Assert(Comparison::isNormalAtom(n)); - - + Assert(n[0].getKind() != PLUS || (n[0]).hasAttribute(Slack()) ); d_propagator.addAtom(n); - - TNode left = n[0]; - TNode right = n[1]; - if(left.getKind() == PLUS){ - //We may need to introduce a slack variable. - Assert(left.getNumChildren() >= 2); - if(!left.hasAttribute(Slack())){ - setupSlack(left); - } - } } Debug("arith_preregister") << "end arith::preRegisterTerm("<< n <<")"<< endl; } @@ -419,6 +421,9 @@ void TheoryArith::check(Effort effortLevel){ } void TheoryArith::splitDisequalities(){ + TimerStat::CodeTimer codeTimer(d_statistics.d_diseqSplitTimer); + ++(d_statistics.d_diseqSplitCalls); + context::CDSet::iterator it = d_diseq.begin(); context::CDSet::iterator it_end = d_diseq.end(); for(; it != it_end; ++ it) { @@ -493,6 +498,11 @@ void TheoryArith::explain(TNode n) { } void TheoryArith::propagate(Effort e) { + while(d_propagator.hasMoreLemmas()){ + Node lemma = d_propagator.getNextLemma(); + d_out->lemma(lemma); + } + if(quickCheckOrMore(e)){ while(d_simplex.hasMoreLemmas()){ Node lemma = d_simplex.popLemma(); diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 85f554849..bba2d19c0 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -255,6 +255,9 @@ private: IntStat d_smallerSetToCurr; TimerStat d_restartTimer; + IntStat d_diseqSplitCalls; + TimerStat d_diseqSplitTimer; + Statistics(); ~Statistics(); }; diff --git a/src/theory/arith/unate_propagator.cpp b/src/theory/arith/unate_propagator.cpp index 069f4f0f3..9c7946712 100644 --- a/src/theory/arith/unate_propagator.cpp +++ b/src/theory/arith/unate_propagator.cpp @@ -30,8 +30,8 @@ using namespace CVC4::kind; using namespace std; -ArithUnatePropagator::ArithUnatePropagator(context::Context* cxt, OutputChannel& out) : - d_arithOut(out), d_orderedListMap() +ArithUnatePropagator::ArithUnatePropagator(context::Context* cxt) : + d_orderedListMap() { } bool ArithUnatePropagator::leftIsSetup(TNode left){ @@ -393,5 +393,5 @@ void ArithUnatePropagator::addImplication(TNode a, TNode b){ Debug("arith-propagate") << "ArithUnatePropagator::addImplication"; Debug("arith-propagate") << "(" << a << ", " << b <<")" << endl; - d_arithOut.lemma(imp); + addLemma(imp); } diff --git a/src/theory/arith/unate_propagator.h b/src/theory/arith/unate_propagator.h index 383b9f8e8..ce78f281a 100644 --- a/src/theory/arith/unate_propagator.h +++ b/src/theory/arith/unate_propagator.h @@ -55,6 +55,7 @@ #include "theory/arith/ordered_set.h" #include +#include namespace CVC4 { namespace theory { @@ -62,11 +63,9 @@ namespace arith { class ArithUnatePropagator { private: - /** - * OutputChannel for the theory of arithmetic. - * The propagator uses this to pass implications back to the SAT solver. - */ - OutputChannel& d_arithOut; + typedef std::queue LemmaQueue; + /** Unate implication queue */ + LemmaQueue d_lemmas; struct OrderedSetTriple { OrderedSet d_leqSet; @@ -79,7 +78,7 @@ private: NodeToOrderedSetMap d_orderedListMap; public: - ArithUnatePropagator(context::Context* cxt, OutputChannel& arith); + ArithUnatePropagator(context::Context* cxt); /** * Adds an atom to the propagator. @@ -90,7 +89,19 @@ public: /** Returns true if v has been added as a left hand side in an atom */ bool hasAnyAtoms(TNode v); + bool hasMoreLemmas() const { return !d_lemmas.empty(); } + + Node getNextLemma() { + Node lemma = d_lemmas.front(); + d_lemmas.pop(); + return lemma; + } private: + void addLemma(Node lemma) { + d_lemmas.push(lemma); + } + + OrderedSetTriple& getOrderedSetTriple(TNode left); OrderedSet& getEqSet(TNode left); OrderedSet& getLeqSet(TNode left); diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index 9de8f94b4..65437ba0e 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -159,6 +159,8 @@ public: d_arith->check(d_level); + TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 0u); + d_arith->propagate(d_level); Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1); @@ -196,6 +198,9 @@ public: d_arith->check(d_level); + TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 0u); + + d_arith->propagate(d_level); Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1); Node lt1ThenLeq1 = NodeBuilder<2>(IMPLIES) << lt1 << leq1; @@ -230,6 +235,8 @@ public: d_arith->check(d_level); + TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 0u); + d_arith->propagate(d_level); Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1); @@ -247,4 +254,29 @@ public: TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA); TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq0ThenLt1); } + + void testConflict() { + Node x = d_nm->mkVar(*d_realType); + Node c0 = d_nm->mkConst(d_zero); + Node c1 = d_nm->mkConst(d_one); + + Node leq0 = d_nm->mkNode(LEQ, x, c0); + Node leq1 = d_nm->mkNode(LEQ, x, c1); + Node gt1 = d_nm->mkNode(NOT, leq1); + + fakeTheoryEnginePreprocess(leq0); + fakeTheoryEnginePreprocess(leq1); + + d_arith->assertFact(leq0); + d_arith->assertFact(gt1); + + d_arith->check(d_level); + + + Node conf = d_nm->mkNode(AND, leq0, gt1); + TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 1u); + + TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), CONFLICT); + TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), conf); + } };