diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 29 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 18 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 33 |
3 files changed, 72 insertions, 8 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 18bea2b8d..c16d8f183 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -54,11 +54,11 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) : d_constants(NodeManager::currentNM()), d_partialModel(c), d_diseq(c), - d_rewriter(&d_constants) + d_rewriter(&d_constants), + d_statistics() { uint64_t ass_id = partial_model::Assignment::getId(); Debug("arithsetup") << "Assignment: " << ass_id << std::endl; - } TheoryArith::~TheoryArith(){ for(vector<Node>::iterator i=d_variables.begin(); i!= d_variables.end(); ++i){ @@ -67,6 +67,20 @@ TheoryArith::~TheoryArith(){ } } +TheoryArith::Statistics::Statistics(): + d_statPivots("theory::arith::pivots",0), + d_statUpdates("theory::arith::updates",0), + d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0), + d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0), + d_statUpdateConflicts("theory::arith::UpdateConflicts", 0) +{ + StatisticsRegistry::registerStat(&d_statPivots); + StatisticsRegistry::registerStat(&d_statUpdates); + StatisticsRegistry::registerStat(&d_statAssertUpperConflicts); + StatisticsRegistry::registerStat(&d_statAssertLowerConflicts); + StatisticsRegistry::registerStat(&d_statUpdateConflicts); +} + bool isBasicSum(TNode n){ if(n.getKind() != kind::PLUS) return false; @@ -260,6 +274,7 @@ bool TheoryArith::AssertUpper(TNode n, TNode original){ Node lbc = d_partialModel.getLowerConstraint(x_i); Node conflict = NodeManager::currentNM()->mkNode(AND, lbc, original); Debug("arith") << "AssertUpper conflict " << conflict << endl; + ++(d_statistics.d_statAssertUpperConflicts); d_out->conflict(conflict); return true; } @@ -294,6 +309,7 @@ bool TheoryArith::AssertLower(TNode n, TNode original){ Node conflict = NodeManager::currentNM()->mkNode(AND, ubc, original); d_out->conflict(conflict); Debug("arith") << "AssertLower conflict " << conflict << endl; + ++(d_statistics.d_statAssertLowerConflicts); return true; } @@ -362,6 +378,7 @@ bool TheoryArith::AssertEquality(TNode n, TNode original){ void TheoryArith::update(TNode x_i, DeltaRational& v){ Assert(!isBasic(x_i)); DeltaRational assignment_x_i = d_partialModel.getAssignment(x_i); + ++(d_statistics.d_statUpdates); Debug("arith") <<"update " << x_i << ": " << assignment_x_i << "|-> " << v << endl; @@ -422,6 +439,7 @@ void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){ } } + ++(d_statistics.d_statPivots); d_tableau.pivot(x_i, x_j); checkBasicVariable(x_j); @@ -507,6 +525,7 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06 DeltaRational l_i = d_partialModel.getLowerBound(x_i); TNode x_j = selectSlackBelow(x_i); if(x_j == TNode::null() ){ + ++(d_statistics.d_statUpdateConflicts); return generateConflictBelow(x_i); //unsat } pivotAndUpdate(x_i, x_j, l_i); @@ -515,6 +534,7 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06 DeltaRational u_i = d_partialModel.getUpperBound(x_i); TNode x_j = selectSlackAbove(x_i); if(x_j == TNode::null() ){ + ++(d_statistics.d_statUpdateConflicts); return generateConflictAbove(x_i); //unsat } pivotAndUpdate(x_i, x_j, u_i); @@ -630,11 +650,6 @@ bool TheoryArith::assertionCases(TNode original, TNode assertion){ return AssertLower(assertion, original); case EQUAL: return AssertEquality(assertion,original); -// if(AssertUpper(assertion, original)){ -// return true; -// }else{ -// return AssertLower(assertion, original); -// } case NOT: { TNode atom = assertion[0]; diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index cb0705f4c..aff60f651 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -31,6 +31,8 @@ #include "theory/arith/arith_rewriter.h" #include "theory/arith/partial_model.h" +#include "util/stats.h" + #include <vector> #include <queue> @@ -94,6 +96,7 @@ private: */ ArithRewriter d_rewriter; + public: TheoryArith(context::Context* c, OutputChannel& out); ~TheoryArith(); @@ -115,6 +118,9 @@ public: void propagate(Effort e) { Unimplemented(); } void explain(TNode n, Effort e) { Unimplemented(); } + void shutdown(){ } + + private: /** * Assert*(n, orig) takes an bound n that is implied by orig. @@ -228,6 +234,18 @@ private: //TODO get rid of this! Node simulatePreprocessing(TNode n); + + /** These fields are designed to be accessable to TheoryArith methods. */ + class Statistics { + public: + IntStat d_statPivots, d_statUpdates, d_statAssertUpperConflicts; + IntStat d_statAssertLowerConflicts, d_statUpdateConflicts; + + Statistics(); + }; + + Statistics d_statistics; + }; }/* CVC4::theory::arith namespace */ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 1912cb026..bf4d8d10c 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -32,6 +32,8 @@ #include "theory/arrays/theory_arrays.h" #include "theory/bv/theory_bv.h" +#include "util/stats.h" + namespace CVC4 { // In terms of abstraction, this is below (and provides services to) @@ -74,24 +76,31 @@ class TheoryEngine { void conflict(TNode conflictNode, bool safe) throw(theory::Interrupted, AssertionException) { Debug("theory") << "EngineOutputChannel::conflict(" << conflictNode << ")" << std::endl; d_conflictNode = conflictNode; + ++(d_engine->d_statistics.d_statConflicts); if(safe) { throw theory::Interrupted(); } } void propagate(TNode, bool) throw(theory::Interrupted, AssertionException) { + ++(d_engine->d_statistics.d_statPropagate); } void lemma(TNode node, bool) throw(theory::Interrupted, AssertionException) { + ++(d_engine->d_statistics.d_statLemma); d_engine->newLemma(node); } void augmentingLemma(TNode node, bool) throw(theory::Interrupted, AssertionException) { + ++(d_engine->d_statistics.d_statAugLemma); d_engine->newAugmentingLemma(node); } void explanation(TNode, bool) throw(theory::Interrupted, AssertionException) { + ++(d_engine->d_statistics.d_statExplanatation); } }; + + EngineOutputChannel d_theoryOut; theory::booleans::TheoryBool d_bool; @@ -100,6 +109,7 @@ class TheoryEngine { theory::arrays::TheoryArrays d_arrays; theory::bv::TheoryBV d_bv; + /** * Check whether a node is in the rewrite cache or not. */ @@ -190,7 +200,8 @@ public: d_uf(ctxt, d_theoryOut), d_arith(ctxt, d_theoryOut), d_arrays(ctxt, d_theoryOut), - d_bv(ctxt, d_theoryOut) { + d_bv(ctxt, d_theoryOut), + d_statistics() { d_theoryOfTable.registerTheory(&d_bool); d_theoryOfTable.registerTheory(&d_uf); @@ -319,6 +330,26 @@ public: return d_theoryOut.d_conflictNode; } +private: + class Statistics { + public: + IntStat d_statConflicts, d_statPropagate, d_statLemma, d_statAugLemma, d_statExplanatation; + Statistics(): + d_statConflicts("theory::conlficts",0), + d_statPropagate("theory::propagate",0), + d_statLemma("theory::lemma",0), + d_statAugLemma("theory::aug_lemma", 0), + d_statExplanatation("theory::explanation", 0) + { + StatisticsRegistry::registerStat(&d_statConflicts); + StatisticsRegistry::registerStat(&d_statPropagate); + StatisticsRegistry::registerStat(&d_statLemma); + StatisticsRegistry::registerStat(&d_statAugLemma); + StatisticsRegistry::registerStat(&d_statExplanatation); + } + }; + Statistics d_statistics; + };/* class TheoryEngine */ }/* CVC4 namespace */ |