From: Christopher L. Conway Date: Thu, 17 Dec 2009 19:04:45 +0000 (+0000) Subject: CvcParserBlack and supporting Makefile changes X-Git-Tag: cvc5-1.0.0~9360 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d4e7b9cce6947498738bd3cfb67c11e3bf6c8dbe;p=cvc5.git CvcParserBlack and supporting Makefile changes --- diff --git a/.cproject b/.cproject index 636868d6e..257d78fe0 100644 --- a/.cproject +++ b/.cproject @@ -19,7 +19,11 @@ - + + + + + @@ -39,8 +43,14 @@ + + + + + + @@ -123,31 +133,185 @@ - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + - + - + - - + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +make + +check +true +true +true + + - - - - diff --git a/.project b/.project index 878b8f93e..9f40fa245 100644 --- a/.project +++ b/.project @@ -9,6 +9,10 @@ org.eclipse.cdt.managedbuilder.core.genmakebuilder clean,full,incremental, + + ?children? + ?name?=outputEntries\|?children?=?name?=entry\\\\\\\|\\\|\|| + ?name? diff --git a/.settings/org.eclipse.cdt.core.prefs b/.settings/org.eclipse.cdt.core.prefs index 720185193..ae53af564 100644 --- a/.settings/org.eclipse.cdt.core.prefs +++ b/.settings/org.eclipse.cdt.core.prefs @@ -1,4 +1,4 @@ -#Sun Dec 06 22:53:15 EST 2009 +#Tue Dec 08 17:39:14 EST 2009 eclipse.preferences.version=1 org.eclipse.cdt.core.formatter.alignment_for_arguments_in_method_invocation=18 org.eclipse.cdt.core.formatter.alignment_for_base_clause_in_type_declaration=80 diff --git a/src/Makefile.am b/src/Makefile.am index f429e8b2a..110ab9855 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -24,10 +24,15 @@ SUBDIRS = util expr context prop smt theory . parser main lib_LTLIBRARIES = libcvc4.la +noinst_LTLIBRARIES = libcvc4_noinst.la + libcvc4_la_LDFLAGS = -version-info $(LIBCVC4_VERSION) -release $(LIBCVC4_RELEASE) libcvc4_la_SOURCES = -libcvc4_la_LIBADD = \ +libcvc4_la_LIBADD = libcvc4_noinst.la + +libcvc4_noinst_la_SOURCES = +libcvc4_noinst_la_LIBADD = \ @builddir@/util/libutil.la \ @builddir@/expr/libexpr.la \ @builddir@/context/libcontext.la \ diff --git a/src/Makefile.in b/src/Makefile.in index de268af16..c650c1503 100644 --- a/src/Makefile.in +++ b/src/Makefile.in @@ -72,17 +72,20 @@ am__base_list = \ sed '$$!N;$$!N;$$!N;$$!N;$$!N;$$!N;$$!N;s/\n/ /g' | \ sed '$$!N;$$!N;$$!N;$$!N;s/\n/ /g' am__installdirs = "$(DESTDIR)$(libdir)" -LTLIBRARIES = $(lib_LTLIBRARIES) -libcvc4_la_DEPENDENCIES = @builddir@/util/libutil.la \ - @builddir@/expr/libexpr.la @builddir@/context/libcontext.la \ - @builddir@/prop/libprop.la \ - @builddir@/prop/minisat/libminisat.la @builddir@/smt/libsmt.la \ - @builddir@/theory/libtheory.la +LTLIBRARIES = $(lib_LTLIBRARIES) $(noinst_LTLIBRARIES) +libcvc4_la_DEPENDENCIES = libcvc4_noinst.la am_libcvc4_la_OBJECTS = libcvc4_la_OBJECTS = $(am_libcvc4_la_OBJECTS) libcvc4_la_LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) \ $(LIBTOOLFLAGS) --mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) \ $(libcvc4_la_LDFLAGS) $(LDFLAGS) -o $@ +libcvc4_noinst_la_DEPENDENCIES = @builddir@/util/libutil.la \ + @builddir@/expr/libexpr.la @builddir@/context/libcontext.la \ + @builddir@/prop/libprop.la \ + @builddir@/prop/minisat/libminisat.la @builddir@/smt/libsmt.la \ + @builddir@/theory/libtheory.la +am_libcvc4_noinst_la_OBJECTS = +libcvc4_noinst_la_OBJECTS = $(am_libcvc4_noinst_la_OBJECTS) DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir) COMPILE = $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) \ $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS) @@ -93,8 +96,8 @@ CCLD = $(CC) LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \ --mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) \ $(LDFLAGS) -o $@ -SOURCES = $(libcvc4_la_SOURCES) -DIST_SOURCES = $(libcvc4_la_SOURCES) +SOURCES = $(libcvc4_la_SOURCES) $(libcvc4_noinst_la_SOURCES) +DIST_SOURCES = $(libcvc4_la_SOURCES) $(libcvc4_noinst_la_SOURCES) RECURSIVE_TARGETS = all-recursive check-recursive dvi-recursive \ html-recursive info-recursive install-data-recursive \ install-dvi-recursive install-exec-recursive \ @@ -293,9 +296,12 @@ AM_CPPFLAGS = AM_CXXFLAGS = -Wall -fvisibility=hidden SUBDIRS = util expr context prop smt theory . parser main lib_LTLIBRARIES = libcvc4.la +noinst_LTLIBRARIES = libcvc4_noinst.la libcvc4_la_LDFLAGS = -version-info $(LIBCVC4_VERSION) -release $(LIBCVC4_RELEASE) libcvc4_la_SOURCES = -libcvc4_la_LIBADD = \ +libcvc4_la_LIBADD = libcvc4_noinst.la +libcvc4_noinst_la_SOURCES = +libcvc4_noinst_la_LIBADD = \ @builddir@/util/libutil.la \ @builddir@/expr/libexpr.la \ @builddir@/context/libcontext.la \ @@ -371,8 +377,19 @@ clean-libLTLIBRARIES: echo "rm -f \"$${dir}/so_locations\""; \ rm -f "$${dir}/so_locations"; \ done + +clean-noinstLTLIBRARIES: + -test -z "$(noinst_LTLIBRARIES)" || rm -f $(noinst_LTLIBRARIES) + @list='$(noinst_LTLIBRARIES)'; for p in $$list; do \ + dir="`echo $$p | sed -e 's|/[^/]*$$||'`"; \ + test "$$dir" != "$$p" || dir=.; \ + echo "rm -f \"$${dir}/so_locations\""; \ + rm -f "$${dir}/so_locations"; \ + done libcvc4.la: $(libcvc4_la_OBJECTS) $(libcvc4_la_DEPENDENCIES) $(libcvc4_la_LINK) -rpath $(libdir) $(libcvc4_la_OBJECTS) $(libcvc4_la_LIBADD) $(LIBS) +libcvc4_noinst.la: $(libcvc4_noinst_la_OBJECTS) $(libcvc4_noinst_la_DEPENDENCIES) + $(LINK) $(libcvc4_noinst_la_OBJECTS) $(libcvc4_noinst_la_LIBADD) $(LIBS) mostlyclean-compile: -rm -f *.$(OBJEXT) @@ -615,7 +632,7 @@ maintainer-clean-generic: clean: clean-recursive clean-am: clean-generic clean-libLTLIBRARIES clean-libtool \ - mostlyclean-am + clean-noinstLTLIBRARIES mostlyclean-am distclean: distclean-recursive -rm -f Makefile @@ -686,16 +703,16 @@ uninstall-am: uninstall-libLTLIBRARIES .PHONY: $(RECURSIVE_CLEAN_TARGETS) $(RECURSIVE_TARGETS) CTAGS GTAGS \ all all-am check check-am clean clean-generic \ - clean-libLTLIBRARIES clean-libtool ctags ctags-recursive \ - distclean distclean-compile distclean-generic \ - distclean-libtool distclean-tags distdir dvi dvi-am html \ - html-am info info-am install install-am install-data \ - install-data-am install-data-local install-dvi install-dvi-am \ - install-exec install-exec-am install-html install-html-am \ - install-info install-info-am install-libLTLIBRARIES \ - install-man install-pdf install-pdf-am install-ps \ - install-ps-am install-strip installcheck installcheck-am \ - installdirs installdirs-am maintainer-clean \ + clean-libLTLIBRARIES clean-libtool clean-noinstLTLIBRARIES \ + ctags ctags-recursive distclean distclean-compile \ + distclean-generic distclean-libtool distclean-tags distdir dvi \ + dvi-am html html-am info info-am install install-am \ + install-data install-data-am install-data-local install-dvi \ + install-dvi-am install-exec install-exec-am install-html \ + install-html-am install-info install-info-am \ + install-libLTLIBRARIES install-man install-pdf install-pdf-am \ + install-ps install-ps-am install-strip installcheck \ + installcheck-am installdirs installdirs-am maintainer-clean \ maintainer-clean-generic mostlyclean mostlyclean-compile \ mostlyclean-generic mostlyclean-libtool pdf pdf-am ps ps-am \ tags tags-recursive uninstall uninstall-am \ diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 7f1ddce1f..86c088246 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -23,13 +23,18 @@ AM_CXXFLAGS = -Wall -fvisibility=hidden SUBDIRS = smt cvc nobase_lib_LTLIBRARIES = libcvc4parser.la +noinst_LTLIBRARIES = libcvc4parser_noinst.la libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS) -libcvc4parser_la_LIBADD = \ +libcvc4parser_la_LIBADD = libcvc4parser_noinst.la + +libcvc4parser_noinst_la_LDFLAGS = $(ANTLR_LDFLAGS) +libcvc4parser_noinst_la_LIBADD = \ @builddir@/smt/libparsersmt.la \ @builddir@/cvc/libparsercvc.la -libcvc4parser_la_SOURCES = \ +libcvc4parser_la_SOURCES = +libcvc4parser_noinst_la_SOURCES = \ parser.h \ parser.cpp \ parser_exception.h \ diff --git a/src/parser/Makefile.in b/src/parser/Makefile.in index f1b430add..3b703efa0 100644 --- a/src/parser/Makefile.in +++ b/src/parser/Makefile.in @@ -72,14 +72,22 @@ am__base_list = \ sed '$$!N;$$!N;$$!N;$$!N;$$!N;$$!N;$$!N;s/\n/ /g' | \ sed '$$!N;$$!N;$$!N;$$!N;s/\n/ /g' am__installdirs = "$(DESTDIR)$(libdir)" -LTLIBRARIES = $(nobase_lib_LTLIBRARIES) -libcvc4parser_la_DEPENDENCIES = @builddir@/smt/libparsersmt.la \ - @builddir@/cvc/libparsercvc.la -am_libcvc4parser_la_OBJECTS = parser.lo antlr_parser.lo +LTLIBRARIES = $(nobase_lib_LTLIBRARIES) $(noinst_LTLIBRARIES) +libcvc4parser_la_DEPENDENCIES = libcvc4parser_noinst.la +am_libcvc4parser_la_OBJECTS = libcvc4parser_la_OBJECTS = $(am_libcvc4parser_la_OBJECTS) -libcvc4parser_la_LINK = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) \ +libcvc4parser_la_LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) \ + $(LIBTOOLFLAGS) --mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) \ + $(libcvc4parser_la_LDFLAGS) $(LDFLAGS) -o $@ +libcvc4parser_noinst_la_DEPENDENCIES = @builddir@/smt/libparsersmt.la \ + @builddir@/cvc/libparsercvc.la +am_libcvc4parser_noinst_la_OBJECTS = parser.lo antlr_parser.lo +libcvc4parser_noinst_la_OBJECTS = \ + $(am_libcvc4parser_noinst_la_OBJECTS) +libcvc4parser_noinst_la_LINK = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) \ $(LIBTOOLFLAGS) --mode=link $(CXXLD) $(AM_CXXFLAGS) \ - $(CXXFLAGS) $(libcvc4parser_la_LDFLAGS) $(LDFLAGS) -o $@ + $(CXXFLAGS) $(libcvc4parser_noinst_la_LDFLAGS) $(LDFLAGS) -o \ + $@ DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir) depcomp = $(SHELL) $(top_srcdir)/config/depcomp am__depfiles_maybe = depfiles @@ -102,8 +110,10 @@ CCLD = $(CC) LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \ --mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) $(AM_LDFLAGS) \ $(LDFLAGS) -o $@ -SOURCES = $(libcvc4parser_la_SOURCES) -DIST_SOURCES = $(libcvc4parser_la_SOURCES) +SOURCES = $(libcvc4parser_la_SOURCES) \ + $(libcvc4parser_noinst_la_SOURCES) +DIST_SOURCES = $(libcvc4parser_la_SOURCES) \ + $(libcvc4parser_noinst_la_SOURCES) RECURSIVE_TARGETS = all-recursive check-recursive dvi-recursive \ html-recursive info-recursive install-data-recursive \ install-dvi-recursive install-exec-recursive \ @@ -305,12 +315,16 @@ AM_CPPFLAGS = \ AM_CXXFLAGS = -Wall -fvisibility=hidden SUBDIRS = smt cvc nobase_lib_LTLIBRARIES = libcvc4parser.la +noinst_LTLIBRARIES = libcvc4parser_noinst.la libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS) -libcvc4parser_la_LIBADD = \ +libcvc4parser_la_LIBADD = libcvc4parser_noinst.la +libcvc4parser_noinst_la_LDFLAGS = $(ANTLR_LDFLAGS) +libcvc4parser_noinst_la_LIBADD = \ @builddir@/smt/libparsersmt.la \ @builddir@/cvc/libparsercvc.la -libcvc4parser_la_SOURCES = \ +libcvc4parser_la_SOURCES = +libcvc4parser_noinst_la_SOURCES = \ parser.h \ parser.cpp \ parser_exception.h \ @@ -389,8 +403,19 @@ clean-nobase_libLTLIBRARIES: echo "rm -f \"$${dir}/so_locations\""; \ rm -f "$${dir}/so_locations"; \ done + +clean-noinstLTLIBRARIES: + -test -z "$(noinst_LTLIBRARIES)" || rm -f $(noinst_LTLIBRARIES) + @list='$(noinst_LTLIBRARIES)'; for p in $$list; do \ + dir="`echo $$p | sed -e 's|/[^/]*$$||'`"; \ + test "$$dir" != "$$p" || dir=.; \ + echo "rm -f \"$${dir}/so_locations\""; \ + rm -f "$${dir}/so_locations"; \ + done libcvc4parser.la: $(libcvc4parser_la_OBJECTS) $(libcvc4parser_la_DEPENDENCIES) $(libcvc4parser_la_LINK) -rpath $(libdir)/. $(libcvc4parser_la_OBJECTS) $(libcvc4parser_la_LIBADD) $(LIBS) +libcvc4parser_noinst.la: $(libcvc4parser_noinst_la_OBJECTS) $(libcvc4parser_noinst_la_DEPENDENCIES) + $(libcvc4parser_noinst_la_LINK) $(libcvc4parser_noinst_la_OBJECTS) $(libcvc4parser_noinst_la_LIBADD) $(LIBS) mostlyclean-compile: -rm -f *.$(OBJEXT) @@ -657,7 +682,7 @@ maintainer-clean-generic: clean: clean-recursive clean-am: clean-generic clean-libtool clean-nobase_libLTLIBRARIES \ - mostlyclean-am + clean-noinstLTLIBRARIES mostlyclean-am distclean: distclean-recursive -rm -rf ./$(DEPDIR) @@ -730,19 +755,19 @@ uninstall-am: uninstall-nobase_libLTLIBRARIES .PHONY: $(RECURSIVE_CLEAN_TARGETS) $(RECURSIVE_TARGETS) CTAGS GTAGS \ all all-am check check-am clean clean-generic clean-libtool \ - clean-nobase_libLTLIBRARIES ctags ctags-recursive distclean \ - distclean-compile distclean-generic distclean-libtool \ - distclean-tags distdir dvi dvi-am html html-am info info-am \ - install install-am install-data install-data-am install-dvi \ - install-dvi-am install-exec install-exec-am install-html \ - install-html-am install-info install-info-am install-man \ - install-nobase_libLTLIBRARIES install-pdf install-pdf-am \ - install-ps install-ps-am install-strip installcheck \ - installcheck-am installdirs installdirs-am maintainer-clean \ - maintainer-clean-generic mostlyclean mostlyclean-compile \ - mostlyclean-generic mostlyclean-libtool pdf pdf-am ps ps-am \ - tags tags-recursive uninstall uninstall-am \ - uninstall-nobase_libLTLIBRARIES + clean-nobase_libLTLIBRARIES clean-noinstLTLIBRARIES ctags \ + ctags-recursive distclean distclean-compile distclean-generic \ + distclean-libtool distclean-tags distdir dvi dvi-am html \ + html-am info info-am install install-am install-data \ + install-data-am install-dvi install-dvi-am install-exec \ + install-exec-am install-html install-html-am install-info \ + install-info-am install-man install-nobase_libLTLIBRARIES \ + install-pdf install-pdf-am install-ps install-ps-am \ + install-strip installcheck installcheck-am installdirs \ + installdirs-am maintainer-clean maintainer-clean-generic \ + mostlyclean mostlyclean-compile mostlyclean-generic \ + mostlyclean-libtool pdf pdf-am ps ps-am tags tags-recursive \ + uninstall uninstall-am uninstall-nobase_libLTLIBRARIES # Tell versions [3.59,3.63) of GNU make to not export all variables. diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index f5ba6f410..cf78d8e34 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -6,13 +6,8 @@ AM_CXXFLAGS_WHITE = -fno-access-control AM_CXXFLAGS_BLACK = AM_CXXFLAGS_PUBLIC = AM_LDFLAGS_WHITE = \ - @abs_top_builddir@/src/context/libcontext.la \ - @abs_top_builddir@/src/expr/libexpr.la \ - @abs_top_builddir@/src/smt/libsmt.la \ - @abs_top_builddir@/src/theory/libtheory.la \ - @abs_top_builddir@/src/util/libutil.la \ - @abs_top_builddir@/src/prop/libprop.la \ - @abs_top_builddir@/src/prop/minisat/libminisat.la + @abs_top_builddir@/src/parser/libcvc4parser_noinst.la \ + @abs_top_builddir@/src/libcvc4_noinst.la AM_LDFLAGS_BLACK = \ $(AM_LDFLAGS_WHITE) AM_LDFLAGS_PUBLIC = \ @@ -20,7 +15,8 @@ AM_LDFLAGS_PUBLIC = \ TESTS = \ expr/node_white \ - expr/node_black + expr/node_black \ + parser/cvc/cvc_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 23153db83..f20905330 100644 --- a/test/unit/Makefile.in +++ b/test/unit/Makefile.in @@ -220,13 +220,8 @@ top_srcdir = @top_srcdir@ @HAVE_CXXTESTGEN_TRUE@AM_CXXFLAGS_BLACK = @HAVE_CXXTESTGEN_TRUE@AM_CXXFLAGS_PUBLIC = @HAVE_CXXTESTGEN_TRUE@AM_LDFLAGS_WHITE = \ -@HAVE_CXXTESTGEN_TRUE@ @abs_top_builddir@/src/context/libcontext.la \ -@HAVE_CXXTESTGEN_TRUE@ @abs_top_builddir@/src/expr/libexpr.la \ -@HAVE_CXXTESTGEN_TRUE@ @abs_top_builddir@/src/smt/libsmt.la \ -@HAVE_CXXTESTGEN_TRUE@ @abs_top_builddir@/src/theory/libtheory.la \ -@HAVE_CXXTESTGEN_TRUE@ @abs_top_builddir@/src/util/libutil.la \ -@HAVE_CXXTESTGEN_TRUE@ @abs_top_builddir@/src/prop/libprop.la \ -@HAVE_CXXTESTGEN_TRUE@ @abs_top_builddir@/src/prop/minisat/libminisat.la +@HAVE_CXXTESTGEN_TRUE@ @abs_top_builddir@/src/parser/libcvc4parser_noinst.la \ +@HAVE_CXXTESTGEN_TRUE@ @abs_top_builddir@/src/libcvc4_noinst.la @HAVE_CXXTESTGEN_TRUE@AM_LDFLAGS_BLACK = \ @HAVE_CXXTESTGEN_TRUE@ $(AM_LDFLAGS_WHITE) @@ -239,7 +234,8 @@ top_srcdir = @top_srcdir@ @HAVE_CXXTESTGEN_FALSE@TESTS = no_cxxtest @HAVE_CXXTESTGEN_TRUE@TESTS = \ @HAVE_CXXTESTGEN_TRUE@ expr/node_white \ -@HAVE_CXXTESTGEN_TRUE@ expr/node_black +@HAVE_CXXTESTGEN_TRUE@ expr/node_black \ +@HAVE_CXXTESTGEN_TRUE@ parser/cvc/cvc_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 new file mode 100644 index 000000000..b34185e01 --- /dev/null +++ b/test/unit/parser/cvc/cvc_parser_black.h @@ -0,0 +1,46 @@ +/* Black box testing of CVC4::Node. */ + +#include +//#include +#include + +#include "expr/expr_manager.h" +#include "parser/cvc/cvc_parser.h" + +using namespace CVC4; +using namespace CVC4::parser; +using namespace std; + +const string d_goodInputs[] = { + "ASSERT TRUE;", + "QUERY TRUE;", + "CHECKSAT FALSE;", + "a, b : BOOLEAN;", + "x, y : INT;", + "a, b : BOOLEAN; QUERY (a => b) AND a => b;" + }; + +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); + TS_ASSERT( !cvcParser.done() ); + while( !cvcParser.done() ) { + TS_ASSERT( cvcParser.parseNextCommand() ); + } + } +};