More fixes

diff --git a/src/parser/cvc/cvc_lexer.g b/src/parser/cvc/cvc_lexer.g
index 47cebbbb0f23131204bcec0ed7f806d607ecbed9..863b15a95c5b1d15ae5ff22bd7d58bfab76f1fd4 100644 (file)
--- a/src/parser/cvc/cvc_lexer.g
+++ b/src/parser/cvc/cvc_lexer.g
@@ -70,6 +70,13 @@ COLON options{ paraphrase = "a colon"; }
   : ':'
   ;
 
+/**
+ * Matches the 'l'
+ */
+SEMICOLON options{ paraphrase = "a semicolon"; } 
+  : ';'
+  ;
+
 /**
  * Matches the ','
  */

diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g
index c7f932a0c020b599ebef6303f7692656a267ed83..a22ce64e7beca36b7c37677a2fc07e3d9b64f7d4 100644 (file)
--- a/src/parser/cvc/cvc_parser.g
+++ b/src/parser/cvc/cvc_parser.g
@@ -54,15 +54,16 @@ command returns [CVC4::Command* cmd = 0]
   Expr f;
   vector<string> ids;
 }
-  : ASSERT   f = formula  { cmd = new AssertCommand(f);   }
-  | QUERY    f = formula  { cmd = new QueryCommand(f);    }
-  | CHECKSAT f = formula  { cmd = new CheckSatCommand(f); }
-  | CHECKSAT              { cmd = new CheckSatCommand();  }
+  : ASSERT   f = formula  SEMICOLON { cmd = new AssertCommand(f);   }
+  | QUERY    f = formula  SEMICOLON { cmd = new QueryCommand(f);    }
+  | 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); 
       cmd = new DeclarationCommand(ids); 
     }
+    SEMICOLON
   | EOF 
   ;
 

diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g
index f7045fa7e3cb6b7f4ae4e0ca32dd8d6ca31056ab..56e1f9f17d88361d4429597bb3bfeb4ae82f5c9f 100644 (file)
--- a/src/parser/smt/smt_parser.g
+++ b/src/parser/smt/smt_parser.g
@@ -70,7 +70,7 @@ benchAttributes returns [CVC4::CommandSequence* cmd_seq = new CommandSequence()]
  * a corresponding command
  * @retrurn a command corresponding to the attribute
  */
-benchAttribute returns [ Command* smt_command = 0]
+benchAttribute returns [Command* smt_command = 0]
 {
   Expr formula;  
   string logic; 
@@ -80,7 +80,7 @@ benchAttribute returns [ Command* smt_command = 0]
   | 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 (pred_symb_decl)+ RPAREN  
+  | C_EXTRAPREDS  LPAREN (predicateDeclaration)+ RPAREN  
   | C_NOTES       STRING_LITERAL        
   | annotation
   ;
@@ -120,100 +120,94 @@ annotatedFormula returns [CVC4::Expr formula]
 /**
  * Matches an annotated proposition atom, which is either a propositional atom 
  * or built of other atoms using a predicate symbol.  
+ * @return expression representing the atom
  */
 annotatedAtom returns [CVC4::Expr atom] 
   : atom = propositionalAtom  
   ;
 
-
-
-
-
- 
-/**
- * Matches an attribute name from the input (:attribute_name).
- */ 
-attribute 
-  :  C_IDENTIFIER
-  ;
-   
 /**
- * Matches the sort symbol, which can be an arbitrary identifier.
- */
-sort_symb returns [std::string s] 
-  : id:IDENTIFIER { s = id->getText(); }
-  ;
-  
-/**
- * Matches an annotation, which is an attribute name, with an optional user value. 
- */
-annotation 
-  : attribute (USER_VALUE)?
+* Matches on of the unary Boolean connectives.
+* @return the kind of the Bollean connective
+*/
+boolConnective returns [CVC4::Kind kind]
+  : NOT      { kind = CVC4::NOT;     } 
+  | IMPLIES  { kind = CVC4::IMPLIES; }
+  | AND      { kind = CVC4::AND;     }
+  | OR       { kind = CVC4::OR;      }
+  | XOR      { kind = CVC4::XOR;     }
+  | IFF      { kind = CVC4::IFF;     }
   ;
-  
+
 /**
- * Matches a predicate symbol. 
- */
-pred_symb returns [std::string p]
-  :  id:IDENTIFIER { p = id->getText(); }
+ * Mathces a sequence of annotaed formulas and puts them into the formulas
+ * vector.
+ * @param formulas the vector to fill with formulas
+ */   
+annotatedFormulas[std::vector<Expr>& formulas]
+{
+  Expr f;
+}
+  : ( f = annotatedFormula { formulas.push_back(f); } )+
   ;
-  
 
 /**
- * Matches a propositional atom. 
+ * Matches a propositional atom and returns the expression of the atom.
+ * @return atom the expression of the atom 
  */
 propositionalAtom returns [CVC4::Expr atom]
 {
   std::string p;
 } 
-   : p = pred_symb {isDeclared(p, SYM_VARIABLE)}? { atom = getVariable(p); }
-      exception catch [antlr::SemanticException ex] {
-        rethrow(ex, "Undeclared variable " + p);
-      }   
+   : p = predicateName[CHECK_DECLARED] { atom = getVariable(p); }
    | TRUE          { atom = getTrueExpr(); }
    | FALSE         { atom = getFalseExpr(); }
    ;
-      
+
 /**
- * Matches on of the unary Boolean connectives.  
+ * Matches a predicate symbol. 
+ * @param check what kind of check to do with the symbol
  */
-boolConnective returns [CVC4::Kind kind]
-  : NOT      { kind = CVC4::NOT;     } 
-  | IMPLIES  { kind = CVC4::IMPLIES; }
-  | AND      { kind = CVC4::AND;     }
-  | OR       { kind = CVC4::OR;      }
-  | XOR      { kind = CVC4::XOR;     }
-  | IFF      { kind = CVC4::IFF;     }
+predicateName[DeclarationCheck check = CHECK_NONE] returns [std::string p]
+  :  p = identifier[check]
   ;
-    
-annotatedFormulas[std::vector<Expr>& formulas]
-{
-  Expr f;
-}
-  : ( f = annotatedFormula { formulas.push_back(f); } )+
+  
+/**
+ * Matches an attribute name from the input (:attribute_name).
+ */ 
+attribute 
+  :  C_IDENTIFIER
+  ;
+      
+/**
+ * Matches the sort symbol, which can be an arbitrary identifier.
+ * @param check the check to perform on the name
+ */
+sortName[DeclarationCheck check = CHECK_NONE] returns [std::string s] 
+  : s = identifier[check]
   ;
-   
+              
 /**
- * Matches the declaration of a predicate symbol.
+ * Matches the declaration of a predicate and declares it
  */
-pred_symb_decl
+predicateDeclaration
 {
   string p_name;
   vector<string> p_sorts;
 }
-  :  LPAREN p_name = pred_symb sort_symbs[p_sorts] RPAREN { newPredicate(p_name, p_sorts); } 
+  :  LPAREN p_name = predicateName[CHECK_UNDECLARED] sortNames[p_sorts] RPAREN { newPredicate(p_name, p_sorts); } 
   ;
   
 /**
  * Matches a sequence of sort symbols and fills them into the given vector.
  */
-sort_symbs[std::vector<std::string>& sorts]
+sortNames[std::vector<std::string>& sorts]
 {
-  std::string type;
+  std::string sort;
 }
-  : ( type = sort_symb { sorts.push_back(type); })* 
+  : ( sort = sortName[CHECK_UNDECLARED] { sorts.push_back(sort); })* 
   ;
-    
+
 /**
  * Matches the status of the benchmark, one of 'sat', 'unsat' or 'unknown'.
  */
@@ -221,4 +215,12 @@ status returns [ SetBenchmarkStatusCommand::BenchmarkStatus status ]
   : SAT       { status = SetBenchmarkStatusCommand::SMT_SATISFIABLE;    }
   | UNSAT     { status = SetBenchmarkStatusCommand::SMT_UNSATISFIABLE;  }
   | UNKNOWN   { status = SetBenchmarkStatusCommand::SMT_UNKNOWN;        }
-  ;
\ No newline at end of file
+  ;
+
+/**
+ * Matches an annotation, which is an attribute name, with an optional user 
+ */
+annotation 
+  : attribute (USER_VALUE)?
+  ;
+    
\ No newline at end of file