Add support for SAT solver Kissat. (#4514)

13 files changed, 348 insertions, 3 deletions

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);