More language bindings work:

* with a patched SWIG, the ocaml bindings build correctly.
** I will provide my patch to the SWIG dev team.
* fixed some class interfaces to play more nicely with SWIG.
* php, perl, tcl now work; examples added.
* improved binding module building and installation.

Also:

Stop #defining NULL ((void*) 0).  This has been in cvc4_public.h for
a long, long time, I forget why I added it in the first place, and
it's a very, very bad idea.  In C++, certain things are permitted
for NULL that aren't permitted for ((void*) 0), like for instance
implicit conversion to any pointer type.  We didn't see an issue
here (until now, when interfacing with SWIG), because GCC is usually
pretty smart at working around such a broken #definition of NULL.
But that's fragile.

New exception-free Command architecture.  Previously, some command
invocations were wrapped in a try {} catch() {} and printed out an
error.  This is much more consistent now.  Each Command invocation
results in a CommandStatus.  The status can be "unsupported",
"error", or "success" (these are each derived classes, though, not
strings, so that they can be easily printed in a language-specific
way... e.g., in SMT-LIBv2, they are printed in a manner consistent
with the spec, and "success" is not printed if the print-success
option is off.)  All Command functionality are now no-throw
functions, which @cconway reports is a Good Thing for Google
(where all C++ exceptions are suspect), and also I think is much
cleaner than the old way in this instance.

Added an --smtlib2 option that enables an "SMT-LIBv2 compliance
mode"---really it just sets a few other options like strictParsing,
inputLanguage, and printSuccess.  In the future we might put other
options into a compliance mode, or we might choose to make it the
default.

1 files changed, 86 insertions, 53 deletions

diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am
index ca09fc3d5..bfc116fd6 100644
--- a/src/bindings/Makefile.am
+++ b/src/bindings/Makefile.am
@@ -12,99 +12,139 @@
 #
 LIBCVC4BINDINGS_VERSION = @CVC4_BINDINGS_LIBRARY_VERSION@
 
+AUTOMAKE_OPTIONS = subdir-objects
+
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4BINDINGSLIB \
 	-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
 AM_CXXFLAGS = -Wall
 
-SUBDIRS = . compat
+SUBDIRS = compat
+
+# any binding-specific flags to pass to swig
+java_cpp_SWIGFLAGS = -package edu.nyu.acsys.CVC4
 
 lib_LTLIBRARIES =
 bin_PROGRAMS =
 javadatadir = $(datadir)/java
+javalibdir = $(datadir)/java
 ocamldatadir = $(libdir)/ocaml/cvc4
+ocamllibdir = $(libdir)/ocaml/cvc4
+perldatadir = $(datadir)/perl5
+perllibdir = $(libdir)/perl5
+phpdatadir = $(datadir)/php
+phplibdir = $(libdir)/php
+pythondatadir = $(datadir)/pyshared
+pythonlibdir = $(libdir)/pyshared
+csharpdatadir = $(datadir)/csharp
+csharplibdir = $(libdir)/csharp
+rubylibdir = $(libdir)/ruby
+tcllibdir = $(libdir)/tcltk
 javadata_DATA =
+javalib_LTLIBRARIES=
 ocamldata_DATA =
+ocamllib_LTLIBRARIES=
+perldata_DATA =
+perllib_LTLIBRARIES =
+phpdata_DATA =
+phplib_LTLIBRARIES =
+pythondata_DATA =
+pythonlib_LTLIBRARIES =
+csharpdata_DATA =
+csharplib_LTLIBRARIES =
+rubylib_LTLIBRARIES =
+tcllib_LTLIBRARIES =
 if CVC4_LANGUAGE_BINDING_JAVA
-lib_LTLIBRARIES += libcvc4bindings_java.la
+javalib_LTLIBRARIES += java/CVC4.la
 javadata_DATA += cvc4.jar
-libcvc4bindings_java_la_LDFLAGS = \
+java_CVC4_la_LDFLAGS = \
+	-module \
 	-version-info $(LIBCVC4BINDINGS_VERSION)
