GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/minisat/minisat.cpp Lines: 135 161 83.9 %
Date: 2021-03-22 Branches: 97 304 31.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file minisat.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, Dejan Jovanovic, Morgan Deters
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
#include "prop/minisat/minisat.h"
18
19
#include "options/base_options.h"
20
#include "options/decision_options.h"
21
#include "options/prop_options.h"
22
#include "options/smt_options.h"
23
#include "prop/minisat/simp/SimpSolver.h"
24
#include "proof/clause_id.h"
25
#include "proof/sat_proof.h"
26
#include "util/statistics_registry.h"
27
28
namespace CVC4 {
29
namespace prop {
30
31
//// DPllMinisatSatSolver
32
33
9027
MinisatSatSolver::MinisatSatSolver(StatisticsRegistry* registry) :
34
  d_minisat(NULL),
35
  d_context(NULL),
36
9027
  d_statistics(registry)
37
9027
{}
38
39
27072
MinisatSatSolver::~MinisatSatSolver()
40
{
41
9024
  delete d_minisat;
42
18048
}
43
44
8004837
SatVariable MinisatSatSolver::toSatVariable(Minisat::Var var) {
45
8004837
  if (var == var_Undef) {
46
    return undefSatVariable;
47
  }
48
8004837
  return SatVariable(var);
49
}
50
51
71668477
Minisat::Lit MinisatSatSolver::toMinisatLit(SatLiteral lit) {
52
71668477
  if (lit == undefSatLiteral) {
53
4433339
    return Minisat::lit_Undef;
54
  }
55
67235138
  return Minisat::mkLit(lit.getSatVariable(), lit.isNegated());
56
}
57
58
28758241
SatLiteral MinisatSatSolver::toSatLiteral(Minisat::Lit lit) {
59
28758241
  if (lit == Minisat::lit_Undef) {
60
    return undefSatLiteral;
61
  }
62
63
57516482
  return SatLiteral(SatVariable(Minisat::var(lit)),
64
57516482
                    Minisat::sign(lit));
65
}
66
67
49807743
SatValue MinisatSatSolver::toSatLiteralValue(Minisat::lbool res) {
68
49807743
  if(res == (Minisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE;
69
22499111
  if(res == (Minisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN;
70
14175915
  Assert(res == (Minisat::lbool((uint8_t)1)));
71
14175915
  return SAT_VALUE_FALSE;
72
}
73
74
1858660
Minisat::lbool MinisatSatSolver::toMinisatlbool(SatValue val)
75
{
76
1858660
  if(val == SAT_VALUE_TRUE) return Minisat::lbool((uint8_t)0);
77
1858660
  if(val == SAT_VALUE_UNKNOWN) return Minisat::lbool((uint8_t)2);
78
  Assert(val == SAT_VALUE_FALSE);
79
  return Minisat::lbool((uint8_t)1);
80
}
81
82
/*bool MinisatSatSolver::tobool(SatValue val)
83
{
84
  if(val == SAT_VALUE_TRUE) return true;
85
  Assert(val == SAT_VALUE_FALSE);
86
  return false;
87
  }*/
88
89
5804456
void MinisatSatSolver::toMinisatClause(SatClause& clause,
90
                                           Minisat::vec<Minisat::Lit>& minisat_clause) {
91
21417528
  for (unsigned i = 0; i < clause.size(); ++i) {
92
15613072
    minisat_clause.push(toMinisatLit(clause[i]));
93
  }
94
5804456
  Assert(clause.size() == (unsigned)minisat_clause.size());
95
5804456
}
96
97
322593
void MinisatSatSolver::toSatClause(const Minisat::Clause& clause,
98
                                       SatClause& sat_clause) {
99
2237666
  for (int i = 0; i < clause.size(); ++i) {
100
1915073
    sat_clause.push_back(toSatLiteral(clause[i]));
101
  }
102
322593
  Assert((unsigned)clause.size() == sat_clause.size());
103
322593
}
104
105
9027
void MinisatSatSolver::initialize(context::Context* context,
106
                                  TheoryProxy* theoryProxy,
107
                                  context::UserContext* userContext,
108
                                  ProofNodeManager* pnm)
109
{
110
9027
  d_context = context;
111
112
9027
  if (options::decisionMode() != options::DecisionMode::INTERNAL)
113
  {
114
6490
    Notice() << "minisat: Incremental solving is forced on (to avoid variable elimination)"
115
             << " unless using internal decision strategy." << std::endl;
116
  }
117
118
  // Create the solver
119
9027
  d_minisat = new Minisat::SimpSolver(
120
      theoryProxy,
121
      d_context,
122
      userContext,
123
      pnm,
124
9027
      options::incrementalSolving()
125
9027
          || options::decisionMode() != options::DecisionMode::INTERNAL);
126
127
9027
  d_statistics.init(d_minisat);
128
9027
}
129
130
// Like initialize() above, but called just before each search when in
131
// incremental mode
132
12417
void MinisatSatSolver::setupOptions() {
133
  // Copy options from CVC4 options structure into minisat, as appropriate
134
135
  // Set up the verbosity
136
591654
  d_minisat->verbosity = (options::verbosity() > 0) ? 1 : -1;
137
138
  // Set up the random decision parameters
139
24834
  d_minisat->random_var_freq = options::satRandomFreq();
140
  // If 0, we use whatever we like (here, the Minisat default seed)
141
24834
  if(options::satRandomSeed() != 0) {
142
    d_minisat->random_seed = double(options::satRandomSeed());
143
  }
144
145
  // Give access to all possible options in the sat solver
146
24834
  d_minisat->var_decay = options::satVarDecay();
147
24834
  d_minisat->clause_decay = options::satClauseDecay();
148
24834
  d_minisat->restart_first = options::satRestartFirst();
149
24834
  d_minisat->restart_inc = options::satRestartInc();
150
12417
}
151
152
2039268
ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) {
153
4078536
  Minisat::vec<Minisat::Lit> minisat_clause;
154
2039268
  toMinisatClause(clause, minisat_clause);
155
2039268
  ClauseId clause_id = ClauseIdError;
156
  // FIXME: This relies on the invariant that when ok() is false
157
  // the SAT solver does not add the clause (which is what Minisat currently does)
158
2039268
  if (!ok()) {
159
7733
    return ClauseIdUndef;
160
  }
161
2031535
  d_minisat->addClause(minisat_clause, removable, clause_id);
162
  // FIXME: to be deleted when we kill old proof code for unsat cores
163
2031535
  Assert(!options::unsatCores() || options::produceProofs()
164
         || clause_id != ClauseIdError);
165
2031535
  return clause_id;
166
}
167
168
790374
SatVariable MinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase) {
169
790374
  return d_minisat->newVar(true, true, isTheoryAtom, preRegister, canErase);
170
}
171
172
SatValue MinisatSatSolver::solve(unsigned long& resource) {
173
  Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
174
  setupOptions();
175
  if(resource == 0) {
176
    d_minisat->budgetOff();
177
  } else {
178
    d_minisat->setConfBudget(resource);
179
  }
180
  Minisat::vec<Minisat::Lit> empty;
181
  unsigned long conflictsBefore = d_minisat->conflicts + d_minisat->resources_consumed;
182
  SatValue result = toSatLiteralValue(d_minisat->solveLimited(empty));
183
  d_minisat->clearInterrupt();
184
  resource = d_minisat->conflicts + d_minisat->resources_consumed - conflictsBefore;
185
  Trace("limit") << "SatSolver::solve(): it took " << resource << " conflicts" << std::endl;
186
  return result;
187
}
188
189
12417
SatValue MinisatSatSolver::solve() {
190
12417
  setupOptions();
191
12417
  d_minisat->budgetOff();
192
12417
  SatValue result = toSatLiteralValue(d_minisat->solve());
193
12396
  d_minisat->clearInterrupt();
194
12396
  return result;
195
}
196
197
2039268
bool MinisatSatSolver::ok() const {
198
2039268
  return d_minisat->okay();
199
}
200
201
void MinisatSatSolver::interrupt() {
202
  d_minisat->interrupt();
203
}
204
205
49795347
SatValue MinisatSatSolver::value(SatLiteral l) {
206
49795347
  return toSatLiteralValue(d_minisat->value(toMinisatLit(l)));
207
}
208
209
SatValue MinisatSatSolver::modelValue(SatLiteral l){
210
  return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l)));
211
}
212
213
bool MinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const {
214
  return true;
215
}
216
217
82860
void MinisatSatSolver::requirePhase(SatLiteral lit) {
218
82860
  Assert(!d_minisat->rnd_pol);
219
82860
  Debug("minisat") << "requirePhase(" << lit << ")" << " " <<  lit.getSatVariable() << " " << lit.isNegated() << std::endl;
220
82860
  SatVariable v = lit.getSatVariable();
221
82860
  d_minisat->freezePolarity(v, lit.isNegated());
222
82860
}
223
224
209424
bool MinisatSatSolver::isDecision(SatVariable decn) const {
225
209424
  return d_minisat->isDecision( decn );
226
}
227
228
1932
SatProofManager* MinisatSatSolver::getProofManager()
229
{
230
1932
  return d_minisat->getProofManager();
231
}
232
233
2292
std::shared_ptr<ProofNode> MinisatSatSolver::getProof()
234
{
235
2292
  return d_minisat->getProof();
236
}
237
238
/** Incremental interface */
239
240
17599
unsigned MinisatSatSolver::getAssertionLevel() const {
241
17599
  return d_minisat->getAssertionLevel();
242
}
243
244
3190
void MinisatSatSolver::push() {
245
3190
  d_minisat->push();
246
3190
}
247
248
3190
void MinisatSatSolver::pop() {
249
3190
  d_minisat->pop();
250
3190
}
251
252
12399
void MinisatSatSolver::resetTrail() { d_minisat->resetTrail(); }
253
254
/// Statistics for MinisatSatSolver
255
256
9027
MinisatSatSolver::Statistics::Statistics(StatisticsRegistry* registry) :
257
    d_registry(registry),
258
    d_statStarts("sat::starts"),
259
    d_statDecisions("sat::decisions"),
260
    d_statRndDecisions("sat::rnd_decisions"),
261
    d_statPropagations("sat::propagations"),
262
    d_statConflicts("sat::conflicts"),
263
    d_statClausesLiterals("sat::clauses_literals"),
264
    d_statLearntsLiterals("sat::learnts_literals"),
265
    d_statMaxLiterals("sat::max_literals"),
266
9027
    d_statTotLiterals("sat::tot_literals")
267
{
268
9027
  d_registry->registerStat(&d_statStarts);
269
9027
  d_registry->registerStat(&d_statDecisions);
270
9027
  d_registry->registerStat(&d_statRndDecisions);
271
9027
  d_registry->registerStat(&d_statPropagations);
272
9027
  d_registry->registerStat(&d_statConflicts);
273
9027
  d_registry->registerStat(&d_statClausesLiterals);
274
9027
  d_registry->registerStat(&d_statLearntsLiterals);
275
9027
  d_registry->registerStat(&d_statMaxLiterals);
276
9027
  d_registry->registerStat(&d_statTotLiterals);
277
9027
}
278
279
18048
MinisatSatSolver::Statistics::~Statistics() {
280
9024
  d_registry->unregisterStat(&d_statStarts);
281
9024
  d_registry->unregisterStat(&d_statDecisions);
282
9024
  d_registry->unregisterStat(&d_statRndDecisions);
283
9024
  d_registry->unregisterStat(&d_statPropagations);
284
9024
  d_registry->unregisterStat(&d_statConflicts);
285
9024
  d_registry->unregisterStat(&d_statClausesLiterals);
286
9024
  d_registry->unregisterStat(&d_statLearntsLiterals);
287
9024
  d_registry->unregisterStat(&d_statMaxLiterals);
288
9024
  d_registry->unregisterStat(&d_statTotLiterals);
289
9024
}
290
291
9027
void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* minisat){
292
9027
  d_statStarts.set(minisat->starts);
293
9027
  d_statDecisions.set(minisat->decisions);
294
9027
  d_statRndDecisions.set(minisat->rnd_decisions);
295
9027
  d_statPropagations.set(minisat->propagations);
296
9027
  d_statConflicts.set(minisat->conflicts);
297
9027
  d_statClausesLiterals.set(minisat->clauses_literals);
298
9027
  d_statLearntsLiterals.set(minisat->learnts_literals);
299
9027
  d_statMaxLiterals.set(minisat->max_literals);
300
9027
  d_statTotLiterals.set(minisat->tot_literals);
301
9027
}
302
303
} /* namespace CVC4::prop */
304
} /* namespace CVC4 */
305
306
307
namespace CVC4 {
308
template<>
309
34246
prop::SatLiteral toSatLiteral< CVC4::Minisat::Solver>(Minisat::Solver::TLit lit) {
310
34246
  return prop::MinisatSatSolver::toSatLiteral(lit);
311
}
312
313
template<>
314
322593
void toSatClause< CVC4::Minisat::Solver> (const CVC4::Minisat::Solver::TClause& minisat_cl,
315
                                      prop::SatClause& sat_cl) {
316
322593
  prop::MinisatSatSolver::toSatClause(minisat_cl, sat_cl);
317
322593
}
318
319
680415
} /* namespace CVC4 */