src/prop/sat_solver_factory.h

   1 /*********************                                                        */
   2 /*! \file sat_solver_factory.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Mathias Preiner, Liana Hadarean, 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 SAT Solver.
  13  **
  14  ** SAT Solver creation facility
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef CVC4__PROP__SAT_SOLVER_FACTORY_H
  20 #define CVC4__PROP__SAT_SOLVER_FACTORY_H
  21
  22 #include <string>
  23 #include <vector>
  24
  25 #include "context/context.h"
  26 #include "prop/minisat/minisat.h"
  27 #include "prop/sat_solver.h"
  28 #include "util/statistics_registry.h"
  29
  30 namespace CVC4 {
  31 namespace prop {
  32
  33 class SatSolverFactory
  34 {
  35  public:
  36   static BVSatSolverInterface* createMinisat(context::Context* mainSatContext,
  37                                              StatisticsRegistry* registry,
  38                                              const std::string& name = "");
  39
  40   static MinisatSatSolver* createCDCLTMinisat(StatisticsRegistry* registry);
  41
  42   static SatSolver* createCryptoMinisat(StatisticsRegistry* registry,
  43                                         const std::string& name = "");
  44
  45   static SatSolver* createCadical(StatisticsRegistry* registry,
  46                                   const std::string& name = "");
  47
  48   static SatSolver* createKissat(StatisticsRegistry* registry,
  49                                  const std::string& name = "");
  50 }; /* class SatSolverFactory */
  51
  52 }  // namespace prop
  53 }  // namespace CVC4
  54
  55 #endif  // CVC4__PROP__SAT_SOLVER_FACTORY_H