-libcvc4bindings_java_la_LIBADD = \
+java_CVC4_la_LIBADD = \
 	-L@builddir@/.. -lcvc4 \
 	-L@builddir@/../parser -lcvc4parser
 endif
 if CVC4_LANGUAGE_BINDING_CSHARP
-lib_LTLIBRARIES += libcvc4bindings_csharp.la
-libcvc4bindings_csharp_la_LDFLAGS = \
+csharplib_LTLIBRARIES += csharp/CVC4.la
+csharp_CVC4_la_LDFLAGS = \
+	-module \
 	-version-info $(LIBCVC4BINDINGS_VERSION)
-libcvc4bindings_csharp_la_LIBADD = \
+csharp_CVC4_la_LIBADD = \
 	-L@builddir@/.. -lcvc4 \
 	-L@builddir@/../parser -lcvc4parser
 endif
 if CVC4_LANGUAGE_BINDING_PERL
-lib_LTLIBRARIES += libcvc4bindings_perl.la
-libcvc4bindings_perl_la_LDFLAGS = \
+perllib_LTLIBRARIES += perl/CVC4.la
+perl_CVC4_la_LDFLAGS = \
+	-module \
 	-version-info $(LIBCVC4BINDINGS_VERSION)
-libcvc4bindings_perl_la_LIBADD = \
+perl_CVC4_la_LIBADD = \
 	-L@builddir@/.. -lcvc4 \
 	-L@builddir@/../parser -lcvc4parser
+perldata_DATA += perl/CVC4.pm
 endif
 if CVC4_LANGUAGE_BINDING_PHP
-lib_LTLIBRARIES += libcvc4bindings_php.la
-libcvc4bindings_php_la_LDFLAGS = \
+phplib_LTLIBRARIES += php/CVC4.la
+php_CVC4_la_LDFLAGS = \
+	-module \
 	-version-info $(LIBCVC4BINDINGS_VERSION)
-libcvc4bindings_php_la_LIBADD = \
+php_CVC4_la_LIBADD = \
 	-L@builddir@/.. -lcvc4 \
 	-L@builddir@/../parser -lcvc4parser
+phpdata_DATA += php/CVC4.php
 endif
 if CVC4_LANGUAGE_BINDING_PYTHON
-lib_LTLIBRARIES += libcvc4bindings_python.la
-libcvc4bindings_python_la_LDFLAGS = \
+pythonlib_LTLIBRARIES += python/CVC4.la
+python_CVC4_la_LDFLAGS = \
+	-module \
 	-version-info $(LIBCVC4BINDINGS_VERSION)
-libcvc4bindings_python_la_LIBADD = \
+python_CVC4_la_LIBADD = \
 	-L@builddir@/.. -lcvc4 \
 	-L@builddir@/../parser -lcvc4parser
+pythondata_DATA += python/CVC4.py
 endif
 if CVC4_LANGUAGE_BINDING_OCAML
-lib_LTLIBRARIES += libcvc4bindings_ocaml.la
+ocamllib_LTLIBRARIES += ocaml/CVC4.la
 bin_PROGRAMS += cvc4_ocaml_top
 # We provide a make rule below, but we have to tell automake to lay off, too,
 # otherwise it tries (and fails) to package the nonexistent cvc4_ocaml_top.c!
 cvc4_ocaml_top_SOURCES =
 ocamldata_DATA += ocaml/swig.cmo ocaml/swig.cmi ocaml/swigp4.cmo ocaml/swigp4.cmi ocaml/CVC4.cmo ocaml/CVC4.cmi
-libcvc4bindings_ocaml_la_LDFLAGS = \
+ocaml_CVC4_la_LDFLAGS = \
+	-module \
 	-version-info $(LIBCVC4BINDINGS_VERSION)
-libcvc4bindings_ocaml_la_LIBADD = \
+ocaml_CVC4_la_LIBADD = \
 	-L@builddir@/.. -lcvc4 \
 	-L@builddir@/../parser -lcvc4parser
 endif
 if CVC4_LANGUAGE_BINDING_RUBY
-lib_LTLIBRARIES += libcvc4bindings_ruby.la
-libcvc4bindings_ruby_la_LDFLAGS = \
+rubylib_LTLIBRARIES += ruby/CVC4.la
+ruby_CVC4_la_LDFLAGS = \
+	-module \
 	-version-info $(LIBCVC4BINDINGS_VERSION)
-libcvc4bindings_ruby_la_LIBADD = \
+ruby_CVC4_la_LIBADD = \
 	-L@builddir@/.. -lcvc4 \
 	-L@builddir@/../parser -lcvc4parser
 endif
 if CVC4_LANGUAGE_BINDING_TCL
-lib_LTLIBRARIES += libcvc4bindings_tcl.la
-libcvc4bindings_tcl_la_LDFLAGS = \
+tcllib_LTLIBRARIES += tcl/CVC4.la
+tcl_CVC4_la_LDFLAGS = \
+	-module \
 	-version-info $(LIBCVC4BINDINGS_VERSION)
-libcvc4bindings_tcl_la_LIBADD = \
+tcl_CVC4_la_LIBADD = \
 	-L@builddir@/.. -lcvc4 \
 	-L@builddir@/../parser -lcvc4parser
 endif
 
-nodist_libcvc4bindings_java_la_SOURCES = java.cpp
-libcvc4bindings_java_la_CXXFLAGS = -fno-strict-aliasing
-nodist_libcvc4bindings_csharp_la_SOURCES = csharp.cpp
-nodist_libcvc4bindings_perl_la_SOURCES = perl.cpp
-nodist_libcvc4bindings_php_la_SOURCES = php.cpp
-nodist_libcvc4bindings_python_la_SOURCES = python.cpp
-nodist_libcvc4bindings_ocaml_la_SOURCES = ocaml.cpp
-nodist_libcvc4bindings_ruby_la_SOURCES = ruby.cpp
-nodist_libcvc4bindings_tcl_la_SOURCES = tcl.cpp
+nodist_java_CVC4_la_SOURCES = java.cpp
+java_CVC4_la_CXXFLAGS = -fno-strict-aliasing
+nodist_csharp_CVC4_la_SOURCES = csharp.cpp
+nodist_perl_CVC4_la_SOURCES = perl.cpp
+nodist_php_CVC4_la_SOURCES = php.cpp
+nodist_python_CVC4_la_SOURCES = python.cpp
+nodist_ocaml_CVC4_la_SOURCES = ocaml.cpp
+nodist_ruby_CVC4_la_SOURCES = ruby.cpp
+nodist_tcl_CVC4_la_SOURCES = tcl.cpp
 
 CLEANFILES = \
 	java.cpp \
@@ -123,7 +163,7 @@ MOSTLYCLEANFILES = \
 	$(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))) \
 	cvc4.jar
 
-libcvc4bindings_java_la-java.lo java.lo: java.cpp
+java_CVC4_la-java.lo java.lo: java.cpp
 	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_CPPFLAGS) -o $@ $<
 cvc4.jar: java.cpp
 	$(AM_V_GEN) \
@@ -133,16 +173,17 @@ cvc4.jar: java.cpp
 	$(JAVAC) -classpath . -d classes `find . -name '*.java'`; \
 	cd classes); \
 	$(JAR) cf $@ -C java/classes .
-java.cpp:;
+#java.cpp:;
 csharp.lo: csharp.cpp
 	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(CSHARP_CPPFLAGS) -o $@ $<
-csharp.cpp:;
+#csharp.cpp:;
 perl.lo: perl.cpp
 	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(PERL_CPPFLAGS) -o $@ $<
-perl.cpp:;
+#perl.cpp:;
+perl/CVC4.pm: perl.cpp
 php.lo: php.cpp
 	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(PHP_CPPFLAGS) -Iphp -o $@ $<
-php.cpp:;
+#php.cpp:;
 python.lo: python.cpp
 	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(PYTHON_CPPFLAGS) -o $@ $<
 ocaml.lo: ocaml.cpp
