GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/cryptominisat.cpp Lines: 86 122 70.5 %
Date: 2021-03-23 Branches: 73 238 30.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file cryptominisat.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, Mathias Preiner, Alex Ozdemir
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 for cvc4 (bitvectors).
15
 **/
16
17
#ifdef CVC4_USE_CRYPTOMINISAT
18
19
#include "prop/cryptominisat.h"
20
21
#include "base/check.h"
22
23
#include <cryptominisat5/cryptominisat.h>
24
25
namespace CVC4 {
26
namespace prop {
27
28
using CMSatVar = unsigned;
29
30
// helper functions
31
namespace {
32
33
6571
CMSat::Lit toInternalLit(SatLiteral lit)
34
{
35
6571
  if (lit == undefSatLiteral)
36
  {
37
    return CMSat::lit_Undef;
38
  }
39
6571
  return CMSat::Lit(lit.getSatVariable(), lit.isNegated());
40
}
41
42
SatLiteral toSatLiteral(CMSat::Lit lit)
43
{
44
  if (lit == CMSat::lit_Undef)
45
  {
46
    return undefSatLiteral;
47
  }
48
  return SatLiteral(lit.var(), lit.sign());
49
}
50
51
160
SatValue toSatLiteralValue(CMSat::lbool res)
52
{
53
160
  if (res == CMSat::l_True) return SAT_VALUE_TRUE;
54
128
  if (res == CMSat::l_Undef) return SAT_VALUE_UNKNOWN;
55
128
  Assert(res == CMSat::l_False);
56
128
  return SAT_VALUE_FALSE;
57
}
58
59
2560
void toInternalClause(SatClause& clause,
60
                      std::vector<CMSat::Lit>& internal_clause)
61
{
62
9122
  for (unsigned i = 0; i < clause.size(); ++i)
63
  {
64
6562
    internal_clause.push_back(toInternalLit(clause[i]));
65
  }
66
2560
  Assert(clause.size() == internal_clause.size());
67
2560
}
68
69
}  // helper functions
70
71
7
CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry* registry,
72
7
                                         const std::string& name)
73
7
    : d_solver(new CMSat::SATSolver()),
74
      d_numVariables(0),
75
      d_okay(true),
76
14
      d_statistics(registry, name)
77
{
78
7
}
79
80
7
void CryptoMinisatSolver::init()
81
{
82
7
  d_true = newVar();
83
7
  d_false = newVar();
84
85
14
  std::vector<CMSat::Lit> clause(1);
86
7
  clause[0] = CMSat::Lit(d_true, false);
87
7
  d_solver->add_clause(clause);
88
89
7
  clause[0] = CMSat::Lit(d_false, true);
90
7
  d_solver->add_clause(clause);
91
7
}
92
93
14
CryptoMinisatSolver::~CryptoMinisatSolver() {}
94
95
ClauseId CryptoMinisatSolver::addXorClause(SatClause& clause,
96
                                           bool rhs,
97
                                           bool removable)
98
{
99
  Debug("sat::cryptominisat") << "Add xor clause " << clause <<" = " << rhs << "\n";
100
101
  if (!d_okay) {
102
    Debug("sat::cryptominisat") << "Solver unsat: not adding clause.\n";
103
    return ClauseIdError;
104
  }
105
106
  ++(d_statistics.d_xorClausesAdded);
107
108
  // ensure all sat literals have positive polarity by pushing
109
  // the negation on the result
110
  std::vector<CMSatVar> xor_clause;
111
  for (unsigned i = 0; i < clause.size(); ++i) {
112
    xor_clause.push_back(toInternalLit(clause[i]).var());
113
    rhs ^= clause[i].isNegated();
114
  }
115
  bool res = d_solver->add_xor_clause(xor_clause, rhs);
116
  d_okay &= res;
117
  return ClauseIdError;
118
}
119
120
2564
ClauseId CryptoMinisatSolver::addClause(SatClause& clause, bool removable){
121
2564
  Debug("sat::cryptominisat") << "Add clause " << clause <<"\n";
122
123
2564
  if (!d_okay) {
124
4
    Debug("sat::cryptominisat") << "Solver unsat: not adding clause.\n";
125
4
    return ClauseIdError;
126
  }
127
128
2560
  ++(d_statistics.d_clausesAdded);
129
130
5120
  std::vector<CMSat::Lit> internal_clause;
131
2560
  toInternalClause(clause, internal_clause);
132
2560
  bool nowOkay = d_solver->add_clause(internal_clause);
133
134
  ClauseId freshId;
135
2560
  freshId = ClauseIdError;
136
137
2560
  d_okay &= nowOkay;
138
2560
  return freshId;
139
}
140
141
bool CryptoMinisatSolver::ok() const { return d_okay; }
142
143
929
SatVariable  CryptoMinisatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase){
144
929
  d_solver->new_var();
145
929
  ++d_numVariables;
146
929
  Assert(d_numVariables == d_solver->nVars());
147
929
  return d_numVariables - 1;
148
}
149
150
3
SatVariable CryptoMinisatSolver::trueVar() {
151
3
  return d_true;
152
}
153
154
4
SatVariable CryptoMinisatSolver::falseVar() {
155
4
  return d_false;
156
}
157
158
void CryptoMinisatSolver::markUnremovable(SatLiteral lit) {
159
  // cryptominisat supports dynamically adding back variables (?)
160
  // so this is a no-op
161
  return;
162
}
163
164
void CryptoMinisatSolver::interrupt(){
165
  d_solver->interrupt_asap();
166
}
167
168
4
SatValue CryptoMinisatSolver::solve(){
169
8
  TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
170
4
  ++d_statistics.d_statCallsToSolve;
171
8
  return toSatLiteralValue(d_solver->solve());
172
}
173
174
SatValue CryptoMinisatSolver::solve(long unsigned int& resource) {
175
  // CMSat::SalverConf conf = d_solver->getConf();
176
  Unreachable() << "Not sure how to set different limits for calls to solve in "
177
                   "Cryptominisat";
178
  return solve();
179
}
180
181
12
SatValue CryptoMinisatSolver::solve(const std::vector<SatLiteral>& assumptions)
182
{
183
24
  TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
184
24
  std::vector<CMSat::Lit> assumpts;
185
21
  for (const SatLiteral& lit : assumptions)
186
  {
187
9
    assumpts.push_back(toInternalLit(lit));
188
  }
189
12
  ++d_statistics.d_statCallsToSolve;
190
24
  return toSatLiteralValue(d_solver->solve(&assumpts));
191
}
192
193
void CryptoMinisatSolver::getUnsatAssumptions(
194
    std::vector<SatLiteral>& assumptions)
