summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/arith/approx_simplex.cpp2
-rw-r--r--src/theory/arith/approx_simplex.h1
-rw-r--r--src/theory/arith/dio_solver.h1
-rw-r--r--src/theory/arith/linear_equality.h1
-rw-r--r--src/theory/arith/simplex.cpp2
-rw-r--r--src/theory/arith/simplex.h1
-rw-r--r--src/theory/arith/theory_arith_private.cpp10
-rw-r--r--src/theory/arrays/array_info.cpp6
-rw-r--r--src/theory/arrays/array_info.h1
-rw-r--r--src/theory/bags/bags_rewriter.h1
-rw-r--r--src/theory/bags/bags_statistics.h1
-rw-r--r--src/theory/bv/abstraction.cpp2
-rw-r--r--src/theory/bv/abstraction.h1
-rw-r--r--src/theory/bv/bv_quick_check.cpp2
-rw-r--r--src/theory/bv/bv_quick_check.h1
-rw-r--r--src/theory/bv/bv_solver_lazy.cpp2
-rw-r--r--src/theory/bv/bv_subtheory_algebraic.cpp2
-rw-r--r--src/theory/quantifiers/quant_conflict_find.cpp4
-rw-r--r--src/theory/strings/sequences_stats.h1
-rw-r--r--src/theory/theory.h1
-rw-r--r--src/theory/theory_inference_manager.h1
-rw-r--r--src/theory/uf/symmetry_breaker.h1
22 files changed, 29 insertions, 16 deletions
diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index ed781fd5e..8d98475ce 100644
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -3001,7 +3001,7 @@ bool ApproxGLPK::guessCoefficientsConstructTableRow(int nid, int M, const Primit
for(size_t i=0; i < d_denomGuesses.size(); ++i){
const Integer& D = d_denomGuesses[i];
if(!guessCoefficientsConstructTableRow(nid, M, vec, D)){
- d_stats.d_averageGuesses.addEntry(i+1);
+ d_stats.d_averageGuesses << i+1;
Debug("approx::gmi") << "guesseditat " << i << " D=" << D << endl;
return false;
}
diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h
index 46e252ec7..a9b179e31 100644
--- a/src/theory/arith/approx_simplex.h
+++ b/src/theory/arith/approx_simplex.h
@@ -26,6 +26,7 @@
#include "util/maybe.h"
#include "util/rational.h"
#include "util/statistics_registry.h"
+#include "util/stats_timer.h"
namespace CVC4 {
namespace theory {
diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h
index 3ce7199c0..dc4711800 100644
--- a/src/theory/arith/dio_solver.h
+++ b/src/theory/arith/dio_solver.h
@@ -31,6 +31,7 @@
#include "theory/arith/normal_form.h"
#include "util/rational.h"
#include "util/statistics_registry.h"
+#include "util/stats_timer.h"
namespace CVC4 {
namespace context {
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index 3cfbfe5db..df4e5f30e 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -38,6 +38,7 @@
#include "theory/arith/tableau.h"
#include "util/maybe.h"
#include "util/statistics_registry.h"
+#include "util/stats_timer.h"
namespace CVC4 {
namespace theory {
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index fc3d919c3..df399d686 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -70,7 +70,7 @@ bool SimplexDecisionProcedure::standardProcessSignals(TimerStat &timer, IntStat&
Debug("recentlyViolated")
<< "It worked? "
- << conflicts.getData()
+ << conflicts.get()
<< " " << curr
<< " " << checkBasicForConflict(curr) << endl;
reportConflict(curr);
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 110093068..5edfc1608 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -62,6 +62,7 @@
#include "util/dense_map.h"
#include "util/result.h"
#include "util/statistics_registry.h"
+#include "util/stats_timer.h"
namespace CVC4 {
namespace theory {
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 1cf4a2993..1faad2a7a 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -2457,7 +2457,7 @@ void TheoryArithPrivate::subsumption(
std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex* approx, int nid, ConstraintP bc, int depth){
++(d_statistics.d_replayLogRecCount);
Debug("approx::replayLogRec") << "replayLogRec()"
- << d_statistics.d_replayLogRecCount.getData() << std::endl;
+ << d_statistics.d_replayLogRecCount.get() << std::endl;
size_t rpvars_size = d_replayVariables.size();
size_t rpcons_size = d_replayConstraints.size();
@@ -2892,7 +2892,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){
TimerStat::CodeTimer codeTimer0(d_statistics.d_solveIntTimer);
++(d_statistics.d_solveIntCalls);
- d_statistics.d_inSolveInteger.setData(1);
+ d_statistics.d_inSolveInteger.set(1);
if(!Theory::fullEffort(effortLevel)){
d_solveIntAttempts++;
@@ -3018,7 +3018,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){
}
}
- d_statistics.d_inSolveInteger.setData(0);
+ d_statistics.d_inSolveInteger.set(0);
}
SimplexDecisionProcedure& TheoryArithPrivate::selectSimplex(bool pass1){
@@ -3532,7 +3532,7 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
default:
Unimplemented();
}
- d_statistics.d_avgUnknownsInARow.addEntry(d_unknownsInARow);
+ d_statistics.d_avgUnknownsInARow << d_unknownsInARow;
size_t nPivots =
options::useFC() ? d_fcSimplex.getPivots() : d_dualSimplex.getPivots();
@@ -4366,7 +4366,7 @@ bool TheoryArithPrivate::unenqueuedVariablesAreConsistent(){
void TheoryArithPrivate::presolve(){
TimerStat::CodeTimer codeTimer(d_statistics.d_presolveTime);
- d_statistics.d_initialTableauSize.setData(d_tableau.size());
+ d_statistics.d_initialTableauSize.set(d_tableau.size());
if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
index 16126b88c..7919892c6 100644
--- a/src/theory/arrays/array_info.cpp
+++ b/src/theory/arrays/array_info.cpp
@@ -470,20 +470,20 @@ void ArrayInfo::mergeInfo(const TNode a, const TNode b){
if(s!= 0) {
- d_avgIndexListLength.addEntry(s);
+ d_avgIndexListLength << s;
++d_listsCount;
}
s = lista_st->size();
d_maxList.maxAssign(s);
if(s!= 0) {
- d_avgStoresListLength.addEntry(s);
+ d_avgStoresListLength << s;
++d_listsCount;
}
s = lista_inst->size();
d_maxList.maxAssign(s);
if(s!=0) {
- d_avgInStoresListLength.addEntry(s);
+ d_avgInStoresListLength << s;
++d_listsCount;
}
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index 499f96bfb..174980474 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -25,6 +25,7 @@
#include "context/cdlist.h"
#include "expr/node.h"
#include "util/statistics_registry.h"
+#include "util/stats_timer.h"
namespace CVC4 {
namespace theory {
diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h
index 51b2e5438..309b06009 100644
--- a/src/theory/bags/bags_rewriter.h
+++ b/src/theory/bags/bags_rewriter.h
@@ -20,6 +20,7 @@
#include "theory/bags/rewrites.h"
#include "theory/theory_rewriter.h"
#include "util/statistics_registry.h"
+#include "util/stats_histogram.h"
namespace CVC4 {
namespace theory {
diff --git a/src/theory/bags/bags_statistics.h b/src/theory/bags/bags_statistics.h
index f59c43cb6..c6b6c7e7a 100644
--- a/src/theory/bags/bags_statistics.h
+++ b/src/theory/bags/bags_statistics.h
@@ -19,6 +19,7 @@
#include "theory/bags/rewrites.h"
#include "util/statistics_registry.h"
+#include "util/stats_histogram.h"
namespace CVC4 {
namespace theory {
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index 157985cf1..3b9df3518 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -528,7 +528,7 @@ void AbstractionModule::finalizeSignatures()
d_funcToSignature[abs_func] = signature;
}
- d_statistics.d_numFunctionsAbstracted.setData(d_signatureToFunc.size());
+ d_statistics.d_numFunctionsAbstracted.set(d_signatureToFunc.size());
Debug("bv-abstraction") << "AbstractionModule::finalizeSignatures abstracted "
<< d_signatureToFunc.size() << " signatures. \n";
diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h
index 726cfd983..e22e221f2 100644
--- a/src/theory/bv/abstraction.h
+++ b/src/theory/bv/abstraction.h
@@ -25,6 +25,7 @@
#include "expr/node.h"
#include "theory/substitutions.h"
#include "util/statistics_registry.h"
+#include "util/stats_timer.h"
namespace CVC4 {
namespace theory {
diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp
index f9b5e80d2..36e77b0b7 100644
--- a/src/theory/bv/bv_quick_check.cpp
+++ b/src/theory/bv/bv_quick_check.cpp
@@ -347,7 +347,7 @@ Node QuickXPlain::minimizeConflict(TNode confl) {
// if (1.5* d_statistics.d_numUnknown.getData() > d_statistics.d_numSolved.getData()) {
// d_period = d_period * 2;
// }
- d_statistics.d_avgMinimizationRatio.addEntry(minimization_ratio);
+ d_statistics.d_avgMinimizationRatio << minimization_ratio;
return utils::mkAnd(minimized);
}
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index b10eb2811..f509c3cb4 100644
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -27,6 +27,7 @@
#include "prop/sat_solver_types.h"
#include "theory/bv/theory_bv_utils.h"
#include "util/statistics_registry.h"
+#include "util/stats_timer.h"
namespace CVC4 {
namespace theory {
diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp
index 7094c831e..9562b69c7 100644
--- a/src/theory/bv/bv_solver_lazy.cpp
+++ b/src/theory/bv/bv_solver_lazy.cpp
@@ -198,7 +198,7 @@ void BVSolverLazy::sendConflict()
Debug("bitvector") << indent() << "BVSolverLazy::check(): conflict "
<< d_conflictNode << std::endl;
d_im.conflict(d_conflictNode, InferenceId::BV_LAZY_CONFLICT);
- d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
+ d_statistics.d_avgConflictSize << d_conflictNode.getNumChildren();
d_conflictNode = Node::null();
}
}
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 38d94ea27..8f774e552 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -668,7 +668,7 @@ bool AlgebraicSolver::useHeuristic() {
return true;
double success_rate = double(d_numSolved)/double(d_numCalls);
- d_statistics.d_useHeuristic.setData(success_rate);
+ d_statistics.d_useHeuristic.set(success_rate);
return success_rate > 0.8;
}
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 17081bb7b..0aafbde56 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -2001,7 +2001,7 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
int prevEt = 0;
if (Trace.isOn("qcf-engine"))
{
- prevEt = d_statistics.d_entailment_checks.getData();
+ prevEt = d_statistics.d_entailment_checks.get();
clSet = double(clock()) / double(CLOCKS_PER_SEC);
Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level
<< "---" << std::endl;
@@ -2070,7 +2070,7 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;
}
Trace("qcf-engine") << std::endl;
- int currEt = d_statistics.d_entailment_checks.getData();
+ int currEt = d_statistics.d_entailment_checks.get();
if (currEt != prevEt)
{
Trace("qcf-engine") << " Entailment checks = " << (currEt - prevEt)
diff --git a/src/theory/strings/sequences_stats.h b/src/theory/strings/sequences_stats.h
index 1597e32a6..e4d122faf 100644
--- a/src/theory/strings/sequences_stats.h
+++ b/src/theory/strings/sequences_stats.h
@@ -21,6 +21,7 @@
#include "theory/strings/infer_info.h"
#include "theory/strings/rewrites.h"
#include "util/statistics_registry.h"
+#include "util/stats_histogram.h"
namespace CVC4 {
namespace theory {
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 68a2e1436..1c23d9041 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -37,6 +37,7 @@
#include "theory/trust_node.h"
#include "theory/valuation.h"
#include "util/statistics_registry.h"
+#include "util/stats_timer.h"
namespace CVC4 {
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index a599afa23..549d81c16 100644
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -26,6 +26,7 @@
#include "theory/output_channel.h"
#include "theory/trust_node.h"
#include "util/statistics_registry.h"
+#include "util/stats_histogram.h"
namespace CVC4 {
diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h
index 9b9cc79d0..2a95e5bc7 100644
--- a/src/theory/uf/symmetry_breaker.h
+++ b/src/theory/uf/symmetry_breaker.h
@@ -55,6 +55,7 @@
#include "expr/node_builder.h"
#include "smt/smt_statistics_registry.h"
#include "util/statistics_registry.h"
+#include "util/stats_timer.h"
namespace CVC4 {
namespace theory {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback