.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
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
# 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"
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"
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); \
# 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, ...).
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])
#
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.
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...";
--- /dev/null
+topdir = ..
+srcdir = examples
+
+include $(topdir)/Makefile.subdir
--- /dev/null
+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 " $@;
--- /dev/null
+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
--- /dev/null
+/********************* */
+/*! \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));
+ }
+}
--- /dev/null
+/********************* */
+/*! \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));
+ }
+}
--- /dev/null
+/********************* */
+/*! \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;
+}
--- /dev/null
+/********************* */
+/*! \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;
+}
--- /dev/null
+/********************* */
+/*! \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;
+}
include/cvc4parser_public.h \
include/cvc4_private.h \
include/cvc4_public.h \
+ include/cvc4.h \
cvc4.i
subversion_versioninfo.cpp: svninfo
$(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' | \
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' | \
AM_CPPFLAGS = \
-D__BUILDING_CVC4BINDINGSLIB \
-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
-AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
+AM_CXXFLAGS = -Wall
SUBDIRS = . compat
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
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 =
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 =
// load jni c++ library
static {
- System.loadLibrary("cvc3jni");
+ System.loadLibrary("cvc4bindings_java_compat");
/*
// for debugging: stop here by waiting for a key press,
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
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
%}
%include "expr/expr_manager.h"
+
+%template(mkConst) CVC4::ExprManager::mkConst< CVC4::Integer >;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Rational>;
+
+%include "expr/expr_manager.h"
--- /dev/null
+/********************* */
+/*! \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 */
--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\
--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\
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,
{ "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 },
// 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) {
interactiveSetByUser = true;
break;
- case PRODUCE_MODELS:
+ case 'm':
produceModels = true;
break;
earlyTypeChecking = true;
break;
- case INCREMENTAL:
+ case 'i':
incrementalSolving = true;
break;
projects / cvc5.git / commitdiff