summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Makefile.am7
-rw-r--r--src/bindings/Makefile.am2
-rw-r--r--src/bindings/compat/Makefile.am2
-rw-r--r--src/bindings/compat/c/Makefile.am2
-rw-r--r--src/bindings/compat/java/Makefile.am2
-rw-r--r--src/bindings/compat/java/src/cvc3/Embedded.java2
-rw-r--r--src/compat/Makefile.am4
-rw-r--r--src/expr/expr_manager.i5
-rw-r--r--src/include/cvc4.h39
-rw-r--r--src/util/options.cpp21
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback