fixup! Class for smt2 asts and functions for creating ASTs

Author: romainbrenguier

src/solvers/smt2/smt2_ast.cpp

@@ -133,11 +133,14 @@ static void print_data(std::ostream &stream, const smt2_astt &ast)
 {
   if(ast.id() == ID_symbol || ast.id() == ID_constant)
   {
-    stream << ast.read().named_sub.at(ID_value).id();
+    INVARIANT(
+      ast.read().named_sub.has_value(),
+      "constant and symbols should have an non-empty `named_sub` field");
+    stream << ast.read().named_sub.value();
   }
   else if(ast.id() == ID_string_constant)
   {
-    stream << '\"' << ast.read().named_sub.at(ID_value).id() << '\"';
+    stream << '\"' << ast.read().sub[0].id() << '\"';
   }
   else if(ast.id() == ID_tuple && ast.read().sub.empty())
   {

src/solvers/smt2/smt2_ast.h

@@ -18,6 +18,7 @@ Author: Romain Brenguier, [email protected]
 #include <util/invariant.h>
 #include <util/irep.h>
 #include <util/mp_arith.h>
+#include <util/optional.h>
 
 /// Base class for Abstract Syntax Tree of SMT2 expressions.
 /// Instances of this class are:
@@ -39,7 +40,7 @@ Author: Romain Brenguier, [email protected]
 ///   - \ref smt2_selector_declarationt, special case of \ref smt2_pairt
 ///   - \ref smt2_constructor_declarationt with id \c ID_declaration
 ///   - \ref smt2_datatype_declarationt with id \c ID_par
-class smt2_astt : public non_sharing_treet<smt2_astt>
+class smt2_astt : public non_sharing_treet<smt2_astt, optionalt<irep_idt>>
 {
 public:
   /// Empty constructor
@@ -69,9 +70,9 @@ class smt2_constantt : public smt2_astt
   }
 
 protected:
-  explicit smt2_constantt(irep_idt id) : smt2_astt(ID_constant)
+  explicit smt2_constantt(irep_idt value) : smt2_astt(ID_constant)
   {
-    write().named_sub[ID_value] = smt2_astt{std::move(id)};
+    write().named_sub = std::move(value);
   }
 };
 
@@ -96,7 +97,7 @@ class smt2_symbolt : public smt2_astt
 public:
   explicit smt2_symbolt(irep_idt symbol) : smt2_astt(ID_symbol)
   {
-    write().named_sub[ID_value] = smt2_astt(std::move(symbol));
+    write().named_sub = std::move(symbol);
   }
 };
 
@@ -106,7 +107,7 @@ class smt2_string_literalt : public smt2_astt
   explicit smt2_string_literalt(irep_idt literal)
     : smt2_astt(ID_string_constant)
   {
-    write().named_sub[ID_value] = smt2_astt(std::move(literal));
+    write().sub.emplace_back(std::move(literal));
   }
 };