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";
     }
@@ -726,32 +726,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)
+std::shared_ptr<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_ast_symbol_leaf("false");
+  if(l==const_literal(true))
+    return smt2_ast_symbol_leaf("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_ast_symbol_leaf("|"+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(literal_without_sign);
 }
 
 std::string smt2_convt::convert_identifier(const irep_idt &identifier)
@@ -1755,7 +1751,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

@@ -23,6 +23,7 @@ Author: Daniel Kroening, [email protected]
 #include <solvers/prop/prop_conv.h>
 #include <solvers/flattening/boolbv_width.h>
 #include <solvers/flattening/pointer_logic.h>
+#include <solvers/smt2/smt2_ast.h>
 
 class typecast_exprt;
 class constant_exprt;
@@ -125,7 +126,7 @@ class smt2_convt:public prop_convt
   // new stuff
   void convert_expr(const exprt &);
   void convert_type(const typet &);
-  void convert_literal(const literalt);
+  std::shared_ptr<smt2_astt> convert_literal(const literalt);
 
 protected:
   const namespacet &ns;