fixing a few broken build-related items, adding test cases

diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am
index 2619b2dacf305f171893593efe0287dce9fbcf83..4c1a5d92b40a829d026a41e4a1685b97a2f7cff0 100644 (file)
--- a/src/parser/cvc/Makefile.am
+++ b/src/parser/cvc/Makefile.am
@@ -18,6 +18,7 @@ libparsercvc_la_SOURCES = \
 BUILT_SOURCES = $(ANTLR_STUFF)
 CLEAN_FILES = $(ANTLR_STUFF)
 
-Antlr%.cpp Antlr%.hpp: %.g
-       $(ANTLR) -o "@builddir@" "@srcdir@/$<"
-
+AntlrCvcLexer.cpp AntlrCvcLexer.hpp: CvcLexer.g
+       $(ANTLR) -o "@builddir@" "$<"
+AntlrCvcParser.cpp AntlrCvcParser.hpp: CvcParser.g
+       $(ANTLR) -o "@builddir@" "$<"

diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am
index 35b5bafd787ba489025312b254bd9335d5dff6f2..6017409fd16882d0ed94b75a629128d3fdd67baa 100644 (file)
--- a/src/parser/smt/Makefile.am
+++ b/src/parser/smt/Makefile.am
@@ -4,23 +4,21 @@ AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB
 
 noinst_LTLIBRARIES = libparsersmt.la
 
-libparsersmt_la_SOURCES = \
-       SmtLexer.g \
-       SmtParser.g \
+ANTLR_STUFF = \
        AntlrSmtLexer.hpp \
        AntlrSmtLexer.cpp \
        AntlrSmtParser.hpp \
        AntlrSmtParser.cpp 
 
-BUILT_SOURCES = \
-       AntlrSmtLexer.hpp \
-       AntlrSmtLexer.cpp \
-       AntlrSmtParser.hpp \
-       AntlrSmtParser.cpp 
-CLEAN_FILES = $(BUILT_SOURCES)
+libparsersmt_la_SOURCES = \
+       SmtLexer.g \
+       SmtParser.g \
+       $(ANTLR_STUFF)
 
-AntlrSmtLexer.cpp AntlrSmtLexer.hpp: SmtLexer.g
-       $(ANTLR) -o "@builddir@" "@srcdir@/SmtLexer.g"
+BUILT_SOURCES = $(ANTLR_STUFF)
+CLEAN_FILES = $(ANTLR_STUFF)
 
+AntlrSmtLexer.cpp AntlrSmtLexer.hpp: SmtLexer.g
+       $(ANTLR) -o "@builddir@" "$<"
 AntlrSmtParser.cpp AntlrSmtParser.hpp: SmtParser.g
-       $(ANTLR) -o "@builddir@" "@srcdir@/SmtParser.g"
+       $(ANTLR) -o "@builddir@" "$<"

diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am
index 61deb03e6d8be2a58ef4b3b49a2152c0329ca8b6..a4a06c10b60b93ee3220baf3093877199d1caaf5 100644 (file)
--- a/test/regress/Makefile.am
+++ b/test/regress/Makefile.am
@@ -1,3 +1,5 @@
 TESTS_ENVIRONMENT = echo
 TESTS = \
+       simple.cvc \
+       simple.smt \
        bug1.cvc

diff --git a/test/regress/simple.cvc b/test/regress/simple.cvc
new file mode 100644 (file)
index 0000000..c1a5dd8
--- /dev/null
+++ b/test/regress/simple.cvc
@@ -0,0 +1,6 @@
+x0, x1, x2, x3 : BOOLEAN;
+ASSERT x1 OR NOT x0;
+ASSERT x0 OR NOT x3;
+ASSERT x3 OR x2;
+ASSERT NOT x1;
+QUERY x2;

diff --git a/test/regress/simple.smt b/test/regress/simple.smt
new file mode 100644 (file)
index 0000000..27a8c2c
--- /dev/null
+++ b/test/regress/simple.smt
@@ -0,0 +1,15 @@
+(benchmark b
+:status unknown
+:logic QF_IDL
+:extrapreds ((x0))
+:extrapreds ((x1))
+:extrapreds ((x2))
+:extrapreds ((x3))
+:formula
+(and (or x1 (not x0))
+     (or x0 (not x3))
+     (or x3 x2)
+     (not x1)
+     x2
+     x3)
+)