GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/bvminisat/bvminisat.h Lines: 12 14 85.7 %
Date: 2021-03-23 Branches: 0 6 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bvminisat.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mathias Preiner, Liana Hadarean, Tim King
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 for cvc4 (bitvectors).
15
 **/
16
17
#include "cvc4_private.h"
18
19
#pragma once
20
21
#include <memory>
22
23
#include "context/cdo.h"
24
#include "prop/bv_sat_solver_notify.h"
25
#include "prop/bvminisat/simp/SimpSolver.h"
26
#include "prop/sat_solver.h"
27
#include "util/resource_manager.h"
28
#include "util/statistics_registry.h"
29
#include "util/stats_timer.h"
30
31
namespace CVC4 {
32
namespace prop {
33
34
class BVMinisatSatSolver : public BVSatSolverInterface,
35
                           public context::ContextNotifyObj
36
{
37
 private:
38
17948
  class MinisatNotify : public BVMinisat::Notify
39
  {
40
    BVSatSolverNotify* d_notify;
41
42
   public:
43
8977
    MinisatNotify(BVSatSolverNotify* notify) : d_notify(notify) {}
44
1844162
    bool notify(BVMinisat::Lit lit) override
45
    {
46
1844162
      return d_notify->notify(toSatLiteral(lit));
47
    }
48
    void notify(BVMinisat::vec<BVMinisat::Lit>& clause) override;
49
1610
    void spendResource(ResourceManager::Resource r) override
50
    {
51
1610
      d_notify->spendResource(r);
52
1610
    }
53
21015735
    void safePoint(ResourceManager::Resource r) override
54
    {
55
21015735
      d_notify->safePoint(r);
56
21015735
    }
57
  };
58
59
  std::unique_ptr<BVMinisat::SimpSolver> d_minisat;
60
  std::unique_ptr<MinisatNotify> d_minisatNotify;
61
62
  unsigned d_assertionsCount;
63
  context::CDO<unsigned> d_assertionsRealCount;
64
  context::CDO<unsigned> d_lastPropagation;
65
66
protected:
67
 void contextNotifyPop() override;
68
69
public:
70
71
  BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name = "");
72
  virtual ~BVMinisatSatSolver();
73
74
  void setNotify(BVSatSolverNotify* notify) override;
75
76
  ClauseId addClause(SatClause& clause, bool removable) override;
77
78
  ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override
79
  {
80
    Unreachable() << "Minisat does not support native XOR reasoning";
81
    return ClauseIdError;
82
  }
83
84
  SatValue propagate() override;
85
86
  SatVariable newVar(bool isTheoryAtom = false,
87
                     bool preRegister = false,
88
                     bool canErase = true) override;
89
90
131
  SatVariable trueVar() override { return d_minisat->trueVar(); }
91
224
  SatVariable falseVar() override { return d_minisat->falseVar(); }
92
93
  void markUnremovable(SatLiteral lit) override;
94
95
  void interrupt() override;
96
97
  SatValue solve() override;
98
  SatValue solve(long unsigned int&) override;
99
  bool ok() const override;
100
  void getUnsatCore(SatClause& unsatCore) override;
101
102
  SatValue value(SatLiteral l) override;
103
  SatValue modelValue(SatLiteral l) override;
104
105
  void unregisterVar(SatLiteral lit);
106
  void renewVar(SatLiteral lit, int level = -1);
107
  unsigned getAssertionLevel() const override;
108
109
  // helper methods for converting from the internal Minisat representation
110
111
  static SatVariable     toSatVariable(BVMinisat::Var var);
112
  static BVMinisat::Lit    toMinisatLit(SatLiteral lit);
113
  static SatLiteral      toSatLiteral(BVMinisat::Lit lit);
114
  static SatValue toSatLiteralValue(BVMinisat::lbool res);
115
116
  static void  toMinisatClause(SatClause& clause, BVMinisat::vec<BVMinisat::Lit>& minisat_clause);
117
  static void  toSatClause    (const BVMinisat::Clause& clause, SatClause& sat_clause);
118
  void addMarkerLiteral(SatLiteral lit) override;
119
120
  void explain(SatLiteral lit, std::vector<SatLiteral>& explanation) override;
121
122
  SatValue assertAssumption(SatLiteral lit, bool propagate) override;
123
124
  void popAssumption() override;
125
126
 private:
127
  /* Disable the default constructor. */
128
  BVMinisatSatSolver() = delete;
129
130
  class Statistics {
131
  public:
132
    StatisticsRegistry* d_registry;
133
    ReferenceStat<uint64_t> d_statStarts, d_statDecisions;
134
    ReferenceStat<uint64_t> d_statRndDecisions, d_statPropagations;
135
    ReferenceStat<uint64_t> d_statConflicts, d_statClausesLiterals;
136
    ReferenceStat<uint64_t> d_statLearntsLiterals,  d_statMaxLiterals;
137
    ReferenceStat<uint64_t> d_statTotLiterals;
138
    ReferenceStat<int> d_statEliminatedVars;
139
    IntStat d_statCallsToSolve;
140
    TimerStat d_statSolveTime;
141
    bool d_registerStats;
142
    Statistics(StatisticsRegistry* registry, const std::string& prefix);
143
    ~Statistics();
144
    void init(BVMinisat::SimpSolver* minisat);
145
  };
146
147
  Statistics d_statistics;
148
};
149
150
} /* CVC4::prop namespace */
151
} /* CVC4 namespace */