smt2_parser: introduce table of commands

This refactors the SMT2 parser to use hash tables instead of chains of
if()...else if()...  for commands.

This enables extensions, and may have a performance benefit as the number of
commands grows.

Author: kroening

src/solvers/smt2/smt2_parser.cpp

@@ -1259,21 +1259,36 @@ typet smt2_parsert::function_signature_declaration()
 
 void smt2_parsert::command(const std::string &c)
 {
-  if(c == "declare-const" || c == "declare-var")
+  auto c_it = commands.find(c);
+  if(c_it == commands.end())
   {
-    // declare-var appears to be a synonym for declare-const that is
-    // accepted by Z3 and CVC4
+    // silently ignore
+    ignore_command();
+  }
+  else
+    c_it->second();
+}
+
+void smt2_parsert::setup_commands()
+{
+  commands["declare-const"] = [this]() {
+    const auto s = smt2_tokenizer.get_buffer();
+
     if(next_token() != smt2_tokenizert::SYMBOL)
-      throw error() << "expected a symbol after '" << c << '\'';
+      throw error() << "expected a symbol after " << s;
 
     irep_idt id = smt2_tokenizer.get_buffer();
     auto type = sort();
 
     if(add_fresh_id(id, exprt(ID_nil, type)) != id)
       throw error() << "identifier '" << id << "' defined twice";
-  }
-  else if(c=="declare-fun")
-  {
+  };
+
+  // declare-var appears to be a synonym for declare-const that is
+  // accepted by Z3 and CVC4
+  commands["declare-var"] = commands["declare-const"];
+
+  commands["declare-fun"] = [this]() {
     if(next_token() != smt2_tokenizert::SYMBOL)
       throw error("expected a symbol after declare-fun");
 
@@ -1282,9 +1297,9 @@ void smt2_parsert::command(const std::string &c)
 
     if(add_fresh_id(id, exprt(ID_nil, type)) != id)
       throw error() << "identifier '" << id << "' defined twice";
-  }
-  else if(c == "define-const")
-  {
+  };
+
+  commands["define-const"] = [this]() {
     if(next_token() != smt2_tokenizert::SYMBOL)
       throw error("expected a symbol after define-const");
 
@@ -1304,9 +1319,9 @@ void smt2_parsert::command(const std::string &c)
     // create the entry
     if(add_fresh_id(id, value) != id)
       throw error() << "identifier '" << id << "' defined twice";
-  }
-  else if(c=="define-fun")
-  {
+  };
+
+  commands["define-fun"] = [this]() {
     if(next_token() != smt2_tokenizert::SYMBOL)
       throw error("expected a symbol after define-fun");
 
@@ -1345,11 +1360,7 @@ void smt2_parsert::command(const std::string &c)
 
     id_map.at(id).type = signature.type;
     id_map.at(id).parameters = signature.parameters;
-  }
-  else if(c=="exit")
-  {
-    exit=true;
-  }
-  else
-    ignore_command();
+  };
+
+  commands["exit"] = [this]() { exit = true; };
 }

src/solvers/smt2/smt2_parser.h

@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_SOLVERS_SMT2_SMT2_PARSER_H
 
 #include <map>
+#include <unordered_map>
 
 #include <util/mathematical_types.h>
 #include <util/std_expr.h>
@@ -22,6 +23,7 @@ class smt2_parsert
   explicit smt2_parsert(std::istream &_in)
     : exit(false), smt2_tokenizer(_in), parenthesis_level(0)
   {
+    setup_commands();
   }
 
   virtual ~smt2_parsert() = default;
@@ -82,10 +84,6 @@ class smt2_parsert
   std::size_t parenthesis_level;
   smt2_tokenizert::tokent next_token();
 
-  void command_sequence();
-
-  virtual void command(const std::string &);
-
   // for let/quantifier bindings, function parameters
   using renaming_mapt=std::map<irep_idt, irep_idt>;
   renaming_mapt renaming_map;
@@ -116,7 +114,6 @@ class smt2_parsert
     }
   };
 
-  void ignore_command();
   exprt expression();
   exprt function_application();
   exprt function_application_ieee_float_op(
@@ -144,6 +141,14 @@ class smt2_parsert
 
   /// Apply typecast to unsignedbv to given expression
   exprt cast_bv_to_unsigned(const exprt &);
+
+  // hashtable for all commands
+  std::unordered_map<std::string, std::function<void()>> commands;
+
+  void command_sequence();
+  void command(const std::string &);
+  void ignore_command();
+  void setup_commands();
 };
 
 #endif // CPROVER_SOLVERS_SMT2_SMT2_PARSER_H

src/solvers/smt2/smt2_solver.cpp

@@ -28,12 +28,13 @@ class smt2_solvert:public smt2_parsert
   smt2_solvert(std::istream &_in, decision_proceduret &_solver)
     : smt2_parsert(_in), solver(_solver), status(NOT_SOLVED)
   {
+    setup_commands();
   }
 
 protected:
   decision_proceduret &solver;
 
-  void command(const std::string &) override;
+  void setup_commands();
   void define_constants();
   void expand_function_applications(exprt &);
 
@@ -118,20 +119,19 @@ void smt2_solvert::expand_function_applications(exprt &expr)
   }
 }
 
-void smt2_solvert::command(const std::string &c)
+void smt2_solvert::setup_commands()
 {
   {
-    if(c == "assert")
-    {
+    commands["assert"] = [this]() {
       exprt e = expression();
       if(e.is_not_nil())
       {
         expand_function_applications(e);
         solver.set_to_true(e);
       }
-    }
-    else if(c == "check-sat")
-    {
+    };
+
+    commands["check-sat"] = [this]() {
       // add constant definitions as constraints
       define_constants();
 
@@ -151,20 +151,20 @@ void smt2_solvert::command(const std::string &c)
         std::cout << "error\n";
         status = NOT_SOLVED;
       }
-    }
-    else if(c == "check-sat-assuming")
-    {
+    };
+
+    commands["check-sat-assuming"] = [this]() {
       throw error("not yet implemented");
-    }
-    else if(c == "display")
-    {
+    };
+
+    commands["display"] = [this]() {
       // this is a command that Z3 appears to implement
       exprt e = expression();
       if(e.is_not_nil())
         std::cout << smt2_format(e) << '\n';
-    }
-    else if(c == "get-value")
-    {
+    };
+
+    commands["get-value"] = [this]() {
       std::vector<exprt> ops;
 
       if(next_token() != smt2_tokenizert::OPEN)
@@ -217,18 +217,18 @@ void smt2_solvert::command(const std::string &c)
       }
 
       std::cout << ")\n";
-    }
-    else if(c == "echo")
-    {
+    };
+
+    commands["echo"] = [this]() {
       if(next_token() != smt2_tokenizert::STRING_LITERAL)
         throw error("expected string literal");
 
       std::cout << smt2_format(constant_exprt(
                      smt2_tokenizer.get_buffer(), string_typet()))
                 << '\n';
-    }
-    else if(c == "get-assignment")
-    {
+    };
+
+    commands["get-assignment"] = [this]() {
       // print satisfying assignment for all named expressions
 
       if(status != SAT)
@@ -256,9 +256,9 @@ void smt2_solvert::command(const std::string &c)
         }
       }
       std::cout << ')' << '\n';
-    }
-    else if(c == "get-model")
-    {
+    };
+
+    commands["get-model"] = [this]() {
       // print a model for all identifiers
 
       if(status != SAT)
@@ -293,9 +293,9 @@ void smt2_solvert::command(const std::string &c)
         }
       }
       std::cout << ')' << '\n';
-    }
-    else if(c == "simplify")
-    {
+    };
+
+    commands["simplify"] = [this]() {
       // this is a command that Z3 appears to implement
       exprt e = expression();
       if(e.is_not_nil())
@@ -305,7 +305,9 @@ void smt2_solvert::command(const std::string &c)
         exprt e_simplified = simplify_expr(e, ns);
         std::cout << smt2_format(e) << '\n';
       }
-    }
+    };
+  }
+
 #if 0
     // TODO:
     | ( declare-const hsymboli hsorti )
@@ -330,9 +332,6 @@ void smt2_solvert::command(const std::string &c)
     | ( set-info hattributei )
     | ( set-option hoptioni )
 #endif
-    else
-      smt2_parsert::command(c);
-  }
 }
 
 class smt2_message_handlert : public message_handlert