src/prop/kissat.h

   1 /*********************                                                        */
   2 /*! \file kissat.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Aina Niemetz
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Wrapper for Kissat SAT Solver.
  13  **
  14  ** Wrapper for the Kissat SAT solver (for theory of bit-vectors).
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef CVC4__PROP__KISSAT_H
  20 #define CVC4__PROP__KISSAT_H
  21
  22 #ifdef CVC4_USE_KISSAT
  23
  24 #include "prop/sat_solver.h"
  25
  26 extern "C" {
  27 #include <kissat/kissat.h>
  28 }
  29
  30 namespace CVC4 {
  31 namespace prop {
  32
  33 class KissatSolver : public SatSolver
  34 {
  35   friend class SatSolverFactory;
  36
  37  public:
  38   ~KissatSolver() override;
  39
  40   ClauseId addClause(SatClause& clause, bool removable) override;
  41
  42   ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override;
  43
  44   SatVariable newVar(bool isTheoryAtom = false,
  45                      bool preRegister = false,
  46                      bool canErase = true) override;
  47
  48   SatVariable trueVar() override;
  49   SatVariable falseVar() override;
  50
  51   SatValue solve() override;
  52   SatValue solve(long unsigned int&) override;
  53   SatValue solve(const std::vector<SatLiteral>& assumptions) override;
  54
  55   void interrupt() override;
  56
  57   SatValue value(SatLiteral l) override;
  58
  59   SatValue modelValue(SatLiteral l) override;
  60
  61   unsigned getAssertionLevel() const override;
  62
  63   bool ok() const override;
  64
  65  private:
  66   struct Statistics
  67   {
  68     StatisticsRegistry* d_registry;
  69     IntStat d_numSatCalls;
  70     IntStat d_numVariables;
  71     IntStat d_numClauses;
  72     TimerStat d_solveTime;
  73     Statistics(StatisticsRegistry* registry, const std::string& prefix);
  74     ~Statistics();
  75   };
  76
  77   /**
  78    * Private to disallow creation outside of SatSolverFactory.
  79    * Function init() must be called after creation.
  80    */
  81   KissatSolver(StatisticsRegistry* registry, const std::string& name = "");
  82   /**
  83    * Initialize SAT solver instance.
  84    * Note: Split out to not call virtual functions in constructor.
  85    */
  86   void init();
  87
  88   kissat* d_solver;
  89
  90   unsigned d_nextVarIdx;
  91   bool d_okay;
  92   SatVariable d_true;
  93   SatVariable d_false;
  94
  95   Statistics d_statistics;
  96 };
  97
  98 }  // namespace prop
  99 }  // namespace CVC4
 100
 101 #endif  // CVC4_USE_KISSAT
 102 #endif  // CVC4__PROP__KISSAT_H