Add support for SAT solver Kissat. (#4514)

4 files changed, 296 insertions, 0 deletions

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