diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-18 10:20:18 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-18 10:20:18 -0600 |
commit | 5a8ec602967719f48a0bd76b84976a9504ae209b (patch) | |
tree | 23b1d4bee40cbe56bfcd7efb7c4b55885668cce2 /src/smt/process_assertions.cpp | |
parent | 639540664a763a2a552d659eb594b04fb2656f5b (diff) |
Minor cleanup of SmtEngine (#5450)
Diffstat (limited to 'src/smt/process_assertions.cpp')
-rw-r--r-- | src/smt/process_assertions.cpp | 37 |
1 files changed, 21 insertions, 16 deletions
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 387085de8..2011e7b83 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -52,8 +52,13 @@ class ScopeCounter unsigned& d_depth; }; -ProcessAssertions::ProcessAssertions(SmtEngine& smt, ResourceManager& rm) - : d_smt(smt), d_resourceManager(rm), d_preprocessingPassContext(nullptr) +ProcessAssertions::ProcessAssertions(SmtEngine& smt, + ResourceManager& rm, + SmtEngineStatistics& stats) + : d_smt(smt), + d_resourceManager(rm), + d_smtStats(stats), + d_preprocessingPassContext(nullptr) { d_true = NodeManager::currentNM()->mkConst(true); } @@ -127,7 +132,7 @@ bool ProcessAssertions::apply(Assertions& as) Chat() << "expanding definitions..." << endl; Trace("simplify") << "ProcessAssertions::simplify(): expanding definitions" << endl; - TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime); + TimerStat::CodeTimer codeTimer(d_smtStats.d_definitionExpansionTime); unordered_map<Node, Node, NodeHashFunction> cache; for (size_t i = 0, nasserts = assertions.size(); i < nasserts; ++i) { @@ -232,7 +237,7 @@ bool ProcessAssertions::apply(Assertions& as) d_passes["sep-skolem-emp"]->apply(&assertions); } - if (d_smt.d_logic.isQuantified()) + if (d_smt.getLogicInfo().isQuantified()) { // remove rewrite rules, apply pre-skolemization to existential quantifiers d_passes["quantifiers-preprocess"]->apply(&assertions); @@ -261,7 +266,7 @@ bool ProcessAssertions::apply(Assertions& as) } // rephrasing normal inputs as sygus problems - if (!d_smt.d_isInternalSubsolver) + if (!d_smt.isInternalSubsolver()) { if (options::sygusInference()) { @@ -281,7 +286,7 @@ bool ProcessAssertions::apply(Assertions& as) noConflict = simplifyAssertions(assertions); if (!noConflict) { - ++(d_smt.d_stats->d_simplifiedToFalse); + ++(d_smtStats.d_simplifiedToFalse); } Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-simplify" << endl; @@ -294,13 +299,13 @@ bool ProcessAssertions::apply(Assertions& as) Debug("smt") << " assertions : " << assertions.size() << endl; { - d_smt.d_stats->d_numAssertionsPre += assertions.size(); + d_smtStats.d_numAssertionsPre += assertions.size(); d_passes["ite-removal"]->apply(&assertions); // This is needed because when solving incrementally, removeITEs may // introduce skolems that were solved for earlier and thus appear in the // substitution map. d_passes["apply-substs"]->apply(&assertions); - d_smt.d_stats->d_numAssertionsPost += assertions.size(); + d_smtStats.d_numAssertionsPost += assertions.size(); } dumpAssertions("pre-repeat-simplify", assertions); @@ -456,7 +461,7 @@ bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions) if ( // check that option is on options::arithMLTrick() && // only useful in arith - d_smt.d_logic.isTheoryEnabled(THEORY_ARITH) && + d_smt.getLogicInfo().isTheoryEnabled(THEORY_ARITH) && // we add new assertions and need this (in practice, this // restriction only disables miplib processing during // re-simplification, which we don't expect to be useful anyway) @@ -550,7 +555,7 @@ Node ProcessAssertions::expandDefinitions( unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly) { - NodeManager* nm = d_smt.d_nodeManager; + NodeManager* nm = d_smt.getNodeManager(); std::stack<std::tuple<Node, Node, bool>> worklist; std::stack<Node> result; worklist.push(std::make_tuple(Node(n), Node(n), false)); @@ -577,9 +582,9 @@ Node ProcessAssertions::expandDefinitions( // we can short circuit (variable) leaves if (n.isVar()) { - SmtEngine::DefinedFunctionMap::const_iterator i = - d_smt.d_definedFunctions->find(n); - if (i != d_smt.d_definedFunctions->end()) + SmtEngine::DefinedFunctionMap* dfuns = d_smt.getDefinedFunctionMap(); + SmtEngine::DefinedFunctionMap::const_iterator i = dfuns->find(n); + if (i != dfuns->end()) { Node f = (*i).second.getFormula(); // must expand its definition @@ -651,9 +656,9 @@ Node ProcessAssertions::expandDefinitions( { // application of a user-defined symbol TNode func = n.getOperator(); - SmtEngine::DefinedFunctionMap::const_iterator i = - d_smt.d_definedFunctions->find(func); - if (i == d_smt.d_definedFunctions->end()) + SmtEngine::DefinedFunctionMap* dfuns = d_smt.getDefinedFunctionMap(); + SmtEngine::DefinedFunctionMap::const_iterator i = dfuns->find(func); + if (i == dfuns->end()) { throw TypeCheckingException( n.toExpr(), |