GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/sat_solver_factory.cpp Lines: 13 15 86.7 %
Date: 2021-03-22 Branches: 6 20 30.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sat_solver_factory.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mathias Preiner, Aina Niemetz, Dejan Jovanovic
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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/kissat.h"
23
#include "prop/minisat/minisat.h"
24
25
namespace CVC4 {
26
namespace prop {
27
28
8975
BVSatSolverInterface* SatSolverFactory::createMinisat(
29
    context::Context* mainSatContext,
30
    StatisticsRegistry* registry,
31
    const std::string& name)
32
{
33
8975
  return new BVMinisatSatSolver(registry, mainSatContext, name);
34
}
35
36
9027
MinisatSatSolver* SatSolverFactory::createCDCLTMinisat(
37
    StatisticsRegistry* registry)
38
{
39
9027
  return new MinisatSatSolver(registry);
40
}
41
42
7
SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry* registry,
43
                                                 const std::string& name)
44
{
45
#ifdef CVC4_USE_CRYPTOMINISAT
46
7
  CryptoMinisatSolver* res = new CryptoMinisatSolver(registry, name);
47
7
  res->init();
48
7
  return res;
49
#else
50
  Unreachable() << "CVC4 was not compiled with Cryptominisat support.";
51
#endif
52
}
53
54
3
SatSolver* SatSolverFactory::createCadical(StatisticsRegistry* registry,
55
                                           const std::string& name)
56
{
57
#ifdef CVC4_USE_CADICAL
58
3
  CadicalSolver* res = new CadicalSolver(registry, name);
59
3
  res->init();
60
3
  return res;
61
#else
62
  Unreachable() << "CVC4 was not compiled with CaDiCaL support.";
63
#endif
64
}
65
66
SatSolver* SatSolverFactory::createKissat(StatisticsRegistry* registry,
67
                                          const std::string& name)
68
{
69
#ifdef CVC4_USE_KISSAT
70
  KissatSolver* res = new KissatSolver(registry, name);
71
  res->init();
72
  return res;
73
#else
74
  Unreachable() << "CVC4 was not compiled with Kissat support.";
75
#endif
76
}
77
78
}  // namespace prop
79
26676
}  // namespace CVC4