summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/arith/theory_arith.cpp29
-rw-r--r--src/theory/arith/theory_arith.h18
-rw-r--r--src/theory/theory_engine.h33
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback