user push/pop support in minisat and simplification; also bindings work

1 files changed, 69 insertions, 9 deletions

diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am
index f9420dbdb..e35ec5e67 100644
--- a/src/bindings/Makefile.am
+++ b/src/bindings/Makefile.am
@@ -30,13 +30,62 @@ libcvc4bindings_java_la_LIBADD = \
 	-L@builddir@/.. -lcvc4 \
 	-L@builddir@/../parser -lcvc4parser
 endif
-#	cvc4bindings_csharp.so \
-#	cvc4bindings_perl.so \
-#	cvc4bindings_php.so \
-#	cvc4bindings_python.so \
-#	cvc4bindings_ocaml.so \
-#	cvc4bindings_ruby.so \
-#	cvc4bindings_tcl.so
+if CVC4_LANGUAGE_BINDING_CSHARP
+lib_LTLIBRARIES += libcvc4bindings_csharp.la
+libcvc4bindings_csharp_la_LDFLAGS = \
+	-version-info $(LIBCVC4BINDINGS_VERSION)
+libcvc4bindings_csharp_la_LIBADD = \
+	-L@builddir@/.. -lcvc4 \
+	-L@builddir@/../parser -lcvc4parser
+endif
+if CVC4_LANGUAGE_BINDING_PERL
+lib_LTLIBRARIES += libcvc4bindings_perl.la
+libcvc4bindings_perl_la_LDFLAGS = \
+	-version-info $(LIBCVC4BINDINGS_VERSION)
+libcvc4bindings_perl_la_LIBADD = \
+	-L@builddir@/.. -lcvc4 \
+	-L@builddir@/../parser -lcvc4parser
+endif
+if CVC4_LANGUAGE_BINDING_PHP
+lib_LTLIBRARIES += libcvc4bindings_php.la
+libcvc4bindings_php_la_LDFLAGS = \
+	-version-info $(LIBCVC4BINDINGS_VERSION)
+libcvc4bindings_php_la_LIBADD = \
+	-L@builddir@/.. -lcvc4 \
+	-L@builddir@/../parser -lcvc4parser
+endif
+if CVC4_LANGUAGE_BINDING_PYTHON
+lib_LTLIBRARIES += libcvc4bindings_python.la
+libcvc4bindings_python_la_LDFLAGS = \
+	-version-info $(LIBCVC4BINDINGS_VERSION)
+libcvc4bindings_python_la_LIBADD = \
+	-L@builddir@/.. -lcvc4 \
+	-L@builddir@/../parser -lcvc4parser
+endif
+if CVC4_LANGUAGE_BINDING_OCAML
+lib_LTLIBRARIES += libcvc4bindings_ocaml.la
+libcvc4bindings_ocaml_la_LDFLAGS = \
+	-version-info $(LIBCVC4BINDINGS_VERSION)
+libcvc4bindings_ocaml_la_LIBADD = \
+	-L@builddir@/.. -lcvc4 \
+	-L@builddir@/../parser -lcvc4parser
+endif
+if CVC4_LANGUAGE_BINDING_RUBY
+lib_LTLIBRARIES += libcvc4bindings_ruby.la
+libcvc4bindings_ruby_la_LDFLAGS = \
+	-version-info $(LIBCVC4BINDINGS_VERSION)
+libcvc4bindings_ruby_la_LIBADD = \
+	-L@builddir@/.. -lcvc4 \
+	-L@builddir@/../parser -lcvc4parser
+endif
+if CVC4_LANGUAGE_BINDING_TCL
+lib_LTLIBRARIES += libcvc4bindings_tcl.la
+libcvc4bindings_tcl_la_LDFLAGS = \
+	-version-info $(LIBCVC4BINDINGS_VERSION)
+libcvc4bindings_tcl_la_LIBADD = \
+	-L@builddir@/.. -lcvc4 \
+	-L@builddir@/../parser -lcvc4parser
+endif
 
 nodist_libcvc4bindings_java_la_SOURCES = java.cpp
 libcvc4bindings_java_la_CXXFLAGS = -fno-strict-aliasing
@@ -66,7 +115,7 @@ MOSTLYCLEANFILES = \
 	cvc4.jar
 
 java.lo: java.cpp
-	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_INCLUDES) -o $@ $<
+	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_CPPFLAGS) -o $@ $<
 cvc4.jar: java.cpp
 	$(AM_V_GEN) \
 	(cd java; \
@@ -77,15 +126,26 @@ cvc4.jar: java.cpp
 	$(JAR) cf $@ -C java/classes .
 java.cpp:
 csharp.cpp:
+perl.lo: perl.cpp
+	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(PERL_CPPFLAGS) -o $@ $<
 perl.cpp:
+php.lo: php.cpp
+	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(PHP_CPPFLAGS) -Iphp -o $@ $<
 php.cpp:
+python.lo: python.cpp
+	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(PYTHON_CPPFLAGS) -o $@ $<
 python.cpp:
 ocaml.cpp:
+python.lo: ruby.cpp
+	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(RUBY_CPPFLAGS) -o $@ $<
 ruby.cpp:
 tcl.cpp:
-$(patsubst %,%.cpp,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))): %.cpp: @srcdir@/../cvc4.i
+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 $@ $<
+$(patsubst %,%.cpp,$(filter-out c c++ java,$(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 $@ $<
 
 $(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,$@) $<