diff options
author | Tim King <taking@cs.nyu.edu> | 2010-06-18 22:24:59 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-06-18 22:24:59 +0000 |
commit | fd6af9181e763cd9564245114cfa47f3952484db (patch) | |
tree | 0b058ad4e0624f1bf11ed9c65d63a4cfbdbdc66e /src/theory | |
parent | 968f250b473d97db537aa7628bf111d15a2db299 (diff) |
Merging the statistics branch into the main trunk. I'll go over how to use this Tuesday during the meeting. You'll need to run autogen and receonfigure after updating.
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 */ |