summaryrefslogtreecommitdiff
path: root/src/smt/process_assertions.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/process_assertions.cpp')
-rw-r--r--src/smt/process_assertions.cpp234
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,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback