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

6 files changed, 101 insertions, 59 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"
diff --git a/src/util/command.cpp b/src/util/command.cpp
index b728a2228..35db79a0d 100644
--- a/src/util/command.cpp
+++ b/src/util/command.cpp
@@ -9,12 +9,14 @@
 
 using namespace CVC4;
 
+void EmptyCommand::invoke(SmtEngine* smt_engine) { }
+
 AssertCommand::AssertCommand(const Expr& e) :
   d_expr(e)
 {
 }
 
-void AssertCommand::invoke(CVC4::SmtEngine* smt_engine)
+void AssertCommand::invoke(SmtEngine* smt_engine)
 {
   smt_engine->assert(d_expr);
 }
@@ -23,18 +25,18 @@ CheckSatCommand::CheckSatCommand()
 {
 }
 
-CheckSatCommand::CheckSatCommand(const Expr& e):
-    d_expr(e)
+CheckSatCommand::CheckSatCommand(const Expr& e) :
+  d_expr(e)
 {
 }
 
-void CheckSatCommand::invoke(CVC4::SmtEngine* smt_engine)
+void CheckSatCommand::invoke(SmtEngine* smt_engine)
 {
   smt_engine->checkSat(d_expr);
 }
 
-QueryCommand::QueryCommand(const Expr& e):
-    d_expr(e)
+QueryCommand::QueryCommand(const Expr& e) :
+  d_expr(e)
 {
 }
 
@@ -43,3 +45,33 @@ void QueryCommand::invoke(CVC4::SmtEngine* smt_engine)
   smt_engine->query(d_expr);
 }
 
+CommandSequence::CommandSequence() :
+  d_last_index(0)
+{
+}
+
+CommandSequence::CommandSequence(Command* cmd) :
+  d_last_index(0)
+{
+  addCommand(cmd);
+}
+
+
+CommandSequence::~CommandSequence()
+{
+  for (unsigned i = d_last_index; i < d_command_sequence.size(); i++)
+    delete d_command_sequence[i];
+}
+
+void CommandSequence::invoke(SmtEngine* smt_engine)
+{
+  for (; d_last_index < d_command_sequence.size(); d_last_index++) {
+    d_command_sequence[d_last_index]->invoke(smt_engine);
+    delete d_command_sequence[d_last_index];
+  }
+}
+
+void CommandSequence::addCommand(Command* cmd)
+{
+  d_command_sequence.push_back(cmd);
+}
diff --git a/src/util/command.h b/src/util/command.h
index 745f6f5e2..c6778f34a 100644
--- a/src/util/command.h
+++ b/src/util/command.h
@@ -12,7 +12,7 @@
 #ifndef __CVC4__COMMAND_H
 #define __CVC4__COMMAND_H
 
-#include "expr/expr.h"
+#include "cvc4.h"
 
 namespace CVC4
 {
@@ -23,7 +23,13 @@ class Command
 {
   public:
     virtual void invoke(CVC4::SmtEngine* smt_engine) = 0;
-    virtual ~Command() {}
+    virtual ~Command() {};
+};
+
+class EmptyCommand : public Command
+{
+  public:
+    virtual void invoke(CVC4::SmtEngine* smt_engine);
 };
 
 class AssertCommand: public Command
@@ -54,6 +60,21 @@ class QueryCommand: public Command
     Expr d_expr;
 };
 
+class CommandSequence: public Command
+{
+  public:
+    CommandSequence();
+    CommandSequence(Command* cmd);
+    ~CommandSequence();
+    void invoke(CVC4::SmtEngine* smt);
+    void addCommand(Command* cmd);
+  private:
+    /** All the commands to be executed (in sequence) */
+    std::vector<Command*> d_command_sequence;
+    /** Next command to be executed */
+    unsigned int d_last_index;
+};
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__COMMAND_H */