diff options
-rw-r--r-- | config/bindings.m4 | 2 | ||||
-rw-r--r-- | examples/README | 6 | ||||
-rw-r--r-- | examples/SimpleVC.rb | 57 | ||||
-rw-r--r-- | src/bindings/Makefile.am | 26 |
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 $@ $< |