Some clean-up, post bv-merge.

Add abc to build id and fix static building.

Add abc to --show-config output and Configuration class API.

Add ability to select abc source path.

Fix arch_flags for abc.

diff --git a/Makefile b/Makefile
index f5d379d6becc7a94177bd6acdb45bc601dde773f..c8126ae9538f76c75f2e377388dbfe7a9cb3f04e 100644 (file)
--- 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 (file)
index 0000000..d86b2f4
--- /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 1ef9191f75de58714eb597d258c0ffe6bb494d6d..ae4e292f459d76e1332bb25c6a341479813ffe4f 100755 (executable)
--- 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 40e2054e6264c46f710b6d6e73cc27176fad0c3f..ea202e94fc1ad1ed85991c14a5e5df73eea8e575 100644 (file)
--- 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 cfd65aef44745019e1e6560ec5898df5da5e95e3..92a9c10ce02e7c55b0815e0b20c3bb6fcb1208a7 100644 (file)
--- 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 97fbb1503019cd4b9f629729fe58ff1d5fa1152a..f5a39703995e0a130417bf38a7afd3e3fd0f0a2a 100755 (executable)
--- 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 34fa20c1dbc2996944a792788970ebb1f91356c7..9531db0cec9552c9865b2c635ed99cf5af87fb75 100644 (file)
--- 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 7723dcb33b17b0cb86353719afe1f8bb85351c46..ee16af2f2c0426715ccca5fbadd0be378a8eaaf5 100644 (file)
--- 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 a5fe46d278023a94db70fd1a38fab4caab537cf4..ebf36b0cdc1ef0bf48b1376dd98a6814a7fee09c 100644 (file)
--- 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 b71969d1557e01d2e86a9c939cc025708f41cca0..6ab25ee5719c480910c97b135b95021a836151df 100644 (file)
--- 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 0d22325e79a3c1a714f50e0172af1cbd3c0f4c7f..05f5c76782fb952581e1d6c79dbb602b40dc1a08 100644 (file)
--- 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 696b67715a71a32a30964b4b7c24f47afbc34f46..c6562b3e6610292ae7db24258b702c187d5c6b60 100644 (file)
--- 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 07ab4b17e2761d833e669e52fc19d6c2a48ae2f7..631a323d391455a32fe373ef5943eeb1fab2c8db 100644 (file)
--- 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 */