smt2 id_map: Do not use nil_typet when we mean "optional"

Use optionalt<typet> instead. nil_typet is deprecated.

Author: tautschnig

src/solvers/smt2/smt2_parser.cpp

@@ -120,7 +120,7 @@ exprt::operandst smt2_parsert::operands()
 
 irep_idt smt2_parsert::get_fresh_id(const irep_idt &id)
 {
-  if(id_map[id].type.is_nil())
+  if(!id_map[id].type.has_value())
     return id; // id not yet used
 
   auto &count=renaming_counters[id];
@@ -754,16 +754,15 @@ exprt smt2_parsert::function_application()
         auto id_it=id_map.find(final_id);
         if(id_it!=id_map.end())
         {
-          if(id_it->second.type.id()==ID_mathematical_function)
+          if(id_it->second.type->id() == ID_mathematical_function)
           {
             return function_application_exprt(
-              symbol_exprt(final_id, id_it->second.type),
+              symbol_exprt(final_id, *(id_it->second.type)),
               op,
-              to_mathematical_function_type(
-                id_it->second.type).codomain());
+              to_mathematical_function_type(*(id_it->second.type)).codomain());
           }
           else
-            return symbol_exprt(final_id, id_it->second.type);
+            return symbol_exprt(final_id, *(id_it->second.type));
         }
 
         throw error() << "unknown function symbol `" << id << '\'';
@@ -964,7 +963,7 @@ exprt smt2_parsert::expression()
       auto id_it = id_map.find(final_id);
       if(id_it != id_map.end())
       {
-        symbol_exprt symbol_expr(final_id, id_it->second.type);
+        symbol_exprt symbol_expr(final_id, *(id_it->second.type));
         if(smt2_tokenizer.token_is_quoted_symbol())
           symbol_expr.set(ID_C_quoted, true);
         return std::move(symbol_expr);

src/solvers/smt2/smt2_parser.h

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include <map>
 
 #include <util/mathematical_types.h>
+#include <util/optional.h>
 #include <util/std_expr.h>
 
 #include "smt2_tokenizer.h"
@@ -33,11 +34,7 @@ class smt2_parsert
 
   struct idt
   {
-    idt():type(nil_typet())
-    {
-    }
-
-    typet type;
+    optionalt<typet> type;
     exprt definition;
     std::vector<irep_idt> parameters;
   };

src/solvers/smt2/smt2_solver.cpp

@@ -51,7 +51,7 @@ void smt2_solvert::define_constants()
 {
   for(const auto &id : id_map)
   {
-    if(id.second.type.id() == ID_mathematical_function)
+    if(id.second.type->id() == ID_mathematical_function)
       continue;
 
     if(id.second.definition.is_nil())
@@ -68,7 +68,7 @@ void smt2_solvert::define_constants()
     exprt def = id.second.definition;
     expand_function_applications(def);
     solver.set_to_true(
-      equal_exprt(symbol_exprt(identifier, id.second.type), def));
+      equal_exprt(symbol_exprt(identifier, *id.second.type), def));
   }
 }
 
@@ -89,11 +89,11 @@ void smt2_solvert::expand_function_applications(exprt &expr)
     {
       const auto &f=f_it->second;
 
-      DATA_INVARIANT(f.type.id()==ID_mathematical_function,
+      DATA_INVARIANT(
+        f.type->id() == ID_mathematical_function,
         "type of function symbol must be mathematical_function_type");
 
-      const auto f_type=
-        to_mathematical_function_type(f.type);
+      const auto f_type = to_mathematical_function_type(*f.type);
 
       const auto &domain = f_type.domain();
 
@@ -272,7 +272,7 @@ void smt2_solvert::command(const std::string &c)
       std::cout << '(';
       for(const auto &id : id_map)
       {
-        const symbol_exprt name(id.first, id.second.type);
+        const symbol_exprt name(id.first, *id.second.type);
         const auto value = simplify_expr(solver.get(name), ns);
 
         if(value.is_not_nil())
@@ -284,10 +284,10 @@ void smt2_solvert::command(const std::string &c)
 
           std::cout << "(define-fun " << smt2_format(name) << ' ';
 
-          if(id.second.type.id() == ID_mathematical_function)
+          if(id.second.type->id() == ID_mathematical_function)
             throw error("models for functions unimplemented");
           else
-            std::cout << "() " << smt2_format(id.second.type);
+            std::cout << "() " << smt2_format(*id.second.type);
 
           std::cout << ' ' << smt2_format(value) << ')';
         }