@@ -155,26 +196,18 @@ ocaml/swigp4.cmo: ocaml/swigp4.ml; $(AM_V_GEN)$(OCAMLFIND) ocamlc -package camlp
 ocaml/swig.ml:; $(AM_V_GEN)cd ocaml && $(SWIG) -ocaml -co swig.ml
 ocaml/swig.mli:; $(AM_V_GEN)cd ocaml && $(SWIG) -ocaml -co swig.mli
 ocaml/swigp4.ml:; $(AM_V_GEN)cd ocaml && $(SWIG) -ocaml -co swigp4.ml
-ocaml.cpp:;
-cvc4_ocaml_top: libcvc4bindings_ocaml.la ocaml/swig.cmo ocaml/swig.cmi ocaml/swigp4.cmo ocaml/CVC4.cmo ocaml/CVC4.cmi libcvc4bindings_ocaml.la
+#ocaml.cpp:;
+cvc4_ocaml_top: ocaml/CVC4.la ocaml/swig.cmo ocaml/swig.cmi ocaml/swigp4.cmo ocaml/CVC4.cmo ocaml/CVC4.cmi
 	$(AM_V_GEN)\
-	$(OCAMLFIND) ocamlmktop -I $(ocamldatadir) -custom -o cvc4_ocaml_top -package camlp4 dynlink.cma camlp4o.cma ocaml/swig.cmo ocaml/swigp4.cmo ocaml/CVC4.cmo -cclib -L.libs -cclib -L. -cclib -lcvc4bindings_ocaml -cclib -lstdc++
+	$(OCAMLFIND) ocamlmktop -I $(ocamldatadir) -custom -o cvc4_ocaml_top -package camlp4 dynlink.cma camlp4o.cma ocaml/swig.cmo ocaml/swigp4.cmo ocaml/CVC4.cmo -cclib ocaml/.libs/CVC4.so -cclib -lstdc++
 ruby.lo: ruby.cpp
 	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(RUBY_CPPFLAGS) -o $@ $<
 tcl.lo: tcl.cpp
 	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(TCL_CPPFLAGS) -o $@ $<
-tcl.cpp:;
-java.cpp: @srcdir@/../cvc4.i
-	$(AM_V_at)mkdir -p $(patsubst %.cpp,%,$@)
-	$(AM_V_GEN)$(SWIG) -Wall -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -$(patsubst %.cpp,%,$@) -outdir $(patsubst %.cpp,%,$@) -package edu.nyu.acsys.CVC4 -o $@ $<
-# somehow, NULL gets translated to ((void*)0) prematurely, and this causes compiler errors ?!
-ruby.cpp python.cpp: @srcdir@/../cvc4.i
-	$(AM_V_at)mkdir -p $(patsubst %.cpp,%,$@)
-	$(AM_V_GEN)$(SWIG) -Wall -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -$(patsubst %.cpp,%,$@) -outdir $(patsubst %.cpp,%,$@) -o $@ $<
-	$(AM_V_at)mv $@ $@.old && sed 's,((void\*) 0),NULL,g' $@.old > $@
-$(patsubst %,%.cpp,$(filter-out c c++ java,$(CVC4_LANGUAGE_BINDINGS))): %.cpp: @srcdir@/../cvc4.i
+#tcl.cpp:;
+$(patsubst %,%.cpp,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))): %.cpp: @srcdir@/../cvc4.i
 	$(AM_V_at)mkdir -p $(patsubst %.cpp,%,$@)
-	$(AM_V_GEN)$(SWIG) -Wall -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -$(patsubst %.cpp,%,$@) -outdir $(patsubst %.cpp,%,$@) -o $@ $<
+	$(AM_V_GEN)$(SWIG) -Wall -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -$(patsubst %.cpp,%,$@) -outdir $(patsubst %.cpp,%,$@) $($(subst .,_,$@)_SWIGFLAGS) -o $@ $<
 
 $(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))): %.d: @srcdir@/../cvc4.i
 	$(AM_V_GEN)$(SWIG) -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -MM -o $(patsubst %.d,%.cpp,$@) $<