GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/minisat/minisat.h Lines: 2 4 50.0 %
Date: 2021-03-23 Branches: 0 6 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file minisat.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mathias Preiner, Haniel Barbosa, Liana Hadarean
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 minisat interface for cvc4.
15
 **/
16
17
#pragma once
18
19
#include "prop/sat_solver.h"
20
#include "prop/minisat/simp/SimpSolver.h"
21
#include "util/statistics_registry.h"
22
23
namespace CVC4 {
24
namespace prop {
25
26
class MinisatSatSolver : public CDCLTSatSolverInterface
27
{
28
 public:
29
  MinisatSatSolver(StatisticsRegistry* registry);
30
  ~MinisatSatSolver() override;
31
32
  static SatVariable     toSatVariable(Minisat::Var var);
33
  static Minisat::Lit    toMinisatLit(SatLiteral lit);
34
  static SatLiteral      toSatLiteral(Minisat::Lit lit);
35
  static SatValue        toSatLiteralValue(Minisat::lbool res);
36
  static Minisat::lbool  toMinisatlbool(SatValue val);
37
  //(Commented because not in use) static bool            tobool(SatValue val);
38
39
  static void  toMinisatClause(SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause);
40
  static void  toSatClause    (const Minisat::Clause& clause, SatClause& sat_clause);
41
  void initialize(context::Context* context,
42
                  TheoryProxy* theoryProxy,
43
                  CVC4::context::UserContext* userContext,
44
                  ProofNodeManager* pnm) override;
45
46
  ClauseId addClause(SatClause& clause, bool removable) override;
47
  ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override
48
  {
49
    Unreachable() << "Minisat does not support native XOR reasoning";
50
  }
51
52
  SatVariable newVar(bool isTheoryAtom,
53
                     bool preRegister,
54
                     bool canErase) override;
55
9029
  SatVariable trueVar() override { return d_minisat->trueVar(); }
56
9029
  SatVariable falseVar() override { return d_minisat->falseVar(); }
57
58
  SatValue solve() override;
59
  SatValue solve(long unsigned int&) override;
60
61
  bool ok() const override;
62
63
  void interrupt() override;
64
65
  SatValue value(SatLiteral l) override;
66
67
  SatValue modelValue(SatLiteral l) override;
68
69
  bool properExplanation(SatLiteral lit, SatLiteral expl) const override;
70
71
  /** Incremental interface */
72
73
  unsigned getAssertionLevel() const override;
74
75
  void push() override;
76
77
  void pop() override;
78
79
  void resetTrail() override;
80
81
  void requirePhase(SatLiteral lit) override;
82
83
  bool isDecision(SatVariable decn) const override;
84
85
  /** Retrieve a pointer to the unerlying solver. */
86
  Minisat::SimpSolver* getSolver() { return d_minisat; }
87
88
  /** Retrieve the proof manager of this SAT solver. */
89
  SatProofManager* getProofManager();
90
91
  /** Retrieve the refutation proof of this SAT solver. */
92
  std::shared_ptr<ProofNode> getProof() override;
93
94
 private:
95
96
  /** The SatSolver used */
97
  Minisat::SimpSolver* d_minisat;
98
99
  /** Context we will be using to synchronize the sat solver */
100
  context::Context* d_context;
101
102
  void setupOptions();
103
104
  class Statistics {
105
  private:
106
    StatisticsRegistry* d_registry;
107
    ReferenceStat<uint64_t> d_statStarts, d_statDecisions;
108
    ReferenceStat<uint64_t> d_statRndDecisions, d_statPropagations;
109
    ReferenceStat<uint64_t> d_statConflicts, d_statClausesLiterals;
110
    ReferenceStat<uint64_t> d_statLearntsLiterals,  d_statMaxLiterals;
111
    ReferenceStat<uint64_t> d_statTotLiterals;
112
  public:
113
    Statistics(StatisticsRegistry* registry);
114
    ~Statistics();
115
    void init(Minisat::SimpSolver* d_minisat);
116
  };/* class MinisatSatSolver::Statistics */
117
  Statistics d_statistics;
118
119
}; /* class MinisatSatSolver */
120
121
}/* CVC4::prop namespace */
122
}/* CVC4 namespace */