GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/bvminisat/bvminisat.cpp Lines: 130 175 74.3 %
Date: 2021-03-22 Branches: 94 282 33.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bvminisat.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, Dejan Jovanovic, 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 "prop/bvminisat/bvminisat.h"
18
19
#include "prop/bvminisat/simp/SimpSolver.h"
20
#include "proof/clause_id.h"
21
#include "util/statistics_registry.h"
22
23
namespace CVC4 {
24
namespace prop {
25
26
8975
BVMinisatSatSolver::BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name)
27
: context::ContextNotifyObj(mainSatContext, false),
28
8975
  d_minisat(new BVMinisat::SimpSolver(mainSatContext)),
29
  d_minisatNotify(nullptr),
30
  d_assertionsCount(0),
31
  d_assertionsRealCount(mainSatContext, 0),
32
  d_lastPropagation(mainSatContext, 0),
33
17950
  d_statistics(registry, name)
34
{
35
8975
  d_statistics.init(d_minisat.get());
36
8975
}
37
38
39
17944
BVMinisatSatSolver::~BVMinisatSatSolver() {
40
17944
}
41
42
void BVMinisatSatSolver::MinisatNotify::notify(
43
    BVMinisat::vec<BVMinisat::Lit>& clause)
44
{
45
  SatClause satClause;
46
  for (unsigned i = 0, n = clause.size(); i < n; ++i)
47
  {
48
    satClause.push_back(toSatLiteral(clause[i]));
49
  }
50
  d_notify->notify(satClause);
51
}
52
53
8975
void BVMinisatSatSolver::setNotify(BVSatSolverNotify* notify) {
54
8975
  d_minisatNotify.reset(new MinisatNotify(notify));
55
8975
  d_minisat->setNotify(d_minisatNotify.get());
56
8975
}
57
58
6976466
ClauseId BVMinisatSatSolver::addClause(SatClause& clause,
59
                                       bool removable) {
60
6976466
  Debug("sat::minisat") << "Add clause " << clause <<"\n";
61
13952932
  BVMinisat::vec<BVMinisat::Lit> minisat_clause;
62
6976466
  toMinisatClause(clause, minisat_clause);
63
  // for(unsigned i = 0; i < minisat_clause.size(); ++i) {
64
  //   d_minisat->setFrozen(BVMinisat::var(minisat_clause[i]), true);
65
  // }
66
6976466
  ClauseId clause_id = ClauseIdError;
67
6976466
  d_minisat->addClause(minisat_clause, clause_id);
68
13952932
  return clause_id;
69
}
70
71
171639
SatValue BVMinisatSatSolver::propagate() {
72
171639
  return toSatLiteralValue(d_minisat->propagateAssumptions());
73
}
74
75
71653
void BVMinisatSatSolver::addMarkerLiteral(SatLiteral lit) {
76
71653
  d_minisat->addMarkerLiteral(BVMinisat::var(toMinisatLit(lit)));
77
71653
  markUnremovable(lit);
78
71653
}
79
80
84079
void BVMinisatSatSolver::explain(SatLiteral lit, std::vector<SatLiteral>& explanation) {
81
168158
  std::vector<BVMinisat::Lit> minisat_explanation;
82
84079
  d_minisat->explain(toMinisatLit(lit), minisat_explanation);
83
458157
  for (unsigned i = 0; i < minisat_explanation.size(); ++i) {
84
374078
    explanation.push_back(toSatLiteral(minisat_explanation[i]));
85
  }
86
84079
}
87
88
619545
SatValue BVMinisatSatSolver::assertAssumption(SatLiteral lit, bool propagate) {
89
619545
  d_assertionsCount ++;
90
619545
  d_assertionsRealCount = d_assertionsRealCount + 1;
91
619545
  return toSatLiteralValue(d_minisat->assertAssumption(toMinisatLit(lit), propagate));
92
}
93
94
3120231
void BVMinisatSatSolver::contextNotifyPop() {
95
3739776
  while (d_assertionsCount > d_assertionsRealCount) {
96
619545
    popAssumption();
97
619545
    d_assertionsCount --;
98
  }
99
2500686
}
100
101
619545
void BVMinisatSatSolver::popAssumption() {
102
619545
  d_minisat->popAssumption();
103
619545
}
104
105
1835652
SatVariable BVMinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase){
106
1835652
  return d_minisat->newVar(true, true, !canErase);
107
}
108
109
71653
void BVMinisatSatSolver::markUnremovable(SatLiteral lit){
110
71653
  d_minisat->setFrozen(BVMinisat::var(toMinisatLit(lit)), true);
111
71653
}
112
113
114
void BVMinisatSatSolver::interrupt(){
115
  d_minisat->interrupt();
116
}
117
118
9172
SatValue BVMinisatSatSolver::solve()
119
{
120
18344
  TimerStat::CodeTimer solveTimer(d_statistics.d_statSolveTime);
121
9172
  ++d_statistics.d_statCallsToSolve;
122
18344
  return toSatLiteralValue(d_minisat->solve());
123
}
124
125
SatValue BVMinisatSatSolver::solve(long unsigned int& resource){
126
  Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
127
  TimerStat::CodeTimer solveTimer(d_statistics.d_statSolveTime);
128
  ++d_statistics.d_statCallsToSolve;
129
  if(resource == 0) {
130
    d_minisat->budgetOff();
131
  } else {
132
    d_minisat->setConfBudget(resource);
133
  }
134
  //  BVMinisat::vec<BVMinisat::Lit> empty;
135
  unsigned long conflictsBefore = d_minisat->conflicts;
136
  SatValue result = toSatLiteralValue(d_minisat->solveLimited());
137
  d_minisat->clearInterrupt();
138
  resource = d_minisat->conflicts - conflictsBefore;
139
  Trace("limit") << "<MinisatSatSolver::solve(): it took " << resource << " conflicts" << std::endl;
140
  return result;
141
}
142
143
bool BVMinisatSatSolver::ok() const { return d_minisat->okay(); }
144
145
12112
void BVMinisatSatSolver::getUnsatCore(SatClause& unsatCore) {
146
  // TODO add assertion to check the call was after an unsat call
147
139702
  for (int i = 0; i < d_minisat->conflict.size(); ++i) {
148
127590
    unsatCore.push_back(toSatLiteral(d_minisat->conflict[i]));
149
  }
150
12112
}
151
152
259577
SatValue BVMinisatSatSolver::value(SatLiteral l){
153
259577
  return toSatLiteralValue(d_minisat->value(toMinisatLit(l)));
154
}
155
156
SatValue BVMinisatSatSolver::modelValue(SatLiteral l){
157
  return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l)));
158
}
159
160
void BVMinisatSatSolver::unregisterVar(SatLiteral lit) {
161
  // this should only be called when user context is implemented
162
  // in the BVSatSolver
163
  Unreachable();
164
}
165
166
void BVMinisatSatSolver::renewVar(SatLiteral lit, int level) {
167
  // this should only be called when user context is implemented
168
  // in the BVSatSolver
169
170
  Unreachable();
171
}
172
173
unsigned BVMinisatSatSolver::getAssertionLevel() const {
174
  // we have no user context implemented so far
175
  return 0;
176
}
177
178
// converting from internal Minisat representation
179
180
SatVariable BVMinisatSatSolver::toSatVariable(BVMinisat::Var var) {
181
  if (var == var_Undef) {
182
    return undefSatVariable;
183
  }
184
  return SatVariable(var);
185
}
186
187
20079423
BVMinisat::Lit BVMinisatSatSolver::toMinisatLit(SatLiteral lit) {
188
20079423
  if (lit == undefSatLiteral) {
189
    return BVMinisat::lit_Undef;
190
  }
191
20079423
  return BVMinisat::mkLit(lit.getSatVariable(), lit.isNegated());
192
}
193
194
2345830
SatLiteral BVMinisatSatSolver::toSatLiteral(BVMinisat::Lit lit) {
195
2345830
  if (lit == BVMinisat::lit_Undef) {
196
    return undefSatLiteral;
197
  }
198
199
4691660
  return SatLiteral(SatVariable(BVMinisat::var(lit)),
200
4691660
                    BVMinisat::sign(lit));
201
}
202
203
1059933
SatValue BVMinisatSatSolver::toSatLiteralValue(BVMinisat::lbool res) {
204
1059933
  if(res == (BVMinisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE;
205
203678
  if(res == (BVMinisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN;
206
203678
  Assert(res == (BVMinisat::lbool((uint8_t)1)));
207
203678
  return SAT_VALUE_FALSE;
208
}
209
210
6976466
void BVMinisatSatSolver::toMinisatClause(SatClause& clause,
211
                                           BVMinisat::vec<BVMinisat::Lit>& minisat_clause) {
212
25949382
  for (unsigned i = 0; i < clause.size(); ++i) {
213
18972916
    minisat_clause.push(toMinisatLit(clause[i]));
214
  }
215
6976466
  Assert(clause.size() == (unsigned)minisat_clause.size());
216
6976466
}
217
218
void BVMinisatSatSolver::toSatClause(const BVMinisat::Clause& clause,
219
                                     SatClause& sat_clause) {
220
  for (int i = 0; i < clause.size(); ++i) {
221
    sat_clause.push_back(toSatLiteral(clause[i]));
222
  }
223
  Assert((unsigned)clause.size() == sat_clause.size());
224
}
225
226
227
// Satistics for BVMinisatSatSolver
228
229
8975
BVMinisatSatSolver::Statistics::Statistics(StatisticsRegistry* registry,
230
8975
                                           const std::string& prefix)
231
    : d_registry(registry),
232
17950
      d_statStarts(prefix + "::bvminisat::starts"),
233
17950
      d_statDecisions(prefix + "::bvminisat::decisions"),
234
17950
      d_statRndDecisions(prefix + "::bvminisat::rnd_decisions"),
235
17950
      d_statPropagations(prefix + "::bvminisat::propagations"),
236
17950
      d_statConflicts(prefix + "::bvminisat::conflicts"),
237
17950
      d_statClausesLiterals(prefix + "::bvminisat::clauses_literals"),
238
17950
      d_statLearntsLiterals(prefix + "::bvminisat::learnts_literals"),
239
17950
      d_statMaxLiterals(prefix + "::bvminisat::max_literals"),
240
17950
      d_statTotLiterals(prefix + "::bvminisat::tot_literals"),
241
17950
      d_statEliminatedVars(prefix + "::bvminisat::eliminated_vars"),
242
17950
      d_statCallsToSolve(prefix + "::bvminisat::calls_to_solve", 0),
243
17950
      d_statSolveTime(prefix + "::bvminisat::solve_time"),
244
224375
      d_registerStats(!prefix.empty())
245
{
246
8975
  if (!d_registerStats)
247
  {
248
    return;
249
  }
250
251
8975
  d_registry->registerStat(&d_statStarts);
252
8975
  d_registry->registerStat(&d_statDecisions);
253
8975
  d_registry->registerStat(&d_statRndDecisions);
254
8975
  d_registry->registerStat(&d_statPropagations);
255
8975
  d_registry->registerStat(&d_statConflicts);
256
8975
  d_registry->registerStat(&d_statClausesLiterals);
257
8975
  d_registry->registerStat(&d_statLearntsLiterals);
258
8975
  d_registry->registerStat(&d_statMaxLiterals);
259
8975
  d_registry->registerStat(&d_statTotLiterals);
260
8975
  d_registry->registerStat(&d_statEliminatedVars);
261
8975
  d_registry->registerStat(&d_statCallsToSolve);
262
8975
  d_registry->registerStat(&d_statSolveTime);
263
}
264
265
17944
BVMinisatSatSolver::Statistics::~Statistics() {
266
8972
  if (!d_registerStats){
267
    return;
268
  }
269
8972
  d_registry->unregisterStat(&d_statStarts);
270
8972
  d_registry->unregisterStat(&d_statDecisions);
271
8972
  d_registry->unregisterStat(&d_statRndDecisions);
272
8972
  d_registry->unregisterStat(&d_statPropagations);
273
8972
  d_registry->unregisterStat(&d_statConflicts);
274
8972
  d_registry->unregisterStat(&d_statClausesLiterals);
275
8972
  d_registry->unregisterStat(&d_statLearntsLiterals);
276
8972
  d_registry->unregisterStat(&d_statMaxLiterals);
277
8972
  d_registry->unregisterStat(&d_statTotLiterals);
278
8972
  d_registry->unregisterStat(&d_statEliminatedVars);
279
8972
  d_registry->unregisterStat(&d_statCallsToSolve);
280
8972
  d_registry->unregisterStat(&d_statSolveTime);
281
8972
}
282
283
8975
void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){
284
8975
  if (!d_registerStats){
285
    return;
286
  }
287
288
8975
  d_statStarts.set(minisat->starts);
289
8975
  d_statDecisions.set(minisat->decisions);
290
8975
  d_statRndDecisions.set(minisat->rnd_decisions);
291
8975
  d_statPropagations.set(minisat->propagations);
292
8975
  d_statConflicts.set(minisat->conflicts);
293
8975
  d_statClausesLiterals.set(minisat->clauses_literals);
294
8975
  d_statLearntsLiterals.set(minisat->learnts_literals);
295
8975
  d_statMaxLiterals.set(minisat->max_literals);
296
8975
  d_statTotLiterals.set(minisat->tot_literals);
297
8975
  d_statEliminatedVars.set(minisat->eliminated_vars);
298
}
299
300
} /* namespace CVC4::prop */
301
26676
} /* namespace CVC4 */