diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-30 23:01:58 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-30 23:01:58 +0000 |
commit | 33e3657c15d6c760206aeaca10b5690af4a78223 (patch) | |
tree | a75475200584ab5e11981827182d979d84f6e1ff | |
parent | 192c5592424e5db0afc72e7316c4698949a2f7e5 (diff) |
interfaces fixes and cleanups...and examples of each interface!
-rw-r--r-- | Makefile | 4 | ||||
-rw-r--r-- | Makefile.am | 21 | ||||
-rw-r--r-- | Makefile.builds.in | 1 | ||||
-rw-r--r-- | configure.ac | 2 | ||||
-rwxr-xr-x | contrib/update-copyright.pl | 6 | ||||
-rw-r--r-- | examples/Makefile | 4 | ||||
-rw-r--r-- | examples/Makefile.am | 67 | ||||
-rw-r--r-- | examples/README | 12 | ||||
-rw-r--r-- | examples/SimpleVC.java | 73 | ||||
-rw-r--r-- | examples/SimpleVCCompat.java | 70 | ||||
-rw-r--r-- | examples/simple_vc_compat_c.c | 61 | ||||
-rw-r--r-- | examples/simple_vc_compat_cxx.cpp | 64 | ||||
-rw-r--r-- | examples/simple_vc_cxx.cpp | 61 | ||||
-rw-r--r-- | src/Makefile.am | 7 | ||||
-rw-r--r-- | src/bindings/Makefile.am | 2 | ||||
-rw-r--r-- | src/bindings/compat/Makefile.am | 2 | ||||
-rw-r--r-- | src/bindings/compat/c/Makefile.am | 2 | ||||
-rw-r--r-- | src/bindings/compat/java/Makefile.am | 2 | ||||
-rw-r--r-- | src/bindings/compat/java/src/cvc3/Embedded.java | 2 | ||||
-rw-r--r-- | src/compat/Makefile.am | 4 | ||||
-rw-r--r-- | src/expr/expr_manager.i | 5 | ||||
-rw-r--r-- | src/include/cvc4.h | 39 | ||||
-rw-r--r-- | src/util/options.cpp | 21 |
23 files changed, 497 insertions, 35 deletions
@@ -27,6 +27,10 @@ test: check .PHONY: doc doc: doc-builds +.PHONY: examples +examples: all + (cd examples && $(MAKE) $(AM_MAKEFLAGS)) + YEAR := $(shell date +%Y) submission: if [ ! -e configure ]; then ./autogen.sh; fi diff --git a/Makefile.am b/Makefile.am index d2b11fe9c..db74bd378 100644 --- a/Makefile.am +++ b/Makefile.am @@ -6,6 +6,11 @@ AUTOMAKE_OPTIONS = foreign ACLOCAL_AMFLAGS = -I config SUBDIRS = src test contrib +DIST_SUBDIRS = $(SUBDIRS) examples + +.PHONY: examples +examples: all + (cd examples && $(MAKE) $(AM_MAKEFLAGS)) .PHONY: units systemtests regress regress0 regress1 regress2 regress3 systemtests regress regress0 regress1 regress2 regress3: all @@ -32,8 +37,8 @@ if COVERAGE_ENABLED # work...) lcov: all $(LCOV) -z -d . - $(MAKE) check -C src - +$(MAKE) check -C test/unit + (cd src && $(MAKE) $(AM_MAKEFLAGS) check) + +(cd test/unit && $(MAKE) $(AM_MAKEFLAGS) check) $(LCOV) -c -d . -t cvc4_units -o cvc4-coverage-full.info $(LCOV) -o cvc4-coverage.info -r cvc4-coverage-full.info $(LCOV_EXCLUDES) mkdir -p "@top_srcdir@/html" @@ -44,8 +49,8 @@ lcov: all lcov-all: all $(LCOV) -z -d . - $(MAKE) check -C src - +$(MAKE) check -C test + (cd src && $(MAKE) $(AM_MAKEFLAGS) check) + +(cd test && $(MAKE) $(AM_MAKEFLAGS) check) $(LCOV) -c -d . -t cvc4_units -o cvc4-coverage-full.info $(LCOV) -o cvc4-coverage.info -r cvc4-coverage-full.info $(LCOV_EXCLUDES) mkdir -p "@top_srcdir@/html" @@ -62,10 +67,10 @@ lcov18: all echo; echo "=== Collecting coverage data from $$testtype unit tests ==="; \ echo $(LCOV) -z -d .; \ $(LCOV) -z -d . || exit 1; \ - echo $(MAKE) check -C src || exit 1; \ - $(MAKE) check -C src || exit 1; \ - echo $(MAKE) check -C test/unit TEST_SUFFIX=_$$testtype || exit 1; \ - $(MAKE) check -C test/unit TEST_SUFFIX=_$$testtype || exit 1; \ + echo "(cd src && $(MAKE) $(AM_MAKEFLAGS) check) || exit 1"; \ + (cd src && $(MAKE) $(AM_MAKEFLAGS) check) || exit 1; \ + echo "(cd test/unit && $(MAKE) $(AM_MAKEFLAGS) check TEST_SUFFIX=_$$testtype) || exit 1"; \ + (cd test/unit && $(MAKE) $(AM_MAKEFLAGS) check TEST_SUFFIX=_$$testtype) || exit 1; \ echo $(LCOV) -c -d . -t $$testtype -o cvc4-coverage-$$testtype-full.info || exit 1; \ $(LCOV) -c -d . -t $$testtype -o cvc4-coverage-$$testtype-full.info || exit 1; \ echo $(LCOV) -o cvc4-coverage-$$testtype.info -r cvc4-coverage-$$testtype-full.info $(LCOV_EXCLUDES); \ diff --git a/Makefile.builds.in b/Makefile.builds.in index 7d2e8586b..21d172623 100644 --- a/Makefile.builds.in +++ b/Makefile.builds.in @@ -121,6 +121,7 @@ endif # set up builds/bin and builds/lib test -e lib || ln -sfv ".$(libdir)" lib test -e bin || ln -sfv ".$(bindir)" bin + rm -f examples; ln -sf "$(CURRENT_BUILD)/examples" examples # The descent into "src" with target "check" is to build check # prerequisites (e.g. CHECK_PROGRAMS, CHECK_LTLIBRARIES, ...). diff --git a/configure.ac b/configure.ac index ea7d4f7ae..b2badafbb 100644 --- a/configure.ac +++ b/configure.ac @@ -954,7 +954,7 @@ AC_SUBST(MAN_DATE) AC_CONFIG_FILES([ Makefile.builds Makefile] - m4_esyscmd([find contrib src test -name Makefile.am | sort | sed 's,\.am$,,']) + m4_esyscmd([find contrib src test examples -name Makefile.am | sort | sed 's,\.am$,,']) ) CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h]) diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl index 397f1426b..7ad839b1d 100755 --- a/contrib/update-copyright.pl +++ b/contrib/update-copyright.pl @@ -33,9 +33,7 @@ # my $excluded_directories = '^(minisat|CVS|generated)$'; -# re-include bounded_token_buffer.{h,cpp} -#my $excluded_paths = '^(src/parser/bounded_token_buffer\.(h|cpp))|(src/parser/antlr_input_imports.cpp)$'; -my $excluded_paths = '^src/parser/antlr_input_imports.cpp$'; +my $excluded_paths = '^(src/parser/antlr_input_imports.cpp|src/bindings/compat/.*)$'; # Years of copyright for the template. E.g., the string # "1985, 1987, 1992, 1997, 2008" or "2006-2009" or whatever. @@ -135,7 +133,7 @@ while($#searchdirs >= 0) { sub handleFile { my ($srcdir, $file) = @_; - return if !($file =~ /\.(c|cc|cpp|C|h|hh|hpp|H|y|yy|ypp|Y|l|ll|lpp|L|g)$/); + return if !($file =~ /\.(c|cc|cpp|C|h|hh|hpp|H|y|yy|ypp|Y|l|ll|lpp|L|g|java)$/); return if ($srcdir.'/'.$file) =~ /$excluded_paths/; return if $modonly &&`svn status "$srcdir/$file" 2>/dev/null` !~ /^M/; print "$srcdir/$file..."; diff --git a/examples/Makefile b/examples/Makefile new file mode 100644 index 000000000..3db5bc0ac --- /dev/null +++ b/examples/Makefile @@ -0,0 +1,4 @@ +topdir = .. +srcdir = examples + +include $(topdir)/Makefile.subdir diff --git a/examples/Makefile.am b/examples/Makefile.am new file mode 100644 index 000000000..8f120e14c --- /dev/null +++ b/examples/Makefile.am @@ -0,0 +1,67 @@ +AM_CPPFLAGS = \ + -I@srcdir@/../src/include -I@srcdir@/../src -I@builddir@/../src $(ANTLR_INCLUDES) +AM_CXXFLAGS = -Wall +AM_CFLAGS = -Wall + +noinst_PROGRAMS = \ + simple_vc_cxx + +if CVC4_BUILD_LIBCOMPAT +noinst_PROGRAMS += \ + simple_vc_compat_cxx +if CVC4_LANGUAGE_BINDING_C +noinst_PROGRAMS += \ + simple_vc_compat_c +endif +endif + +noinst_DATA = + +if CVC4_LANGUAGE_BINDING_JAVA +noinst_DATA += \ + SimpleVC.class +if CVC4_BUILD_LIBCOMPAT +noinst_DATA += \ + SimpleVCCompat.class +endif +endif + +simple_vc_cxx_SOURCES = \ + simple_vc_cxx.cpp +simple_vc_cxx_LDADD = \ + @builddir@/../src/parser/libcvc4parser.la \ + @builddir@/../src/libcvc4.la + +simple_vc_compat_cxx_SOURCES = \ + simple_vc_compat_cxx.cpp +simple_vc_compat_cxx_LDADD = \ + @builddir@/../src/compat/libcvc4compat.la \ + @builddir@/../src/parser/libcvc4parser.la \ + @builddir@/../src/libcvc4.la + +simple_vc_compat_c_SOURCES = \ + simple_vc_compat_c.c +simple_vc_compat_c_LDADD = \ + @builddir@/../src/bindings/compat/c/libcvc4bindings_c_compat.la + +SimpleVC.class: SimpleVC.java + $(AM_V_JAVAC)$(JAVAC) -classpath "@builddir@/../src/bindings/cvc4.jar" -d "@builddir@" $< +SimpleVCCompat.class: SimpleVCCompat.java + $(AM_V_JAVAC)$(JAVAC) -classpath "@builddir@/../src/bindings/compat/java/cvc4compat.jar" -d "@builddir@" $< + +if STATIC_BINARY +simple_vc_cxx_LINK = $(CXXLINK) -all-static +simple_vc_compat_cxx_LINK = $(CXXLINK) -all-static +simple_vc_compat_c_LINK = $(LINK) -all-static +else +simple_vc_cxx_LINK = $(CXXLINK) +simple_vc_compat_cxx_LINK = $(CXXLINK) +simple_vc_compat_c_LINK = $(LINK) +endif + +MOSTLYCLEANFILES = $(noinst_DATA) + +# for silent automake rules +AM_V_JAVAC = $(am__v_JAVAC_$(V)) +am__v_JAVAC_ = $(am__v_JAVAC_$(AM_DEFAULT_VERBOSITY)) +am__v_JAVAC_0 = @echo " JAVAC " $@; diff --git a/examples/README b/examples/README new file mode 100644 index 000000000..1ba0a54e6 --- /dev/null +++ b/examples/README @@ -0,0 +1,12 @@ +These are examples of how to use CVC4 with each of its in-memory, library +interfaces. They are essentially "hello world" examples, and do not +fully demonstrate the interfaces, but function as a starting point to +using simple expressions and solving functionality through each library. + +These examples are built as a separate step. After building CVC4, you +can make the examples by running "make" from inside the examples +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 diff --git a/examples/SimpleVC.java b/examples/SimpleVC.java new file mode 100644 index 000000000..e6a667e16 --- /dev/null +++ b/examples/SimpleVC.java @@ -0,0 +1,73 @@ +/********************* */ +/*! \file SimpleVC.java + ** \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 Java interface + ** + ** A simple demonstration of the Java interface. + ** + ** To run the resulting class file, you need to do something like the + ** following: + ** + ** java \ + ** -classpath path/to/cvc4.jar \ + ** -Djava.library.path=/dir/containing/libcvc4bindings_java.so \ + ** SimpleVC + ** + ** For example, if you are building CVC4 without specifying your own + ** build directory, the build process puts everything in builds/, and + ** you can run this example (after building it with "make") like this: + ** + ** java \ + ** -classpath builds/examples:builds/src/bindings/cvc4.jar \ + ** -Djava.library.path=builds/src/bindings/.libs \ + ** SimpleVC + **/ + +import edu.nyu.acsys.CVC4.*; +import edu.nyu.acsys.CVC4.Integer;// to override java.lang.Integer name lookup + +public class SimpleVC { + public static void main(String[] args) { + System.loadLibrary("cvc4bindings_java"); + + ExprManager em = new ExprManager(); + SmtEngine smt = new SmtEngine(em); + + // Prove that for integers x and y: + // x > 0 AND y > 0 => 2x + y >= 3 + + Type integer = em.integerType(); + + Expr x = em.mkVar("x", integer); + Expr y = em.mkVar("y", integer); + Expr zero = em.mkConst(new Integer(0)); + + Expr x_positive = em.mkExpr(Kind.GT, x, zero); + Expr y_positive = em.mkExpr(Kind.GT, y, zero); + + Expr two = em.mkConst(new Integer(2)); + Expr twox = em.mkExpr(Kind.MULT, two, x); + Expr twox_plus_y = em.mkExpr(Kind.PLUS, twox, y); + + Expr three = em.mkConst(new Integer(3)); + Expr twox_plus_y_geq_3 = em.mkExpr(Kind.GEQ, twox_plus_y, three); + + BoolExpr formula = + new BoolExpr(em.mkExpr(Kind.AND, x_positive, y_positive)). + impExpr(new BoolExpr(twox_plus_y_geq_3)); + + System.out.println("Checking validity of formula " + formula + " with CVC4."); + System.out.println("CVC4 should report VALID."); + System.out.println("Result from CVC4 is: " + smt.query(formula)); + } +} diff --git a/examples/SimpleVCCompat.java b/examples/SimpleVCCompat.java new file mode 100644 index 000000000..107b5504e --- /dev/null +++ b/examples/SimpleVCCompat.java @@ -0,0 +1,70 @@ +/********************* */ +/*! \file SimpleVCCompat.java + ** \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 Java compatibility interface + ** (quite similar to the old CVC3 Java interface) + ** + ** A simple demonstration of the Java compatibility interface + ** (quite similar to the old CVC3 Java interface). + ** + ** To run the resulting class file, you need to do something like the + ** following: + ** + ** java \ + ** -classpath path/to/cvc4compat.jar \ + ** -Djava.library.path=/dir/containing/libcvc4bindings_java_compat.so \ + ** SimpleVCCompat + ** + ** For example, if you are building CVC4 without specifying your own + ** build directory, the build process puts everything in builds/, and + ** you can run this example (after building it with "make") like this: + ** + ** java \ + ** -classpath builds/examples:builds/src/bindings/compat/java/cvc4compat.jar \ + ** -Djava.library.path=builds/src/bindings/compat/java/.libs \ + ** SimpleVCCompat + **/ + +import cvc3.*; + +public class SimpleVCCompat { + public static void main(String[] args) { + ValidityChecker vc = ValidityChecker.create(); + + // Prove that for integers x and y: + // x > 0 AND y > 0 => 2x + y >= 3 + + Type integer = vc.intType(); + + Expr x = vc.varExpr("x", integer); + Expr y = vc.varExpr("y", integer); + Expr zero = vc.ratExpr(0); + + Expr x_positive = vc.gtExpr(x, zero); + Expr y_positive = vc.gtExpr(y, zero); + + Expr two = vc.ratExpr(2); + Expr twox = vc.multExpr(two, x); + Expr twox_plus_y = vc.plusExpr(twox, y); + + Expr three = vc.ratExpr(3); + Expr twox_plus_y_geq_3 = vc.geExpr(twox_plus_y, three); + + Expr formula = vc.impliesExpr(vc.andExpr(x_positive, y_positive), + twox_plus_y_geq_3); + + System.out.println("Checking validity of formula " + formula + " with CVC4."); + System.out.println("CVC4 should report VALID."); + System.out.println("Result from CVC4 is: " + vc.query(formula)); + } +} diff --git a/examples/simple_vc_compat_c.c b/examples/simple_vc_compat_c.c new file mode 100644 index 000000000..9bcb52280 --- /dev/null +++ b/examples/simple_vc_compat_c.c @@ -0,0 +1,61 @@ +/********************* */ +/*! \file simple_vc_compat_c.c + ** \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 C compatibility interface + ** (quite similar to the old CVC3 C interface) + ** + ** A simple demonstration of the C compatibility interface + ** (quite similar to the old CVC3 C interface). + **/ + +#include <stdio.h> +#include <stdlib.h> + +// #include <cvc4/compat/c_interface.h> +#include "bindings/compat/c/c_interface.h" + +int main() { + VC vc = vc_createValidityChecker(NULL); + + // Prove that for integers x and y: + // x > 0 AND y > 0 => 2x + y >= 3 + + Type integer = vc_intType(vc); + + Expr x = vc_varExpr(vc, "x", integer); + Expr y = vc_varExpr(vc, "y", integer); + Expr zero = vc_ratExpr(vc, 0, 1); + + Expr x_positive = vc_gtExpr(vc, x, zero); + Expr y_positive = vc_gtExpr(vc, y, zero); + + Expr two = vc_ratExpr(vc, 2, 1); + Expr twox = vc_multExpr(vc, two, x); + Expr twox_plus_y = vc_plusExpr(vc, twox, y); + + Expr three = vc_ratExpr(vc, 3, 1); + Expr twox_plus_y_geq_3 = vc_geExpr(vc, twox_plus_y, three); + + Expr formula = vc_impliesExpr(vc, vc_andExpr(vc, x_positive, y_positive), + twox_plus_y_geq_3); + + char* formulaString = vc_printExprString(vc, formula); + + printf("Checking validity of formula %s with CVC4.\n", formulaString); + printf("CVC4 should return 1 (meaning VALID).\n"); + printf("Result from CVC4 is: %d\n", vc_query(vc, formula)); + + free(formulaString); + + return 0; +} diff --git a/examples/simple_vc_compat_cxx.cpp b/examples/simple_vc_compat_cxx.cpp new file mode 100644 index 000000000..c178d1aba --- /dev/null +++ b/examples/simple_vc_compat_cxx.cpp @@ -0,0 +1,64 @@ +/********************* */ +/*! \file simple_vc_compat_cxx.cpp + ** \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 C++ compatibility interface + ** (quite similar to the old CVC3 C++ interface) + ** + ** A simple demonstration of the C++ compatibility interface (quite + ** similar to the old CVC3 C++ interface). Note that the library is + ** named "libcvc4compat," to mark it as being part of CVC4, but the + ** header file is "cvc3_compat.h" to indicate the similarity to the + ** CVC3 interface, and the namespace is "CVC3". CVC3::Expr and + ** CVC4::Expr are incompatible; to avoid confusion, it is best to not + ** include both the CVC3 and CVC4 interface headers. + **/ + +#include <iostream> + +// #include <cvc4/compat/cvc3_compat.h> +#include "compat/cvc3_compat.h" + +using namespace std; +using namespace CVC3; + +int main() { + ValidityChecker* vc = ValidityChecker::create(); + + // Prove that for integers x and y: + // x > 0 AND y > 0 => 2x + y >= 3 + + Type integer = vc->intType(); + + Expr x = vc->varExpr("x", integer); + Expr y = vc->varExpr("y", integer); + Expr zero = vc->ratExpr(0); + + Expr x_positive = vc->gtExpr(x, zero); + Expr y_positive = vc->gtExpr(y, zero); + + Expr two = vc->ratExpr(2); + Expr twox = vc->multExpr(two, x); + Expr twox_plus_y = vc->plusExpr(twox, y); + + Expr three = vc->ratExpr(3); + Expr twox_plus_y_geq_3 = vc->geExpr(twox_plus_y, three); + + Expr formula = vc->impliesExpr(vc->andExpr(x_positive, y_positive), + twox_plus_y_geq_3); + + cout << "Checking validity of formula " << formula << " with CVC4." << endl; + cout << "CVC4 should report VALID." << endl; + cout << "Result from CVC4 is: " << vc->query(formula) << endl; + + return 0; +} diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp new file mode 100644 index 000000000..3b5db7c02 --- /dev/null +++ b/examples/simple_vc_cxx.cpp @@ -0,0 +1,61 @@ +/********************* */ +/*! \file simple_vc_cxx.cpp + ** \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 C++ interface + ** + ** A simple demonstration of the C++ interface. Compare to the Java + ** interface in SimpleVC.java; they are virtually line-by-line + ** identical. + **/ + +#include <iostream> + +//#include <cvc4.h> +#include "smt/smt_engine.h" + +using namespace std; +using namespace CVC4; + +int main() { + ExprManager em; + SmtEngine smt(&em); + + // Prove that for integers x and y: + // x > 0 AND y > 0 => 2x + y >= 3 + + Type integer = em.integerType(); + + Expr x = em.mkVar("x", integer); + Expr y = em.mkVar("y", integer); + Expr zero = em.mkConst(Integer(0)); + + Expr x_positive = em.mkExpr(kind::GT, x, zero); + Expr y_positive = em.mkExpr(kind::GT, y, zero); + + Expr two = em.mkConst(Integer(2)); + Expr twox = em.mkExpr(kind::MULT, two, x); + Expr twox_plus_y = em.mkExpr(kind::PLUS, twox, y); + + Expr three = em.mkConst(Integer(3)); + Expr twox_plus_y_geq_3 = em.mkExpr(kind::GEQ, twox_plus_y, three); + + BoolExpr formula = + BoolExpr(em.mkExpr(kind::AND, x_positive, y_positive)). + impExpr(BoolExpr(twox_plus_y_geq_3)); + + cout << "Checking validity of formula " << formula << " with CVC4." << endl; + cout << "CVC4 should report VALID." << endl; + cout << "Result from CVC4 is: " << smt.query(formula) << endl; + + return 0; +} diff --git a/src/Makefile.am b/src/Makefile.am index 5b245d303..63fcf590d 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -63,6 +63,7 @@ EXTRA_DIST = \ include/cvc4parser_public.h \ include/cvc4_private.h \ include/cvc4_public.h \ + include/cvc4.h \ cvc4.i subversion_versioninfo.cpp: svninfo @@ -94,7 +95,8 @@ svninfo.tmp: $(AM_V_GEN)(cd "$(top_srcdir)" && svn info && echo "Modifications: `test -z \"\`svn status -q\`\" && echo false || echo true`") >"$@" 2>/dev/null || true install-data-local: - (echo include/cvc4_public.h; \ + (echo include/cvc4.h; \ + echo include/cvc4_public.h; \ find * -name '*.h' | \ xargs grep -l '^# *include *"cvc4.*_public\.h"'; \ (cd "$(srcdir)" && find * -name '*.h' | \ @@ -115,7 +117,8 @@ install-data-local: done uninstall-local: - -(echo include/cvc4_public.h; \ + -(echo include/cvc4.h; \ + echo include/cvc4_public.h; \ find * -name '*.h' | \ xargs grep -l '^# *include *"cvc4.*_public\.h"'; \ (cd "$(srcdir)" && find * -name '*.h' | \ diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am index 2552e39d6..f9420dbdb 100644 --- a/src/bindings/Makefile.am +++ b/src/bindings/Makefile.am @@ -15,7 +15,7 @@ LIBCVC4BINDINGS_VERSION = @CVC4_BINDINGS_LIBRARY_VERSION@ AM_CPPFLAGS = \ -D__BUILDING_CVC4BINDINGSLIB \ -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) +AM_CXXFLAGS = -Wall SUBDIRS = . compat diff --git a/src/bindings/compat/Makefile.am b/src/bindings/compat/Makefile.am index e5ea3b399..2aa714458 100644 --- a/src/bindings/compat/Makefile.am +++ b/src/bindings/compat/Makefile.am @@ -1,7 +1,7 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4BINDINGSLIB \ -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. -AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) +AM_CXXFLAGS = -Wall if CVC4_BUILD_LIBCOMPAT SUBDIRS = c java diff --git a/src/bindings/compat/c/Makefile.am b/src/bindings/compat/c/Makefile.am index ceabe16db..c7298a927 100644 --- a/src/bindings/compat/c/Makefile.am +++ b/src/bindings/compat/c/Makefile.am @@ -15,7 +15,7 @@ LIBCVC4BINDINGS_VERSION = @CVC4_BINDINGS_LIBRARY_VERSION@ AM_CPPFLAGS = \ -D__BUILDING_CVC4BINDINGSLIB \ -I@srcdir@/../../../include -I@srcdir@/../../.. -I@builddir@/../../.. -AM_CXXFLAGS = -Wall -Wno-return-type $(FLAG_VISIBILITY_HIDDEN) +AM_CXXFLAGS = -Wall -Wno-return-type lib_LTLIBRARIES = diff --git a/src/bindings/compat/java/Makefile.am b/src/bindings/compat/java/Makefile.am index 25765f0f0..14701ebb3 100644 --- a/src/bindings/compat/java/Makefile.am +++ b/src/bindings/compat/java/Makefile.am @@ -15,7 +15,7 @@ LIBCVC4BINDINGS_VERSION = @CVC4_BINDINGS_LIBRARY_VERSION@ AM_CPPFLAGS = \ -D__BUILDING_CVC4BINDINGSLIB \ -I@srcdir@/../../../include -I@srcdir@/../../.. -I@builddir@/../../.. -I@builddir@/cvc3 -AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) +AM_CXXFLAGS = -Wall lib_LTLIBRARIES = data_DATA = diff --git a/src/bindings/compat/java/src/cvc3/Embedded.java b/src/bindings/compat/java/src/cvc3/Embedded.java index 87d67d743..c645f2655 100644 --- a/src/bindings/compat/java/src/cvc3/Embedded.java +++ b/src/bindings/compat/java/src/cvc3/Embedded.java @@ -12,7 +12,7 @@ public abstract class Embedded { // load jni c++ library static { - System.loadLibrary("cvc3jni"); + System.loadLibrary("cvc4bindings_java_compat"); /* // for debugging: stop here by waiting for a key press, diff --git a/src/compat/Makefile.am b/src/compat/Makefile.am index 936a63559..a79301c18 100644 --- a/src/compat/Makefile.am +++ b/src/compat/Makefile.am @@ -15,7 +15,7 @@ LIBCVC4COMPAT_VERSION = @CVC4_COMPAT_LIBRARY_VERSION@ AM_CPPFLAGS = \ -D__BUILDING_CVC4COMPATLIB \ -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. $(ANTLR_INCLUDES) -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) +AM_CXXFLAGS = -Wall -Wno-unknown-pragmas if CVC4_BUILD_LIBCOMPAT @@ -40,10 +40,12 @@ libcvc4compat_noinst_la_LIBADD = \ libcvc4compat_la_SOURCES = \ cvc3_compat.h \ cvc3_compat.cpp +libcvc4compat_la_CXXFLAGS = -fno-strict-aliasing libcvc4compat_noinst_la_SOURCES = \ cvc3_compat.h \ cvc3_compat.cpp +libcvc4compat_noinst_la_CXXFLAGS = -fno-strict-aliasing else diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i index 739da614a..90d0942b4 100644 --- a/src/expr/expr_manager.i +++ b/src/expr/expr_manager.i @@ -3,3 +3,8 @@ %} %include "expr/expr_manager.h" + +%template(mkConst) CVC4::ExprManager::mkConst< CVC4::Integer >; +%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Rational>; + +%include "expr/expr_manager.h" diff --git a/src/include/cvc4.h b/src/include/cvc4.h new file mode 100644 index 000000000..cfe11fb82 --- /dev/null +++ b/src/include/cvc4.h @@ -0,0 +1,39 @@ +/********************* */ +/*! \file cvc4.h + ** \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 Main header file for CVC4 library functionality + ** + ** Main header file for CVC4 library functionality. Includes the + ** most-commonly used CVC4 public-facing class interfaces. + **/ + +#ifndef __CVC4__CVC4_H +#define __CVC4__CVC4_H + +#include <cvc4/smt/smt_engine.h> + +#include <cvc4/expr/expr_manager.h> +#include <cvc4/expr/expr.h> +#include <cvc4/expr/command.h> + +#include <cvc4/util/datatype.h> +#include <cvc4/util/integer.h> +#include <cvc4/util/rational.h> +#include <cvc4/util/exception.h> +#include <cvc4/util/options.h> +#include <cvc4/util/configuration.h> + +#include <cvc4/parser/parser.h> +#include <cvc4/parser/parser_builder.h> + +#endif /* __CVC4__CVC4_H */ diff --git a/src/util/options.cpp b/src/util/options.cpp index 6b79a84bf..38dcf12c9 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -123,7 +123,7 @@ static const string optionsDescription = "\ --print-expr-types print types with variables when printing exprs\n\ --interactive run interactively\n\ --no-interactive do not run interactively\n\ - --produce-models support the get-value command\n\ + --produce-models | -m support the get-value command\n\ --produce-assignments support the get-assignment command\n\ --lazy-definition-expansion expand define-fun lazily\n\ --simplification=MODE choose simplification mode, see --simplification=help\n\ @@ -138,7 +138,7 @@ static const string optionsDescription = "\ --disable-variable-removal enable permanent removal of variables in arithmetic (UNSAFE! experts only)\n\ --disable-arithmetic-propagation turns on arithmetic propagation\n\ --disable-symmetry-breaker turns off UF symmetry breaker (Deharbe et al., CADE 2011)\n\ - --incremental enable incremental solving\n"; + --incremental | -i enable incremental solving\n"; static const string languageDescription = "\ Languages currently supported as arguments to the -L / --lang option:\n\ @@ -281,12 +281,10 @@ enum OptionValue { NO_STATIC_LEARNING, INTERACTIVE, NO_INTERACTIVE, - PRODUCE_MODELS, PRODUCE_ASSIGNMENTS, NO_TYPE_CHECKING, LAZY_TYPE_CHECKING, EAGER_TYPE_CHECKING, - INCREMENTAL, REPLAY, REPLAY_LOG, PIVOT_RULE, @@ -355,19 +353,14 @@ static struct option cmdlineOptions[] = { { "no-static-learning", no_argument, NULL, NO_STATIC_LEARNING }, { "interactive", no_argument , NULL, INTERACTIVE }, { "no-interactive", no_argument , NULL, NO_INTERACTIVE }, - { "produce-models", no_argument , NULL, PRODUCE_MODELS }, + { "produce-models", no_argument , NULL, 'm' }, { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS }, { "no-type-checking", no_argument , NULL, NO_TYPE_CHECKING }, { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING }, { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING }, - { "incremental", no_argument , NULL, INCREMENTAL }, + { "incremental", no_argument , NULL, 'i' }, { "replay" , required_argument, NULL, REPLAY }, { "replay-log" , required_argument, NULL, REPLAY_LOG }, - { "produce-models", no_argument , NULL, PRODUCE_MODELS }, - { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS }, - { "no-type-checking", no_argument, NULL, NO_TYPE_CHECKING }, - { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING }, - { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING }, { "pivot-rule" , required_argument, NULL, PIVOT_RULE }, { "pivot-threshold" , required_argument, NULL, ARITHMETIC_PIVOT_THRESHOLD }, { "prop-row-length" , required_argument, NULL, ARITHMETIC_PROP_MAX_LENGTH }, @@ -405,7 +398,7 @@ throw(OptionException) { // permitted. cmdlineOptions specifies all the long-options and the // return value for getopt_long() should they be encountered. while((c = getopt_long(argc, argv, - ":hVvqL:d:t:", + ":himVvqL:d:t:", cmdlineOptions, NULL)) != -1) { switch(c) { @@ -614,7 +607,7 @@ throw(OptionException) { interactiveSetByUser = true; break; - case PRODUCE_MODELS: + case 'm': produceModels = true; break; @@ -637,7 +630,7 @@ throw(OptionException) { earlyTypeChecking = true; break; - case INCREMENTAL: + case 'i': incrementalSolving = true; break; |