From 614670f98a9ab2d3cfcb9f364a1b06d78f63ebb0 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Tue, 20 Mar 2018 16:11:15 -0700 Subject: [PATCH] Add support for CaDiCaL as eager BV SAT solver. (#1675) --- COPYING | 3 +- config/cadical.m4 | 90 ++++++++++++++++ config/cryptominisat.m4 | 3 +- configure.ac | 20 ++++ contrib/get-cadical | 22 ++++ src/Makefile.am | 7 ++ src/base/configuration.cpp | 28 +++-- src/base/configuration.h | 2 + src/base/configuration_private.h | 6 ++ src/options/bv_bitblast_mode.h | 7 +- src/options/options_handler.cpp | 51 +++++++-- src/prop/cadical.cpp | 165 +++++++++++++++++++++++++++++ src/prop/cadical.h | 90 ++++++++++++++++ src/prop/cryptominisat.cpp | 4 +- src/prop/cryptominisat.h | 2 +- src/prop/sat_solver_factory.cpp | 17 ++- src/prop/sat_solver_factory.h | 25 +++-- src/theory/bv/eager_bitblaster.cpp | 13 ++- 18 files changed, 512 insertions(+), 43 deletions(-) create mode 100644 config/cadical.m4 create mode 100755 contrib/get-cadical create mode 100644 src/prop/cadical.cpp create mode 100644 src/prop/cadical.h 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::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 + +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 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 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 #include @@ -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, -- 2.30.2