aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorDan Liew <daniel.liew@imperial.ac.uk>2014-12-13 16:07:01 +0000
committerDan Liew <daniel.liew@imperial.ac.uk>2014-12-13 16:07:01 +0000
commit5acb6356d1fdf6b87c8669e8eb88c720b8dc3ee9 (patch)
treef4b4267158dd5ba37748fe283feece662044e741
parent381de54fc6b9a73bb296ec92198f7789c457e818 (diff)
downloadklee-5acb6356d1fdf6b87c8669e8eb88c720b8dc3ee9.tar.gz
Add a few line breaks to make the code more readable in
ExprSMTLIBPrinter
-rw-r--r--lib/Expr/ExprSMTLIBPrinter.cpp8
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;