summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--COPYING3
-rw-r--r--config/cadical.m490
-rw-r--r--config/cryptominisat.m43
-rw-r--r--configure.ac20
-rwxr-xr-xcontrib/get-cadical22
-rw-r--r--src/Makefile.am7
-rw-r--r--src/base/configuration.cpp28
-rw-r--r--src/base/configuration.h2
-rw-r--r--src/base/configuration_private.h6
-rw-r--r--src/options/bv_bitblast_mode.h7
-rw-r--r--src/options/options_handler.cpp51
-rw-r--r--src/prop/cadical.cpp165
-rw-r--r--src/prop/cadical.h90
-rw-r--r--src/prop/cryptominisat.cpp4
-rw-r--r--src/prop/cryptominisat.h2
-rw-r--r--src/prop/sat_solver_factory.cpp17
-rw-r--r--src/prop/sat_solver_factory.h25
-rw-r--r--src/theory/bv/eager_bitblaster.cpp13
18 files changed, 512 insertions, 43 deletions
diff --git a/COPYING b/COPYING
index 66750d6d7..d6d727360 100644
--- a/COPYING
+++ b/COPYING
@@ -82,7 +82,8 @@ GMP) may (and do) remain under the more permissive modified BSD license.
CVC4 optionally links against the following libraries:
ABC (https://bitbucket.org/alanmi/abc)
- Cryptominisat4.0 (https://github.com/msoos/cryptominisat)
+ CaDiCaL (https://github.com/arminbiere/cadical)
+ CryptoMiniSat (https://github.com/msoos/cryptominisat)
LFSC checker (https://github.com/CVC4/LFSC)
Linking CVC4 against these libraries does not affect the license terms of the
diff --git a/config/cadical.m4 b/config/cadical.m4
new file mode 100644
index 000000000..77625b036
--- /dev/null
+++ b/config/cadical.m4
@@ -0,0 +1,90 @@
+# CVC4_CHECK_FOR_CADICAL
+# ------------------
+# Look for CaDiCaL and link it in, but only if user requested.
+AC_DEFUN([CVC4_CHECK_FOR_CADICAL], [
+AC_MSG_CHECKING([whether user requested CaDiCaL support])
+
+have_libcadical=0
+CADICAL_LIBS=
+CADICAL_LDFLAGS=
+
+have_libcadical=0
+if test "$with_cadical" = no; then
+ AC_MSG_RESULT([no, CaDiCaL disabled by user])
+elif test -n "$with_cadical"; then
+ AC_MSG_RESULT([yes, CaDiCaL requested by user])
+ AC_ARG_VAR(CADICAL_HOME, [path to top level of CaDiCaL source tree])
+ AC_ARG_WITH(
+ [cadical-dir],
+ AS_HELP_STRING(
+ [--with-cadical-dir=PATH],
+ [path to top level of CaDiCaL source tree]
+ ),
+ CADICAL_HOME="$withval",
+ [ if test -z "$CADICAL_HOME" && ! test -e "$ac_abs_confdir/cadical/build/libcadical.a"; then
+ AC_MSG_FAILURE([must give --with-cadical-dir=PATH, define environment variable CADICAL_HOME, or use contrib/get-cadical to setup CaDiCaL for CVC4!])
+ fi
+ ]
+ )
+
+ # Check if CaDiCaL was installed via contrib/get-cadical
+ AC_MSG_CHECKING([whether CaDiCaL was already installed via contrib/get-cadical])
+ if test -z "$CADICAL_HOME" && test -e "$ac_abs_confdir/cadical/build/libcadical.a"; then
+ CADICAL_HOME="$ac_abs_confdir/cadical"
+ AC_MSG_RESULT([yes, $CADICAL_HOME])
+ else
+ AC_MSG_RESULT([no])
+ fi
+
+ if ! test -d "$CADICAL_HOME" || ! test -e "$CADICAL_HOME/build/libcadical.a" ; then
+ AC_MSG_FAILURE([either $CADICAL_HOME is not a CaDiCaL source tree or it's not yet built $CADICAL_HOME/build/libcadical.a])
+ fi
+
+ AC_MSG_CHECKING([how to link CaDiCaL])
+
+ CVC4_TRY_CADICAL
+
+ if test -z "$CADICAL_LIBS"; then
+ AC_MSG_FAILURE([cannot link against libcadical!])
+ else
+ AC_MSG_RESULT([$CADICAL_LIBS])
+ have_libcadical=1
+ fi
+
+ CADICAL_LDFLAGS="-L$CADICAL_HOME/build"
+
+else
+ AC_MSG_RESULT([no, user didn't request CaDiCaL])
+ with_cadical=no
+fi
+
+])# CVC4_CHECK_FOR_CADICAL
+
+# CVC4_TRY_CADICAL
+# ------------------------------
+# Try AC_CHECK_LIB(cadical) with the given linking libraries
+AC_DEFUN([CVC4_TRY_CADICAL], [
+if test -z "$CADICAL_LIBS"; then
+ AC_LANG_PUSH([C++])
+
+ cvc4_save_LIBS="$LIBS"
+ cvc4_save_LDFLAGS="$LDFLAGS"
+ cvc4_save_CPPFLAGS="$CPPFLAGS"
+
+ LDFLAGS="-L$CADICAL_HOME/build"
+ CPPFLAGS="$CPPFLAGS -I$CADICAL_HOME/src"
+ LIBS="-lcadical"
+
+ AC_LINK_IFELSE(
+ [AC_LANG_PROGRAM([[#include <cadical.hpp>]],
+ [[CaDiCaL::Solver test();]])], [CADICAL_LIBS="-lcadical"],
+ [CADICAL_LIBS=])
+
+ LDFLAGS="$cvc4_save_LDFLAGS"
+ CPPFLAGS="$cvc4_save_CPPFLAGS"
+ LIBS="$cvc4_save_LIBS"
+
+ AC_LANG_POP([C++])
+fi
+])# CVC4_TRY_CADICAL
+
diff --git a/config/cryptominisat.m4 b/config/cryptominisat.m4
index 8f2f5bc51..7ddb895b5 100644
--- a/config/cryptominisat.m4
+++ b/config/cryptominisat.m4
@@ -40,8 +40,6 @@ elif test -n "$with_cryptominisat"; then
AC_MSG_FAILURE([either $CRYPTOMINISAT_HOME is not an cryptominisat install tree or it's not yet built])
fi
- CPPFLAGS="$CPPFLAGS -I$CRYPTOMINISAT_HOME/install/include"
-
AC_MSG_CHECKING([how to link cryptominisat])
dnl TODO FIXME:
@@ -77,6 +75,7 @@ if test -z "$CRYPTOMINISAT_LIBS"; then
cvc4_save_CPPFLAGS="$CPPFLAGS"
LDFLAGS="-L$CRYPTOMINISAT_HOME/install/lib"
+ CPPFLAGS="$CPPFLAGS -I$CRYPTOMINISAT_HOME/install/include"
LIBS="-lcryptominisat5 $1"
AC_LINK_IFELSE(
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
diff --git a/contrib/get-cadical b/contrib/get-cadical
new file mode 100755
index 000000000..a4be17d51
--- /dev/null
+++ b/contrib/get-cadical
@@ -0,0 +1,22 @@
+#!/bin/bash
+#
+source "$(dirname "$0")/get-script-header.sh"
+
+if [ -e cadical ]; then
+ echo 'error: file or directory "cadical" exists; please move it out of the way.' >&2
+ exit 1
+fi
+
+commit="b44ce4f0e64aa400358ae3a8adb45b24ae6e742c"
+
+git clone https://github.com/arminbiere/cadical cadical
+cd cadical
+git checkout $commit
+
+CXXFLAGS="-fPIC" ./configure && make -j$(nproc)
+
+echo
+echo "Using CaDiCaL commit $commit"
+echo
+echo ===================== Now configure CVC4 with =====================
+echo ./configure --with-cadical
diff --git a/src/Makefile.am b/src/Makefile.am
index 4f5730d63..c6f8a7ad1 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -114,6 +114,8 @@ libcvc4_la_SOURCES = \
proof/uf_proof.h \
proof/unsat_core.cpp \
proof/unsat_core.h \
+ prop/cadical.cpp \
+ prop/cadical.h \
prop/cnf_stream.cpp \
prop/cnf_stream.h \
prop/cryptominisat.cpp \
@@ -561,6 +563,11 @@ libcvc4_la_LIBADD += $(ABC_LIBS)
libcvc4_la_LDFLAGS += $(ABC_LDFLAGS)
endif
+if CVC4_USE_CADICAL
+libcvc4_la_LIBADD += $(CADICAL_LIBS)
+libcvc4_la_LDFLAGS += $(CADICAL_LDFLAGS)
+endif
+
if CVC4_USE_CRYPTOMINISAT
libcvc4_la_LIBADD += $(CRYPTOMINISAT_LIBS)
libcvc4_la_LDFLAGS += $(CRYPTOMINISAT_LDFLAGS)
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index 7e7da1500..7ceb64885 100644
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -134,7 +134,10 @@ std::string Configuration::copyright() {
<< "\n\n";
if (Configuration::isBuiltWithAbc()
- || Configuration::isBuiltWithLfsc()) {
+ || Configuration::isBuiltWithLfsc()
+ || Configuration::isBuiltWithCadical()
+ || Configuration::isBuiltWithCryptominisat())
+ {
ss << "This version of CVC4 is linked against the following non-(L)GPL'ed\n"
<< "third party libraries.\n\n";
if (Configuration::isBuiltWithAbc()) {
@@ -147,10 +150,22 @@ std::string Configuration::copyright() {
<< " See http://github.com/CVC4/LFSC for copyright and\n"
<< " licensing information.\n\n";
}
+ if (Configuration::isBuiltWithCadical())
+ {
+ ss << " CaDiCaL - Simplified Satisfiability Solver\n"
+ << " See https://github.com/arminbiere/cadical for copyright "
+ << "information.\n\n";
+ }
+ if (Configuration::isBuiltWithCryptominisat())
+ {
+ ss << " CryptoMiniSat - An Advanced SAT Solver\n"
+ << " See https://github.com/msoos/cryptominisat for copyright "
+ << "information.\n\n";
+ }
}
- if (Configuration::isBuiltWithGmp()
- || Configuration::isBuiltWithCryptominisat()) {
+ if (Configuration::isBuiltWithGmp())
+ {
ss << "This version of CVC4 is linked against the following third party\n"
<< "libraries covered by the LGPLv3 license.\n"
<< "See licenses/lgpl-3.0.txt for more information.\n\n";
@@ -158,11 +173,6 @@ std::string Configuration::copyright() {
ss << " GMP - Gnu Multi Precision Arithmetic Library\n"
<< " See http://gmplib.org for copyright information.\n\n";
}
- if (Configuration::isBuiltWithCryptominisat()) {
- ss << " CryptoMiniSat - An Advanced SAT Solver\n"
- << " See http://github.com/msoos/cryptominisat for copyright "
- << "information.\n\n";
- }
}
if (Configuration::isBuiltWithCln()
@@ -228,6 +238,8 @@ bool Configuration::isBuiltWithAbc() {
return IS_ABC_BUILD;
}
+bool Configuration::isBuiltWithCadical() { return IS_CADICAL_BUILD; }
+
bool Configuration::isBuiltWithCryptominisat() {
return IS_CRYPTOMINISAT_BUILD;
}
diff --git a/src/base/configuration.h b/src/base/configuration.h
index 29f23ab18..897f234d7 100644
--- a/src/base/configuration.h
+++ b/src/base/configuration.h
@@ -95,6 +95,8 @@ public:
static bool isBuiltWithAbc();
+ static bool isBuiltWithCadical();
+
static bool isBuiltWithCryptominisat();
static bool isBuiltWithReadline();
diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h
index eba45cc61..cf9117100 100644
--- a/src/base/configuration_private.h
+++ b/src/base/configuration_private.h
@@ -114,6 +114,12 @@ namespace CVC4 {
# define IS_ABC_BUILD false
#endif /* CVC4_USE_ABC */
+#if CVC4_USE_CADICAL
+#define IS_CADICAL_BUILD true
+#else /* CVC4_USE_CADICAL */
+#define IS_CADICAL_BUILD false
+#endif /* CVC4_USE_CADICAL */
+
#if CVC4_USE_CRYPTOMINISAT
# define IS_CRYPTOMINISAT_BUILD true
#else /* CVC4_USE_CRYPTOMINISAT */
diff --git a/src/options/bv_bitblast_mode.h b/src/options/bv_bitblast_mode.h
index 5bc5f601f..79f859cd4 100644
--- a/src/options/bv_bitblast_mode.h
+++ b/src/options/bv_bitblast_mode.h
@@ -61,11 +61,12 @@ enum BvSlicerMode {
};/* enum BvSlicerMode */
/** Enumeration of sat solvers that can be used. */
-enum SatSolverMode {
+enum SatSolverMode
+{
SAT_SOLVER_MINISAT,
SAT_SOLVER_CRYPTOMINISAT,
-};/* enum SatSolver */
-
+ SAT_SOLVER_CADICAL,
+}; /* enum SatSolver */
}/* CVC4::theory::bv namespace */
}/* CVC4::theory namespace */
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 61f7646ee..9b2eb1cb2 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -1042,25 +1042,29 @@ void OptionsHandler::abcEnabledBuild(std::string option, std::string value)
void OptionsHandler::satSolverEnabledBuild(std::string option, bool value)
{
-#ifndef CVC4_USE_CRYPTOMINISAT
- if(value) {
+#if !defined(CVC4_USE_CRYPTOMINISAT) && !defined(CVC4_USE_CADICAL)
+ if (value)
+ {
std::stringstream ss;
- ss << "option `" << option << "' requires an cryptominisat-enabled build of CVC4; this binary was not built with cryptominisat support";
+ ss << "option `" << option
+ << "' requires a CVC4 to be built with CryptoMiniSat or CaDiCaL";
throw OptionException(ss.str());
}
-#endif /* CVC4_USE_CRYPTOMINISAT */
+#endif
}
void OptionsHandler::satSolverEnabledBuild(std::string option,
std::string value)
{
-#ifndef CVC4_USE_CRYPTOMINISAT
- if(!value.empty()) {
+#if !defined(CVC4_USE_CRYPTOMINISAT) && !defined(CVC4_USE_CADICAL)
+ if (!value.empty())
+ {
std::stringstream ss;
- ss << "option `" << option << "' requires an cryptominisat-enabled build of CVC4; this binary was not built with cryptominisat support";
+ ss << "option `" << option
+ << "' requires a CVC4 to be built with CryptoMiniSat or CaDiCaL";
throw OptionException(ss.str());
}
-#endif /* CVC4_USE_CRYPTOMINISAT */
+#endif
}
const std::string OptionsHandler::s_bvSatSolverHelp = "\
@@ -1068,6 +1072,8 @@ Sat solvers currently supported by the --bv-sat-solver option:\n\
\n\
minisat (default)\n\
\n\
+cadical\n\
+\n\
cryptominisat\n\
";
@@ -1080,13 +1086,14 @@ theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option,
if (options::incrementalSolving() &&
options::incrementalSolving.wasSetByUser()) {
- throw OptionException(std::string("Cryptominsat does not support incremental mode. \n\
+ throw OptionException(std::string("CryptoMinSat does not support incremental mode. \n\
Try --bv-sat-solver=minisat"));
}
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY &&
options::bitblastMode.wasSetByUser()) {
- throw OptionException(std::string("Cryptominsat does not support lazy bit-blsating. \n\
+ throw OptionException(
+ std::string("CryptoMiniSat does not support lazy bit-blasting. \n\
Try --bv-sat-solver=minisat"));
}
if (!options::bitvectorToBool.wasSetByUser()) {
@@ -1099,6 +1106,29 @@ theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option,
// options::skolemizeArguments.set(true);
// }
return theory::bv::SAT_SOLVER_CRYPTOMINISAT;
+ }
+ else if (optarg == "cadical")
+ {
+ if (options::incrementalSolving()
+ && options::incrementalSolving.wasSetByUser())
+ {
+ throw OptionException(
+ std::string("CaDiCaL does not support incremental mode. \n\
+ Try --bv-sat-solver=minisat"));
+ }
+
+ if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY
+ && options::bitblastMode.wasSetByUser())
+ {
+ throw OptionException(
+ std::string("CaDiCaL does not support lazy bit-blasting. \n\
+ Try --bv-sat-solver=minisat"));
+ }
+ if (!options::bitvectorToBool.wasSetByUser())
+ {
+ options::bitvectorToBool.set(true);
+ }
+ return theory::bv::SAT_SOLVER_CADICAL;
} else if(optarg == "help") {
puts(s_bvSatSolverHelp.c_str());
exit(1);
@@ -1658,6 +1688,7 @@ void OptionsHandler::showConfiguration(std::string option) {
print_config_cond("abc", Configuration::isBuiltWithAbc());
print_config_cond("cln", Configuration::isBuiltWithCln());
print_config_cond("glpk", Configuration::isBuiltWithGlpk());
+ print_config_cond("cadical", Configuration::isBuiltWithCadical());
print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat());
print_config_cond("gmp", Configuration::isBuiltWithGmp());
print_config_cond("lfsc", Configuration::isBuiltWithLfsc());
diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp
new file mode 100644
index 000000000..3fd210699
--- /dev/null
+++ b/src/prop/cadical.cpp
@@ -0,0 +1,165 @@
+/********************* */
+/*! \file cadical.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mathias Preiner
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Wrapper for CaDiCaL SAT Solver.
+ **
+ ** Implementation of the CaDiCaL SAT solver for CVC4 (bitvectors).
+ **/
+
+#include "prop/cadical.h"
+
+#ifdef CVC4_USE_CADICAL
+
+#include "proof/sat_proof.h"
+
+namespace CVC4 {
+namespace prop {
+
+using CadicalLit = int;
+using CadicalVar = int;
+
+// helper functions
+namespace {
+
+SatValue toSatValue(int result)
+{
+ if (result == 10) return SAT_VALUE_TRUE;
+ if (result == 20) return SAT_VALUE_FALSE;
+ Assert(result == 0);
+ return SAT_VALUE_UNKNOWN;
+}
+
+SatValue toSatValueLit(int value)
+{
+ if (value == 1) return SAT_VALUE_TRUE;
+ Assert(value == -1);
+ return SAT_VALUE_FALSE;
+}
+
+CadicalLit toCadicalLit(const SatLiteral lit)
+{
+ return lit.isNegated() ? -lit.getSatVariable() : lit.getSatVariable();
+}
+
+CadicalVar toCadicalVar(SatVariable var) { return var; }
+
+} // namespace helper functions
+
+CadicalSolver::CadicalSolver(StatisticsRegistry* registry,
+ const std::string& name)
+ : d_solver(new CaDiCaL::Solver()),
+ // Note: CaDiCaL variables start with index 1 rather than 0 since negated
+ // literals are represented as the negation of the index.
+ d_nextVarIdx(1),
+ d_statistics(registry, name)
+{
+ d_true = newVar();
+ d_false = newVar();
+
+ d_solver->set("quiet", 1); // CaDiCaL is verbose by default
+ d_solver->add(toCadicalVar(d_true));
+ d_solver->add(0);
+ d_solver->add(-toCadicalVar(d_false));
+ d_solver->add(0);
+}
+
+CadicalSolver::~CadicalSolver() {}
+
+ClauseId CadicalSolver::addClause(SatClause& clause, bool removable)
+{
+ for (const SatLiteral& lit : clause)
+ {
+ d_solver->add(toCadicalLit(lit));
+ }
+ d_solver->add(0);
+ ++d_statistics.d_numClauses;
+ return ClauseIdError;
+}
+
+ClauseId CadicalSolver::addXorClause(SatClause& clause,
+ bool rhs,
+ bool removable)
+{
+ Unreachable("CaDiCaL does not support adding XOR clauses.");
+}
+
+SatVariable CadicalSolver::newVar(bool isTheoryAtom,
+ bool preRegister,
+ bool canErase)
+{
+ ++d_statistics.d_numVariables;
+ return d_nextVarIdx++;
+}
+
+SatVariable CadicalSolver::trueVar() { return d_true; }
+
+SatVariable CadicalSolver::falseVar() { return d_false; }
+
+SatValue CadicalSolver::solve()
+{
+ TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
+ SatValue res = toSatValue(d_solver->solve());
+ d_okay = (res == SAT_VALUE_TRUE);
+ ++d_statistics.d_numSatCalls;
+ return res;
+}
+
+SatValue CadicalSolver::solve(long unsigned int&)
+{
+ Unimplemented("Setting limits for CaDiCaL not supported yet");
+};
+
+void CadicalSolver::interrupt() { d_solver->terminate(); }
+
+SatValue CadicalSolver::value(SatLiteral l)
+{
+ Assert(d_okay);
+ return toSatValueLit(d_solver->val(toCadicalLit(l)));
+}
+
+SatValue CadicalSolver::modelValue(SatLiteral l)
+{
+ Assert(d_okay);
+ return value(l);
+}
+
+unsigned CadicalSolver::getAssertionLevel() const
+{
+ Unreachable("CaDiCal does not support assertion levels.");
+}
+
+bool CadicalSolver::ok() const { return d_okay; }
+
+CadicalSolver::Statistics::Statistics(StatisticsRegistry* registry,
+ const std::string& prefix)
+ : d_registry(registry),
+ d_numSatCalls("theory::bv::" + prefix + "::cadical::calls_to_solve", 0),
+ d_numVariables("theory::bv::" + prefix + "::cadical::variables", 0),
+ d_numClauses("theory::bv::" + prefix + "::cadical::clauses", 0),
+ d_solveTime("theory::bv::" + prefix + "::cadical::solve_time")
+{
+ d_registry->registerStat(&d_numSatCalls);
+ d_registry->registerStat(&d_numVariables);
+ d_registry->registerStat(&d_numClauses);
+ d_registry->registerStat(&d_solveTime);
+}
+
+CadicalSolver::Statistics::~Statistics() {
+ d_registry->unregisterStat(&d_numSatCalls);
+ d_registry->unregisterStat(&d_numVariables);
+ d_registry->unregisterStat(&d_numClauses);
+ d_registry->unregisterStat(&d_solveTime);
+}
+
+} // namespace prop
+} // namespace CVC4
+
+#endif // CVC4_USE_CADICAL
diff --git a/src/prop/cadical.h b/src/prop/cadical.h
new file mode 100644
index 000000000..2e2c1cc51
--- /dev/null
+++ b/src/prop/cadical.h
@@ -0,0 +1,90 @@
+/********************* */
+/*! \file cadical.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mathias Preiner
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Wrapper for CaDiCaL SAT Solver.
+ **
+ ** Implementation of the CaDiCaL SAT solver for CVC4 (bitvectors).
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PROP__CADICAL_H
+#define __CVC4__PROP__CADICAL_H
+
+#ifdef CVC4_USE_CADICAL
+
+#include "prop/sat_solver.h"
+
+#include <cadical.hpp>
+
+namespace CVC4 {
+namespace prop {
+
+class CadicalSolver : public SatSolver
+{
+ public:
+ CadicalSolver(StatisticsRegistry* registry, const std::string& name = "");
+
+ ~CadicalSolver() override;
+
+ ClauseId addClause(SatClause& clause, bool removable) override;
+
+ ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override;
+
+ SatVariable newVar(bool isTheoryAtom = false,
+ bool preRegister = false,
+ bool canErase = true) override;
+
+ SatVariable trueVar() override;
+
+ SatVariable falseVar() override;
+
+ SatValue solve() override;
+
+ SatValue solve(long unsigned int&) override;
+
+ void interrupt() override;
+
+ SatValue value(SatLiteral l) override;
+
+ SatValue modelValue(SatLiteral l) override;
+
+ unsigned getAssertionLevel() const override;
+
+ bool ok() const override;
+
+ private:
+ std::unique_ptr<CaDiCaL::Solver> d_solver;
+
+ unsigned d_nextVarIdx;
+ bool d_okay;
+ SatVariable d_true;
+ SatVariable d_false;
+
+ struct Statistics
+ {
+ StatisticsRegistry* d_registry;
+ IntStat d_numSatCalls;
+ IntStat d_numVariables;
+ IntStat d_numClauses;
+ TimerStat d_solveTime;
+ Statistics(StatisticsRegistry* registry, const std::string& prefix);
+ ~Statistics();
+ };
+
+ Statistics d_statistics;
+};
+
+} // namespace prop
+} // namespace CVC4
+
+#endif // CVC4_USE_CADICAL
+#endif // __CVC4__PROP__CADICAL_H
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index c48a54afb..249a5eabb 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -79,9 +79,7 @@ CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry* registry,
}
-CryptoMinisatSolver::~CryptoMinisatSolver() {
- delete d_solver;
-}
+CryptoMinisatSolver::~CryptoMinisatSolver() {}
ClauseId CryptoMinisatSolver::addXorClause(SatClause& clause,
bool rhs,
diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h
index 32c05974b..c1782b6c0 100644
--- a/src/prop/cryptominisat.h
+++ b/src/prop/cryptominisat.h
@@ -38,7 +38,7 @@ namespace prop {
class CryptoMinisatSolver : public SatSolver {
private:
- CMSat::SATSolver* d_solver;
+ std::unique_ptr<CMSat::SATSolver> d_solver;
unsigned d_numVariables;
bool d_okay;
SatVariable d_true;
diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index 69fca59e1..0a8246667 100644
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -17,6 +17,7 @@
#include "prop/sat_solver_factory.h"
#include "prop/bvminisat/bvminisat.h"
+#include "prop/cadical.h"
#include "prop/cryptominisat.h"
#include "prop/minisat/minisat.h"
@@ -31,6 +32,12 @@ BVSatSolverInterface* SatSolverFactory::createMinisat(
return new BVMinisatSatSolver(registry, mainSatContext, name);
}
+DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat(
+ StatisticsRegistry* registry)
+{
+ return new MinisatSatSolver(registry);
+}
+
SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry* registry,
const std::string& name)
{
@@ -41,10 +48,14 @@ SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry* registry,
#endif
}
-DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat(
- StatisticsRegistry* registry)
+SatSolver* SatSolverFactory::createCadical(StatisticsRegistry* registry,
+ const std::string& name)
{
- return new MinisatSatSolver(registry);
+#ifdef CVC4_USE_CADICAL
+ return new CadicalSolver(registry, name);
+#else
+ Unreachable("CVC4 was not compiled with CaDiCaL support.");
+#endif
}
} // namespace prop
diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h
index fac8c9083..8d6e405d8 100644
--- a/src/prop/sat_solver_factory.h
+++ b/src/prop/sat_solver_factory.h
@@ -16,7 +16,8 @@
#include "cvc4_private.h"
-#pragma once
+#ifndef __CVC4__PROP__SAT_SOLVER_FACTORY_H
+#define __CVC4__PROP__SAT_SOLVER_FACTORY_H
#include <string>
#include <vector>
@@ -28,17 +29,25 @@
namespace CVC4 {
namespace prop {
-class SatSolverFactory {
-public:
-
+class SatSolverFactory
+{
+ public:
static BVSatSolverInterface* createMinisat(context::Context* mainSatContext,
StatisticsRegistry* registry,
const std::string& name = "");
- static DPLLSatSolverInterface* createDPLLMinisat(StatisticsRegistry* registry);
+
+ static DPLLSatSolverInterface* createDPLLMinisat(
+ StatisticsRegistry* registry);
+
static SatSolver* createCryptoMinisat(StatisticsRegistry* registry,
const std::string& name = "");
-};/* class SatSolverFactory */
+ static SatSolver* createCadical(StatisticsRegistry* registry,
+ const std::string& name = "");
+
+}; /* class SatSolverFactory */
+
+} // namespace prop
+} // namespace CVC4
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
+#endif // __CVC4__PROP__SAT_SOLVER_FACTORY_H
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index f8317cf15..25610af2b 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -44,8 +44,10 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
d_bitblastingRegistrar = new BitblastingRegistrar(this);
d_nullContext = new context::Context();
- switch (options::bvSatSolver()) {
- case SAT_SOLVER_MINISAT: {
+ switch (options::bvSatSolver())
+ {
+ case SAT_SOLVER_MINISAT:
+ {
prop::BVSatSolverInterface* minisat =
prop::SatSolverFactory::createMinisat(
d_nullContext, smtStatisticsRegistry(), "EagerBitblaster");
@@ -54,12 +56,15 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
d_satSolver = minisat;
break;
}
+ case SAT_SOLVER_CADICAL:
+ d_satSolver = prop::SatSolverFactory::createCadical(
+ smtStatisticsRegistry(), "EagerBitblaster");
+ break;
case SAT_SOLVER_CRYPTOMINISAT:
d_satSolver = prop::SatSolverFactory::createCryptoMinisat(
smtStatisticsRegistry(), "EagerBitblaster");
break;
- default:
- Unreachable("Unknown SAT solver type");
+ default: Unreachable("Unknown SAT solver type");
}
d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback