diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-26 04:43:19 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-26 11:43:19 +0100 |
commit | 70f0cddbce01fa17622b7b70b638794181aefec5 (patch) | |
tree | d49d38744a10ae902f38ef8508647329e01cb05b /src/smt/process_assertions.cpp | |
parent | c41a2e9be2422a211b9687833c97ba37485cd946 (diff) |
Move expand definitions to its own file (#5528)
We are changing our policy on how expand definitions is handled during preprocessing.
This will require some additions to expand definitions handling. This PR makes a standalone module for expanding definitions.
Diffstat (limited to 'src/smt/process_assertions.cpp')
-rw-r--r-- | src/smt/process_assertions.cpp | 234 |
1 files changed, 3 insertions, 231 deletions
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 2011e7b83..c68b73336 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -53,9 +53,11 @@ class ScopeCounter }; ProcessAssertions::ProcessAssertions(SmtEngine& smt, + ExpandDefs& exDefs, ResourceManager& rm, SmtEngineStatistics& stats) : d_smt(smt), + d_exDefs(exDefs), d_resourceManager(rm), d_smtStats(stats), d_preprocessingPassContext(nullptr) @@ -128,21 +130,7 @@ bool ProcessAssertions::apply(Assertions& as) << "ProcessAssertions::processAssertions() : pre-definition-expansion" << endl; dumpAssertions("pre-definition-expansion", assertions); - { - Chat() << "expanding definitions..." << endl; - Trace("simplify") << "ProcessAssertions::simplify(): expanding definitions" - << endl; - TimerStat::CodeTimer codeTimer(d_smtStats.d_definitionExpansionTime); - unordered_map<Node, Node, NodeHashFunction> cache; - for (size_t i = 0, nasserts = assertions.size(); i < nasserts; ++i) - { - Node expd = expandDefinitions(assertions[i], cache); - if (expd != assertions[i]) - { - assertions.replace(i, expd); - } - } - } + d_exDefs.expandAssertions(assertions, false); Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-definition-expansion" << endl; @@ -550,222 +538,6 @@ void ProcessAssertions::dumpAssertions(const char* key, } } -Node ProcessAssertions::expandDefinitions( - TNode n, - unordered_map<Node, Node, NodeHashFunction>& cache, - bool expandOnly) -{ - 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)); - // The worklist is made of triples, each is input / original node then the - // output / rewritten node and finally a flag tracking whether the children - // have been explored (i.e. if this is a downward or upward pass). - - do - { - spendResource(ResourceManager::Resource::PreprocessStep); - - // n is the input / original - // node is the output / result - Node node; - bool childrenPushed; - std::tie(n, node, childrenPushed) = worklist.top(); - worklist.pop(); - - // Working downwards - if (!childrenPushed) - { - Kind k = n.getKind(); - - // we can short circuit (variable) leaves - if (n.isVar()) - { - 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 - Node fe = expandDefinitions(f, cache, expandOnly); - // replacement must be closed - if ((*i).second.getFormals().size() > 0) - { - result.push( - nm->mkNode(LAMBDA, - nm->mkNode(BOUND_VAR_LIST, (*i).second.getFormals()), - fe)); - continue; - } - // don't bother putting in the cache - result.push(fe); - continue; - } - // don't bother putting in the cache - result.push(n); - continue; - } - - // maybe it's in the cache - unordered_map<Node, Node, NodeHashFunction>::iterator cacheHit = - cache.find(n); - if (cacheHit != cache.end()) - { - TNode ret = (*cacheHit).second; - result.push(ret.isNull() ? n : ret); - continue; - } - - // otherwise expand it - bool doExpand = false; - if (k == APPLY_UF) - { - // Always do beta-reduction here. The reason is that there may be - // operators such as INTS_MODULUS in the body of the lambda that would - // otherwise be introduced by beta-reduction via the rewriter, but are - // not expanded here since the traversal in this function does not - // traverse the operators of nodes. Hence, we beta-reduce here to - // ensure terms in the body of the lambda are expanded during this - // call. - if (n.getOperator().getKind() == LAMBDA) - { - doExpand = true; - } - else - { - // We always check if this operator corresponds to a defined function. - doExpand = d_smt.isDefinedFunction(n.getOperator().toExpr()); - } - } - if (doExpand) - { - vector<Node> formals; - TNode fm; - if (n.getOperator().getKind() == LAMBDA) - { - TNode op = n.getOperator(); - // lambda - for (unsigned i = 0; i < op[0].getNumChildren(); i++) - { - formals.push_back(op[0][i]); - } - fm = op[1]; - } - else - { - // application of a user-defined symbol - TNode func = n.getOperator(); - SmtEngine::DefinedFunctionMap* dfuns = d_smt.getDefinedFunctionMap(); - SmtEngine::DefinedFunctionMap::const_iterator i = dfuns->find(func); - if (i == dfuns->end()) - { - throw TypeCheckingException( - n.toExpr(), - string("Undefined function: `") + func.toString() + "'"); - } - DefinedFunction def = (*i).second; - formals = def.getFormals(); - - if (Debug.isOn("expand")) - { - Debug("expand") << "found: " << n << endl; - Debug("expand") << " func: " << func << endl; - string name = func.getAttribute(expr::VarNameAttr()); - Debug("expand") << " : \"" << name << "\"" << endl; - } - if (Debug.isOn("expand")) - { - Debug("expand") << " defn: " << def.getFunction() << endl - << " ["; - if (formals.size() > 0) - { - copy(formals.begin(), - formals.end() - 1, - ostream_iterator<Node>(Debug("expand"), ", ")); - Debug("expand") << formals.back(); - } - Debug("expand") << "]" << endl - << " " << def.getFunction().getType() << endl - << " " << def.getFormula() << endl; - } - - fm = def.getFormula(); - } - - Node instance = fm.substitute(formals.begin(), - formals.end(), - n.begin(), - n.begin() + formals.size()); - Debug("expand") << "made : " << instance << endl; - - Node expanded = expandDefinitions(instance, cache, expandOnly); - cache[n] = (n == expanded ? Node::null() : expanded); - result.push(expanded); - continue; - } - else if (!expandOnly) - { - // do not do any theory stuff if expandOnly is true - - theory::Theory* t = d_smt.getTheoryEngine()->theoryOf(node); - - Assert(t != NULL); - TrustNode trn = t->expandDefinition(n); - node = trn.isNull() ? Node(n) : trn.getNode(); - } - - // the partial functions can fall through, in which case we still - // consider their children - worklist.push(std::make_tuple( - Node(n), node, true)); // Original and rewritten result - - for (size_t i = 0; i < node.getNumChildren(); ++i) - { - worklist.push( - std::make_tuple(node[i], - node[i], - false)); // Rewrite the children of the result only - } - } - else - { - // Working upwards - // Reconstruct the node from it's (now rewritten) children on the stack - - Debug("expand") << "cons : " << node << endl; - if (node.getNumChildren() > 0) - { - // cout << "cons : " << node << endl; - NodeBuilder<> nb(node.getKind()); - if (node.getMetaKind() == metakind::PARAMETERIZED) - { - Debug("expand") << "op : " << node.getOperator() << endl; - // cout << "op : " << node.getOperator() << endl; - nb << node.getOperator(); - } - for (size_t i = 0, nchild = node.getNumChildren(); i < nchild; ++i) - { - Assert(!result.empty()); - Node expanded = result.top(); - result.pop(); - // cout << "exchld : " << expanded << endl; - Debug("expand") << "exchld : " << expanded << endl; - nb << expanded; - } - node = nb; - } - // Only cache once all subterms are expanded - cache[n] = n == node ? Node::null() : node; - result.push(node); - } - } while (!worklist.empty()); - - AlwaysAssert(result.size() == 1); - - return result.top(); -} - void ProcessAssertions::collectSkolems( IteSkolemMap& iskMap, TNode n, |