Add bvt output helper

This is useful to debug the propositional encoding.

Author: tautschnig

src/solvers/prop/literal.cpp

@@ -20,3 +20,14 @@ std::ostream &operator << (std::ostream &out, literalt l)
   else
     return out << (l.sign()?"-":"") << l.var_no();
 }
+
+std::ostream &operator<<(std::ostream &out, const bvt &bv)
+{
+  for(auto it = bv.begin(); it != bv.end(); ++it)
+  {
+    out << *it;
+    if(std::next(it) != bv.end())
+      out << ' ';
+  }
+  return out;
+}

src/solvers/prop/literal.h

@@ -200,4 +200,6 @@ inline bool is_true (const literalt &l) { return (l.is_true()); }
 // bit-vectors
 typedef std::vector<literalt> bvt;
 
+std::ostream &operator<<(std::ostream &out, const bvt &bv);
+
 #endif // CPROVER_SOLVERS_PROP_LITERAL_H