diff options
Diffstat (limited to 'src/theory')
24 files changed, 96 insertions, 109 deletions
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index be16d684d..2ae658e6b 100644 --- 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 508c9d8ff..dfa543ff3 100644 --- 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 a36ec2e16..c04e8bde9 100644 --- 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 354b58376..101b64173 100644 --- 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 d163bf7f9..d941d018f 100644 --- 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 888c95692..456f627d0 100644 --- 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 61bbf667d..902a4dbe0 100644 --- 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 f88810fca..509e59b19 100644 --- 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 2c543b3da..bd4040dd7 100644 --- 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 bed922830..54c9cb08a 100644 --- 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 6cd4a3314..189898c0c 100644 --- 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 fa234fcde..4c4b7c723 100644 --- 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 fd9ad0c6a..47f2b9245 100644 --- 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 1992c0ae3..90bd6275c 100644 --- 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 d91eace99..18fadd052 100644 --- 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 5be4a4601..748c5c1c6 100644 --- 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 a458eec30..9fe3b713f 100644 --- 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 0107b80c8..fd64a4ae6 100644 --- 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 6bafbb0de..71857b7a5 100644 --- 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 17551b528..d0b3ec181 100644 --- 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 069767968..2ef4f42bf 100644 --- 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 0571a67b7..f38cda90a 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -343,13 +343,6 @@ public: } /** - * 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. */ context::Context* getSatContext() const { diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index a6c42f584..375027d34 100644 --- 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 38ddb1246..b3fb8e211 100644 --- 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), |