Use ASTs in smt2_conv::convert_literal

This is in preparation for making convert_expr return an AST.

Author: romainbrenguier

src/solvers/smt2/smt2_conv.cpp

@@ -106,7 +106,7 @@ void smt2_convt::write_footer(std::ostream &os)
     forall_literals(it, assumptions)
     {
       os << "(assert ";
-      convert_literal(*it);
+      print(convert_literal(*it), out);
       os << ")"
          << "\n";
     }
@@ -655,32 +655,28 @@ literalt smt2_convt::convert(const exprt &expr)
 
   out << "; convert\n";
   out << "(define-fun ";
-  convert_literal(l);
+  print(convert_literal(l), out);
   out << " () Bool ";
   convert_expr(expr);
   out << ")" << "\n";
 
   return l;
 }
 
-void smt2_convt::convert_literal(const literalt l)
+smt2_astt smt2_convt::convert_literal(const literalt l)
 {
   if(l==const_literal(false))
-    out << "false";
-  else if(l==const_literal(true))
-    out << "true";
-  else
-  {
-    if(l.sign())
-      out << "(not ";
+    return smt2_astt("false");
+  if(l == const_literal(true))
+    return smt2_astt("true");
 
-    out << "|B" << l.var_no() << "|";
+  std::string literal_name = "B" + std::to_string(l.var_no());
+  smt2_identifiers.insert(literal_name);
+  auto literal_without_sign = smt2_astt("|" + literal_name + "|");
 
-    if(l.sign())
-      out << ")";
-
-    smt2_identifiers.insert("B"+std::to_string(l.var_no()));
-  }
+  if(!l.sign())
+    return literal_without_sign;
+  return smt2_not(std::move(literal_without_sign));
 }
 
 std::string smt2_convt::convert_identifier(const irep_idt &identifier)
@@ -1697,7 +1693,7 @@ void smt2_convt::convert_expr(const exprt &expr)
   }
   else if(expr.id()==ID_literal)
   {
-    convert_literal(to_literal_expr(expr).get_literal());
+    print(convert_literal(to_literal_expr(expr).get_literal()), out);
   }
   else if(expr.id()==ID_forall ||
           expr.id()==ID_exists)

src/solvers/smt2/smt2_conv.h

@@ -20,9 +20,10 @@ Author: Daniel Kroening, [email protected]
 #include <util/irep_hash_container.h>
 #endif
 
-#include <solvers/prop/prop_conv.h>
 #include <solvers/flattening/boolbv_width.h>
 #include <solvers/flattening/pointer_logic.h>
+#include <solvers/prop/prop_conv.h>
+#include <solvers/smt2/smt2_ast.h>
 
 class typecast_exprt;
 class constant_exprt;
@@ -131,7 +132,7 @@ class smt2_convt:public prop_convt
 
   void convert_expr(const exprt &);
   void convert_type(const typet &);
-  void convert_literal(const literalt);
+  smt2_astt convert_literal(const literalt);
 
   std::size_t get_number_of_solver_calls() const override;