GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/cryptominisat.h Lines: 0 1 0.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file cryptominisat.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-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.
13
 **
14
 ** Implementation of the cryptominisat sat solver for cvc4 (bitvectors).
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__PROP__CRYPTOMINISAT_H
20
#define CVC4__PROP__CRYPTOMINISAT_H
21
22
#ifdef CVC4_USE_CRYPTOMINISAT
23
24
#include "prop/sat_solver.h"
25
#include "util/stats_timer.h"
26
27
// Cryptominisat has name clashes with the other Minisat implementations since
28
// the Minisat implementations export var_Undef, l_True, ... as macro whereas
29
// Cryptominisat uses static const. In order to avoid these conflicts we
30
// forward declare CMSat::SATSolver and include the cryptominisat header only
31
// in cryptominisat.cpp.
32
namespace CMSat {
33
  class SATSolver;
34
}
35
36
namespace CVC4 {
37
namespace prop {
38
39
class CryptoMinisatSolver : public SatSolver
40
{
41
  friend class SatSolverFactory;
42
43
 public:
44
  ~CryptoMinisatSolver() override;
45
46
  ClauseId addClause(SatClause& clause, bool removable) override;
47
  ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override;
48
49
  bool nativeXor() override { return true; }
50
51
  SatVariable newVar(bool isTheoryAtom = false,
52
                     bool preRegister = false,
53
                     bool canErase = true) override;
54
55
  SatVariable trueVar() override;
56
  SatVariable falseVar() override;
57
58
  void markUnremovable(SatLiteral lit);
59
60
  void interrupt() override;
61
62
  SatValue solve() override;
63
  SatValue solve(long unsigned int&) override;
64
  SatValue solve(const std::vector<SatLiteral>& assumptions) override;
65
  void getUnsatAssumptions(std::vector<SatLiteral>& assumptions) override;
66
67
  bool ok() const override;
68
  SatValue value(SatLiteral l) override;
69
  SatValue modelValue(SatLiteral l) override;
70
71
  unsigned getAssertionLevel() const override;
72
73
 private:
74
  class Statistics
75
  {
76
   public:
77
    StatisticsRegistry* d_registry;
78
    IntStat d_statCallsToSolve;
79
    IntStat d_xorClausesAdded;
80
    IntStat d_clausesAdded;
81
    TimerStat d_solveTime;
82
    bool d_registerStats;
83
    Statistics(StatisticsRegistry* registry, const std::string& prefix);
84
    ~Statistics();
85
  };
86
87
  /**
88
   * Private to disallow creation outside of SatSolverFactory.
89
   * Function init() must be called after creation.
90
   */
91
  CryptoMinisatSolver(StatisticsRegistry* registry,
92
                      const std::string& name = "");
93
  /**
94
   * Initialize SAT solver instance.
95
   * Note: Split out to not call virtual functions in constructor.
96
   */
97
  void init();
98
99
  std::unique_ptr<CMSat::SATSolver> d_solver;
100
  unsigned d_numVariables;
101
  bool d_okay;
102
  SatVariable d_true;
103
  SatVariable d_false;
104
105
  Statistics d_statistics;
106
};
107
108
}  // namespace prop
109
}  // namespace CVC4
110
111
#endif  // CVC4_USE_CRYPTOMINISAT
112
#endif  // CVC4__PROP__CRYPTOMINISAT_H