From 614670f98a9ab2d3cfcb9f364a1b06d78f63ebb0 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Tue, 20 Mar 2018 16:11:15 -0700 Subject: Add support for CaDiCaL as eager BV SAT solver. (#1675) --- 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 ++- 13 files changed, 377 insertions(+), 40 deletions(-) create mode 100644 src/prop/cadical.cpp create mode 100644 src/prop/cadical.h (limited to 'src') 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, -- cgit v1.2.3