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 /src | |
parent | 192c5592424e5db0afc72e7316c4698949a2f7e5 (diff) |
interfaces fixes and cleanups...and examples of each interface!
Diffstat (limited to 'src')
-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 |
10 files changed, 64 insertions, 22 deletions
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; |