diff options
| -rw-r--r-- | lib/Expr/ExprSMTLIBPrinter.cpp | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp index d93411bf..c4a6876e 100644 --- a/lib/Expr/ExprSMTLIBPrinter.cpp +++ b/lib/Expr/ExprSMTLIBPrinter.cpp @@ -689,8 +689,10 @@ void ExprSMTLIBPrinter::scan(const ref<Expr> &e) { void ExprSMTLIBPrinter::scanBindingExprDeps() { if (!bindings.size()) return; + // Mutual dependency storage typedef std::map<const ref<Expr>, std::set<ref<Expr> > > ExprDepMap; + // A map from binding Expr (need abbreviating) "e" to the set of binding Expr // that are sub expressions of "e" (i.e. "e" uses these sub expressions). // usesSubExprMap[a].count(b) == 1 means that binding Expr "a" uses @@ -698,15 +700,18 @@ void ExprSMTLIBPrinter::scanBindingExprDeps() { // One can think of this map representing the "depends on" edges // in a "dependency graph" where nodes are binding Expr roots ExprDepMap usesSubExprMap; + // A map from Binding Expr "e" to the set of binding Expr that use "e" // subExprOfMap[a].count(b) == 1 means that binding Expr "a" is a sub Expr // of binding Expr "b". // One can think of this map as representing the edges in the previously // mentioned "dependency graph" except the direction of the edges - // has been reversed + // have been reversed ExprDepMap subExprOfMap; + // Working queue holding expressions with no dependencies std::vector<ref<Expr> > nonDepBindings; + // Iterate over bindings and collect dependencies for (BindingMap::const_iterator it = bindings.begin(); it != bindings.end(); ++it) { @@ -734,6 +739,7 @@ void ExprSMTLIBPrinter::scanBindingExprDeps() { nonDepBindings.push_back(it->first); } assert(nonDepBindings.size() && "there must be expr bindings with no deps"); + // Unroll the dependency tree starting with zero-dep expressions // and redefine bindings unsigned counter = 1; |