Use ASTs in convert_expr

This is in preparation for making convert_expr return an AST.

Author: romainbrenguier

src/solvers/smt2/smt2_conv.cpp

@@ -928,28 +928,25 @@ void smt2_convt::convert_expr(const exprt &expr)
       "given expression should have at least two operands",
       expr.id_string());
 
-    out << "(";
-
-    if(expr.id()==ID_concatenation)
-      out << "concat";
-    else if(expr.id()==ID_bitand)
-      out << "bvand";
-    else if(expr.id()==ID_bitor)
-      out << "bvor";
-    else if(expr.id()==ID_bitxor)
-      out << "bvxor";
-    else if(expr.id()==ID_bitnand)
-      out << "bvnand";
-    else if(expr.id()==ID_bitnor)
-      out << "bvnor";
-
-    forall_operands(it, expr)
-    {
-      out << " ";
-      flatten2bv(*it);
-    }
+    auto node = make_shared_tree([&]{
+      if(expr.id()==ID_concatenation)
+        return "concat";
+      else if(expr.id()==ID_bitand)
+        return "bvand";
+      else if(expr.id()==ID_bitor)
+        return "bvor";
+      else if(expr.id()==ID_bitxor)
+        return "bvxor";
+      else if(expr.id()==ID_bitnand)
+        return "bvnand";
+      else if(expr.id()==ID_bitnor)
+        return "bvnor";
+      UNREACHABLE;
+    }());
 
-    out << ")";
+    for(const exprt &e : expr.operands())
+      node->add_child(flatten2bv(e));
+    print(node, out);
   }
   else if(expr.id()==ID_bitnot)
   {