Make statistics output consistent. (#1647)

* Fixes --hide-zero-stats (and really skips the 0 values)
* Removes the additional newline after each statistic
* Introduces theory::getStatsPrefix(TheoryId) to generate consistent
  prefixes for statistics based on the theory id
  (e.g., THEORY_BV -> "theory::bv").

diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp
index f099b017aefda11f66ff77cb0402be06f5047e84..1917ea2d155f1eb0fd420ee272858188732e4ea4 100644 (file)
--- a/examples/sets-translate/sets_translate.cpp
+++ b/examples/sets-translate/sets_translate.cpp
@@ -314,7 +314,7 @@ int main(int argc, char* argv[])
             cout << SetBenchmarkLogicCommand(logicinfo.getLogicString()) << endl;
           }
         } else {
-          logicinfo.enableTheory(theory::THEORY_ARRAY);
+          logicinfo.enableTheory(theory::THEORY_ARRAYS);
           // we print logic string only for Quantifiers, for Z3 stuff
           // we don't set the logic
         }

diff --git a/src/expr/kind_template.cpp b/src/expr/kind_template.cpp
index 5f92af62253fed611225226692e39d785a54c7bb..aa9107a184800772587c8a826fbb81fa230220be 100644 (file)
--- a/src/expr/kind_template.cpp
+++ b/src/expr/kind_template.cpp
@@ -91,5 +91,15 @@ ${type_constant_to_theory_id}
   throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad type constant");
 }
 
+std::string getStatsPrefix(TheoryId theoryId) {
+  switch(theoryId) {
+${theory_stats_prefixes}
+#line 98 "${template}"
+  default:
+    break;
+  }
+  return "unknown";
+}
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */

diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 9247f50dd1988b9d45a8152f5d53056376b6990c..6ebbb32c2bc94ee56e921d5ffc2d86a50f754e8e 100644 (file)
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -99,6 +99,7 @@ CVC4_PUBLIC inline TheoryId& operator++(TheoryId& id) {
 std::ostream& operator<<(std::ostream& out, TheoryId theoryId);
 TheoryId kindToTheoryId(::CVC4::Kind k) CVC4_PUBLIC;
 TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) CVC4_PUBLIC;
+std::string getStatsPrefix(TheoryId theoryId) CVC4_PUBLIC;
 
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */

diff --git a/src/expr/mkkind b/src/expr/mkkind
index 2b1901f5dd37dcb8373e587e3613193bcffdae3f..5e5be7c4532cce097db81bb41ef763a12099e33d 100755 (executable)
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -75,6 +75,7 @@ seen_theory_builtin=false
 
 theory_enum=
 theory_descriptions=
