summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CMakeLists.txt56
-rw-r--r--cmake/FindKissat.cmake17
-rwxr-xr-xconfigure.sh36
-rwxr-xr-xcontrib/get-kissat26
-rw-r--r--src/CMakeLists.txt6
-rw-r--r--src/base/configuration.cpp9
-rw-r--r--src/base/configuration.h2
-rw-r--r--src/base/configuration_private.h6
-rw-r--r--src/options/bv_options.toml2
-rw-r--r--src/options/options_handler.cpp17
-rw-r--r--src/options/options_handler.h5
-rw-r--r--src/prop/kissat.cpp179
-rw-r--r--src/prop/kissat.h102
-rw-r--r--src/prop/sat_solver_factory.cpp13
-rw-r--r--src/prop/sat_solver_factory.h2
-rw-r--r--src/theory/bv/bitblast/aig_bitblaster.cpp4
-rw-r--r--src/theory/bv/bitblast/eager_bitblaster.cpp4
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback