Update copyright headers.

[cvc5.git] / src / prop / sat_solver_factory.cpp

diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index 092ec72f2234a9942592e2949448eb3a97a88fde..cfdbc8b048978be905825f2a919734c8568d9fe9 100644 (file)
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -2,10 +2,10 @@
 /*! \file sat_solver_factory.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Tim King, Morgan Deters
+ **   Mathias Preiner, Aina Niemetz, Dejan Jovanovic
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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
  **
@@ -16,19 +16,64 @@
 
 #include "prop/sat_solver_factory.h"
 
-#include "prop/minisat/minisat.h"
 #include "prop/bvminisat/bvminisat.h"
+#include "prop/cadical.h"
+#include "prop/cryptominisat.h"
+#include "prop/kissat.h"
+#include "prop/minisat/minisat.h"
 
 namespace CVC4 {
 namespace prop {
 
-BVSatSolverInterface* SatSolverFactory::createMinisat(context::Context* mainSatContext, StatisticsRegistry* registry, const std::string& name) {
+BVSatSolverInterface* SatSolverFactory::createMinisat(
+    context::Context* mainSatContext,
+    StatisticsRegistry* registry,
+    const std::string& name)
+{
   return new BVMinisatSatSolver(registry, mainSatContext, name);
 }
 
-DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat(StatisticsRegistry* registry) {
+DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat(
+    StatisticsRegistry* registry)
+{
   return new MinisatSatSolver(registry);
 }
 
-} /* CVC4::prop namespace */
-} /* CVC4 namespace */
+SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry* registry,
+                                                 const std::string& name)
+{
+#ifdef CVC4_USE_CRYPTOMINISAT
+  CryptoMinisatSolver* res = new CryptoMinisatSolver(registry, name);
+  res->init();
+  return res;
+#else
+  Unreachable() << "CVC4 was not compiled with Cryptominisat support.";
+#endif
+}
+
+SatSolver* SatSolverFactory::createCadical(StatisticsRegistry* registry,
+                                           const std::string& name)
+{
+#ifdef CVC4_USE_CADICAL
+  CadicalSolver* res = new CadicalSolver(registry, name);
+  res->init();
+  return res;
+#else
+  Unreachable() << "CVC4 was not compiled with CaDiCaL support.";
+#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