smt2irep now returns optional

This is follow-up from a discussion in #4395 and clarifies the contract of
this function.

Author: Daniel Kroening

src/solvers/smt2/smt2_dec.cpp

@@ -143,7 +143,12 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in)
 
   while(in)
   {
-    irept parsed = smt2irep(in, get_message_handler());
+    auto parsed_opt = smt2irep(in, get_message_handler());
+
+    if(!parsed_opt.has_value())
+      break;
+
+    const auto &parsed = parsed_opt.value();
 
     if(parsed.id()=="sat")
       res=resultt::D_SATISFIABLE;

src/solvers/smt2/smt2irep.cpp

@@ -22,47 +22,33 @@ class smt2irept:public smt2_tokenizert
   {
   }
 
-  inline irept operator()()
-  {
-    parse();
-    return result;
-  }
-
-  bool parse();
+  optionalt<irept> operator()();
 
 protected:
   messaget log;
-  irept result;
 };
 
-bool smt2irept::parse()
+optionalt<irept> smt2irept::operator()()
 {
   try
   {
     std::stack<irept> stack;
-    result.clear();
 
     while(true)
     {
       switch(next_token())
       {
       case END_OF_FILE:
         if(stack.empty())
-        {
-          result = irept(irep_idt());
-          return false;
-        }
+          return {};
         else
           throw error("unexpected end of file");
 
       case STRING_LITERAL:
       case NUMERAL:
       case SYMBOL:
         if(stack.empty())
-        {
-          result = irept(buffer);
-          return false; // all done!
-        }
+          return irept(buffer); // all done!
         else
           stack.top().get_sub().push_back(irept(buffer));
         break;
@@ -82,10 +68,7 @@ bool smt2irept::parse()
           stack.pop();
 
           if(stack.empty())
-          {
-            result = tmp;
-            return false; // all done!
-          }
+            return tmp; // all done!
 
           stack.top().get_sub().push_back(tmp);
           break;
@@ -100,11 +83,11 @@ bool smt2irept::parse()
   {
     log.error().source_location.set_line(e.get_line_no());
     log.error() << e.what() << messaget::eom;
-    return true;
+    return {};
   }
 }
 
-irept smt2irep(std::istream &in, message_handlert &message_handler)
+optionalt<irept> smt2irep(std::istream &in, message_handlert &message_handler)
 {
   return smt2irept(in, message_handler)();
 }

src/solvers/smt2/smt2irep.h

@@ -13,9 +13,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <iosfwd>
 
 #include <util/irep.h>
+#include <util/optional.h>
 
 class message_handlert;
 
-irept smt2irep(std::istream &, message_handlert &);
+optionalt<irept> smt2irep(std::istream &, message_handlert &);
 
 #endif // CPROVER_SOLVERS_SMT2_SMT2IREP_H