smt2irep now uses smt2_tokenizert

Author: Daniel Kroening

src/solvers/smt2/smt2irep.cpp

@@ -11,76 +11,84 @@ Author: Daniel Kroening, [email protected]
 #include <cassert>
 #include <stack>
 
-#include "smt2_parser.h"
+#include "smt2_tokenizer.h"
 
-class smt2irept:public smt2_parsert
+class smt2irept:public smt2_tokenizert
 {
 public:
-  explicit smt2irept(std::istream &_in):smt2_parsert(_in)
+  explicit smt2irept(std::istream &_in):smt2_tokenizert(_in)
   {
   }
 
   inline irept operator()()
   {
-    smt2_parsert::operator()();
+    parse();
     return result;
   }
 
+  bool parse() override;
+
 protected:
   irept result;
-  std::stack<irept> stack;
-
-  // overload from smt2_parsert
-
-  virtual void symbol()
-  {
-    if(stack.empty())
-      result=irept(buffer);
-    else
-      stack.top().get_sub().push_back(irept(buffer));
-  }
-
-  virtual void string_literal()
-  {
-    symbol(); // we don't distinguish
-  }
-
-  virtual void numeral()
-  {
-    symbol(); // we don't distinguish
-  }
-
-  // '('
-  virtual void open_expression()
-  {
-    // produce sub-irep
-    stack.push(irept());
-  }
-
-  // ')'
-  virtual void close_expression()
-  {
-    // done with sub-irep
-    assert(!stack.empty()); // unexpected )
-
-    irept tmp=stack.top();
-    stack.pop();
-
-    if(stack.empty())
-      result=tmp;
-    else
-      stack.top().get_sub().push_back(tmp);
-  }
+};
 
-  virtual void keyword()
-  {
-    // ignore
-  }
+bool smt2irept::parse()
+{
+  std::stack<irept> stack;
+  result.clear();
 
-  virtual void error(const std::string &message)
+  while(true)
   {
+    switch(next_token())
+    {
+    case END_OF_FILE:
+      error() << "unexpected end of file" << eom;
+      return true;
+
+    case STRING_LITERAL:
+    case NUMERAL:
+    case SYMBOL:
+      if(stack.empty())
+      {
+        result=irept(buffer);
+        return false; // all done!
+      }
+      else
+        stack.top().get_sub().push_back(irept(buffer));
+      break;
+
+    case OPEN: // '('
+      // produce sub-irep
+      stack.push(irept());
+      break;
+
+    case CLOSE: // ')'
+      // done with sub-irep
+      if(stack.empty())
+      {
+        error() << "unexpected ')'" << eom;
+        return true;
+      }
+      else
+      {
+        irept tmp=stack.top();
+        stack.pop();
+
+        if(stack.empty())
+        {
+          result=tmp;
+          return false; // all done!
+        }
+
+        stack.top().get_sub().push_back(tmp);
+        break;
+      }
+
+    default:
+      return true;
+    }
   }
-};
+}
 
 irept smt2irep(std::istream &in)
 {