smt2 parser: track parenthesis level

The tokenizer is changed to split reading tokens and consuming them; the
parser counts the parentheses.

Author: Daniel Kroening

src/solvers/smt2/smt2_parser.cpp

@@ -12,6 +12,25 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 
+smt2_parsert::tokent smt2_parsert::next_token()
+{
+  const auto token = smt2_tokenizert::next_token();
+
+  if(token == OPEN)
+    parenthesis_level++;
+  else if(token == CLOSE)
+    parenthesis_level--;
+
+  return token;
+}
+
+void smt2_parsert::skip_to_end_of_list()
+{
+  while(parenthesis_level > 0)
+    if(next_token() == END_OF_FILE)
+      return;
+}
+
 void smt2_parsert::command_sequence()
 {
   exit=false;

src/solvers/smt2/smt2_parser.h

@@ -18,9 +18,8 @@ Author: Daniel Kroening, [email protected]
 class smt2_parsert:public smt2_tokenizert
 {
 public:
-  explicit smt2_parsert(std::istream &_in):
-    smt2_tokenizert(_in),
-    exit(false)
+  explicit smt2_parsert(std::istream &_in)
+    : smt2_tokenizert(_in), exit(false), parenthesis_level(0)
   {
   }
 
@@ -43,8 +42,25 @@ class smt2_parsert:public smt2_tokenizert
   using id_mapt=std::map<irep_idt, idt>;
   id_mapt id_map;
 
+  struct smt2_format
+  {
+    explicit smt2_format(const typet &_type) : type(_type)
+    {
+    }
+
+    const typet type;
+  };
+
+  /// This skips tokens until all bracketed expressions are closed
+  void skip_to_end_of_list();
+
 protected:
   bool exit;
+
+  // we override next_token to track the parenthesis level
+  std::size_t parenthesis_level;
+  tokent next_token() override;
+
   void command_sequence();
 
   virtual void command(const std::string &);

src/solvers/smt2/smt2_tokenizer.cpp

@@ -198,8 +198,15 @@ smt2_tokenizert::tokent smt2_tokenizert::get_string_literal()
 smt2_tokenizert::tokent smt2_tokenizert::next_token()
 {
   if(peeked)
-    return peeked=false, token;
+    peeked = false;
+  else
+    get_token_from_stream();
+
+  return token;
+}
 
+void smt2_tokenizert::get_token_from_stream()
+{
   char ch;
 
   while(in->get(ch))
@@ -231,60 +238,76 @@ smt2_tokenizert::tokent smt2_tokenizert::next_token()
 
     case '(':
       // produce sub-expression
-      return token=OPEN;
+      token = OPEN;
+      return;
 
     case ')':
       // done with sub-expression
-      return token=CLOSE;
+      token = CLOSE;
+      return;
 
     case '|': // quoted symbol
-      return token=get_quoted_symbol();
+      token = get_quoted_symbol();
+      return;
 
     case '"': // string literal
-      return token=get_string_literal();
+      token = get_string_literal();
+      return;
 
     case ':': // keyword
-      return token=get_simple_symbol();
+      token = get_simple_symbol();
+      return;
 
     case '#':
       if(in->get(ch))
       {
         if(ch=='b')
-          return token=get_bin_numeral();
+        {
+          token = get_bin_numeral();
+          return;
+        }
         else if(ch=='x')
-          return token=get_hex_numeral();
+        {
+          token = get_hex_numeral();
+          return;
+        }
         else
         {
           error() << "unknown numeral token" << eom;
-          return token=ERROR;
+          token=ERROR;
+          return;
         }
       }
       else
       {
         error() << "unexpected EOF in numeral token" << eom;
-        return token=ERROR;
+        token=ERROR;
+        return;
       }
       break;
 
     default: // likely a simple symbol or a numeral
       if(isdigit(ch))
       {
         in->unget();
-        return token=get_decimal_numeral();
+        token = get_decimal_numeral();
+        return;
       }
       else if(is_simple_symbol_character(ch))
       {
         in->unget();
-        return token=get_simple_symbol();
+        token = get_simple_symbol();
+        return;
       }
       else
       {
         // illegal character, error
         error() << "unexpected character `" << ch << '\'' << eom;
-        return token=ERROR;
+        token=ERROR;
+        return;
       }
     }
   }
 
-  return token=END_OF_FILE;
+  token = END_OF_FILE;
 }

src/solvers/smt2/smt2_tokenizer.h

@@ -16,8 +16,8 @@ Author: Daniel Kroening, [email protected]
 class smt2_tokenizert:public parsert
 {
 public:
-  explicit smt2_tokenizert(std::istream &_in):
-    ok(true), peeked(false), token(NONE)
+  explicit smt2_tokenizert(std::istream &_in)
+    : ok(true), peeked(false), token(NONE)
   {
     in=&_in;
     line_no=1;
@@ -35,15 +35,15 @@ class smt2_tokenizert:public parsert
                       NUMERAL, SYMBOL, OPEN, CLOSE };
   tokent token;
 
-  tokent next_token();
+  virtual tokent next_token();
 
   tokent peek()
   {
     if(peeked)
       return token;
     else
     {
-      next_token();
+      get_token_from_stream();
       peeked=true;
       return token;
     }
@@ -56,6 +56,10 @@ class smt2_tokenizert:public parsert
     return messaget::error();
   }
 
+  /// skip any tokens until all parentheses are closed
+  /// or the end of file is reached
+  void skip_to_end_of_list();
+
 private:
   tokent get_decimal_numeral();
   tokent get_hex_numeral();
@@ -64,6 +68,9 @@ class smt2_tokenizert:public parsert
   tokent get_quoted_symbol();
   tokent get_string_literal();
   static bool is_simple_symbol_character(char);
+
+  /// read a token from the input stream and store it in 'token'
+  void get_token_from_stream();
 };
 
 #endif // CPROVER_SOLVERS_SMT2_SMT2_PARSER_H