SMT2 parser with explicit stack

src/solvers/smt2/smt2_parser.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "smt2_parser.h"
 
 #include "smt2_format.h"
+#include "smt2irep.h"
 
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
@@ -1010,6 +1011,29 @@ exprt smt2_parsert::bv_mod(const exprt::operandst &operands, bool is_signed)
 
 exprt smt2_parsert::expression()
 {
+  auto irep_opt = smt2irep(smt2_tokenizer);
+
+  if(!irep_opt.has_value())
+    throw error("EOF in an expression");
+
+  auto &irep_as_expr = static_cast<exprt &>(irep_opt.value());
+
+  // transform into exprt, without recursion using post-order
+  // traversal
+  irep_as_expr.visit_post([](exprt &expr) {
+    // is it a function application?
+    if(expr.get_sub().size() >= 2)
+    {
+    }
+    else
+    {
+      // literal or symbol
+    }
+  });
+
+  return irep_as_expr;
+
+#if 0
   switch(next_token())
   {
   case smt2_tokenizert::SYMBOL:
@@ -1076,6 +1100,7 @@ exprt smt2_parsert::expression()
   }
 
   UNREACHABLE;
+#endif
 }
 
 void smt2_parsert::setup_expressions()

src/solvers/smt2/smt2irep.cpp

@@ -14,82 +14,90 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "smt2_tokenizer.h"
 
-class smt2irept:public smt2_tokenizert
+class smt2irept
 {
 public:
-  smt2irept(std::istream &_in, message_handlert &message_handler)
-    : smt2_tokenizert(_in), log(message_handler)
+  explicit smt2irept(smt2_tokenizert &_tokenizer)
+    : tokenizer(_tokenizer)
   {
   }
 
   std::optional<irept> operator()();
 
 protected:
-  messaget log;
+  smt2_tokenizert tokenizer;
 };
 
 std::optional<irept> smt2irept::operator()()
 {
-  try
-  {
-    std::stack<irept> stack;
+  std::stack<irept> stack;
 
-    while(true)
+  while(true)
+  {
+    switch(tokenizer.next_token())
     {
-      switch(next_token())
+    case smt2_tokenizert::END_OF_FILE:
+      if(stack.empty())
+        return {};
+      else
+        throw tokenizer.error("unexpected end of file");
+
+    case smt2_tokenizert::STRING_LITERAL:
+    case smt2_tokenizert::NUMERAL:
+    case smt2_tokenizert::SYMBOL:
+      if(stack.empty())
+        return irept(tokenizer.get_buffer()); // all done!
+      else
+        stack.top().get_sub().push_back(irept(tokenizer.get_buffer()));
+      break;
+
+    case smt2_tokenizert::OPEN: // '('
+      // produce sub-irep
+      stack.push(irept());
+      break;
+
+    case smt2_tokenizert::CLOSE: // ')'
+      // done with sub-irep
+      if(stack.empty())
+        throw tokenizer.error("unexpected ')'");
+      else
       {
-      case END_OF_FILE:
-        if(stack.empty())
-          return {};
-        else
-          throw error("unexpected end of file");
+        irept tmp = stack.top();
+        stack.pop();
 
-      case STRING_LITERAL:
-      case NUMERAL:
-      case SYMBOL:
         if(stack.empty())
-          return irept(buffer); // all done!
-        else
-          stack.top().get_sub().push_back(irept(buffer));
-        break;
+          return tmp; // all done!
 
-      case OPEN: // '('
-        // produce sub-irep
-        stack.push(irept());
+        stack.top().get_sub().push_back(tmp);
         break;
-
-      case CLOSE: // ')'
-        // done with sub-irep
-        if(stack.empty())
-          throw error("unexpected ')'");
-        else
-        {
-          irept tmp = stack.top();
-          stack.pop();
-
-          if(stack.empty())
-            return tmp; // all done!
-
-          stack.top().get_sub().push_back(tmp);
-          break;
-        }
-
-      case NONE:
-      case KEYWORD:
-        throw error("unexpected token");
       }
+
+    case smt2_tokenizert::NONE:
+    case smt2_tokenizert::KEYWORD:
+      throw tokenizer.error("unexpected token");
     }
   }
-  catch(const smt2_errort &e)
+}
+
+std::optional<irept>
+smt2irep(std::istream &in, message_handlert &message_handler)
+{
+  try
+  {
+    smt2_tokenizert tokenizer{in};
+    return smt2irept{tokenizer}();
+  }
+  catch(const smt2_tokenizert::smt2_errort &e)
   {
+    messaget log{message_handler};
     log.error().source_location.set_line(e.get_line_no());
     log.error() << e.what() << messaget::eom;
     return {};
   }
 }
 
 std::optional<irept>
-smt2irep(std::istream &in, message_handlert &message_handler)
+smt2irep(smt2_tokenizert &tokenizer)
 {
-  return smt2irept(in, message_handler)();
+  return smt2irept{tokenizer}();
 }

src/solvers/smt2/smt2irep.h

@@ -16,8 +16,16 @@ Author: Daniel Kroening, kroening@kroening.com
 class irept;
 class message_handlert;
 
-/// returns an irep for an SMT-LIB2 expression read from a given stream
-/// returns {} when EOF is encountered before reading non-whitespace input
+/// Returns an irep for an SMT-LIB2 expression read from a given stream
+/// Returns {} when EOF is encountered before reading non-whitespace input
+/// or on other parsing errors.
 std::optional<irept> smt2irep(std::istream &, message_handlert &);
 
+class smt2_tokenizert;
+
+/// Returns an irep for an SMT-LIB2 expression read from a given tokenizer.
+/// Returns {} when EOF is encountered before reading non-whitespace input.
+/// Throws smt2_errort on parsing errors.
+std::optional<irept> smt2irep(smt2_tokenizert &);
+
 #endif // CPROVER_SOLVERS_SMT2_SMT2IREP_H