diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-05-22 06:41:50 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-05-22 08:41:50 -0500 |
commit | c531152e6a707b66b885e508ea61e2a67e195ccc (patch) | |
tree | a18a2d342b03db1700a963470f2064cf3ac8d086 | |
parent | ae33f11d0f4156b4d21b9e77f6df59ec0f9e8184 (diff) |
Add support for SAT solver Kissat. (#4514)
-rw-r--r-- | CMakeLists.txt | 56 | ||||
-rw-r--r-- | cmake/FindKissat.cmake | 17 | ||||
-rwxr-xr-x | configure.sh | 36 | ||||
-rwxr-xr-x | contrib/get-kissat | 26 | ||||
-rw-r--r-- | src/CMakeLists.txt | 6 | ||||
-rw-r--r-- | src/base/configuration.cpp | 9 | ||||
-rw-r--r-- | src/base/configuration.h | 2 | ||||
-rw-r--r-- | src/base/configuration_private.h | 6 | ||||
-rw-r--r-- | src/options/bv_options.toml | 2 | ||||
-rw-r--r-- | src/options/options_handler.cpp | 17 | ||||
-rw-r--r-- | src/options/options_handler.h | 5 | ||||
-rw-r--r-- | src/prop/kissat.cpp | 179 | ||||
-rw-r--r-- | src/prop/kissat.h | 102 | ||||
-rw-r--r-- | src/prop/sat_solver_factory.cpp | 13 | ||||
-rw-r--r-- | src/prop/sat_solver_factory.h | 2 | ||||
-rw-r--r-- | src/theory/bv/bitblast/aig_bitblaster.cpp | 4 | ||||
-rw-r--r-- | src/theory/bv/bitblast/eager_bitblaster.cpp | 4 |
17 files changed, 451 insertions, 35 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index c535890e1..d34d6ebfe 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -67,6 +67,9 @@ endif() if(GMP_DIR) list(APPEND CMAKE_PREFIX_PATH "${GMP_DIR}") endif() +if(KISSAT_DIR) + list(APPEND CMAKE_PREFIX_PATH "${KISSAT_DIR}") +endif() if(LFSC_DIR) list(APPEND CMAKE_PREFIX_PATH "${LFSC_DIR}") endif() @@ -143,8 +146,9 @@ option(ENABLE_PROFILING "Enable support for gprof profiling") cvc4_option(USE_ABC "Use ABC for AIG bit-blasting") cvc4_option(USE_CADICAL "Use CaDiCaL SAT solver") cvc4_option(USE_CLN "Use CLN instead of GMP") -cvc4_option(USE_GLPK "Use GLPK simplex solver") cvc4_option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver") +cvc4_option(USE_GLPK "Use GLPK simplex solver") +cvc4_option(USE_KISSAT "Use Kissat SAT solver") cvc4_option(USE_READLINE "Use readline for better interactive support") # >> 2-valued: ON OFF # > for options where we don't need to detect if set by user (default: OFF) @@ -167,6 +171,7 @@ set(CXXTEST_DIR "" CACHE STRING "Set CxxTest install directory") set(DRAT2ER_DIR "" CACHE STRING "Set drat2er install directory") set(GLPK_DIR "" CACHE STRING "Set GLPK install directory") set(GMP_DIR "" CACHE STRING "Set GMP install directory") +set(KISSAT_DIR "" CACHE STRING "Set Kissat install directory") set(LFSC_DIR "" CACHE STRING "Set LFSC install directory") set(SYMFPU_DIR "" CACHE STRING "Set SymFPU install directory") @@ -483,6 +488,11 @@ if(USE_GLPK) add_definitions(-DCVC4_USE_GLPK) endif() +if(USE_KISSAT) + find_package(Kissat REQUIRED) + add_definitions(-DCVC4_USE_KISSAT) +endif() + if(USE_LFSC) set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --with-lfsc) find_package(LFSC REQUIRED) @@ -587,9 +597,9 @@ string(REPLACE ";" " " CVC4_DEFINITIONS "${CVC4_DEFINITIONS}") message("CVC4 ${CVC4_RELEASE_STRING}") message("") if(ENABLE_COMP_INC_TRACK) - message("Build profile : ${CVC4_BUILD_PROFILE_STRING} (incremental)") + message("Build profile : ${CVC4_BUILD_PROFILE_STRING} (incremental)") else() - message("Build profile : ${CVC4_BUILD_PROFILE_STRING}") + message("Build profile : ${CVC4_BUILD_PROFILE_STRING}") endif() message("") print_config("GPL :" ENABLE_GPL) @@ -627,55 +637,59 @@ print_config("CaDiCaL :" USE_CADICAL) print_config("CryptoMiniSat :" USE_CRYPTOMINISAT) print_config("drat2er :" USE_DRAT2ER) print_config("GLPK :" USE_GLPK) +print_config("Kissat :" USE_KISSAT) print_config("LFSC :" USE_LFSC) if(CVC4_USE_CLN_IMP) - message("MP library : cln") + message("MP library : cln") else() - message("MP library : gmp") + message("MP library : gmp") endif() print_config("Readline :" ${USE_READLINE}) print_config("SymFPU :" ${USE_SYMFPU}) message("") if(ABC_DIR) - message("ABC dir : ${ABC_DIR}") + message("ABC dir : ${ABC_DIR}") endif() if(ANTLR_DIR) - message("ANTLR dir : ${ANTLR_DIR}") + message("ANTLR dir : ${ANTLR_DIR}") endif() if(CADICAL_DIR) - message("CADICAL dir : ${CADICAL_DIR}") + message("CADICAL dir : ${CADICAL_DIR}") endif() if(CRYPTOMINISAT_DIR) - message("CRYPTOMINISAT dir : ${CRYPTOMINISAT_DIR}") + message("CRYPTOMINISAT dir : ${CRYPTOMINISAT_DIR}") endif() if(DRAT2ER_DIR) - message("DRAT2ER dir : ${DRAT2ER_DIR}") + message("DRAT2ER dir : ${DRAT2ER_DIR}") endif() if(GLPK_DIR) - message("GLPK dir : ${GLPK_DIR}") + message("GLPK dir : ${GLPK_DIR}") endif() if(GMP_DIR) - message("GMP dir : ${GMP_DIR}") + message("GMP dir : ${GMP_DIR}") +endif() +if(KISSAT_DIR) + message("KISSAT dir : ${KISSAT_DIR}") endif() if(LFSC_DIR) - message("LFSC dir : ${LFSC_DIR}") + message("LFSC dir : ${LFSC_DIR}") endif() if(SYMFPU_DIR) - message("SYMFPU dir : ${SYMFPU_DIR}") + message("SYMFPU dir : ${SYMFPU_DIR}") endif() message("") -message("CPPLAGS (-D...) : ${CVC4_DEFINITIONS}") -message("CXXFLAGS : ${CMAKE_CXX_FLAGS}") -message("CFLAGS : ${CMAKE_C_FLAGS}") -message("Linker flags : ${CMAKE_EXE_LINKER_FLAGS}") +message("CPPLAGS (-D...) : ${CVC4_DEFINITIONS}") +message("CXXFLAGS : ${CMAKE_CXX_FLAGS}") +message("CFLAGS : ${CMAKE_C_FLAGS}") +message("Linker flags : ${CMAKE_EXE_LINKER_FLAGS}") message("") -message("Install prefix : ${CMAKE_INSTALL_PREFIX}") +message("Install prefix : ${CMAKE_INSTALL_PREFIX}") message("") if(GPL_LIBS) message( - "CVC4 license : GPLv3 (due to optional libraries; see below)" + "CVC4 license : GPLv3 (due to optional libraries; see below)" "\n" "\n" "Please note that CVC4 will be built against the following GPLed libraries:" @@ -692,7 +706,7 @@ if(GPL_LIBS) ) else() message( - "CVC4 license : modified BSD" + "CVC4 license : modified BSD" "\n" "\n" "Note that this configuration is NOT built against any GPL'ed libraries, so" diff --git a/cmake/FindKissat.cmake b/cmake/FindKissat.cmake new file mode 100644 index 000000000..cc5311ad4 --- /dev/null +++ b/cmake/FindKissat.cmake @@ -0,0 +1,17 @@ +# Find Kissat +# Kissat_FOUND - found Kissat lib +# Kissat_INCLUDE_DIR - the Kissat include directory +# Kissat_LIBRARIES - Libraries needed to use Kissat + +find_path(Kissat_INCLUDE_DIR NAMES kissat/kissat.h) +find_library(Kissat_LIBRARIES NAMES kissat) + +include(FindPackageHandleStandardArgs) +find_package_handle_standard_args(Kissat + DEFAULT_MSG Kissat_INCLUDE_DIR Kissat_LIBRARIES) + +mark_as_advanced(Kissat_INCLUDE_DIR Kissat_LIBRARIES) +if(Kissat_LIBRARIES) + message(STATUS "Found Kissat library: ${Kissat_LIBRARIES}") +endif() + diff --git a/configure.sh b/configure.sh index 070e2c230..21a444082 100755 --- a/configure.sh +++ b/configure.sh @@ -63,6 +63,7 @@ The following flags enable optional packages (disable with --no-<option name>). --cadical use the CaDiCaL SAT solver --cryptominisat use the CryptoMiniSat SAT solver --drat2er use drat2er (required for eager BV proofs) + --kissat use the Kissat SAT solver --lfsc use the LFSC proof checker --symfpu use SymFPU for floating point solver --readline support the readline library @@ -76,6 +77,7 @@ Optional Path to Optional Packages: --cxxtest-dir=PATH path to CxxTest installation --glpk-dir=PATH path to top level of GLPK installation --gmp-dir=PATH path to top level of GMP installation + --kissat-dir=PATH path to top level of Kissat source tree --lfsc-dir=PATH path to top level of LFSC source tree --symfpu-dir=PATH path to top level of SymFPU source tree @@ -110,8 +112,6 @@ buildtype=default abc=default asan=default -ubsan=default -tsan=default assertions=default best=default cadical=default @@ -119,30 +119,33 @@ cln=default comp_inc=default coverage=default cryptominisat=default -debug_symbols=default debug_context_mm=default +debug_symbols=default drat2er=default dumping=default -gpl=default -win64=default -ninja=default glpk=default +gpl=default +kissat=default lfsc=default muzzle=default +ninja=default optimized=default +profiling=default proofs=default +python2=default +python3=default +python_bindings=default +readline=default shared=default static_binary=default statistics=default symfpu=default tracing=default +tsan=default +ubsan=default unit_testing=default -python2=default -python3=default -python_bindings=default valgrind=default -profiling=default -readline=default +win64=default language_bindings_java=default language_bindings_python=default @@ -155,6 +158,7 @@ drat2er_dir=default cxxtest_dir=default glpk_dir=default gmp_dir=default +kissat_dir=default lfsc_dir=default symfpu_dir=default @@ -228,6 +232,9 @@ do --gpl) gpl=ON;; --no-gpl) gpl=OFF;; + --kissat) kissat=ON;; + --no-kissat) kissat=OFF;; + --win64) win64=ON;; --no-win64) win64=OFF;; @@ -325,6 +332,9 @@ do --gmp-dir) die "missing argument to $1 (try -h)" ;; --gmp-dir=*) gmp_dir=${1##*=} ;; + --kissat-dir) die "missing argument to $1 (try -h)" ;; + --kissat-dir=*) kissat_dir=${1##*=} ;; + --lfsc-dir) die "missing argument to $1 (try -h)" ;; --lfsc-dir=*) lfsc_dir=${1##*=} ;; @@ -418,6 +428,8 @@ cmake_opts="" && cmake_opts="$cmake_opts -DUSE_DRAT2ER=$drat2er" [ $glpk != default ] \ && cmake_opts="$cmake_opts -DUSE_GLPK=$glpk" +[ $kissat != default ] \ + && cmake_opts="$cmake_opts -DUSE_KISSAT=$kissat" [ $lfsc != default ] \ && cmake_opts="$cmake_opts -DUSE_LFSC=$lfsc" [ $symfpu != default ] \ @@ -444,6 +456,8 @@ cmake_opts="" && cmake_opts="$cmake_opts -DGLPK_DIR=$glpk_dir" [ "$gmp_dir" != default ] \ && cmake_opts="$cmake_opts -DGMP_DIR=$gmp_dir" +[ "$kissat_dir" != default ] \ + && cmake_opts="$cmake_opts -DKISSAT=$kissat_dir" [ "$lfsc_dir" != default ] \ && cmake_opts="$cmake_opts -DLFSC_DIR=$lfsc_dir" [ "$symfpu_dir" != default ] \ diff --git a/contrib/get-kissat b/contrib/get-kissat new file mode 100755 index 000000000..7b513caef --- /dev/null +++ b/contrib/get-kissat @@ -0,0 +1,26 @@ +#!/usr/bin/env bash + +set -e -o pipefail + +source "$(dirname "$0")/get-script-header.sh" + +KISSAT_DIR="${DEPS_DIR}/kissat" +version="sc2020-039805f2" + +check_dep_dir "${KISSAT_DIR}" + +# Download and build Kissat +setup_dep \ + "http://fmv.jku.at/kissat/kissat-$version.tar.xz" "$KISSAT_DIR" +cd "${KISSAT_DIR}" + +./configure -fPIC --quiet +make -j${NPROC} +install_lib build/libkissat.a +install_includes src/kissat.h kissat + +echo +echo "Using Kissat version $version" +echo +echo ===================== Now configure CVC4 with ===================== +echo ./configure.sh --kissat diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 66a1fee16..ff11897e9 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -190,6 +190,8 @@ libcvc4_add_sources( prop/cnf_stream.h prop/cryptominisat.cpp prop/cryptominisat.h + prop/kissat.cpp + prop/kissat.h prop/minisat/core/Dimacs.h prop/minisat/core/Solver.cc prop/minisat/core/Solver.h @@ -841,6 +843,10 @@ if(USE_CRYPTOMINISAT) target_link_libraries(cvc4 ${CryptoMiniSat_LIBRARIES}) target_include_directories(cvc4 PRIVATE ${CryptoMiniSat_INCLUDE_DIR}) endif() +if(USE_KISSAT) + target_link_libraries(cvc4 ${Kissat_LIBRARIES}) + target_include_directories(cvc4 PRIVATE ${Kissat_INCLUDE_DIR}) +endif() if(USE_DRAT2ER) target_link_libraries(cvc4 ${Drat2Er_LIBRARIES}) target_include_directories(cvc4 PRIVATE ${Drat2Er_INCLUDE_DIR}) diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp index a1fd01c96..5df579b86 100644 --- a/src/base/configuration.cpp +++ b/src/base/configuration.cpp @@ -138,6 +138,7 @@ std::string Configuration::copyright() { if (Configuration::isBuiltWithAbc() || Configuration::isBuiltWithLfsc() || Configuration::isBuiltWithCadical() || Configuration::isBuiltWithCryptominisat() + || Configuration::isBuiltWithKissat() || Configuration::isBuiltWithSymFPU()) { ss << "This version of CVC4 is linked against the following non-(L)GPL'ed\n" @@ -164,6 +165,12 @@ std::string Configuration::copyright() { << " See https://github.com/msoos/cryptominisat for copyright " << "information.\n\n"; } + if (Configuration::isBuiltWithKissat()) + { + ss << " Kissat - Simplified Satisfiability Solver\n" + << " See https://fmv.jku.at/kissat for copyright " + << "information.\n\n"; + } if (Configuration::isBuiltWithSymFPU()) { ss << " SymFPU - The Symbolic Floating Point Unit\n" @@ -250,6 +257,8 @@ bool Configuration::isBuiltWithCryptominisat() { return IS_CRYPTOMINISAT_BUILD; } +bool Configuration::isBuiltWithKissat() { return IS_KISSAT_BUILD; } + bool Configuration::isBuiltWithDrat2Er() { return IS_DRAT2ER_BUILD; } bool Configuration::isBuiltWithReadline() { diff --git a/src/base/configuration.h b/src/base/configuration.h index 72ccb2301..7de4a337b 100644 --- a/src/base/configuration.h +++ b/src/base/configuration.h @@ -99,6 +99,8 @@ public: static bool isBuiltWithCryptominisat(); + static bool isBuiltWithKissat(); + static bool isBuiltWithDrat2Er(); static bool isBuiltWithReadline(); diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h index 77db0b51c..e77752420 100644 --- a/src/base/configuration_private.h +++ b/src/base/configuration_private.h @@ -126,6 +126,12 @@ namespace CVC4 { # define IS_DRAT2ER_BUILD false #endif /* CVC4_USE_DRAT2ER */ +#if CVC4_USE_KISSAT +#define IS_KISSAT_BUILD true +#else /* CVC4_USE_KISSAT */ +#define IS_KISSAT_BUILD false +#endif /* CVC4_USE_KISSAT */ + #if CVC4_USE_LFSC #define IS_LFSC_BUILD true #else /* CVC4_USE_LFSC */ diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index 05dc6b716..5c8cd8f58 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -56,6 +56,8 @@ header = "options/bv_options.h" name = "cryptominisat" [[option.mode.CADICAL]] name = "cadical" +[[option.mode.KISSAT]] + name = "kissat" [[option]] name = "bitblastMode" diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 9253ea1c8..af811e085 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -51,6 +51,10 @@ void throwLazyBBUnsupported(options::SatSolverMode m) { sat_solver = "CaDiCaL"; } + else if (m == options::SatSolverMode::KISSAT) + { + sat_solver = "Kissat"; + } else { Assert(m == options::SatSolverMode::CRYPTOMINISAT); @@ -166,7 +170,17 @@ void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m) throw OptionException(ss.str()); } - if (m == SatSolverMode::CRYPTOMINISAT || m == SatSolverMode::CADICAL) + if (m == SatSolverMode::KISSAT && !Configuration::isBuiltWithKissat()) + { + std::stringstream ss; + ss << "option `" << option + << "' requires a Kissat build of CVC4; this binary was not built with " + "Kissat support"; + throw OptionException(ss.str()); + } + + if (m == SatSolverMode::CRYPTOMINISAT || m == SatSolverMode::CADICAL + || m == SatSolverMode::KISSAT) { if (options::bitblastMode() == options::BitblastMode::LAZY && options::bitblastMode.wasSetByUser()) @@ -443,6 +457,7 @@ void OptionsHandler::showConfiguration(std::string option) { print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat()); print_config_cond("drat2er", Configuration::isBuiltWithDrat2Er()); print_config_cond("gmp", Configuration::isBuiltWithGmp()); + print_config_cond("kissat", Configuration::isBuiltWithKissat()); print_config_cond("lfsc", Configuration::isBuiltWithLfsc()); print_config_cond("readline", Configuration::isBuiltWithReadline()); print_config_cond("symfpu", Configuration::isBuiltWithSymFPU()); diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 396b2c8ea..283558709 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -140,10 +140,11 @@ public: template<class T> void OptionsHandler::checkSatSolverEnabled(std::string option, T m) { -#if !defined(CVC4_USE_CRYPTOMINISAT) && !defined(CVC4_USE_CADICAL) +#if !defined(CVC4_USE_CRYPTOMINISAT) && !defined(CVC4_USE_CADICAL) \ + && !defined(CVC4_USE_KISSAT) std::stringstream ss; ss << "option `" << option - << "' requires CVC4 to be built with CryptoMiniSat or CaDiCaL"; + << "' requires CVC4 to be built with CryptoMiniSat or CaDiCaL or Kissat"; throw OptionException(ss.str()); #endif } diff --git a/src/prop/kissat.cpp b/src/prop/kissat.cpp new file mode 100644 index 000000000..0440fcd4e --- /dev/null +++ b/src/prop/kissat.cpp @@ -0,0 +1,179 @@ +/********************* */ +/*! \file kissat.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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 Kissat SAT Solver. + ** + ** Wrapper for the Kissat SAT solver (for theory of bit-vectors). + **/ + +#include "prop/kissat.h" + +#ifdef CVC4_USE_KISSAT + +#include "base/check.h" +#include "proof/sat_proof.h" + +namespace CVC4 { +namespace prop { + +using KissatLit = int32_t; +using KissatVar = int32_t; + +// helper functions +namespace { + +SatValue toSatValue(int32_t result) +{ + if (result == 10) return SAT_VALUE_TRUE; + if (result == 20) return SAT_VALUE_FALSE; + Assert(result == 0); + return SAT_VALUE_UNKNOWN; +} + +/** + * Helper to convert the value of a literal as returned by Kissat to the + * corresponding true/false SAT_VALUE. + * Note: Kissat returns lit/-lit for true/false. Older versions returned 1/-1. + */ +SatValue toSatValueLit(int value) +{ + if (value > 0) return SAT_VALUE_TRUE; + Assert(value < 0); + return SAT_VALUE_FALSE; +} + +/** Helper to convert SatLiteral to KissatLit. */ +KissatLit toKissatLit(const SatLiteral lit) +{ + return lit.isNegated() ? -lit.getSatVariable() : lit.getSatVariable(); +} + +/** Helper to convert a SatVariable to a KissatVar. */ +KissatVar toKissatVar(SatVariable var) { return var; } + +} // namespace + +KissatSolver::KissatSolver(StatisticsRegistry* registry, + const std::string& name) + : d_solver(kissat_init()), + // Note: Kissat 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) +{ +} + +void KissatSolver::init() +{ + d_true = newVar(); + d_false = newVar(); + kissat_add(d_solver, toKissatVar(d_true)); + kissat_add(d_solver, 0); + kissat_add(d_solver, -toKissatVar(d_false)); + kissat_add(d_solver, 0); +} + +KissatSolver::~KissatSolver() { kissat_release(d_solver); } + +ClauseId KissatSolver::addClause(SatClause& clause, bool removable) +{ + for (const SatLiteral& lit : clause) + { + kissat_add(d_solver, toKissatLit(lit)); + } + kissat_add(d_solver, 0); + ++d_statistics.d_numClauses; + return ClauseIdError; +} + +ClauseId KissatSolver::addXorClause(SatClause& clause, bool rhs, bool removable) +{ + Unreachable() << "Kissat does not support adding XOR clauses."; +} + +SatVariable KissatSolver::newVar(bool isTheoryAtom, + bool preRegister, + bool canErase) +{ + ++d_statistics.d_numVariables; + return d_nextVarIdx++; +} + +SatVariable KissatSolver::trueVar() { return d_true; } + +SatVariable KissatSolver::falseVar() { return d_false; } + +SatValue KissatSolver::solve() +{ + TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime); + SatValue res = toSatValue(kissat_solve(d_solver)); + d_okay = (res == SAT_VALUE_TRUE); + ++d_statistics.d_numSatCalls; + return res; +} + +SatValue KissatSolver::solve(long unsigned int&) +{ + Unimplemented() << "Setting limits for Kissat not supported yet"; +}; + +SatValue KissatSolver::solve(const std::vector<SatLiteral>& assumptions) +{ + Unimplemented() << "Incremental solving with Kissat not supported yet"; +} + +void KissatSolver::interrupt() { kissat_terminate(d_solver); } + +SatValue KissatSolver::value(SatLiteral l) +{ + Assert(d_okay); + return toSatValueLit(kissat_value(d_solver, toKissatLit(l))); +} + +SatValue KissatSolver::modelValue(SatLiteral l) +{ + Assert(d_okay); + return value(l); +} + +unsigned KissatSolver::getAssertionLevel() const +{ + Unreachable() << "Kissat does not support assertion levels."; +} + +bool KissatSolver::ok() const { return d_okay; } + +KissatSolver::Statistics::Statistics(StatisticsRegistry* registry, + const std::string& prefix) + : d_registry(registry), + d_numSatCalls("theory::bv::" + prefix + "::Kissat::calls_to_solve", 0), + d_numVariables("theory::bv::" + prefix + "::Kissat::variables", 0), + d_numClauses("theory::bv::" + prefix + "::Kissat::clauses", 0), + d_solveTime("theory::bv::" + prefix + "::Kissat::solve_time") +{ + d_registry->registerStat(&d_numSatCalls); + d_registry->registerStat(&d_numVariables); + d_registry->registerStat(&d_numClauses); + d_registry->registerStat(&d_solveTime); +} + +KissatSolver::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_KISSAT diff --git a/src/prop/kissat.h b/src/prop/kissat.h new file mode 100644 index 000000000..35b33daeb --- /dev/null +++ b/src/prop/kissat.h @@ -0,0 +1,102 @@ +/********************* */ +/*! \file kissat.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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 Kissat SAT Solver. + ** + ** Wrapper for the Kissat SAT solver (for theory of bit-vectors). + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__PROP__KISSAT_H +#define CVC4__PROP__KISSAT_H + +#ifdef CVC4_USE_KISSAT + +#include "prop/sat_solver.h" + +extern "C" { +#include <kissat/kissat.h> +} + +namespace CVC4 { +namespace prop { + +class KissatSolver : public SatSolver +{ + friend class SatSolverFactory; + + public: + ~KissatSolver() 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; + SatValue solve(const std::vector<SatLiteral>& assumptions) override; + + void interrupt() override; + + SatValue value(SatLiteral l) override; + + SatValue modelValue(SatLiteral l) override; + + unsigned getAssertionLevel() const override; + + bool ok() const override; + + private: + 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(); + }; + + /** + * Private to disallow creation outside of SatSolverFactory. + * Function init() must be called after creation. + */ + KissatSolver(StatisticsRegistry* registry, const std::string& name = ""); + /** + * Initialize SAT solver instance. + * Note: Split out to not call virtual functions in constructor. + */ + void init(); + + kissat* d_solver; + + unsigned d_nextVarIdx; + bool d_okay; + SatVariable d_true; + SatVariable d_false; + + Statistics d_statistics; +}; + +} // namespace prop +} // namespace CVC4 + +#endif // CVC4_USE_KISSAT +#endif // CVC4__PROP__KISSAT_H diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp index 460ab3ece..8f18a6055 100644 --- a/src/prop/sat_solver_factory.cpp +++ b/src/prop/sat_solver_factory.cpp @@ -19,6 +19,7 @@ #include "prop/bvminisat/bvminisat.h" #include "prop/cadical.h" #include "prop/cryptominisat.h" +#include "prop/kissat.h" #include "prop/minisat/minisat.h" namespace CVC4 { @@ -58,5 +59,17 @@ SatSolver* SatSolverFactory::createCadical(StatisticsRegistry* registry, #endif } +SatSolver* SatSolverFactory::createKissat(StatisticsRegistry* registry, + const std::string& name) +{ +#ifdef CVC4_USE_KISSAT + KissatSolver* res = new KissatSolver(registry, name); + res->init(); + return res; +#else + Unreachable() << "CVC4 was not compiled with Kissat support."; +#endif +} + } // namespace prop } // namespace CVC4 diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h index 5f8649768..04b5d73a6 100644 --- a/src/prop/sat_solver_factory.h +++ b/src/prop/sat_solver_factory.h @@ -45,6 +45,8 @@ class SatSolverFactory static SatSolver* createCadical(StatisticsRegistry* registry, const std::string& name = ""); + static SatSolver* createKissat(StatisticsRegistry* registry, + const std::string& name = ""); }; /* class SatSolverFactory */ } // namespace prop diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp index ea9867b0f..295090699 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.cpp +++ b/src/theory/bv/bitblast/aig_bitblaster.cpp @@ -164,6 +164,10 @@ AigBitblaster::AigBitblaster() solver = prop::SatSolverFactory::createCryptoMinisat( smtStatisticsRegistry(), "AigBitblaster"); break; + case options::SatSolverMode::KISSAT: + solver = prop::SatSolverFactory::createKissat(smtStatisticsRegistry(), + "AigBitblaster"); + break; default: CVC4_FATAL() << "Unknown SAT solver type"; } d_satSolver.reset(solver); diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index bddde4cb7..0ba69c8b8 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -60,6 +60,10 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c) solver = prop::SatSolverFactory::createCryptoMinisat( smtStatisticsRegistry(), "EagerBitblaster"); break; + case options::SatSolverMode::KISSAT: + solver = prop::SatSolverFactory::createKissat(smtStatisticsRegistry(), + "EagerBitblaster"); + break; default: Unreachable() << "Unknown SAT solver type"; } d_satSolver.reset(solver); |