src/prop/sat_solver_factory.cpp

   1 /*********************                                                        */
   2 /*! \file sat_solver_factory.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Mathias Preiner, Liana Hadarean, Dejan Jovanovic
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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 creation facility.
  13  **
  14  ** SAT Solver.
  15  **/
  16
  17 #include "prop/sat_solver_factory.h"
  18
  19 #include "prop/bvminisat/bvminisat.h"
  20 #include "prop/cadical.h"
  21 #include "prop/cryptominisat.h"
  22 #include "prop/minisat/minisat.h"
  23
  24 namespace CVC4 {
  25 namespace prop {
  26
  27 BVSatSolverInterface* SatSolverFactory::createMinisat(
  28     context::Context* mainSatContext,
  29     StatisticsRegistry* registry,
  30     const std::string& name)
  31 {
  32   return new BVMinisatSatSolver(registry, mainSatContext, name);
  33 }
  34
  35 DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat(
  36     StatisticsRegistry* registry)
  37 {
  38   return new MinisatSatSolver(registry);
  39 }
  40
  41 SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry* registry,
  42                                                  const std::string& name)
  43 {
  44 #ifdef CVC4_USE_CRYPTOMINISAT
  45   return new CryptoMinisatSolver(registry, name);
  46 #else
  47   Unreachable() << "CVC4 was not compiled with Cryptominisat support.";
  48 #endif
  49 }
  50
  51 SatSolver* SatSolverFactory::createCadical(StatisticsRegistry* registry,
  52                                            const std::string& name)
  53 {
  54 #ifdef CVC4_USE_CADICAL
  55   return new CadicalSolver(registry, name);
  56 #else
  57   Unreachable() << "CVC4 was not compiled with CaDiCaL support.";
  58 #endif
  59 }
  60
  61 }  // namespace prop
  62 }  // namespace CVC4