diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-03-20 16:11:15 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-03-20 16:11:15 -0700 |
| commit | 614670f98a9ab2d3cfcb9f364a1b06d78f63ebb0 (patch) | |
| tree | 7dbdfbbae495fed26877c51267f6775f618f5d33 /configure.ac | |
| parent | 62f58d62c6c597eeb9cae5e08d74f21c4a5c5c40 (diff) | |
Add support for CaDiCaL as eager BV SAT solver. (#1675)
Diffstat (limited to 'configure.ac')
| -rw-r--r-- | configure.ac | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/configure.ac b/configure.ac index 5dd8ae691..3fe7587eb 100644 --- a/configure.ac +++ b/configure.ac @@ -130,6 +130,7 @@ if test -z "${enable_optimized+set}" -a \ -z "${with_cln+set}" -a \ -z "${with_glpk+set}" -a \ -z "${with_abc+set}" -a \ + -z "${with_cadical+set}" -a \ -z "${with_cryptominisat+set}" -a \ -z "${with_lfsc+set}"; then custom_build_profile=no @@ -235,6 +236,11 @@ if test -n "${with_abc+set}"; then btargs="$btargs abc" fi fi +if test -n "${with_cadical+set}"; then + if test "$with_cadical" = yes; then + btargs="$btargs cadical" + fi +fi if test -n "${with_cryptominisat+set}"; then if test "$with_cryptominisat" = yes; then btargs="$btargs cryptominisat" @@ -880,6 +886,19 @@ AC_SUBST([ABC_LDFLAGS]) AC_SUBST([ABC_LIBS]) +# Build with libcadical +AC_ARG_WITH([cadical], + [AS_HELP_STRING([--with-cadical], + [use the CaDiCaL SAT solver])], [], [with_cadical=]) +CVC4_CHECK_FOR_CADICAL +if test $have_libcadical -eq 1; then + CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_CADICAL" + CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$CADICAL_HOME/src" +fi +AM_CONDITIONAL([CVC4_USE_CADICAL], [test $have_libcadical -eq 1]) +AC_SUBST([CADICAL_LDFLAGS]) +AC_SUBST([CADICAL_LIBS]) + # Build with libcryptominisat AC_ARG_WITH([cryptominisat], [AS_HELP_STRING([--with-cryptominisat], @@ -1566,6 +1585,7 @@ Multithreaded: $support_multithreaded Portfolio : $with_portfolio ABC : $with_abc +CaDiCaL : $with_cadical Cryptominisat: $with_cryptominisat GLPK : $with_glpk LFSC : $with_lfsc |