From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 7 Dec 2009 23:23:33 +0000 (+0000)
Subject: fixing a few broken build-related items, adding test cases
X-Git-Tag: cvc5-1.0.0~9389
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=abe5fb451ae66a4bedc88d870e99f76de4eb323c;p=cvc5.git

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 2619b2dac..4c1a5d92b 100644
--- 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 35b5bafd7..6017409fd 100644
--- 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 61deb03e6..a4a06c10b 100644
--- 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
index 000000000..c1a5dd840
--- /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
index 000000000..27a8c2cd0
--- /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)
+)