summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--config/bindings.m42
-rw-r--r--examples/README6
-rw-r--r--examples/SimpleVC.rb57
-rw-r--r--src/bindings/Makefile.am26
4 files changed, 79 insertions, 12 deletions
diff --git a/config/bindings.m4 b/config/bindings.m4
index 5306c8c77..61b93a8cb 100644
--- a/config/bindings.m4
+++ b/config/bindings.m4
@@ -105,7 +105,7 @@ else
AC_MSG_RESULT([tcl support will be built])
AC_ARG_VAR(TCL_CPPFLAGS, [flags to pass to compiler when building tcl bindings])
CPPFLAGS="$CPPFLAGS $TCL_CPPFLAGS"
- cvc4_build_tcl_bindings=yes
+ AC_CHECK_HEADER([tcl.h], [cvc4_build_tcl_bindings=yes], [binding_error=yes])
;;
ocaml)
AC_MSG_RESULT([OCaml support will be built])
diff --git a/examples/README b/examples/README
index 1ba0a54e6..0861092e7 100644
--- a/examples/README
+++ b/examples/README
@@ -9,4 +9,8 @@ directory. With the default configuration, you'll find them in
builds/examples in the top-level source directory (if you configured
your own build directory, you'll find them there).
--- Morgan Deters <mdeters@cs.nyu.edu> Fri, 30 Sep 2011 16:19:46 -0400
+Many of the examples (python, ocaml, ruby, etc.) do not need to be
+compiled to run. These are not compiled by "make"---see the comments
+in the files for ideas on how to run them.
+
+-- Morgan Deters <mdeters@cs.nyu.edu> Wed, 16 Nov 2011 02:48:19 -0500
diff --git a/examples/SimpleVC.rb b/examples/SimpleVC.rb
new file mode 100644
index 000000000..ef4d82983
--- /dev/null
+++ b/examples/SimpleVC.rb
@@ -0,0 +1,57 @@
+###################### ##
+##! \file SimpleVC.rb
+### \verbatim
+### Original author: mdeters
+### Major contributors: none
+### Minor contributors (to current version): none
+### This file is part of the CVC4 prototype.
+### Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+### Courant Institute of Mathematical Sciences
+### New York University
+### See the file COPYING in the top-level source directory for licensing
+### information.\endverbatim
+###
+### \brief A simple demonstration of the Ruby interface
+###
+### A simple demonstration of the Ruby interface. Compare to the
+### C++ interface in simple_vc_cxx.cpp; they are quite similar.
+###
+### To run, use something like:
+###
+### ln -s ../builds/src/bindings/.libs/libcvc4bindings_ruby.so.0.0.0 CVC4.so
+### ruby SimpleVC.rb
+####
+
+require 'CVC4'
+include CVC4 # CVC4::Integer still has to be qualified
+
+em = ExprManager.new
+smt = SmtEngine.new(em)
+
+# Prove that for integers x and y:
+# x > 0 AND y > 0 => 2x + y >= 3
+
+integer = em.integerType
+
+x = em.mkVar("x", integer)
+y = em.mkVar("y", integer)
+zero = em.mkConst(CVC4::Integer.new(0))
+
+x_positive = em.mkExpr(GT, x, zero)
+y_positive = em.mkExpr(GT, y, zero)
+
+two = em.mkConst(CVC4::Integer.new(2))
+twox = em.mkExpr(MULT, two, x)
+twox_plus_y = em.mkExpr(PLUS, twox, y)
+
+three = em.mkConst(CVC4::Integer.new(3))
+twox_plus_y_geq_3 = em.mkExpr(GEQ, twox_plus_y, three)
+
+formula = BoolExpr.new(em.mkExpr(AND, x_positive, y_positive)).impExpr(BoolExpr.new(twox_plus_y_geq_3))
+
+puts "Checking validity of formula " + formula.toString + " with CVC4."
+puts "CVC4 should report VALID."
+puts "Result from CVC4 is: " + smt.query(formula).toString
+
+exit
+
diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am
index 2a2754c37..ca09fc3d5 100644
--- a/src/bindings/Makefile.am
+++ b/src/bindings/Makefile.am
@@ -69,6 +69,9 @@ endif
if CVC4_LANGUAGE_BINDING_OCAML
lib_LTLIBRARIES += libcvc4bindings_ocaml.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 = \
-version-info $(LIBCVC4BINDINGS_VERSION)
@@ -130,19 +133,18 @@ cvc4.jar: java.cpp
$(JAVAC) -classpath . -d classes `find . -name '*.java'`; \
cd classes); \
$(JAR) cf $@ -C java/classes .
-java.cpp:
-perl.lo: csharp.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:;
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 $@ $<
-python.cpp:
ocaml.lo: ocaml.cpp
$(AM_V_CXX)$(LTCXXCOMPILE) -c $(OCAML_CPPFLAGS) -o $@ $<
ocaml/swig.cmo: ocaml/swig.ml ocaml/swig.cmi; $(AM_V_GEN)$(OCAMLC) -I ocaml -c -o $@ $<
@@ -153,19 +155,23 @@ 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
+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
$(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++
ruby.lo: ruby.cpp
$(AM_V_CXX)$(LTCXXCOMPILE) -c $(RUBY_CPPFLAGS) -o $@ $<
-ruby.cpp:
tcl.lo: tcl.cpp
$(AM_V_CXX)$(LTCXXCOMPILE) -c $(TCL_CPPFLAGS) -o $@ $<
-tcl.cpp:
+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
$(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 $@ $<
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback