CvcParserBlack and supporting Makefile changes

diff --git a/.cproject b/.cproject
index 636868d6e1d4f043f5f6bac620f5b9cac1f2c66e..257d78fe05b1e3369fbdbb27919ec9b932d73bc0 100644 (file)
--- a/.cproject
+++ b/.cproject
@@ -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 &quot;${plugin_state_location}/${specs_file}&quot;'" 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 &quot;${plugin_state_location}/specs.cpp&quot;'" 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 &quot;${plugin_state_location}/specs.c&quot;'" 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 &quot;${plugin_state_location}/${specs_file}&quot;'" 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 &quot;${plugin_state_location}/specs.cpp&quot;'" 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 &quot;${plugin_state_location}/specs.c&quot;'" 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">

diff --git a/.project b/.project
index 878b8f93e088ffd411834447868b02537c6fc85c..9f40fa24590b32c32efd5c9fcd624b54bb20fdd8 100644 (file)
--- a/.project
+++ b/.project
@@ -9,6 +9,10 @@
                        <name>org.eclipse.cdt.managedbuilder.core.genmakebuilder</name>
                        <triggers>clean,full,incremental,</triggers>
                        <arguments>
+                               <dictionary>
+                                       <key>?children?</key>
+                                       <value>?name?=outputEntries\|?children?=?name?=entry\\\\\\\|\\\|\||</value>
+                               </dictionary>
                                <dictionary>
                                        <key>?name?</key>
                                        <value></value>

diff --git a/.settings/org.eclipse.cdt.core.prefs b/.settings/org.eclipse.cdt.core.prefs
index 720185193b4d90b1d2cdfc2162843d57584f9077..ae53af564af911fa0d7156fe9d03a98383338f02 100644 (file)
--- 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 f429e8b2a5d369e0c0b529278591a781ea2ba38d..110ab985584cb58a8231ba1facfc23dda0819f78 100644 (file)
--- 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 de268af1633e698c3de73c178342da414a6ff579..c650c15033509066ebd025a62958dfc533a991d1 100644 (file)
--- 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 7f1ddce1f626e41cde6b2a32e469047c8f051c41..86c088246edbd15b26cf9030d5f0f91c2f2734d5 100644 (file)
--- 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 f1b430add26b036baa5574b278397f372207b261..3b703efa01077ab94e6640aa2e717eff6d141486 100644 (file)
--- 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 f5ba6f4100fc33279361041219eb0e702d9aa135..cf78d8e347652a3da8d084e30c69fd5c0248a47b 100644 (file)
--- 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 23153db83e79921042239639f02c3f8edfb2156a..f20905330dcfe37c6ddf7d66d39f47d2854246fb 100644 (file)
--- 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 (file)
index 0000000..b34185e
--- /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() );
+      }
+  }
+};