diff options
| -rw-r--r-- | .cproject | 190 | ||||
| -rw-r--r-- | .project | 4 | ||||
| -rw-r--r-- | .settings/org.eclipse.cdt.core.prefs | 2 | ||||
| -rw-r--r-- | src/Makefile.am | 7 | ||||
| -rw-r--r-- | src/Makefile.in | 57 | ||||
| -rw-r--r-- | src/parser/Makefile.am | 9 | ||||
| -rw-r--r-- | src/parser/Makefile.in | 73 | ||||
| -rw-r--r-- | test/unit/Makefile.am | 12 | ||||
| -rw-r--r-- | test/unit/Makefile.in | 12 | ||||
| -rw-r--r-- | test/unit/parser/cvc/cvc_parser_black.h | 46 |
10 files changed, 335 insertions, 77 deletions
@@ -19,7 +19,11 @@ <folderInfo id="cdt.managedbuild.toolchain.gnu.base.1461790692.1059214216" name="/" resourcePath=""> <toolChain id="cdt.managedbuild.toolchain.gnu.base.1311293674" name="cdt.managedbuild.toolchain.gnu.base" superClass="cdt.managedbuild.toolchain.gnu.base"> <targetPlatform archList="all" binaryParser="org.eclipse.cdt.core.ELF" id="cdt.managedbuild.target.gnu.platform.base.1799734525" name="Debug Platform" osList="linux,hpux,aix,qnx" superClass="cdt.managedbuild.target.gnu.platform.base"/> -<builder buildPath="${workspace_loc/cvc4/}" id="cdt.managedbuild.target.gnu.builder.base.549477204" incrementalBuildTarget="all" keepEnvironmentInBuildfile="false" managedBuildOn="false" name="Gnu Make Builder" parallelBuildOn="false" parallelizationNumber="-1" superClass="cdt.managedbuild.target.gnu.builder.base"/> +<builder buildPath="${workspace_loc/cvc4/}" id="cdt.managedbuild.target.gnu.builder.base.549477204" incrementalBuildTarget="all" keepEnvironmentInBuildfile="false" managedBuildOn="false" name="Gnu Make Builder" parallelBuildOn="false" parallelizationNumber="-1" superClass="cdt.managedbuild.target.gnu.builder.base"> +<outputEntries> +<entry flags="VALUE_WORKSPACE_PATH|RESOLVED" kind="outputPath" name=""/> +</outputEntries> +</builder> <tool id="cdt.managedbuild.tool.gnu.archiver.base.888684090" name="GCC Archiver" superClass="cdt.managedbuild.tool.gnu.archiver.base"/> <tool id="cdt.managedbuild.tool.gnu.cpp.compiler.base.1803857875" name="GCC C++ Compiler" superClass="cdt.managedbuild.tool.gnu.cpp.compiler.base"> <inputType id="cdt.managedbuild.tool.gnu.cpp.compiler.input.1333398893" superClass="cdt.managedbuild.tool.gnu.cpp.compiler.input"/> @@ -39,8 +43,14 @@ </tool> </toolChain> </folderInfo> +<sourceEntries> +<entry excluding="parser" flags="VALUE_WORKSPACE_PATH|RESOLVED" kind="sourcePath" name=""/> +</sourceEntries> </configuration> </storageModule> +<storageModule moduleId="org.eclipse.cdt.core.externalSettings"/> +<storageModule moduleId="org.eclipse.cdt.internal.ui.text.commentOwnerProjectMappings"/> +<storageModule moduleId="org.eclipse.cdt.core.language.mapping"/> <storageModule moduleId="scannerConfiguration"> <autodiscovery enabled="true" problemReportingEnabled="true" selectedProfileId=""/> <profile id="org.eclipse.cdt.make.core.GCCStandardMakePerProjectProfile"> @@ -123,31 +133,185 @@ <parser enabled="true"/> </scannerInfoProvider> </profile> -<profile id="org.eclipse.cdt.managedbuilder.xlc.core.XLCManagedMakePerProjectProfile"> +<scannerConfigBuildInfo instanceId="cdt.managedbuild.toolchain.gnu.base.1461790692;cdt.managedbuild.toolchain.gnu.base.1461790692.1059214216;cdt.managedbuild.tool.gnu.cpp.compiler.base.1803857875;cdt.managedbuild.tool.gnu.cpp.compiler.input.1333398893"> +<autodiscovery enabled="true" problemReportingEnabled="true" selectedProfileId="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileCPP"/> +<profile id="org.eclipse.cdt.make.core.GCCStandardMakePerProjectProfile"> +<buildOutputProvider> +<openAction enabled="true" filePath=""/> +<parser enabled="true"/> +</buildOutputProvider> +<scannerInfoProvider id="specsFile"> +<runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/> +<parser enabled="true"/> +</scannerInfoProvider> +</profile> +<profile id="org.eclipse.cdt.make.core.GCCStandardMakePerFileProfile"> +<buildOutputProvider> +<openAction enabled="true" filePath=""/> +<parser enabled="true"/> +</buildOutputProvider> +<scannerInfoProvider id="makefileGenerator"> +<runAction arguments="-f ${project_name}_scd.mk" command="make" useDefault="true"/> +<parser enabled="true"/> +</scannerInfoProvider> +</profile> +<profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfile"> +<buildOutputProvider> +<openAction enabled="true" filePath=""/> +<parser enabled="true"/> +</buildOutputProvider> +<scannerInfoProvider id="specsFile"> +<runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/> +<parser enabled="true"/> +</scannerInfoProvider> +</profile> +<profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileCPP"> +<buildOutputProvider> +<openAction enabled="true" filePath=""/> +<parser enabled="true"/> +</buildOutputProvider> +<scannerInfoProvider id="specsFile"> +<runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.cpp" command="g++" useDefault="true"/> +<parser enabled="true"/> +</scannerInfoProvider> +</profile> +<profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileC"> <buildOutputProvider> -<openAction enabled="false" filePath=""/> -<parser enabled="false"/> +<openAction enabled="true" filePath=""/> +<parser enabled="true"/> </buildOutputProvider> <scannerInfoProvider id="specsFile"> -<runAction arguments="-E -v ${plugin_state_location}/${specs_file}" command="${XL_compilerRoot}/xlc" useDefault="true"/> +<runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.c" command="gcc" useDefault="true"/> <parser enabled="true"/> </scannerInfoProvider> </profile> -<profile id="org.eclipse.cdt.managedbuilder.xlc.core.XLCManagedMakePerProjectProfileCPP"> +<profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfile"> <buildOutputProvider> -<openAction enabled="false" filePath=""/> -<parser enabled="false"/> +<openAction enabled="true" filePath=""/> +<parser enabled="true"/> </buildOutputProvider> <scannerInfoProvider id="specsFile"> -<runAction arguments="-E -v ${plugin_state_location}/${specs_file}" command="${XL_compilerRoot}/xlC" useDefault="true"/> +<runAction arguments="-c 'gcc -E -P -v -dD "${plugin_state_location}/${specs_file}"'" command="sh" useDefault="true"/> <parser enabled="true"/> </scannerInfoProvider> </profile> +<profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileCPP"> +<buildOutputProvider> +<openAction enabled="true" filePath=""/> +<parser enabled="true"/> +</buildOutputProvider> +<scannerInfoProvider id="specsFile"> +<runAction arguments="-c 'g++ -E -P -v -dD "${plugin_state_location}/specs.cpp"'" command="sh" useDefault="true"/> +<parser enabled="true"/> +</scannerInfoProvider> +</profile> +<profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileC"> +<buildOutputProvider> +<openAction enabled="true" filePath=""/> +<parser enabled="true"/> +</buildOutputProvider> +<scannerInfoProvider id="specsFile"> +<runAction arguments="-c 'gcc -E -P -v -dD "${plugin_state_location}/specs.c"'" command="sh" useDefault="true"/> +<parser enabled="true"/> +</scannerInfoProvider> +</profile> +</scannerConfigBuildInfo> +<scannerConfigBuildInfo instanceId="cdt.managedbuild.toolchain.gnu.base.1461790692;cdt.managedbuild.toolchain.gnu.base.1461790692.1059214216;cdt.managedbuild.tool.gnu.c.compiler.base.1860041504;cdt.managedbuild.tool.gnu.c.compiler.input.814325769"> +<autodiscovery enabled="true" problemReportingEnabled="true" selectedProfileId="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileC"/> +<profile id="org.eclipse.cdt.make.core.GCCStandardMakePerProjectProfile"> +<buildOutputProvider> +<openAction enabled="true" filePath=""/> +<parser enabled="true"/> +</buildOutputProvider> +<scannerInfoProvider id="specsFile"> +<runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/> +<parser enabled="true"/> +</scannerInfoProvider> +</profile> +<profile id="org.eclipse.cdt.make.core.GCCStandardMakePerFileProfile"> +<buildOutputProvider> +<openAction enabled="true" filePath=""/> +<parser enabled="true"/> +</buildOutputProvider> +<scannerInfoProvider id="makefileGenerator"> +<runAction arguments="-f ${project_name}_scd.mk" command="make" useDefault="true"/> +<parser enabled="true"/> +</scannerInfoProvider> +</profile> +<profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfile"> +<buildOutputProvider> +<openAction enabled="true" filePath=""/> +<parser enabled="true"/> +</buildOutputProvider> +<scannerInfoProvider id="specsFile"> +<runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/> +<parser enabled="true"/> +</scannerInfoProvider> +</profile> +<profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileCPP"> +<buildOutputProvider> +<openAction enabled="true" filePath=""/> +<parser enabled="true"/> +</buildOutputProvider> +<scannerInfoProvider id="specsFile"> +<runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.cpp" command="g++" useDefault="true"/> +<parser enabled="true"/> +</scannerInfoProvider> +</profile> +<profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileC"> +<buildOutputProvider> +<openAction enabled="true" filePath=""/> +<parser enabled="true"/> +</buildOutputProvider> +<scannerInfoProvider id="specsFile"> +<runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.c" command="gcc" useDefault="true"/> +<parser enabled="true"/> +</scannerInfoProvider> +</profile> +<profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfile"> +<buildOutputProvider> +<openAction enabled="true" filePath=""/> +<parser enabled="true"/> +</buildOutputProvider> +<scannerInfoProvider id="specsFile"> +<runAction arguments="-c 'gcc -E -P -v -dD "${plugin_state_location}/${specs_file}"'" command="sh" useDefault="true"/> +<parser enabled="true"/> +</scannerInfoProvider> +</profile> +<profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileCPP"> +<buildOutputProvider> +<openAction enabled="true" filePath=""/> +<parser enabled="true"/> +</buildOutputProvider> +<scannerInfoProvider id="specsFile"> +<runAction arguments="-c 'g++ -E -P -v -dD "${plugin_state_location}/specs.cpp"'" command="sh" useDefault="true"/> +<parser enabled="true"/> +</scannerInfoProvider> +</profile> +<profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileC"> +<buildOutputProvider> +<openAction enabled="true" filePath=""/> +<parser enabled="true"/> +</buildOutputProvider> +<scannerInfoProvider id="specsFile"> +<runAction arguments="-c 'gcc -E -P -v -dD "${plugin_state_location}/specs.c"'" command="sh" useDefault="true"/> +<parser enabled="true"/> +</scannerInfoProvider> +</profile> +</scannerConfigBuildInfo> +</storageModule> +<storageModule moduleId="org.eclipse.cdt.make.core.buildtargets"> +<buildTargets> +<target name="check" path="" targetID="org.eclipse.cdt.build.MakeTargetBuilder"> +<buildCommand>make</buildCommand> +<buildArguments/> +<buildTarget>check</buildTarget> +<stopOnError>true</stopOnError> +<useDefaultCommand>true</useDefaultCommand> +<runAllBuilders>true</runAllBuilders> +</target> +</buildTargets> </storageModule> -<storageModule moduleId="org.eclipse.cdt.core.externalSettings"/> -<storageModule moduleId="org.eclipse.cdt.internal.ui.text.commentOwnerProjectMappings"/> -<storageModule moduleId="org.eclipse.cdt.core.language.mapping"/> -<storageModule moduleId="org.eclipse.cdt.make.core.buildtargets"/> </cconfiguration> </storageModule> <storageModule moduleId="cdtBuildSystem" version="4.0.0"> @@ -10,6 +10,10 @@ <triggers>clean,full,incremental,</triggers> <arguments> <dictionary> + <key>?children?</key> + <value>?name?=outputEntries\|?children?=?name?=entry\\\\\\\|\\\|\||</value> + </dictionary> + <dictionary> <key>?name?</key> <value></value> </dictionary> 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 <cxxtest/TestSuite.h> +//#include <string> +#include <sstream> + +#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() ); + } + } +}; |