Added an EmptyCommand and a CommandSequence commands and changed the parser a bit.

4 files changed, 40 insertions, 51 deletions

diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp
index 74def84cb..25f1cfd78 100644
--- a/src/parser/parser_state.cpp
+++ b/src/parser/parser_state.cpp
@@ -62,6 +62,10 @@ void ParserState::setPromptNextLine()
 void ParserState::increaseLineNumber()
 {
   ++d_input_line;
+  if (d_interactive) {
+    std::cout << getCurrentPrompt();
+    setPromptNextLine();
+  }
 }
 
 int ParserState::getLineNumber() const
@@ -74,12 +78,6 @@ std::string ParserState::getFileName() const
   return d_file_name;
 }
 
-void ParserState::getParsedCommands(vector<Command*>& commands_vector)
-{
-  d_commands.swap(commands_vector);
-  d_commands.clear();
-}
-
 } // End namespace parser
 
 } // End namespace CVC3
diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h
index fbb0afe70..8b18ff22f 100644
--- a/src/parser/parser_state.h
+++ b/src/parser/parser_state.h
@@ -19,14 +19,11 @@
 
 #include <vector>
 #include <iostream>
-#include <util/command.h>
+#include "cvc4.h"
 
 namespace CVC4
 {
 
-class Expr;
-class ExprManager;
-
 namespace parser
 {
 
@@ -80,17 +77,6 @@ class ParserState
     int read(char* buffer, int size);
 
     /**
-     * Returns the vector of parsed commands in the given vector (and forgets
-     * about them in the local state.
-     */
-    void getParsedCommands(std::vector<CVC4::Command*>& commands_vector);
-
-    /**
-     * Adds the commands in the given vector.
-     */
-    void addCommands(std::vector<CVC4::Command*>& commands_vector);
-
-    /**
      * Makes room for a new string literal (empties the buffer).
      */
     void newStringLiteral();
@@ -118,11 +104,6 @@ class ParserState
     std::string getBenchmarkName() const;
 
     /**
-     * Add the command to the list of commands.
-     */
-    void addCommand(const Command* cmd);
-
-    /**
      * Set the status of the parsed benchmark.
      */
     void setBenchmarkStatus(BenchmarkStatus status);
@@ -145,7 +126,7 @@ class ParserState
     /**
      * Creates a new expression, given the kind and the children
      */
-    CVC4::Expr* newExpression(CVC4::Kind kind, std::vector<CVC4::Expr*>& children);
+    CVC4::Expr* newExpression(CVC4::Kind kind, std::vector<CVC4::Expr>& children);
 
     /**
      * Returns a new TRUE Boolean constant.
@@ -162,6 +143,17 @@ class ParserState
      */
     CVC4::Expr* getNewVariableByName(const std::string var_name) const;
 
+    /**
+     * Sets the command that is the result of the parser.
+     */
+    void setCommand(CVC4::Command* cmd);
+
+    /**
+     * Sets the interactive flag on/off. If on, every time we go to a new line
+     * (via increaseLineNumber()) the prompt will be printed to stdout.
+     */
+    void setInteractive(bool interactive = true);
+
   private:
 
     /** Counter for uniqueID of bound variables */
@@ -190,9 +182,6 @@ class ParserState
 
     /** The name of the benchmark if any */
     std::string d_benchmark_name;
-
-    /** The vector of parsed commands if parsed as a whole */
-    std::vector<CVC4::Command*> d_commands;
 };
 
 }/* CVC4::parser namespace */
diff --git a/src/parser/smtlib.ypp b/src/parser/smtlib.ypp
index 8e6d99f6e..b1aeaa570 100644
--- a/src/parser/smtlib.ypp
+++ b/src/parser/smtlib.ypp
@@ -11,9 +11,8 @@
  ** commands in SMT-LIB language.
  **/
 
