summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile6
-rw-r--r--config/abc.m4135
-rwxr-xr-xconfig/build-type4
-rw-r--r--config/cvc4.m46
-rw-r--r--configure.ac42
-rwxr-xr-xcontrib/get-abc10
-rw-r--r--src/Makefile.am5
-rw-r--r--src/main/options_handlers.h3
-rw-r--r--src/main/portfolio.cpp2
-rw-r--r--src/smt/smt_engine.cpp33
-rw-r--r--src/util/configuration.cpp6
-rw-r--r--src/util/configuration.h4
-rw-r--r--src/util/configuration_private.h8
13 files changed, 208 insertions, 56 deletions
diff --git a/Makefile b/Makefile
index f5d379d6b..c8126ae95 100644
--- a/Makefile
+++ b/Makefile
@@ -54,7 +54,7 @@ submission submission-main:
exit 1; \
fi
./autogen.sh
- ./configure competition --disable-shared --enable-static-binary --with-cln --with-glpk --with-abc --enable-gpl
+ ./configure competition --disable-shared --enable-static-binary --with-cln --with-glpk --with-abc --without-readline --enable-gpl
$(MAKE)
strip builds/bin/cvc4
$(MAKE) check
@@ -81,7 +81,7 @@ submission-application:
exit 1; \
fi
./autogen.sh
- ./configure competition --disable-shared --enable-static-binary --with-cln --with-glpk --with-abc --enable-gpl CXXFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK CFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK
+ ./configure competition --disable-shared --enable-static-binary --with-cln --with-glpk --with-abc --without-readline --enable-gpl CXXFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK CFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK
$(MAKE)
strip builds/bin/cvc4
$(MAKE) check
@@ -108,7 +108,7 @@ submission-parallel:
exit 1; \
fi
./autogen.sh
- ./configure competition --disable-shared --enable-static-binary --with-gmp --with-portfolio --with-glpk --with-abc --enable-gpl
+ ./configure competition --disable-shared --enable-static-binary --with-gmp --with-portfolio --with-glpk --with-abc --without-readline --enable-gpl
$(MAKE)
strip builds/bin/pcvc4
# some test cases fail (and are known to fail)
diff --git a/config/abc.m4 b/config/abc.m4
new file mode 100644
index 000000000..d86b2f465
--- /dev/null
+++ b/config/abc.m4
@@ -0,0 +1,135 @@
+# CVC4_CHECK_FOR_ABC
+# ------------------
+# Look for abc and link it in, but only if user requested.
+AC_DEFUN([CVC4_CHECK_FOR_ABC], [
+AC_MSG_CHECKING([whether user requested abc support])
+LIBABC=
+have_libabc=0
+ABC_LIBS=
+if test "$with_abc" = no; then
+ AC_MSG_RESULT([no, abc disabled by user])
+elif test "$with_abc" = yes; then
+ AC_MSG_RESULT([yes, abc requested by user])
+
+ # Get the location of all the ABC stuff
+ AC_ARG_VAR(ABC_HOME, [path to top level of abc source tree])
+ AC_ARG_WITH(
+ [abc-dir],
+ AS_HELP_STRING(
+ [--with-abc-dir=PATH],
+ [path to top level of abc source tree]
+ ),
+ [ABC_HOME="$withval"],
+ [ if test -z "$ABC_HOME"; then
+ AC_MSG_FAILURE([must give --with-abc-dir=PATH or define environment variable ABC_HOME!])
+ fi
+ ]
+ )
+ if ! test -d "$ABC_HOME" || ! test -x "$ABC_HOME/arch_flags"; then
+ AC_MSG_FAILURE([either $ABC_HOME is not an abc source tree or it's not yet built])
+ fi
+
+ AC_MSG_CHECKING([for arch_flags to use with libabc])
+ libabc_arch_flags="$("$ABC_HOME/arch_flags")"
+ AC_MSG_RESULT([$libabc_arch_flags])
+ CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$ABC_HOME/src $libabc_arch_flags"
+ ABC_LDFLAGS="-L$ABC_HOME"
+
+ dnl Try a bunch of combinations until something works :-/
+ cvc4_save_LDFLAGS="$LDFLAGS"
+ ABC_LIBS=
+ CPPFLAGS="$CPPFLAGS -I$ABC_HOME/src $libabc_arch_flags"
+ LDFLAGS="$LDFLAGS $ABC_LDFLAGS"
+ AC_CHECK_HEADER([base/abc/abc.h], [], [AC_MSG_FAILURE([cannot find abc.h, the ABC header!])])
+ AC_MSG_CHECKING([how to link abc])
+ CVC4_TRY_ABC_WITH([])
+ CVC4_TRY_ABC_WITH([-lm])
+ CVC4_TRY_ABC_WITH([-lm -lrt])
+ CVC4_TRY_ABC_WITH([-lm -lrt -ldl])
+ CVC4_TRY_ABC_WITH([-lm -lrt -lreadline -ldl])
+ CVC4_TRY_ABC_WITH([-lm -lpthread])
+ CVC4_TRY_ABC_WITH([-lm -lpthread -lrt])
+ CVC4_TRY_ABC_WITH([-lm -lpthread -lrt -ldl])
+ CVC4_TRY_ABC_WITH([-lm -lpthread -lrt -lreadline -ldl])
+ dnl CVC4_TRY_ABC_WITH([-lm -rdynamic -lreadline -lpthread -lrt -ldl])
+ if test -z "$ABC_LIBS"; then
+ AC_MSG_FAILURE([cannot link against libabc!])
+ else
+ AC_MSG_RESULT([$ABC_LIBS])
+ # make sure it works in static builds, too
+ if test "$enable_static_binary" = yes; then
+ ABC_LIBS=
+ AC_MSG_CHECKING([whether statically-linked abc is functional])
+ CVC4_TRY_STATIC_ABC_WITH([])
+ CVC4_TRY_STATIC_ABC_WITH([-lm])
+ CVC4_TRY_STATIC_ABC_WITH([-lm -lrt])
+ CVC4_TRY_STATIC_ABC_WITH([-lm -lrt -ldl])
+ CVC4_TRY_STATIC_ABC_WITH([-lm -lrt -lreadline -ldl])
+ CVC4_TRY_STATIC_ABC_WITH([-lm -lpthread])
+ CVC4_TRY_STATIC_ABC_WITH([-lm -lpthread -lrt])
+ CVC4_TRY_STATIC_ABC_WITH([-lm -lpthread -lrt -ldl])
+ CVC4_TRY_STATIC_ABC_WITH([-lm -lpthread -lrt -lreadline -ldl])
+ if test -n "$ABC_LIBS"; then
+ AC_MSG_RESULT([yes, it works])
+ with_abc=yes
+ else
+ AC_MSG_RESULT([no])
+ AC_MSG_FAILURE([abc installation appears incompatible with static-binary])
+ fi
+ else
+ with_abc=yes
+ fi
+ fi
+ if test "$with_abc" = yes; then
+ have_libabc=1
+ else
+ with_abc=no
+ have_libreadline=0
+ ABC_LIBS=
+ fi
+ LDFLAGS="$cvc4_save_LDFLAGS"
+else
+ AC_MSG_RESULT([no, user didn't request abc])
+ with_abc=no
+fi
+])# CVC4_CHECK_FOR_ABC
+
+# CVC4_TRY_ABC_WITH(LIBS)
+# -----------------------
+# Try AC_CHECK_LIB(abc) with the given linking libraries
+AC_DEFUN([CVC4_TRY_ABC_WITH], [
+if test -z "$ABC_LIBS"; then
+ AC_LANG_PUSH([C++])
+ cvc4_save_LIBS="$LIBS"
+ LIBS="-labc $1"
+ AC_LINK_IFELSE([AC_LANG_PROGRAM([extern "C" { void Abc_Start(); }],
+ [Abc_Start()])],
+ [ABC_LIBS="-labc $1"],
+ [])
+ LIBS="$cvc4_save_LIBS"
+ AC_LANG_POP([C++])
+fi
+])# CVC4_TRY_ABC_WITH
+
+# CVC4_TRY_STATIC_ABC_WITH(LIBS)
+# ------------------------------
+# Try AC_CHECK_LIB(abc) with the given linking libraries
+AC_DEFUN([CVC4_TRY_STATIC_ABC_WITH], [
+if test -z "$ABC_LIBS"; then
+ AC_LANG_PUSH([C++])
+ cvc4_save_LIBS="$LIBS"
+ cvc4_save_LDFLAGS="$LDFLAGS"
+ LDFLAGS="-static $LDFLAGS"
+ LIBS="-labc-static $1"
+ AC_LINK_IFELSE([AC_LANG_PROGRAM([extern "C" { void Abc_Start(); }],
+ [Abc_Start()])],
+ [ABC_LIBS="-labc-static $1"],
+ [ LIBS="-labc $1"
+ AC_LINK_IFELSE([AC_LANG_PROGRAM([extern "C" { void Abc_Start(); }],
+ [Abc_Start()])],
+ [ABC_LIBS="-labc $1"]) ])
+ LIBS="$cvc4_save_LIBS"
+ LDFLAGS="$cvc4_save_LDFLAGS"
+ AC_LANG_POP([C++])
+fi
+])# CVC4_TRY_STATIC_ABC_WITH
diff --git a/config/build-type b/config/build-type
index 1ef9191f7..ae4e292f4 100755
--- a/config/build-type
+++ b/config/build-type
@@ -33,7 +33,7 @@
# Also you can specify "cln" or "gmp". If "gmp", the build dir
# contains the string "gmp". (gmp is considered the default.)
#
-# Also for glpk.
+# Also for glpk and abc.
#
if [ $# -eq 0 ]; then
@@ -55,7 +55,7 @@ while [ $# -gt 0 ]; do
done
build_type_suffix=
-for arg in cln glpk staticbinary optimized proof debugsymbols statistics replay assertions tracing muzzle coverage profiling; do
+for arg in cln glpk abc staticbinary optimized proof debugsymbols statistics replay assertions tracing muzzle coverage profiling; do
if eval [ -n '"${'$arg'+set}"' ]; then
if eval [ '"${'$arg'}"' -eq 0 ]; then
build_type_suffix=$build_type_suffix-no$arg
diff --git a/config/cvc4.m4 b/config/cvc4.m4
index 40e2054e6..ea202e94f 100644
--- a/config/cvc4.m4
+++ b/config/cvc4.m4
@@ -79,6 +79,12 @@ handle_option() {
if expr "$ac_option" : '.*-glpk' >/dev/null || expr "$ac_option" : '.*-glpk-' >/dev/null; then
eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--with-glpk\""'
fi
+ if expr "$ac_option" : '.*-noabc' >/dev/null || expr "$ac_option" : '.*-noabc-' >/dev/null; then
+ eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--without-abc\""'
+ fi
+ if expr "$ac_option" : '.*-abc' >/dev/null || expr "$ac_option" : '.*-abc-' >/dev/null; then
+ eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--with-abc\""'
+ fi
for x in cln gmp; do
if expr "$ac_option" : '.*-no'$x'$' >/dev/null || expr "$ac_option" : '.*-no'$x'-' >/dev/null; then
eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--without-$x\""'
diff --git a/configure.ac b/configure.ac
index cfd65aef4..92a9c10ce 100644
--- a/configure.ac
+++ b/configure.ac
@@ -113,7 +113,7 @@ AC_ARG_WITH([build],
if test -z "${with_build+set}"; then
with_build=production
fi
-if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_dumping+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}" -a -z "${enable_statistics+set}" -a -z "${enable_replay+set}" -a -z "${with_gmp+set}" -a -z "${with_cln+set}" -a -z "${with_glpk+set}"; then
+if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_dumping+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}" -a -z "${enable_statistics+set}" -a -z "${enable_replay+set}" -a -z "${with_gmp+set}" -a -z "${with_cln+set}" -a -z "${with_glpk+set}" -a -z "${with_abc+set}"; then
custom_build_profile=no
else
custom_build_profile=yes
@@ -208,6 +208,11 @@ if test -n "${with_glpk+set}"; then
btargs="$btargs glpk"
fi
fi
+if test -n "${with_abc+set}"; then
+ if test "$with_abc" = yes; then
+ btargs="$btargs abc"
+ fi
+fi
AC_MSG_RESULT([$with_build])
AM_INIT_AUTOMAKE([1.11 no-define tar-pax parallel-tests color-tests subdir-objects])
@@ -254,9 +259,6 @@ AC_ARG_WITH(
]
)
-# [chris 8/24/2010] --with-gmp has no practical effect, since GMP is
-# the default. Could be useful if other options are added later.
-
AC_ARG_WITH(
[gmp],
AS_HELP_STRING(
@@ -748,26 +750,17 @@ fi
AM_CONDITIONAL([CVC4_USE_GLPK], [test $have_libglpk -eq 1])
AC_SUBST([GLPK_LIBS])
-AC_ARG_WITH(
- [abc],
- AS_HELP_STRING(
- [--with-abc],
- [use the ABC AIG library]
- ),
- [case "$withval" in
- y|ye|yes|Y|YE|YES) cvc4_use_abc=1 ;;
- n|no|N|NO) cvc4_use_abc=0 ;;
- esac
- ]
-)
-
-if test $cvc4_use_abc -eq 1; then
- # must add dl and pthread separately and before abc
- AC_CHECK_LIB(dl, dlopen, , [AC_MSG_ERROR([dl not found])], [])
- AC_CHECK_LIB(pthread, pthread_create, , [AC_MSG_ERROR([pthread not found])], [])
- AC_CHECK_LIB(abc, Abc_Start, , [AC_MSG_ERROR([abc not found])], [-lm -ldl -rdynamic -lreadline -ltermcap -lpthread -lrt -ldl])
- AC_DEFINE_UNQUOTED(CVC4_USE_ABC, [], [Defined if linked against the ABC AIG library.])
+# Build with libabc (defined in config/abc.m4)
+AC_ARG_WITH([abc],
+ [AS_HELP_STRING([--with-abc],
+ [use the ABC AIG library])], [], [with_abc=])
+CVC4_CHECK_FOR_ABC
+if test $have_libabc -eq 1; then
+ CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_ABC"
fi
+AM_CONDITIONAL([CVC4_USE_ABC], [test $have_libabc -eq 1])
+AC_SUBST([ABC_LDFLAGS])
+AC_SUBST([ABC_LIBS])
# Check to see if this version/architecture of GNU C++ explicitly
# instantiates __gnu_cxx::hash<uint64_t> or not. Some do, some don't.
@@ -1238,7 +1231,7 @@ AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full releas
CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }${BOOST_CPPFLAGS:+$BOOST_CPPFLAGS }$CVC4CPPFLAGS"
CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions"
-LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS -ldl"
+LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
# visibility flag not supported for Windows builds
# also increase default stack size for Windows binaries
@@ -1455,6 +1448,7 @@ Portfolio : $with_portfolio
MP library : $mplibrary
GLPK : $with_glpk
+ABC : $with_abc
Readline : $with_readline
CPPFLAGS : $CPPFLAGS
diff --git a/contrib/get-abc b/contrib/get-abc
index 97fbb1503..f5a397039 100755
--- a/contrib/get-abc
+++ b/contrib/get-abc
@@ -1,4 +1,4 @@
-#!/bin/bash -x
+#!/bin/bash
#
set -e
@@ -42,11 +42,13 @@ cd alanmi-abc-$commit
cp src/base/main/main.c src/base/main/main.c.orig
sed 's,^// *#define ABC_LIB *$,#define ABC_LIB,' src/base/main/main.c.orig > src/base/main/main.c
-make libabc.a OPTFLAGS=-O
+# Build optimized, without readline, without pthreads.
+# These aren't necessary for our usage and we don't want the dependencies.
+make libabc.a OPTFLAGS=-O READLINE=0 PTHREADS=0
mv libabc.a libabc-static.a
make clean
-make libabc.a OPTFLAGS='-O -fPIC'
+make libabc.a OPTFLAGS='-O -fPIC' READLINE=0 PTHREADS=0
echo
echo ===================== Now configure CVC4 with =====================
-echo ./configure --with-abc=`pwd`
+echo ./configure --with-abc --with-abc-dir=`pwd`
diff --git a/src/Makefile.am b/src/Makefile.am
index 34fa20c1d..9531db0ce 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -433,6 +433,11 @@ if CVC4_USE_GLPK
libcvc4_la_LIBADD += $(GLPK_LIBS)
endif
+if CVC4_USE_ABC
+libcvc4_la_LIBADD += $(ABC_LIBS)
+libcvc4_la_LDFLAGS += $(ABC_LDFLAGS)
+endif
+
BUILT_SOURCES = \
theory/rewriter_tables.h \
theory/theory_traits.h \
diff --git a/src/main/options_handlers.h b/src/main/options_handlers.h
index 7723dcb33..ee16af2f2 100644
--- a/src/main/options_handlers.h
+++ b/src/main/options_handlers.h
@@ -65,8 +65,9 @@ inline void showConfiguration(std::string option, SmtEngine* smt) {
printf("\n");
printf("cudd : %s\n", Configuration::isBuiltWithCudd() ? "yes" : "no");
printf("cln : %s\n", Configuration::isBuiltWithCln() ? "yes" : "no");
- printf("glpk : %s\n", Configuration::isBuiltWithGlpk() ? "yes" : "no");
printf("gmp : %s\n", Configuration::isBuiltWithGmp() ? "yes" : "no");
+ printf("glpk : %s\n", Configuration::isBuiltWithGlpk() ? "yes" : "no");
+ printf("abc : %s\n", Configuration::isBuiltWithAbc() ? "yes" : "no");
printf("tls : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no");
exit(0);
}
diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp
index a5fe46d27..ebf36b0cd 100644
--- a/src/main/portfolio.cpp
+++ b/src/main/portfolio.cpp
@@ -95,7 +95,7 @@ std::pair<int, S> runPortfolio(int numThreads,
for(int t = 0; t < numThreads; ++t) {
if(optionWaitToJoin) {
threads[t].join();
- }
+ }
}
std::pair<int, S> retval(global_winner, threads_returnValue[global_winner]);
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b71969d15..6ab25ee57 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -367,9 +367,9 @@ private:
void bvToBool();
// Abstract common structure over small domains to UF
- // return true if changes were made.
- void bvAbstraction();
-
+ // return true if changes were made.
+ void bvAbstraction();
+
// Simplify ITE structure
bool simpITE();
@@ -1085,7 +1085,7 @@ void SmtEngine::setDefaults() {
Notice() << "SmtEngine: turning off incremental to support eager bit-blasting" << endl;
setOption("incremental", SExpr("false"));
}
-
+
if (! options::bvEagerExplanations.wasSetByUser() &&
d_logic.isTheoryEnabled(THEORY_ARRAY) &&
d_logic.isTheoryEnabled(THEORY_BV)) {
@@ -1093,8 +1093,6 @@ void SmtEngine::setDefaults() {
options::bvEagerExplanations.set(true);
}
-
-
// Turn on arith rewrite equalities only for pure arithmetic
if(! options::arithRewriteEq.wasSetByUser()) {
bool arithRewriteEq = d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified();
@@ -2006,11 +2004,11 @@ void SmtEnginePrivate::bvAbstraction() {
d_assertionsToPreprocess[i] = Rewriter::rewrite(new_assertions[i]);
}
// if we are using the lazy solver and the abstraction
- // applies, then UF symbols were introduced
+ // applies, then UF symbols were introduced
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY &&
changed) {
LogicRequest req(d_smt);
- req.widenLogic(THEORY_UF);
+ req.widenLogic(THEORY_UF);
}
}
@@ -2577,7 +2575,7 @@ bool SmtEnginePrivate::simplifyAssertions()
// before ppRewrite check if only core theory for BV theory
d_smt.d_theoryEngine->staticInitializeBVOptions(d_assertionsToCheck);
-
+
// Theory preprocessing
if (d_smt.d_earlyTheoryPP) {
Chat() << "...doing early theory preprocessing..." << endl;
@@ -2870,18 +2868,17 @@ void SmtEnginePrivate::processAssertions() {
Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
-
+
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER &&
!d_smt.d_logic.isPure(THEORY_BV)) {
throw ModalException("Eager bit-blasting does not currently support theory combination. "
"Note that in a QF_BV problem UF symbols can be introduced for division. "
- "Try --bv-div-zero-const to interpret division by zero as a constant.");
+ "Try --bv-div-zero-const to interpret division by zero as a constant.");
}
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
- d_smt.d_theoryEngine->mkAckermanizationAsssertions(d_assertionsToPreprocess);
+ d_smt.d_theoryEngine->mkAckermanizationAsssertions(d_assertionsToPreprocess);
}
-
if ( options::bvAbstraction() &&
!options::incrementalSolving()) {
@@ -2889,7 +2886,7 @@ void SmtEnginePrivate::processAssertions() {
bvAbstraction();
dumpAssertions("post-bv-abstraction", d_assertionsToPreprocess);
}
-
+
dumpAssertions("pre-boolean-terms", d_assertionsToPreprocess);
{
Chat() << "rewriting Boolean terms..." << endl;
@@ -2952,7 +2949,7 @@ void SmtEnginePrivate::processAssertions() {
bvToBool();
dumpAssertions("post-bv-to-bool", d_assertionsToPreprocess);
}
-
+
if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
dumpAssertions("pre-strings-pp", d_assertionsToPreprocess);
CVC4::theory::strings::StringsPreprocess sp;
@@ -3174,10 +3171,10 @@ void SmtEnginePrivate::processAssertions() {
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
for (unsigned i = 0; i < d_assertionsToCheck.size(); ++i) {
Node eager_atom = NodeManager::currentNM()->mkNode(kind::BITVECTOR_EAGER_ATOM, d_assertionsToCheck[i]);
- d_assertionsToCheck[i] = eager_atom;
+ d_assertionsToCheck[i] = eager_atom;
}
}
-
+
// Push the formula to decision engine
if(noConflict) {
Chat() << "pushing to decision engine..." << endl;
@@ -3191,6 +3188,7 @@ void SmtEnginePrivate::processAssertions() {
dumpAssertions("post-everything", d_assertionsToCheck);
+ // Push the formula to SAT
{
Chat() << "converting to CNF..." << endl;
TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_cnfConversionTime);
@@ -3198,7 +3196,6 @@ void SmtEnginePrivate::processAssertions() {
d_smt.d_propEngine->assertFormula(d_assertionsToCheck[i]);
}
}
-
d_assertionsProcessed = true;
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index 0d22325e7..05f5c7678 100644
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): Liana Hadarean, Tim King, ACSYS, Christopher L. Conway, Dejan Jovanovic, Francois Bobot
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
@@ -125,6 +125,10 @@ bool Configuration::isBuiltWithGlpk() {
return IS_GLPK_BUILD;
}
+bool Configuration::isBuiltWithAbc() {
+ return IS_ABC_BUILD;
+}
+
bool Configuration::isBuiltWithCudd() {
return false;
}
diff --git a/src/util/configuration.h b/src/util/configuration.h
index 696b67715..c6562b3e6 100644
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): ACSYS, Liana Hadarean, Tim King, Francois Bobot
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
@@ -91,6 +91,8 @@ public:
static bool isBuiltWithGlpk();
+ static bool isBuiltWithAbc();
+
static bool isBuiltWithReadline();
static bool isBuiltWithCudd();
diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h
index 07ab4b17e..631a323d3 100644
--- a/src/util/configuration_private.h
+++ b/src/util/configuration_private.h
@@ -5,7 +5,7 @@
** Major contributors: ACSYS, Morgan Deters
** Minor contributors (to current version): Liana Hadarean, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
@@ -107,6 +107,12 @@ namespace CVC4 {
# define IS_GLPK_BUILD false
#endif /* CVC4_USE_GLPK */
+#if CVC4_USE_ABC
+# define IS_ABC_BUILD true
+#else /* CVC4_USE_ABC */
+# define IS_ABC_BUILD false
+#endif /* CVC4_USE_ABC */
+
#ifdef HAVE_LIBREADLINE
# define IS_READLINE_BUILD true
#else /* HAVE_LIBREADLINE */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback