From: Christopher L. Conway <christopherleeconway@gmail.com>
Date: Thu, 17 Dec 2009 20:30:43 +0000 (+0000)
Subject: Adding more parser tests
X-Git-Tag: cvc5-1.0.0~9358
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=24bf38210981fcddcc7e236c2a67095ea6345513;p=cvc5.git

Adding more parser tests
---

diff --git a/src/parser/smt/smt_lexer.g b/src/parser/smt/smt_lexer.g
index 70f60a0bc..bc8c05fdd 100644
--- a/src/parser/smt/smt_lexer.g
+++ b/src/parser/smt/smt_lexer.g
@@ -150,3 +150,9 @@ STRING_LITERAL options { paraphrase = "a string literal"; }
   :  '\"' (~('\"'))* '\"'
   ;
   
+/**
+ * Matches the comments and ignores them
+ */
+COMMENT options { paraphrase = "comment"; }
+  : ';' (~('\n' | '\r'))*                    { $setType(antlr::Token::SKIP); }
+  ;
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index cf78d8e34..d8f321f10 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -16,7 +16,8 @@ AM_LDFLAGS_PUBLIC = \
 TESTS = \
 	expr/node_white \
 	expr/node_black \
-	parser/cvc/cvc_parser_black
+	parser/cvc/cvc_parser_black \
+	parser/smt/smt_parser_black
 
 # without these here, LTCXXCOMPILE, CXXLINK, etc., aren't set :-(
 noinst_LTLIBRARIES = libdummy.la
diff --git a/test/unit/Makefile.in b/test/unit/Makefile.in
index f20905330..251ef2dfe 100644
--- a/test/unit/Makefile.in
+++ b/test/unit/Makefile.in
@@ -235,7 +235,8 @@ top_srcdir = @top_srcdir@
 @HAVE_CXXTESTGEN_TRUE@TESTS = \
 @HAVE_CXXTESTGEN_TRUE@	expr/node_white \
 @HAVE_CXXTESTGEN_TRUE@	expr/node_black \
-@HAVE_CXXTESTGEN_TRUE@	parser/cvc/cvc_parser_black
+@HAVE_CXXTESTGEN_TRUE@	parser/cvc/cvc_parser_black \
+@HAVE_CXXTESTGEN_TRUE@	parser/smt/smt_parser_black
 
 
 # without these here, LTCXXCOMPILE, CXXLINK, etc., aren't set :-(
diff --git a/test/unit/parser/cvc/cvc_parser_black.h b/test/unit/parser/cvc/cvc_parser_black.h
index b34185e01..e99cce44d 100644
--- a/test/unit/parser/cvc/cvc_parser_black.h
+++ b/test/unit/parser/cvc/cvc_parser_black.h
@@ -1,9 +1,10 @@
-/* Black box testing of CVC4::Node. */
+/* Black box testing of CVC4::parser::CvcParser. */
 
 #include <cxxtest/TestSuite.h>
 //#include <string>
 #include <sstream>
 
+#include "expr/expr.h"
 #include "expr/expr_manager.h"
 #include "parser/cvc/cvc_parser.h"
 
@@ -11,36 +12,97 @@ using namespace CVC4;
 using namespace CVC4::parser;
 using namespace std;
 
-const string d_goodInputs[] = {
+const string goodInputs[] = {
+      "", // empty string is OK
       "ASSERT TRUE;",
       "QUERY TRUE;",
       "CHECKSAT FALSE;",
       "a, b : BOOLEAN;",
       "x, y : INT;",
-      "a, b : BOOLEAN; QUERY (a => b) AND a => b;"
+      "a, b : BOOLEAN; QUERY (a => b) AND a => b;",
+      "%% nothing but a comment",
+      "% a comment\nASSERT TRUE %a command\n% another comment"
   };
 
+/* The following expressions are good in a context where a, b, and c have been declared as BOOLEAN. */
+const string goodBooleanExprs[] = {
+    "a AND b",
+    "a AND b OR c",
+    "(a => b) AND a => b",
+    "(a <=> b) AND (NOT a)",
+    "(a XOR b) <=> (a OR b) AND (NOT (a AND b))"
+};
+
+const string badInputs[] = {
+      ";", // no command
+      "ASSERT;", // no args
+      "QUERY",
+      "CHECKSAT;",
+      "a, b : boolean;", // lowercase boolean isn't a type
+      "0x : INT;", // 0x isn't an identifier
+      "a, b : BOOLEAN\nQUERY (a => b) AND a => b;" // no semicolon after decl
+  };
+
+/* The following expressions are bad even in a context where a, b, and c have been declared as BOOLEAN. */
+const string badBooleanExprs[] = {
+    "",
+    "a AND", // wrong arity
+    "AND(a,b)", // not infix
+    "(OR (AND a b) c)", // not infix
+    "a IMPLIES b", // should be =>
+    "a NOT b", // wrong arity, not infix
+    "a and b" // wrong case
+};
+
 class CvcParserBlack : public CxxTest::TestSuite {
 private:
-
   ExprManager *d_exprManager;
 
-
 public:
   void setUp() {
-//    cout << "In setUp()\n";
     d_exprManager = new ExprManager();
-//    cout << "Leaving setUp()\n";
   }
 
   void testGoodInputs() {
-//    cout << "In testGoodInputs()\n";
-    for( int i=0; i < sizeof(d_goodInputs); ++i ) {
-      istringstream stream(d_goodInputs[i]);
-      CvcParser cvcParser(d_exprManager,stream);
+    //    cout << "In testGoodInputs()\n";
+    for(int i = 0; i < sizeof(goodInputs); ++i) {
+      istringstream stream(goodInputs[i]);
+      CvcParser cvcParser(d_exprManager, stream);
       TS_ASSERT( !cvcParser.done() );
-      while( !cvcParser.done() ) {
-        TS_ASSERT( cvcParser.parseNextCommand() );
+      while(!cvcParser.done()) {
+        TS_ASSERT( cvcParser.parseNextCommand() != NULL );
       }
+    }
   }
+
+  void testBadInputs() {
+    //    cout << "In testGoodInputs()\n";
+    for(int i = 0; i < sizeof(badInputs); ++i) {
+      istringstream stream(badInputs[i]);
+      CvcParser cvcParser(d_exprManager, stream);
+      TS_ASSERT_THROWS( cvcParser.parseNextCommand(), ParserException );
+    }
+  }
+
+  void testGoodBooleanExprs() {
+    //    cout << "In testGoodInputs()\n";
+    for(int i = 0; i < sizeof(goodBooleanExprs); ++i) {
+      istringstream stream(goodBooleanExprs[i]);
+      CvcParser cvcParser(d_exprManager, stream);
+      TS_ASSERT( !cvcParser.done() );
+      while(!cvcParser.done()) {
+        TS_ASSERT( !cvcParser.parseNextExpression().isNull() );
+      }
+    }
+  }
+
+  void testBadBooleanExprs() {
+    //    cout << "In testGoodInputs()\n";
+    for(int i = 0; i < sizeof(badBooleanExprs); ++i) {
+      istringstream stream(badBooleanExprs[i]);
+      CvcParser cvcParser(d_exprManager, stream);
+      TS_ASSERT_THROWS( cvcParser.parseNextExpression(), ParserException );
+    }
+  }
+
 };