-#include "cvc4_expr.h"
-#include "parser/parser_state.h"
-#include "util/command.h"
+#include "cvc4.h"
+#include "parser_state.h"
 
 // Exported shared data
 namespace CVC4 {
@@ -43,13 +42,13 @@ int smtliberror(const char *s) { return _global_parser_state->parseError(s); }
 %union {
 
   std::string *p_string;
-  std::vector<std::string*> *p_string_vector;
+  std::vector<std::string> *p_string_vector;
 
   CVC4::Expr *p_expression;
-  std::vector<CVC4::Expr*> *p_expression_vector;
+  std::vector<CVC4::Expr> *p_expression_vector;
 
   CVC4::Command *p_command;
-  std::vector<CVC4::Command*> *p_command_vector;
+  CVC4::CommandSequence *p_command_sequence;
 
   CVC4::parser::ParserState::BenchmarkStatus d_bench_status;
   
@@ -57,8 +56,6 @@ int smtliberror(const char *s) { return _global_parser_state->parseError(s); }
   
 };
 
-%start benchmark
-
 %token <p_string> NUMERAL_TOK
 %token <p_string> SYM_TOK
 %token <p_string> STRING_TOK
@@ -104,29 +101,34 @@ int smtliberror(const char *s) { return _global_parser_state->parseError(s); }
 %type <p_expression> an_formula an_atom prop_atom
 %type <p_expression_vector> an_formulas;
 %type <d_kind> connective;
+%type <p_command> bench_attribute
+%type <p_command_sequence> bench_attributes  
 
+%start benchmark
+ 
 %%
 
 benchmark:
     LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK {
       _global_parser_state->setBenchmarkName(*$3);
+      _global_parser_state->setCommand($4);
     }    
-  | EOF_TOK
+  | EOF_TOK { _global_parser_state->setCommand(new EmptyCommand()); }
 ; 
 
 bench_name: SYM_TOK;
 
 bench_attributes:
-    bench_attribute
-  | bench_attributes bench_attribute
+    bench_attribute                   { $$ = new CommandSequence($1); }
+  | bench_attributes bench_attribute  { $$ = $1; $$->addCommand($2);  }
 ;
-
+ 
 bench_attribute:
-  | COLON_TOK FORMULA_TOK an_formula  { _global_parser_state->addCommand(new CheckSatCommand(*$3)); delete $3; }  
-  | COLON_TOK STATUS_TOK status       { _global_parser_state->setBenchmarkStatus($3); } 
-  | COLON_TOK LOGIC_TOK logic_name    { _global_parser_state->setBenchmarkLogic(*$3); delete $3; } 
-  | COLON_TOK EXTRAPREDS_TOK LPAREN_TOK pred_symb_decls RPAREN_TOK
-  | annotation
+    COLON_TOK FORMULA_TOK an_formula  { $$ = new CheckSatCommand(*$3); delete $3; }  
+  | COLON_TOK STATUS_TOK status       { $$ = new EmptyCommand(); _global_parser_state->setBenchmarkStatus($3); } 
+  | COLON_TOK LOGIC_TOK logic_name    { $$ = new EmptyCommand(); _global_parser_state->setBenchmarkLogic(*$3); delete $3; } 
+  | COLON_TOK EXTRAPREDS_TOK LPAREN_TOK pred_symb_decls RPAREN_TOK { $$ = new EmptyCommand(); }
+  | annotation { $$ = new EmptyCommand(); }
 ;  
  
 logic_name: SYM_TOK;
@@ -152,8 +154,8 @@ pred_sig:
 ;
 
 an_formulas:
-    an_formula             { $$ = new vector<Expr*>; $$->push_back($1); delete $1; }
-  | an_formulas an_formula { $$ = $1;                $$->push_back($2); delete $2; }
+    an_formula             { $$ = new vector<Expr>; $$->push_back(*$1); delete $1; }
+  | an_formulas an_formula { $$ = $1;               $$->push_back(*$2); delete $2; }
 ;
 
 an_formula:
diff --git a/src/parser/smtlib_scanner.lpp b/src/parser/smtlib_scanner.lpp
index 4d9cb8213..70026bd4c 100644
--- a/src/parser/smtlib_scanner.lpp
+++ b/src/parser/smtlib_scanner.lpp
@@ -17,8 +17,8 @@
 %option noyymore
 %option yylineno
 %option prefix="smtlib"
-
-%{
+  
+%{ 
 
 #include <iostream>
 #include "parser_state.h"