Minor changes to parser

diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index e7169a02bf4727d5f7a92865bd349a0b689a9861..961915523d60be83acaeb705f05cf375e5245b73 100644 (file)
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -72,19 +72,19 @@ Expr AntlrParser::mkExpr(Kind kind, const std::vector<Expr>& children) {
   return d_exprManager->mkExpr(kind, children);
 }
 
-void AntlrParser::newPredicate(std::string p_name, const std::vector<
-    std::string>& p_sorts) {
-  if(p_sorts.size() == 0) {
-    d_varSymbolTable.bindName(p_name, d_exprManager->mkVar());
+void AntlrParser::newPredicate(std::string name, 
+                               const std::vector< std::string>& sorts) {
+  if(sorts.size() == 0) {
+    d_varSymbolTable.bindName(name, d_exprManager->mkVar());
   } else {
     Unhandled("Non unary predicate not supported yet!");
   }
 }
 
-void AntlrParser::newPredicates(const std::vector<std::string>& p_names) {
-  vector<string> sorts;
-  for(unsigned i = 0; i < p_names.size(); ++i) {
-    newPredicate(p_names[i], sorts);
+void AntlrParser::newPredicates(const std::vector<std::string>& names, 
+                                const std::vector< std::string>& sorts) {
+  for(unsigned i = 0; i < names.size(); ++i) {
+    newPredicate(names[i], sorts);
   }
 }
 

diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h
index f83ccd5f2851028bf3c61cbc3095f4179af6f0fe..5cbb7411efbe32b33e4c6a165ec8db268109a66c 100644 (file)
--- a/src/parser/antlr_parser.h
+++ b/src/parser/antlr_parser.h
@@ -168,17 +168,21 @@ protected:
   Expr mkExpr(Kind kind, const std::vector<Expr>& children);
 
   /**
-   * Creates a new predicated over the given sorts.
-   * @param p_name the name of the predicate
-   * @param p_sorts the arity sorts
+   * Creates a new predicate over the given sorts. The predicate
+   * has arity sorts.size().
+   * @param name the name of the predicate
+   * @param sorts the sorts
    */
-  void newPredicate(std::string p_name, const std::vector<std::string>& p_sorts);
+  void newPredicate(std::string name, 
+                    const std::vector<std::string>& sorts);
 
   /**
-   * Creates new predicates of given types.
+   * Creates new predicates over the given sorts. Each predicate
+   * will have arity sorts.size().
    * @param p_names the names of the predicates
    */
-  void newPredicates(const std::vector<std::string>& p_names);
+  void newPredicates(const std::vector<std::string>& names,
+                     const std::vector<std::string>& sorts);
 
   /**
    * Returns the precedence rank of the kind.

diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g
index 51473312ebe5a374f40a52542566f691c9e70fd6..cb9c9b1607155bd74e6aea82984ddb8e66f8dee5 100644 (file)
--- a/src/parser/cvc/cvc_parser.g
+++ b/src/parser/cvc/cvc_parser.g
@@ -59,8 +59,9 @@ command returns [CVC4::Command* cmd = 0]
   | CHECKSAT f = formula  SEMICOLON { cmd = new CheckSatCommand(f); }
   | CHECKSAT              SEMICOLON { cmd = new CheckSatCommand();  }
   | identifierList[ids, CHECK_UNDECLARED] COLON type { 
-      // [chris 12/15/2009] FIXME: decls may not be BOOLEAN
-      newPredicates(ids); 
+      // FIXME: switch on type (may not be predicates)
+      vector<string> sorts;
+      newPredicates(ids,sorts); 
       cmd = new DeclarationCommand(ids); 
     }
     SEMICOLON
@@ -239,4 +240,4 @@ boolAtom returns [CVC4::Expr atom]
 predicateSymbol[DeclarationCheck check = CHECK_NONE] returns [std::string pSymbol]
   : pSymbol = identifier[check]
   ;
- 
\ No newline at end of file
+ 

diff --git a/src/parser/smt/smt_lexer.g b/src/parser/smt/smt_lexer.g
index 0b38e1c2eb5673789cdbe089fbbb4556dbf75c16..a82e54e30f1bb0a0d949d8f2f1889659ba5347d5 100644 (file)
--- a/src/parser/smt/smt_lexer.g
+++ b/src/parser/smt/smt_lexer.g
@@ -42,13 +42,13 @@ tokens {
   UNKNOWN       = "unknown";
   BENCHMARK     = "benchmark";
   // The SMT attribute tokens
-  C_LOGIC       = ":logic";
-  C_ASSUMPTION  = ":assumption";
-  C_FORMULA     = ":formula";
-  C_STATUS      = ":status";
-  C_EXTRASORTS  = ":extrasorts";
-  C_EXTRAFUNS   = ":extrafuns";
-  C_EXTRAPREDS  = ":extrapreds";
+  LOGIC_ATTR       = ":logic";
+  ASSUMPTION_ATTR  = ":assumption";
+  FORMULA_ATTR     = ":formula";
+  STATUS_ATTR      = ":status";
+  EXTRASORTS_ATTR  = ":extrasorts";
+  EXTRAFUNS_ATTR   = ":extrafuns";
+  EXTRAPREDS_ATTR  = ":extrapreds";
   C_NOTES       = ":notes";
 }
 

diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g
index 88216336d3ebb42f2bb10ee83536d7a49c5d1d51..84b38c5cfe2efebd56e3da5befc6912444f0376e 100644 (file)
--- a/src/parser/smt/smt_parser.g
+++ b/src/parser/smt/smt_parser.g
@@ -55,8 +55,8 @@ benchmark returns [Command* cmd]
   ;
 
 /**
- * Matchecs sequence of benchmark attributes and returns a pointer to a command 
- * sequence command.
+ * Matches a sequence of benchmark attributes and returns a pointer to a 
+ * command sequence.
  * @return the command sequence 
  */
 benchAttributes returns [CVC4::CommandSequence* cmd_seq = new CommandSequence()]
@@ -77,12 +77,16 @@ benchAttribute returns [Command* smt_command = 0]
   string logic; 
   SetBenchmarkStatusCommand::BenchmarkStatus b_status = SetBenchmarkStatusCommand::SMT_UNKNOWN;
 }
-  : C_LOGIC       logic = identifier                  { smt_command = new SetBenchmarkLogicCommand(logic);   }      
-  | C_ASSUMPTION  formula = annotatedFormula          { smt_command = new AssertCommand(formula);   }       
-  | C_FORMULA     formula = annotatedFormula          { smt_command = new CheckSatCommand(formula); }
-  | C_STATUS      b_status = status                   { smt_command = new SetBenchmarkStatusCommand(b_status); }        
-  | C_EXTRAPREDS  LPAREN (predicateDeclaration)+ RPAREN  
-  | C_NOTES       STRING_LITERAL        
+  : LOGIC_ATTR logic = identifier 
+    { smt_command = new SetBenchmarkLogicCommand(logic);   }      
+  | ASSUMPTION_ATTR formula = annotatedFormula          
+    { smt_command = new AssertCommand(formula);   }       
+  | FORMULA_ATTR formula = annotatedFormula          
+    { smt_command = new CheckSatCommand(formula); }
+  | STATUS_ATTR b_status = status                   
+    { smt_command = new SetBenchmarkStatusCommand(b_status); }        
+  | EXTRAPREDS_ATTR LPAREN (predicateDeclaration)+ RPAREN  
+  | NOTES_ATTR STRING_LITERAL        
   | annotation
   ;
 
@@ -224,4 +228,4 @@ status returns [ SetBenchmarkStatusCommand::BenchmarkStatus status ]
 annotation 
   : attribute (USER_VALUE)?
   ;
-    
\ No newline at end of file
+    

diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 8a1f781dc551412b584d3f434edc58cac43c69b9..dbfd1359889e3251a108ac14ff92c2c8a4d8392d 100644 (file)
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -133,7 +133,7 @@ class SmtParserBlack : public CxxTest::TestSuite {
 
   void tryGoodInputs(Parser::InputLanguage d_lang, const string goodInputs[], int numInputs) {
     for(int i = 0; i < numInputs; ++i) {
-      cout << "Testing input: '" << goodInputs[i] << "'\n";
+      cout << "Testing good input: '" << goodInputs[i] << "'\n";
       istringstream stream(goodInputs[i]);
       Parser* smtParser = Parser::getNewParser(d_exprManager, d_lang, stream);
       TS_ASSERT( !smtParser->done() );
@@ -149,7 +149,7 @@ class SmtParserBlack : public CxxTest::TestSuite {
 
   void tryBadInputs(Parser::InputLanguage d_lang, const string badInputs[], int numInputs) {
     for(int i = 0; i < numInputs; ++i) {
-      cout << "Testing input: '" << badInputs[i] << "'\n";
+      cout << "Testing bad input: '" << badInputs[i] << "'\n";
       istringstream stream(badInputs[i]);
       Parser* smtParser = Parser::getNewParser(d_exprManager, d_lang, stream);
       TS_ASSERT_THROWS( while(smtParser->parseNextCommand()); , ParserException );
@@ -161,7 +161,7 @@ class SmtParserBlack : public CxxTest::TestSuite {
     cout << "Using context: " << context << endl;
     for(int i = 0; i < numExprs; ++i) {
       try {
-        cout << "Testing expr: '" << goodBooleanExprs[i] << "'\n";
+        cout << "Testing good expr: '" << goodBooleanExprs[i] << "'\n";
         istringstream stream(context + goodBooleanExprs[i]);
         Parser* parser = Parser::getNewParser(d_exprManager, d_lang, stream);
         TS_ASSERT( !parser->done() );
@@ -184,7 +184,7 @@ class SmtParserBlack : public CxxTest::TestSuite {
 
   void tryBadExprs(Parser::InputLanguage d_lang,const string badBooleanExprs[], int numExprs) {
     for(int i = 0; i < numExprs; ++i) {
-      cout << "Testing expr: '" << badBooleanExprs[i] << "'\n";
+      cout << "Testing bad expr: '" << badBooleanExprs[i] << "'\n";
       istringstream stream(badBooleanExprs[i]);
       Parser* smtParser = Parser::getNewParser(d_exprManager, d_lang, stream);
       TS_ASSERT_THROWS( smtParser->parseNextExpression(), ParserException );