195
{
196
  for (const CMSat::Lit& lit : d_solver->get_conflict())
197
  {
198
    assumptions.push_back(toSatLiteral(~lit));
199
  }
200
}
201
202
144
SatValue CryptoMinisatSolver::value(SatLiteral l){
203
288
  const std::vector<CMSat::lbool> model = d_solver->get_model();
204
144
  CMSatVar var = l.getSatVariable();
205
144
  Assert(var < model.size());
206
144
  CMSat::lbool value = model[var];
207
288
  return toSatLiteralValue(value);
208
}
209
210
SatValue CryptoMinisatSolver::modelValue(SatLiteral l) { return value(l); }
211
212
unsigned CryptoMinisatSolver::getAssertionLevel() const {
213
  Unreachable() << "No interface to get assertion level in Cryptominisat";
214
  return -1;
215
}
216
217
// Satistics for CryptoMinisatSolver
218
219
7
CryptoMinisatSolver::Statistics::Statistics(StatisticsRegistry* registry,
220
7
                                            const std::string& prefix) :
221
  d_registry(registry),
222
14
  d_statCallsToSolve("theory::bv::"+prefix+"::cryptominisat::calls_to_solve", 0),
223
14
  d_xorClausesAdded("theory::bv::"+prefix+"::cryptominisat::xor_clauses", 0),
224
14
  d_clausesAdded("theory::bv::"+prefix+"::cryptominisat::clauses", 0),
225
14
  d_solveTime("theory::bv::"+prefix+"::cryptominisat::solve_time"),
226
63
  d_registerStats(!prefix.empty())
227
{
228
7
  if (!d_registerStats)
229
    return;
230
231
7
  d_registry->registerStat(&d_statCallsToSolve);
232
7
  d_registry->registerStat(&d_xorClausesAdded);
233
7
  d_registry->registerStat(&d_clausesAdded);
234
7
  d_registry->registerStat(&d_solveTime);
235
}
236
237
14
CryptoMinisatSolver::Statistics::~Statistics() {
238
7
  if (!d_registerStats)
239
    return;
240
7
  d_registry->unregisterStat(&d_statCallsToSolve);
241
7
  d_registry->unregisterStat(&d_xorClausesAdded);
242
7
  d_registry->unregisterStat(&d_clausesAdded);
243
7
  d_registry->unregisterStat(&d_solveTime);
244
7
}
245
246
}  // namespace prop
247
26685
}  // namespace CVC4
248
#endif