diff options
author | Tim King <taking@cs.nyu.edu> | 2011-04-04 20:18:11 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-04-04 20:18:11 +0000 |
commit | 2935af06e3fae46418c10450df9e02465f0a8038 (patch) | |
tree | 39c1fbd55347ab44e665bfaff97e151a2c3e00a7 /src | |
parent | 97f2f155ad238f48b35050088c3cf60cc326b1f3 (diff) |
Reverts previous commit r1636.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 38 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 3 | ||||
-rw-r--r-- | src/theory/arith/unate_propagator.cpp | 6 | ||||
-rw-r--r-- | src/theory/arith/unate_propagator.h | 23 |
4 files changed, 23 insertions, 47 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 524cdcafe..c22b0019d 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), + d_propagator(c, out), d_simplex(d_partialModel, d_tableau), d_DELTA_ZERO(0), d_statistics() @@ -86,9 +86,7 @@ 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_diseqSplitCalls("theory::arith::diseqSplitCalls", 0), - d_diseqSplitTimer("theory::arith::diseqSplitTimer") + d_restartTimer("theory::arith::restartTimer") { StatisticsRegistry::registerStat(&d_statUserVariables); StatisticsRegistry::registerStat(&d_statSlackVariables); @@ -105,9 +103,6 @@ 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(){ @@ -126,9 +121,6 @@ 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) { @@ -176,15 +168,21 @@ 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; } @@ -421,9 +419,6 @@ void TheoryArith::check(Effort effortLevel){ } void TheoryArith::splitDisequalities(){ - TimerStat::CodeTimer codeTimer(d_statistics.d_diseqSplitTimer); - ++(d_statistics.d_diseqSplitCalls); - context::CDSet<Node, NodeHashFunction>::iterator it = d_diseq.begin(); context::CDSet<Node, NodeHashFunction>::iterator it_end = d_diseq.end(); for(; it != it_end; ++ it) { @@ -498,11 +493,6 @@ 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 bba2d19c0..85f554849 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -255,9 +255,6 @@ 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 9c7946712..069f4f0f3 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) : - d_orderedListMap() +ArithUnatePropagator::ArithUnatePropagator(context::Context* cxt, OutputChannel& out) : + d_arithOut(out), 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; - addLemma(imp); + d_arithOut.lemma(imp); } diff --git a/src/theory/arith/unate_propagator.h b/src/theory/arith/unate_propagator.h index ce78f281a..383b9f8e8 100644 --- a/src/theory/arith/unate_propagator.h +++ b/src/theory/arith/unate_propagator.h @@ -55,7 +55,6 @@ #include "theory/arith/ordered_set.h" #include <ext/hash_map> -#include <queue> namespace CVC4 { namespace theory { @@ -63,9 +62,11 @@ namespace arith { class ArithUnatePropagator { private: - typedef std::queue<Node> LemmaQueue; - /** Unate implication queue */ - LemmaQueue d_lemmas; + /** + * OutputChannel for the theory of arithmetic. + * The propagator uses this to pass implications back to the SAT solver. + */ + OutputChannel& d_arithOut; struct OrderedSetTriple { OrderedSet d_leqSet; @@ -78,7 +79,7 @@ private: NodeToOrderedSetMap d_orderedListMap; public: - ArithUnatePropagator(context::Context* cxt); + ArithUnatePropagator(context::Context* cxt, OutputChannel& arith); /** * Adds an atom to the propagator. @@ -89,19 +90,7 @@ 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); |