+theory_stats_prefixes=
 
 function theory {
   # theory ID T header
@@ -108,6 +109,9 @@ function theory {
   theory_enum="${theory_enum}  $1,
 "
   theory_descriptions="${theory_descriptions}  case ${theory_id}: out << \"${theory_id}\"; break;
+"
+  prefix=$(echo "$theory_id" | tr '[:upper:]' '[:lower:]')
+  theory_stats_prefixes="${theory_stats_prefixes}  case ${theory_id}: return \"theory::${prefix#theory_}\"; break;
 "
 }
 
@@ -416,6 +420,7 @@ for var in \
     type_constant_groundterms \
     type_properties_includes \
     theory_descriptions \
+    theory_stats_prefixes \
     template \
     ; do
   eval text="\${text//\\\$\\{$var\\}/\${$var}}"

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index a7666dfcfc26ffa4f2871b97643ed5d49503c844..94c0c9e237b43efa188067de0ac4a44480b00084 100644 (file)
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -260,26 +260,29 @@ void CommandExecutor::printStatsFilterZeros(std::ostream& out,
 
   std::getline(iss, statName, ',');
 
-  while( !iss.eof() ) {
-
+  while (!iss.eof())
+  {
     std::getline(iss, statValue, '\n');
 
-    double curFloat;
-    std::istringstream iss_stat_value (statValue);
-    iss_stat_value >> curFloat;
-    bool isFloat = iss_stat_value.good();
+    bool skip = false;
+    try
+    {
+      double dval = std::stod(statValue);
+      skip = (dval == 0.0);
+    }
+    // Value can not be converted, don't skip
+    catch (const std::invalid_argument&) {}
+    catch (const std::out_of_range&) {}
 
-    if( (isFloat && curFloat == 0) ||
-        statValue == " \"0\"" ||
-        statValue == " \"[]\"") {
-      // skip
-    } else {
+    skip = skip || (statValue == " \"0\"" || statValue == " \"[]\"");
+
+    if (!skip)
+    {
       out << statName << "," << statValue << std::endl;
     }
 
     std::getline(iss, statName, ',');
   }
-
 }
 
 void CommandExecutor::flushOutputStreams() {

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index d55b9f54b5e25283a49947e6c5d62b4dc274df84..332c66be1b05f644f271de0dde27c8ab7c5d4707 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -317,7 +317,7 @@ bool Smt2::isOperatorEnabled(const std::string& name) const {
 bool Smt2::isTheoryEnabled(Theory theory) const {
   switch(theory) {
   case THEORY_ARRAYS:
-    return d_logic.isTheoryEnabled(theory::THEORY_ARRAY);
+    return d_logic.isTheoryEnabled(theory::THEORY_ARRAYS);
   case THEORY_BITVECTORS:
     return d_logic.isTheoryEnabled(theory::THEORY_BV);
   case THEORY_CORE:
@@ -477,7 +477,7 @@ void Smt2::setLogic(std::string name) {
     }
   }
 
-  if(d_logic.isTheoryEnabled(theory::THEORY_ARRAY)) {
+  if(d_logic.isTheoryEnabled(theory::THEORY_ARRAYS)) {
     addTheory(THEORY_ARRAYS);
   }
 

diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp
index 511a82617a83ecd5e1c59aa50ae3276f3de1445a..b0290fb3e3dde8ac549b626d37b3211fc0b73231 100644 (file)
--- a/src/proof/array_proof.cpp
+++ b/src/proof/array_proof.cpp
@@ -1232,9 +1232,9 @@ std::string ArrayProof::skolemToLiteral(Expr skolem) {
 }
 
 void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
-  Assert (theory::Theory::theoryOf(term) == theory::THEORY_ARRAY);
+  Assert (theory::Theory::theoryOf(term) == theory::THEORY_ARRAYS);
 
-  if (theory::Theory::theoryOf(term) != theory::THEORY_ARRAY) {
+  if (theory::Theory::theoryOf(term) != theory::THEORY_ARRAYS) {
     // We can get here, for instance, if there's a (select ite ...), e.g. a non-array term
     // hiding as a subterm of an array term. In that case, send it back to the dispatcher.
     d_proofEngine->printBoundTerm(term, os, map);

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 89adf6c2b90b1b7b2db46ec1b52a1719a0543e52..f0fdf38b53455e370c6cd214656c1261976fb380 100644 (file)
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -123,7 +123,7 @@ BitVectorProof* ProofManager::getBitVectorProof() {
 
 ArrayProof* ProofManager::getArrayProof() {
   Assert (options::proof());
-  TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_ARRAY);
+  TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_ARRAYS);
   return (ArrayProof*)pf;
 }
 

diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 47a1191ada28eb4eaac1a4f44b5b43ea861d43ae..0dd573dc6c693545bfe385092dfec2a81503cd64 100644 (file)
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -83,7 +83,7 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) {
         return;
       }
 
-      if (id == theory::THEORY_ARRAY) {
+      if (id == theory::THEORY_ARRAYS) {
         d_theoryProofTable[id] = new LFSCArrayProof((theory::arrays::TheoryArrays*)th, this);
         return;
       }
@@ -169,9 +169,9 @@ void TheoryProofEngine::registerTerm(Expr term) {
 
   // A special case: the array theory needs to know of every skolem, even if
   // it belongs to another theory (e.g., a BV skolem)
-  if (ProofManager::getSkolemizationManager()->isSkolem(term) && theory_id != theory::THEORY_ARRAY) {
+  if (ProofManager::getSkolemizationManager()->isSkolem(term) && theory_id != theory::THEORY_ARRAYS) {
     Debug("pf::tp::register") << "TheoryProofEngine::registerTerm: registering a non-array skolem: " << term << std::endl;
-    getTheoryProof(theory::THEORY_ARRAY)->registerTerm(term);
+    getTheoryProof(theory::THEORY_ARRAYS)->registerTerm(term);
   }
 
   d_registrationCache.insert(term);
@@ -272,7 +272,7 @@ void LFSCTheoryProofEngine::printSort(Type type, std::ostream& os) {
   }
 
   if (type.isArray()) {
-    getTheoryProof(theory::THEORY_ARRAY)->printOwnedSort(type, os);
+    getTheoryProof(theory::THEORY_ARRAYS)->printOwnedSort(type, os);
     return;
   }
 
@@ -989,7 +989,7 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
     th = new theory::uf::TheoryUF(&fakeContext, &fakeContext, oc, v,
                                   ProofManager::currentPM()->getLogicInfo(),
                                   "replay::");
-  } else if (d_theory->getId()==theory::THEORY_ARRAY) {
+  } else if (d_theory->getId()==theory::THEORY_ARRAYS) {
     th = new theory::arrays::TheoryArrays(&fakeContext, &fakeContext, oc, v,
                                           ProofManager::currentPM()->getLogicInfo(),
                                           "replay::");
@@ -1067,7 +1067,7 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
 }
 
 bool TheoryProofEngine::supportedTheory(theory::TheoryId id) {
-  return (id == theory::THEORY_ARRAY ||
+  return (id == theory::THEORY_ARRAYS ||
           id == theory::THEORY_ARITH ||
           id == theory::THEORY_BV ||
           id == theory::THEORY_UF ||

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index edd0d5a1162ae71d0189f4c7c3ea6083b45ab8d7..e3632c08d386f0858f755c0827ab6e35fad13872 100644 (file)
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -239,22 +239,18 @@ void BVMinisatSatSolver::toSatClause(const BVMinisat::Clause& clause,
 BVMinisatSatSolver::Statistics::Statistics(StatisticsRegistry* registry,
                                            const std::string& prefix)
     : d_registry(registry),
-      d_statStarts("theory::bv::" + prefix + "bvminisat::starts"),
-      d_statDecisions("theory::bv::" + prefix + "bvminisat::decisions"),
-      d_statRndDecisions("theory::bv::" + prefix + "bvminisat::rnd_decisions"),
-      d_statPropagations("theory::bv::" + prefix + "bvminisat::propagations"),
-      d_statConflicts("theory::bv::" + prefix + "bvminisat::conflicts"),
-      d_statClausesLiterals("theory::bv::" + prefix
-                            + "bvminisat::clauses_literals"),
-      d_statLearntsLiterals("theory::bv::" + prefix
-                            + "bvminisat::learnts_literals"),
-      d_statMaxLiterals("theory::bv::" + prefix + "bvminisat::max_literals"),
-      d_statTotLiterals("theory::bv::" + prefix + "bvminisat::tot_literals"),
-      d_statEliminatedVars("theory::bv::" + prefix
-                           + "bvminisat::eliminated_vars"),
-      d_statCallsToSolve("theory::bv::" + prefix
-                         + "bvminisat::calls_to_solve", 0),
-      d_statSolveTime("theory::bv::" + prefix + "bvminisat::solve_time"),
+      d_statStarts(prefix + "::bvminisat::starts"),
+      d_statDecisions(prefix + "::bvminisat::decisions"),
+      d_statRndDecisions(prefix + "::bvminisat::rnd_decisions"),
+      d_statPropagations(prefix + "::bvminisat::propagations"),
+      d_statConflicts(prefix + "::bvminisat::conflicts"),
+      d_statClausesLiterals(prefix + "::bvminisat::clauses_literals"),
+      d_statLearntsLiterals(prefix + "::bvminisat::learnts_literals"),
+      d_statMaxLiterals(prefix + "::bvminisat::max_literals"),
+      d_statTotLiterals(prefix + "::bvminisat::tot_literals"),
+      d_statEliminatedVars(prefix + "::bvminisat::eliminated_vars"),
+      d_statCallsToSolve(prefix + "::bvminisat::calls_to_solve", 0),
+      d_statSolveTime(prefix + "::bvminisat::solve_time"),
       d_registerStats(!prefix.empty())
 {
   if (!d_registerStats)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 74d6c1b1084ff93e5834694dc003d549d4abb5f3..ae00b4cafc0b7c59ed377f5b81da32fa36951fa4 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1502,7 +1502,7 @@ void SmtEngine::setDefaults() {
     d_logic = log;
     d_logic.lock();
   }
-  if(d_logic.isTheoryEnabled(THEORY_ARRAY) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_SETS)) {
+  if(d_logic.isTheoryEnabled(THEORY_ARRAYS) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_SETS)) {
     if(!d_logic.isTheoryEnabled(THEORY_UF)) {
       LogicInfo log(d_logic.getUnlockedCopy());
       Trace("smt") << "because a theory that permits Boolean terms is enabled, also enabling UF" << endl;
@@ -1528,9 +1528,9 @@ void SmtEngine::setDefaults() {
   }
 
   // If in arrays, set the UF handler to arrays
-  if(d_logic.isTheoryEnabled(THEORY_ARRAY) && ( !d_logic.isQuantified() ||
+  if(d_logic.isTheoryEnabled(THEORY_ARRAYS) && ( !d_logic.isQuantified() ||
      (d_logic.isQuantified() && !d_logic.isTheoryEnabled(THEORY_UF)))) {
-    Theory::setUninterpretedSortOwner(THEORY_ARRAY);
+    Theory::setUninterpretedSortOwner(THEORY_ARRAYS);
   } else {
     Theory::setUninterpretedSortOwner(THEORY_UF);
   }
@@ -1540,7 +1540,7 @@ void SmtEngine::setDefaults() {
   // QF_LIA logics. --K [2014/10/15]
   if(! options::doITESimp.wasSetByUser()) {
     bool qf_aufbv = !d_logic.isQuantified() &&
-      d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+      d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
       d_logic.isTheoryEnabled(THEORY_UF) &&
       d_logic.isTheoryEnabled(THEORY_BV);
     bool qf_lia = !d_logic.isQuantified() &&
@@ -1566,7 +1566,7 @@ void SmtEngine::setDefaults() {
   }
   if(! options::simplifyWithCareEnabled.wasSetByUser() ){
     bool qf_aufbv = !d_logic.isQuantified() &&
-      d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+      d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
       d_logic.isTheoryEnabled(THEORY_UF) &&
       d_logic.isTheoryEnabled(THEORY_BV);
 
@@ -1577,7 +1577,7 @@ void SmtEngine::setDefaults() {
   // Turn off array eager index splitting for QF_AUFLIA
   if(! options::arraysEagerIndexSplitting.wasSetByUser()) {
     if (not d_logic.isQuantified() &&
-        d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+        d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
         d_logic.isTheoryEnabled(THEORY_UF) &&
         d_logic.isTheoryEnabled(THEORY_ARITH)) {
       Trace("smt") << "setting array eager index splitting to false" << endl;
@@ -1587,8 +1587,8 @@ void SmtEngine::setDefaults() {
   // Turn on model-based arrays for QF_AX (unless models are enabled)
   // if(! options::arraysModelBased.wasSetByUser()) {
   //   if (not d_logic.isQuantified() &&
-  //       d_logic.isTheoryEnabled(THEORY_ARRAY) &&
-  //       d_logic.isPure(THEORY_ARRAY) &&
+  //       d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
+  //       d_logic.isPure(THEORY_ARRAYS) &&
   //       !options::produceModels() &&
   //       !options::checkModels()) {
   //     Trace("smt") << "turning on model-based array solver" << endl;
@@ -1598,7 +1598,7 @@ void SmtEngine::setDefaults() {
   // Turn on multiple-pass non-clausal simplification for QF_AUFBV
   if(! options::repeatSimp.wasSetByUser()) {
     bool repeatSimp = !d_logic.isQuantified() &&
-                      (d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+                      (d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
                       d_logic.isTheoryEnabled(THEORY_UF) &&
                       d_logic.isTheoryEnabled(THEORY_BV)) &&
                       !options::unsatCores();
@@ -1616,7 +1616,7 @@ void SmtEngine::setDefaults() {
                    !options::produceAssignments() &&
                    !options::checkModels() &&
                    !options::unsatCores() &&
-                   (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_BV));
+                   (d_logic.isTheoryEnabled(THEORY_ARRAYS) && d_logic.isTheoryEnabled(THEORY_BV));
     Trace("smt") << "setting unconstrained simplification to " << uncSimp << endl;
     options::unconstrainedSimp.set(uncSimp);
   }
@@ -1657,7 +1657,7 @@ void SmtEngine::setDefaults() {
   }
 
   if (! options::bvEagerExplanations.wasSetByUser() &&
-      d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+      d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
       d_logic.isTheoryEnabled(THEORY_BV)) {
     Trace("smt") << "enabling eager bit-vector explanations " << endl;
     options::bvEagerExplanations.set(true);
@@ -1720,13 +1720,13 @@ void SmtEngine::setDefaults() {
           ) ||
         // QF_AUFBV or QF_ABV or QF_UFBV
         (not d_logic.isQuantified() &&
-         (d_logic.isTheoryEnabled(THEORY_ARRAY) ||
+         (d_logic.isTheoryEnabled(THEORY_ARRAYS) ||
           d_logic.isTheoryEnabled(THEORY_UF)) &&
          d_logic.isTheoryEnabled(THEORY_BV)
          ) ||
         // QF_AUFLIA (and may be ends up enabling QF_AUFLRA?)
         (not d_logic.isQuantified() &&
-         d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+         d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
          d_logic.isTheoryEnabled(THEORY_UF) &&
          d_logic.isTheoryEnabled(THEORY_ARITH)
          ) ||
@@ -1747,7 +1747,7 @@ void SmtEngine::setDefaults() {
       d_logic.hasEverything() || d_logic.isTheoryEnabled(THEORY_STRINGS) ? false :
       ( // QF_AUFLIA
         (not d_logic.isQuantified() &&
-         d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+         d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
          d_logic.isTheoryEnabled(THEORY_UF) &&
          d_logic.isTheoryEnabled(THEORY_ARITH)
          ) ||

diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index be16d684df34d593f5f2b0f30886cac8e496e79b..2ae658e6b29f835e55b48ce07376694ef3ee1af5 100644 (file)
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -4,7 +4,7 @@
 # src/theory/builtin/kinds.
 #
 
-theory THEORY_ARRAY ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_arrays.h"
+theory THEORY_ARRAYS ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_arrays.h"
 typechecker "theory/arrays/theory_arrays_type_rules.h"
 
 properties polite stable-infinite parametric

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 508c9d8ff084fd895e49f97eb9ac050e2773898c..dfa543ff37229dedab8e5e2d76c704cc7396b1f9 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -58,7 +58,7 @@ const bool d_solveWrite2 = false;
 TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u,
                            OutputChannel& out, Valuation valuation,
                            const LogicInfo& logicInfo, std::string name)
-    : Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo, name),
+    : Theory(THEORY_ARRAYS, c, u, out, valuation, logicInfo, name),
       d_numRow(name + "theory::arrays::number of Row lemmas", 0),
       d_numExt(name + "theory::arrays::number of Ext lemmas", 0),
       d_numProp(name + "theory::arrays::number of propagations", 0),
@@ -69,15 +69,15 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u,
       d_numGetModelValConflicts(name + "theory::arrays::number of getModelVal conflicts", 0),
       d_numSetModelValSplits(name + "theory::arrays::number of setModelVal splits", 0),
       d_numSetModelValConflicts(name + "theory::arrays::number of setModelVal conflicts", 0),
-      d_ppEqualityEngine(u, name + "theory::arrays::TheoryArraysPP" , true),
+      d_ppEqualityEngine(u, name + "theory::arrays::pp" , true),
       d_ppFacts(u),
       //      d_ppCache(u),
       d_literalsToPropagate(c),
       d_literalsToPropagateIndex(c, 0),
       d_isPreRegistered(c),
-      d_mayEqualEqualityEngine(c, name + "theory::arrays::TheoryArraysMayEqual", true),
+      d_mayEqualEqualityEngine(c, name + "theory::arrays::mayEqual", true),
       d_notify(*this),
-      d_equalityEngine(d_notify, c, name + "theory::arrays::TheoryArrays", true),
+      d_equalityEngine(d_notify, c, name + "theory::arrays", true),
       d_conflict(c, false),
       d_backtracker(c),
       d_infoMap(c, &d_backtracker, name),
@@ -681,7 +681,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
 
     if (node.getType().isArray()) {
       d_mayEqualEqualityEngine.addTerm(node);
-      d_equalityEngine.addTriggerTerm(node, THEORY_ARRAY);
+      d_equalityEngine.addTriggerTerm(node, THEORY_ARRAYS);
     }
     else {
       d_equalityEngine.addTerm(node);
@@ -723,7 +723,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     if (d_equalityEngine.hasTerm(node)) {
       break;
     }
-    d_equalityEngine.addTriggerTerm(node, THEORY_ARRAY);
+    d_equalityEngine.addTriggerTerm(node, THEORY_ARRAYS);
 
     TNode a = d_equalityEngine.getRepresentative(node[0]);
 
@@ -786,7 +786,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     d_infoMap.setConstArr(node, node);
     d_mayEqualEqualityEngine.addTerm(node);
     Assert(d_mayEqualEqualityEngine.getRepresentative(node) == node);
-    d_equalityEngine.addTriggerTerm(node, THEORY_ARRAY);
+    d_equalityEngine.addTriggerTerm(node, THEORY_ARRAYS);
     d_defValues[node] = defaultValue;
     break;
   }
@@ -795,7 +795,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     if (node.getType().isArray()) {
       // The may equal needs the node
       d_mayEqualEqualityEngine.addTerm(node);
-      d_equalityEngine.addTriggerTerm(node, THEORY_ARRAY);
+      d_equalityEngine.addTriggerTerm(node, THEORY_ARRAYS);
       Assert(d_equalityEngine.getSize(node) == 1);
     }
     else {
@@ -849,7 +849,7 @@ Node TheoryArrays::explain(TNode literal, eq::EqProof* proof) {
 
 void TheoryArrays::addSharedTerm(TNode t) {
   Debug("arrays::sharing") << spaces(getSatContext()->getLevel()) << "TheoryArrays::addSharedTerm(" << t << ")" << std::endl;
-  d_equalityEngine.addTriggerTerm(t, THEORY_ARRAY);
+  d_equalityEngine.addTriggerTerm(t, THEORY_ARRAYS);
   if (t.getType().isArray()) {
     d_sharedArrays.insert(t);
   }
@@ -882,7 +882,7 @@ void TheoryArrays::checkPair(TNode r1, TNode r2)
 
   TNode x = r1[1];
   TNode y = r2[1];
-  Assert(d_equalityEngine.isTriggerTerm(x, THEORY_ARRAY));
+  Assert(d_equalityEngine.isTriggerTerm(x, THEORY_ARRAYS));
 
   if (d_equalityEngine.hasTerm(x) && d_equalityEngine.hasTerm(y) &&
       (d_equalityEngine.areEqual(x,y) || d_equalityEngine.areDisequal(x,y,false))) {
@@ -909,14 +909,14 @@ void TheoryArrays::checkPair(TNode r1, TNode r2)
     }
   }
 
-  if (!d_equalityEngine.isTriggerTerm(y, THEORY_ARRAY)) {
+  if (!d_equalityEngine.isTriggerTerm(y, THEORY_ARRAYS)) {
     Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): not connected to shared terms, skipping" << std::endl;
     return;
   }
 
   // Get representative trigger terms
-  TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_ARRAY);
-  TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_ARRAY);
+  TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_ARRAYS);
+  TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_ARRAYS);
   EqualityStatus eqStatusDomain = d_valuation.getEqualityStatus(x_shared, y_shared);
   switch (eqStatusDomain) {
     case EQUALITY_TRUE_AND_PROPAGATED:
@@ -987,11 +987,11 @@ void TheoryArrays::computeCareGraph()
       Assert(d_equalityEngine.hasTerm(r1));
       TNode x = r1[1];
 
-      if (!d_equalityEngine.isTriggerTerm(x, THEORY_ARRAY)) {
+      if (!d_equalityEngine.isTriggerTerm(x, THEORY_ARRAYS)) {
         Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): not connected to shared terms, skipping" << std::endl;
         continue;
       }
-      Node x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_ARRAY);
+      Node x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_ARRAYS);
 
       // Get the model value of index and find all reads that read from that same model value: these are the pairs we have to check
       // Also, insert this read in the list at the proper index

diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index a36ec2e163d7a3561122df47121f236eba7248c8..c04e8bde9ddba4063b70f7de00643d0dd67c82d0 100644 (file)
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -1111,9 +1111,10 @@ AbstractionModule::ArgsTableEntry& AbstractionModule::ArgsTable::getEntry(TNode
 }
 
 AbstractionModule::Statistics::Statistics(const std::string& name)
-  : d_numFunctionsAbstracted(name + "theory::bv::AbstractioModule::NumFunctionsAbstracted", 0)
-  , d_numArgsSkolemized(name + "theory::bv::AbstractioModule::NumArgsSkolemized", 0)
-  , d_abstractionTime(name + "theory::bv::AbstractioModule::AbstractionTime")
+    : d_numFunctionsAbstracted(name + "::abstraction::NumFunctionsAbstracted",
+                               0),
+      d_numArgsSkolemized(name + "::abstraction::NumArgsSkolemized", 0),
+      d_abstractionTime(name + "::abstraction::AbstractionTime")
 {
   smtStatisticsRegistry()->registerStat(&d_numFunctionsAbstracted);
   smtStatisticsRegistry()->registerStat(&d_numArgsSkolemized);

diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp
index 354b5837633041013bd6a7386b53222126127879..101b6417328c9427dfc16a4edc2a449f4967bb66 100644 (file)
--- a/src/theory/bv/bv_quick_check.cpp
+++ b/src/theory/bv/bv_quick_check.cpp
@@ -353,13 +353,13 @@ Node QuickXPlain::minimizeConflict(TNode confl) {
 }
 
 QuickXPlain::Statistics::Statistics(const std::string& name)
-  : d_xplainTime("theory::bv::"+name+"::QuickXplain::Time")
-  , d_numSolved("theory::bv::"+name+"::QuickXplain::NumSolved", 0)
-  , d_numUnknown("theory::bv::"+name+"::QuickXplain::NumUnknown", 0)
-  , d_numUnknownWasUnsat("theory::bv::"+name+"::QuickXplain::NumUnknownWasUnsat", 0)
-  , d_numConflictsMinimized("theory::bv::"+name+"::QuickXplain::NumConflictsMinimized", 0)
-  , d_finalPeriod("theory::bv::"+name+"::QuickXplain::FinalPeriod", 0)
-  , d_avgMinimizationRatio("theory::bv::"+name+"::QuickXplain::AvgMinRatio")
+  : d_xplainTime(name + "::QuickXplain::Time")
+  , d_numSolved(name + "::QuickXplain::NumSolved", 0)
+  , d_numUnknown(name + "::QuickXplain::NumUnknown", 0)
+  , d_numUnknownWasUnsat(name + "::QuickXplain::NumUnknownWasUnsat", 0)
+  , d_numConflictsMinimized(name + "::QuickXplain::NumConflictsMinimized", 0)
+  , d_finalPeriod(name + "::QuickXplain::FinalPeriod", 0)
+  , d_avgMinimizationRatio(name + "::QuickXplain::AvgMinRatio")
 {
   smtStatisticsRegistry()->registerStat(&d_xplainTime);
   smtStatisticsRegistry()->registerStat(&d_numSolved);

diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index d163bf7f96d2b4a3e2197b5d1ea464703255f23d..d941d018f40c23d41ecd65737065758eadc931a8 100644 (file)
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -117,7 +117,7 @@ class QuickXPlain {
     IntStat d_numConflictsMinimized;
     IntStat d_finalPeriod;
     AverageStat d_avgMinimizationRatio;
-    Statistics(const std::string&);
+    Statistics(const std::string& name);
     ~Statistics();
   };
   BVQuickCheck* d_solver;

diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 888c9569261f33cecb88a4a74c260c38c04363e3..456f627d0f182d5f4e14f6612e5e8eb23f8ed586 100644 (file)
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -229,7 +229,7 @@ void SubstitutionEx::storeCache(TNode from, TNode to, Node reason) {
 AlgebraicSolver::AlgebraicSolver(context::Context* c, TheoryBV* bv)
   : SubtheorySolver(c, bv)
   , d_modelMap(NULL)
-  , d_quickSolver(new BVQuickCheck("alg", bv))
+  , d_quickSolver(new BVQuickCheck("theory::bv::algebraic", bv))
   , d_isComplete(c, false)
   , d_isDifficult(c, false)
   , d_budget(options::bitvectorAlgebraicBudget())
@@ -239,7 +239,7 @@ AlgebraicSolver::AlgebraicSolver(context::Context* c, TheoryBV* bv)
   , d_numSolved(0)
   , d_numCalls(0)
   , d_ctx(new context::Context())
-  , d_quickXplain(options::bitvectorQuickXplain() ? new QuickXPlain("alg", d_quickSolver) : NULL)
+  , d_quickXplain(options::bitvectorQuickXplain() ? new QuickXPlain("theory::bv::algebraic", d_quickSolver) : NULL)
   , d_statistics()
 {}
 
@@ -778,14 +778,14 @@ Node AlgebraicSolver::getModelValue(TNode node) {
 }
 
 AlgebraicSolver::Statistics::Statistics()
-  : d_numCallstoCheck("theory::bv::AlgebraicSolver::NumCallsToCheck", 0)
-  , d_numSimplifiesToTrue("theory::bv::AlgebraicSolver::NumSimplifiesToTrue", 0)
-  , d_numSimplifiesToFalse("theory::bv::AlgebraicSolver::NumSimplifiesToFalse", 0)
-  , d_numUnsat("theory::bv::AlgebraicSolver::NumUnsat", 0)
-  , d_numSat("theory::bv::AlgebraicSolver::NumSat", 0)
-  , d_numUnknown("theory::bv::AlgebraicSolver::NumUnknown", 0)
-  , d_solveTime("theory::bv::AlgebraicSolver::SolveTime")
-  , d_useHeuristic("theory::bv::AlgebraicSolver::UseHeuristic", 0.2)
+  : d_numCallstoCheck("theory::bv::algebraic::NumCallsToCheck", 0)
+  , d_numSimplifiesToTrue("theory::bv::algebraic::NumSimplifiesToTrue", 0)
+  , d_numSimplifiesToFalse("theory::bv::algebraic::NumSimplifiesToFalse", 0)
+  , d_numUnsat("theory::bv::algebraic::NumUnsat", 0)
+  , d_numSat("theory::bv::algebraic::NumSat", 0)
+  , d_numUnknown("theory::bv::algebraic::NumUnknown", 0)
+  , d_solveTime("theory::bv::algebraic::SolveTime")
+  , d_useHeuristic("theory::bv::algebraic::UseHeuristic", 0.2)
 {
   smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
   smtStatisticsRegistry()->registerStat(&d_numSimplifiesToTrue);

diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 61bbf667d437d1cde122e45eae38d8a07afbb4ff..902a4dbe0352b643b7d75bc6540d31cdffcca95d 100644 (file)
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -36,9 +36,9 @@ namespace bv {
 
 BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv)
   : SubtheorySolver(c, bv),
-    d_bitblaster(new TLazyBitblaster(c, bv, bv->getFullInstanceName() + "lazy")),
+    d_bitblaster(new TLazyBitblaster(c, bv, "theory::bv::lazy")),
     d_bitblastQueue(c),
-    d_statistics(bv->getFullInstanceName()),
+    d_statistics(),
     d_validModelCache(c, true),
     d_lemmaAtomsQueue(c),
     d_useSatPropagation(options::bitvectorPropagate()),
@@ -54,9 +54,9 @@ BitblastSolver::~BitblastSolver() {
   delete d_bitblaster;
 }
 
-BitblastSolver::Statistics::Statistics(const std::string &instanceName)
-  : d_numCallstoCheck(instanceName + "theory::bv::BitblastSolver::NumCallsToCheck", 0)
-  , d_numBBLemmas(instanceName + "theory::bv::BitblastSolver::NumTimesLemmasBB", 0)
+BitblastSolver::Statistics::Statistics()
+  : d_numCallstoCheck("theory::bv::BitblastSolver::NumCallsToCheck", 0)
+  , d_numBBLemmas("theory::bv::BitblastSolver::NumTimesLemmasBB", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
   smtStatisticsRegistry()->registerStat(&d_numBBLemmas);

diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index f88810fcac6e97d8ea194a4414a4eff78b0a5750..509e59b1962b9d4e1cbb948ec2266ab71b764ef0 100644 (file)
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -39,7 +39,7 @@ class BitblastSolver : public SubtheorySolver {
   struct Statistics {
     IntStat d_numCallstoCheck;
     IntStat d_numBBLemmas;
-    Statistics(const std::string &instanceName);
+    Statistics();
     ~Statistics();
   };
   /** Bitblaster */

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 2c543b3dae8fd5bdf6f00a7d8cdf28a8a0334cce..bd4040dd77951175f146e2aab4c6609c5ffea3a7 100644 (file)
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -34,7 +34,7 @@ using namespace CVC4::theory::bv::utils;
 CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv)
   : SubtheorySolver(c, bv),
     d_notify(*this),
-    d_equalityEngine(d_notify, c, "theory::bv::TheoryBV", true),
+    d_equalityEngine(d_notify, c, "theory::bv::ee", true),
     d_slicer(new Slicer()),
     d_isComplete(c, true),
     d_lemmaThreshold(16),

diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp
index bed922830c4003d1fa9d5a642b7037208bfa8a9f..54c9cb08a1584f7c9d69a3e13c8efc23f7d95e9b 100644 (file)
--- a/src/theory/bv/bv_to_bool.cpp
+++ b/src/theory/bv/bv_to_bool.cpp
@@ -241,12 +241,12 @@ void BvToBoolPreprocessor::liftBvToBool(const std::vector<Node>& assertions, std
 }
 
 BvToBoolPreprocessor::Statistics::Statistics()
-  : d_numTermsLifted("theory::bv::BvToBoolPreprocess::NumberOfTermsLifted", 0)
-  , d_numAtomsLifted("theory::bv::BvToBoolPreprocess::NumberOfAtomsLifted", 0)
-  , d_numTermsForcedLifted("theory::bv::BvToBoolPreprocess::NumberOfTermsForcedLifted", 0)
-  , d_numTermsLowered("theory::bv::BvToBoolPreprocess::NumberOfTermsLowered", 0)
-  , d_numAtomsLowered("theory::bv::BvToBoolPreprocess::NumberOfAtomsLowered", 0)    
-  , d_numTermsForcedLowered("theory::bv::BvToBoolPreprocess::NumberOfTermsForcedLowered", 0)
+  : d_numTermsLifted("theory::bv::BvToBool::NumTermsLifted", 0)
+  , d_numAtomsLifted("theory::bv::BvToBool::NumAtomsLifted", 0)
+  , d_numTermsForcedLifted("theory::bv::BvToBool::NumTermsForcedLifted", 0)
+  , d_numTermsLowered("theory::bv::BvToBool::NumTermsLowered", 0)
+  , d_numAtomsLowered("theory::bv::BvToBool::NumAtomsLowered", 0)
+  , d_numTermsForcedLowered("theory::bv::BvToBool::NumTermsForcedLowered", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_numTermsLifted);
   smtStatisticsRegistry()->registerStat(&d_numAtomsLifted);

diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index 6cd4a3314f038a2d61b70fc4e6fa75fe58c5d38e..189898c0c2f5af7d6a6b90db60b7923e51395950 100644 (file)
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -369,13 +369,13 @@ void TLazyBitblaster::getConflict(std::vector<TNode>& conflict)
 }
 
 TLazyBitblaster::Statistics::Statistics(const std::string& prefix) :
-  d_numTermClauses("theory::bv::"+prefix+"::NumberOfTermSatClauses", 0),
-  d_numAtomClauses("theory::bv::"+prefix+"::NumberOfAtomSatClauses", 0),
-  d_numTerms("theory::bv::"+prefix+"::NumberOfBitblastedTerms", 0),
-  d_numAtoms("theory::bv::"+prefix+"::NumberOfBitblastedAtoms", 0),
-  d_numExplainedPropagations("theory::bv::"+prefix+"::NumberOfExplainedPropagations", 0),
-  d_numBitblastingPropagations("theory::bv::"+prefix+"::NumberOfBitblastingPropagations", 0),
-  d_bitblastTimer("theory::bv::"+prefix+"::BitblastTimer")
+  d_numTermClauses(prefix + "::NumTermSatClauses", 0),
+  d_numAtomClauses(prefix + "::NumAtomSatClauses", 0),
+  d_numTerms(prefix + "::NumBitblastedTerms", 0),
+  d_numAtoms(prefix + "::NumBitblastedAtoms", 0),
+  d_numExplainedPropagations(prefix + "::NumExplainedPropagations", 0),
+  d_numBitblastingPropagations(prefix + "::NumBitblastingPropagations", 0),
+  d_bitblastTimer(prefix + "::BitblastTimer")
 {
   smtStatisticsRegistry()->registerStat(&d_numTermClauses);
   smtStatisticsRegistry()->registerStat(&d_numAtomClauses);

diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index fa234fcde7d8e60cfcdf76a8e7505ca89794639a..4c4b7c72336b0bb9795cfe91f5c09b01f27808b8 100644 (file)
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -640,12 +640,12 @@ std::string UnionFind::debugPrint(TermId id) {
 }
 
 UnionFind::Statistics::Statistics():
-  d_numNodes("theory::bv::slicer::NumberOfNodes", 0),
-  d_numRepresentatives("theory::bv::slicer::NumberOfRepresentatives", 0),
-  d_numSplits("theory::bv::slicer::NumberOfSplits", 0),
-  d_numMerges("theory::bv::slicer::NumberOfMerges", 0),
+  d_numNodes("theory::bv::slicer::NumNodes", 0),
+  d_numRepresentatives("theory::bv::slicer::NumRepresentatives", 0),
+  d_numSplits("theory::bv::slicer::NumSplits", 0),
+  d_numMerges("theory::bv::slicer::NumMerges", 0),
   d_avgFindDepth("theory::bv::slicer::AverageFindDepth"),
-  d_numAddedEqualities("theory::bv::slicer::NumberOfEqualitiesAdded", Slicer::d_numAddedEqualities)
+  d_numAddedEqualities("theory::bv::slicer::NumEqualitiesAdded", Slicer::d_numAddedEqualities)
 {
   smtStatisticsRegistry()->registerStat(&d_numRepresentatives);
   smtStatisticsRegistry()->registerStat(&d_numSplits);

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index fd9ad0c6a48679f652a28e2fe376efad78f39418..47f2b9245e51f17c1ab78e6a79d97df31ad49c7b 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -51,7 +51,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u,
     d_sharedTermsSet(c),
     d_subtheories(),
     d_subtheoryMap(),
-    d_statistics(getFullInstanceName()),
+    d_statistics(),
     d_staticLearnCache(),
     d_BVDivByZero(),
     d_BVRemByZero(),
@@ -64,7 +64,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u,
     d_literalsToPropagateIndex(c, 0),
     d_propagatedBy(c),
     d_eagerSolver(NULL),
-    d_abstractionModule(new AbstractionModule(getFullInstanceName())),
+    d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))),
     d_isCoreTheory(false),
     d_calledPreregister(false),
     d_needsLastCallCheck(false),
@@ -130,14 +130,14 @@ void TheoryBV::spendResource(unsigned amount)
   getOutputChannel().spendResource(amount);
 }
 
-TheoryBV::Statistics::Statistics(const std::string &name):
-  d_avgConflictSize(name + "theory::bv::AvgBVConflictSize"),
-  d_solveSubstitutions(name + "theory::bv::NumberOfSolveSubstitutions", 0),
-  d_solveTimer(name + "theory::bv::solveTimer"),
-  d_numCallsToCheckFullEffort(name + "theory::bv::NumberOfFullCheckCalls", 0),
-  d_numCallsToCheckStandardEffort(name + "theory::bv::NumberOfStandardCheckCalls", 0),
-  d_weightComputationTimer(name + "theory::bv::weightComputationTimer"),
-  d_numMultSlice(name + "theory::bv::NumMultSliceApplied", 0)
+TheoryBV::Statistics::Statistics():
+  d_avgConflictSize("theory::bv::AvgBVConflictSize"),
+  d_solveSubstitutions("theory::bv::NumSolveSubstitutions", 0),
+  d_solveTimer("theory::bv::solveTimer"),
+  d_numCallsToCheckFullEffort("theory::bv::NumFullCheckCalls", 0),
+  d_numCallsToCheckStandardEffort("theory::bv::NumStandardCheckCalls", 0),
+  d_weightComputationTimer("theory::bv::weightComputationTimer"),
+  d_numMultSlice("theory::bv::NumMultSliceApplied", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_avgConflictSize);
   smtStatisticsRegistry()->registerStat(&d_solveSubstitutions);

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 1992c0ae3a1f55499b8b1b43bc2feee7f8681afd..90bd6275cebbe83551f68325ccc8a6683db5639b 100644 (file)
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -117,7 +117,7 @@ private:
     IntStat     d_numCallsToCheckStandardEffort;
     TimerStat   d_weightComputationTimer;
     IntStat     d_numMultSlice;
-    Statistics(const std::string &name);
+    Statistics();
     ~Statistics();
   };
 

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index d91eace99164c57f69aa447026634c49a1872505..18fadd05249d5c398edb1d6d3da4a49054f2719d 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -50,7 +50,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
       d_infer_exp(c),
       d_term_sk( u ),
       d_notify( *this ),
-      d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes", true),
+      d_equalityEngine(d_notify, c, "theory::datatypes", true),
       d_labels( c ),
       d_selector_apps( c ),
       //d_consEqc( c ),

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 5be4a46010355bed6cb7eb521fd99093acbdf976..748c5c1c648e9ce50ffb284b2394779093723b6f 100644 (file)
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -100,7 +100,7 @@ TheoryFp::TheoryFp(context::Context *c, context::UserContext *u,
                    const LogicInfo &logicInfo)
     : Theory(THEORY_FP, c, u, out, valuation, logicInfo),
       d_notification(*this),
-      d_equalityEngine(d_notification, c, "theory::fp::TheoryFp", true),
+      d_equalityEngine(d_notification, c, "theory::fp::ee", true),
       d_registeredTerms(u),
       d_conv(u),
       d_expansionRequested(false),

diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index a458eec304df96f75d0632f65e042bcb3be8cf77..9fe3b713f027a0df75543262dd7438ebd4a4d602 100644 (file)
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -264,7 +264,7 @@ std::string LogicInfo::getLogicString() const {
       if(!isQuantified()) {
         ss << "QF_";
       }
-      if(d_theories[THEORY_ARRAY]) {
+      if(d_theories[THEORY_ARRAYS]) {
         ss << (d_sharingTheories == 1 ? "AX" : "A");
         ++seen;
       }
@@ -385,11 +385,11 @@ void LogicInfo::setLogicString(std::string logicString)
       enableQuantifiers();
     }
     if(!strncmp(p, "AX", 2)) {
-      enableTheory(THEORY_ARRAY);
+      enableTheory(THEORY_ARRAYS);
       p += 2;
     } else {
       if(*p == 'A') {
-        enableTheory(THEORY_ARRAY);
+        enableTheory(THEORY_ARRAYS);
         ++p;
       }
       if(!strncmp(p, "UF", 2)) {

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 0107b80c8c3680920c6c03c3486a2035dd10142d..fd64a4ae61f8f4cf3950be2e31a6638c03ff1ddd 100644 (file)
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -39,7 +39,7 @@ TheorySep::TheorySep(context::Context* c, context::UserContext* u, OutputChannel
   Theory(THEORY_SEP, c, u, out, valuation, logicInfo),
   d_lemmas_produced_c(u),
   d_notify(*this),
-  d_equalityEngine(d_notify, c, "theory::sep::TheorySep", true),
+  d_equalityEngine(d_notify, c, "theory::sep::ee", true),
   d_conflict(c, false),
   d_reduce(u),
   d_infer(c),

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 6bafbb0de0cee0dabf391ea01b2c63d2e65dc67b..71857b7a58a2609b8e842fcc9fd01fa4019bb2e3 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -49,7 +49,7 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
   d_var_elim(u),
   d_external(external),
   d_notify(*this),
-  d_equalityEngine(d_notify, c, "theory::sets::TheorySetsPrivate", true),
+  d_equalityEngine(d_notify, c, "theory::sets::ee", true),
   d_conflict(c)
 {
 

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 17551b52839654c648fa150d54f60847dfb6374c..d0b3ec18165d3b8bea308a542a3df6eb77b0c1af 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -63,7 +63,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u,
     : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
       RMAXINT(LONG_MAX),
       d_notify( *this ),
-      d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings", true),
+      d_equalityEngine(d_notify, c, "theory::strings", true),
       d_conflict(c, false),
       d_infer(c),
       d_infer_exp(c),
@@ -3995,11 +3995,11 @@ Node TheoryStrings::ppRewrite(TNode atom) {
 
 // Stats
 TheoryStrings::Statistics::Statistics():
-  d_splits("TheoryStrings::NumOfSplitOnDemands", 0),
-  d_eq_splits("TheoryStrings::NumOfEqSplits", 0),
-  d_deq_splits("TheoryStrings::NumOfDiseqSplits", 0),
-  d_loop_lemmas("TheoryStrings::NumOfLoops", 0),
-  d_new_skolems("TheoryStrings::NumOfNewSkolems", 0)
+  d_splits("theory::strings::NumOfSplitOnDemands", 0),
+  d_eq_splits("theory::strings::NumOfEqSplits", 0),
+  d_deq_splits("theory::strings::NumOfDiseqSplits", 0),
+  d_loop_lemmas("theory::strings::NumOfLoops", 0),
+  d_new_skolems("theory::strings::NumOfNewSkolems", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_splits);
   smtStatisticsRegistry()->registerStat(&d_eq_splits);

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 069767968a980f6ecf26aede2c93466a4ee724c3..2ef4f42bf6e6bf860195a4abac835288a42788e6 100644 (file)
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -69,8 +69,8 @@ Theory::Theory(TheoryId id,
       d_careGraph(NULL),
       d_quantEngine(NULL),
       d_extTheory(NULL),
-      d_checkTime(getFullInstanceName() + "::checkTime"),
-      d_computeCareGraphTime(getFullInstanceName() + "::computeCareGraphTime"),
+      d_checkTime(getStatsPrefix(id) + "::checkTime"),
+      d_computeCareGraphTime(getStatsPrefix(id) + "::computeCareGraphTime"),
       d_sharedTerms(satContext),
       d_out(&out),
       d_valuation(valuation),
@@ -337,12 +337,6 @@ EntailmentCheckParameters::EntailmentCheckParameters(TheoryId tid)
   : d_tid(tid) {
 }
 
-std::string Theory::getFullInstanceName() const {
-  std::stringstream ss;
-  ss << "theory<" << d_id << ">" << d_instanceName;
-  return ss.str();
-}
-
 EntailmentCheckParameters::~EntailmentCheckParameters(){}
 
 TheoryId EntailmentCheckParameters::getTheoryId() const {

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 0571a67b7915899ab731be6ebf4056e4a410d0c3..f38cda90a65c3b72f2e1d045dadcbad6f45338ff 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -342,13 +342,6 @@ public:
     return d_id;
   }
 
-  /**
-   * Returns a string that uniquely identifies this theory solver w.r.t. the
-   * SmtEngine.
-   */
-  std::string getFullInstanceName() const;
-
-
   /**
    * Get the SAT context associated to this Theory.
    */

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index a6c42f5848e3f829c100d0d6c73c6fe276f63e3a..375027d34583972e6e585215c4af2b0773444ab6 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -2361,12 +2361,12 @@ bool TheoryEngine::useTheoryAlternative(const std::string& name) {
 
 
 TheoryEngine::Statistics::Statistics(theory::TheoryId theory):
-    conflicts(mkName("theory<", theory, ">::conflicts"), 0),
-    propagations(mkName("theory<", theory, ">::propagations"), 0),
-    lemmas(mkName("theory<", theory, ">::lemmas"), 0),
-    requirePhase(mkName("theory<", theory, ">::requirePhase"), 0),
-    flipDecision(mkName("theory<", theory, ">::flipDecision"), 0),
-    restartDemands(mkName("theory<", theory, ">::restartDemands"), 0)
+    conflicts(getStatsPrefix(theory) + "::conflicts", 0),
+    propagations(getStatsPrefix(theory) + "::propagations", 0),
+    lemmas(getStatsPrefix(theory) + "::lemmas", 0),
+    requirePhase(getStatsPrefix(theory) + "::requirePhase", 0),
+    flipDecision(getStatsPrefix(theory) + "::flipDecision", 0),
+    restartDemands(getStatsPrefix(theory) + "::restartDemands", 0)
 {
   smtStatisticsRegistry()->registerStat(&conflicts);
   smtStatisticsRegistry()->registerStat(&propagations);

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 38ddb1246bc5881abd02a9c77517b42f0cd1c0dd..b3fb8e2112479521f69db3d63ebd2fe0c5f9636b 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -47,8 +47,7 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u,
       /* The strong theory solver can be notified by EqualityEngine::init(),
        * so make sure it's initialized first. */
       d_thss(NULL),
-      d_equalityEngine(d_notify, c, instanceName + "theory::uf::TheoryUF",
-                       true),
+      d_equalityEngine(d_notify, c, instanceName + "theory::uf::ee", true),
       d_conflict(c, false),
       d_extensionality_deq(u),
       d_uf_std_skolem(u),

diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp
index 9273f21672871b93954aea561f128eef28f2bc5f..04078ef50657b44ef6dc8ba2a92cd7ceaca86a74 100644 (file)
--- a/src/util/statistics.cpp
+++ b/src/util/statistics.cpp
@@ -112,8 +112,8 @@ void StatisticsBase::flushInformation(std::ostream &out) const {
       out << d_prefix << s_regDelim;
     }
     s->flushStat(out);
-    out << std::endl;
   }
+  out << std::endl;
 #endif /* CVC4_STATISTICS_ON */
 }
 
@@ -126,8 +126,8 @@ void StatisticsBase::safeFlushInformation(int fd) const {
       safe_print(fd, s_regDelim);
     }
     s->safeFlushStat(fd);
-    safe_print(fd, "\n");
   }
+  safe_print(fd, "\n");
 #endif /* CVC4_STATISTICS_ON */
 }