From 6f1454d2082d4e8783c3b35c30144ff557b99444 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 10 Jun 2014 17:52:26 -0400 Subject: [PATCH] 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. --- Makefile | 6 +- config/abc.m4 | 135 +++++++++++++++++++++++++++++++ config/build-type | 4 +- config/cvc4.m4 | 6 ++ configure.ac | 42 +++++----- contrib/get-abc | 10 ++- src/Makefile.am | 5 ++ src/main/options_handlers.h | 3 +- src/main/portfolio.cpp | 2 +- src/smt/smt_engine.cpp | 33 ++++---- src/util/configuration.cpp | 6 +- src/util/configuration.h | 4 +- src/util/configuration_private.h | 8 +- 13 files changed, 208 insertions(+), 56 deletions(-) create mode 100644 config/abc.m4 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 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 runPortfolio(int numThreads, for(int t = 0; t < numThreads; ++t) { if(optionWaitToJoin) { threads[t].join(); - } + } } std::pair 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 */ -- 2.30.2