diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/approx_simplex.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/approx_simplex.h | 1 | ||||
-rw-r--r-- | src/theory/arith/dio_solver.h | 1 | ||||
-rw-r--r-- | src/theory/arith/linear_equality.h | 1 | ||||
-rw-r--r-- | src/theory/arith/simplex.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/simplex.h | 1 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 10 | ||||
-rw-r--r-- | src/theory/arrays/array_info.cpp | 6 | ||||
-rw-r--r-- | src/theory/arrays/array_info.h | 1 | ||||
-rw-r--r-- | src/theory/bags/bags_rewriter.h | 1 | ||||
-rw-r--r-- | src/theory/bags/bags_statistics.h | 1 | ||||
-rw-r--r-- | src/theory/bv/abstraction.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/abstraction.h | 1 | ||||
-rw-r--r-- | src/theory/bv/bv_quick_check.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_quick_check.h | 1 | ||||
-rw-r--r-- | src/theory/bv/bv_solver_lazy.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_algebraic.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 4 | ||||
-rw-r--r-- | src/theory/strings/sequences_stats.h | 1 | ||||
-rw-r--r-- | src/theory/theory.h | 1 | ||||
-rw-r--r-- | src/theory/theory_inference_manager.h | 1 | ||||
-rw-r--r-- | src/theory/uf/symmetry_breaker.h | 1 |
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 { |