about summary refs log tree commit diff homepage
path: root/lib/Solver/IndependentSolver.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Solver/IndependentSolver.cpp')
-rw-r--r--lib/Solver/IndependentSolver.cpp33
1 files changed, 19 insertions, 14 deletions
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index d9fc77dc..3c0b9b26 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -15,6 +15,7 @@
 
 #include "klee/util/ExprUtil.h"
 
+#include "llvm/Support/raw_ostream.h"
 #include <map>
 #include <vector>
 #include <ostream>
@@ -60,7 +61,7 @@ public:
     return false;
   }
 
-  void print(std::ostream &os) const {
+  void print(llvm::raw_ostream &os) const {
     bool first = true;
     os << "{";
     for (typename set_ty::iterator it = s.begin(), ie = s.end(); 
@@ -76,8 +77,9 @@ public:
   }
 };
 
-template<class T>
-inline std::ostream &operator<<(std::ostream &os, const ::DenseSet<T> &dis) {
+template <class T>
+inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os,
+                                     const ::DenseSet<T> &dis) {
   dis.print(os);
   return os;
 }
@@ -124,7 +126,7 @@ public:
     return *this;
   }
 
-  void print(std::ostream &os) const {
+  void print(llvm::raw_ostream &os) const {
     os << "{";
     bool first = true;
     for (std::set<const Array*>::iterator it = wholeObjects.begin(), 
@@ -214,7 +216,8 @@ public:
   }
 };
 
-inline std::ostream &operator<<(std::ostream &os, const IndependentElementSet &ies) {
+inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os,
+                                     const IndependentElementSet &ies) {
   ies.print(os);
   return os;
 }
@@ -247,20 +250,22 @@ IndependentElementSet getIndependentConstraints(const Query& query,
     worklist.swap(newWorklist);
   } while (!done);
 
+#if 0
   if (0) {
     std::set< ref<Expr> > reqset(result.begin(), result.end());
-    std::cerr << "--\n";
-    std::cerr << "Q: " << query.expr << "\n";
-    std::cerr << "\telts: " << IndependentElementSet(query.expr) << "\n";
+    errs() << "--\n";
+    errs() << "Q: " << query.expr << "\n";
+    errs() << "\telts: " << IndependentElementSet(query.expr) << "\n";
     int i = 0;
-  for (ConstraintManager::const_iterator it = query.constraints.begin(), 
-         ie = query.constraints.end(); it != ie; ++it) {
-      std::cerr << "C" << i++ << ": " << *it;
-      std::cerr << " " << (reqset.count(*it) ? "(required)" : "(independent)") << "\n";
-      std::cerr << "\telts: " << IndependentElementSet(*it) << "\n";
+    for (ConstraintManager::const_iterator it = query.constraints.begin(),
+        ie = query.constraints.end(); it != ie; ++it) {
+      errs() << "C" << i++ << ": " << *it;
+      errs() << " " << (reqset.count(*it) ? "(required)" : "(independent)") << "\n";
+      errs() << "\telts: " << IndependentElementSet(*it) << "\n";
     }
-    std::cerr << "elts closure: " << eltsClosure << "\n";
+    errs() << "elts closure: " << eltsClosure << "\n";
   }
+#endif
 
   return eltsClosure;
 }