GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/cadical.cpp Lines: 66 95 69.5 %
Date: 2021-03-23 Branches: 42 166 25.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file cadical.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mathias Preiner, Andres Noetzli, 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 Wrapper for CaDiCaL SAT Solver.
13
 **
14
 ** Implementation of the CaDiCaL SAT solver for CVC4 (bitvectors).
15
 **/
16
17
#include "prop/cadical.h"
18
19
#ifdef CVC4_USE_CADICAL
20
21
#include "base/check.h"
22
23
namespace CVC4 {
24
namespace prop {
25
26
using CadicalLit = int;
27
using CadicalVar = int;
28
29
// helper functions
30
namespace {
31
32
12
SatValue toSatValue(int result)
33
{
34
12
  if (result == 10) return SAT_VALUE_TRUE;
35
3
  if (result == 20) return SAT_VALUE_FALSE;
36
  Assert(result == 0);
37
  return SAT_VALUE_UNKNOWN;
38
}
39
40
/* Note: CaDiCaL returns lit/-lit for true/false. Older versions returned 1/-1.
41
 */
42
144
SatValue toSatValueLit(int value)
43
{
44
144
  if (value > 0) return SAT_VALUE_TRUE;
45
33
  Assert(value < 0);
46
33
  return SAT_VALUE_FALSE;
47
}
48
49
6711
CadicalLit toCadicalLit(const SatLiteral lit)
50
{
51
6711
  return lit.isNegated() ? -lit.getSatVariable() : lit.getSatVariable();
52
}
53
54
6
CadicalVar toCadicalVar(SatVariable var) { return var; }
55
56
}  // namespace helper functions
57
58
3
CadicalSolver::CadicalSolver(StatisticsRegistry* registry,
59
3
                             const std::string& name)
60
3
    : d_solver(new CaDiCaL::Solver()),
61
      // Note: CaDiCaL variables start with index 1 rather than 0 since negated
62
      //       literals are represented as the negation of the index.
63
      d_nextVarIdx(1),
64
      d_inSatMode(false),
65
6
      d_statistics(registry, name)
66
{
67
3
}
68
69
3
void CadicalSolver::init()
70
{
71
3
  d_true = newVar();
72
3
  d_false = newVar();
73
74
3
  d_solver->set("quiet", 1);  // CaDiCaL is verbose by default
75
3
  d_solver->add(toCadicalVar(d_true));
76
3
  d_solver->add(0);
77
3
  d_solver->add(-toCadicalVar(d_false));
78
3
  d_solver->add(0);
79
3
}
80
81
6
CadicalSolver::~CadicalSolver() {}
82
83
2556
ClauseId CadicalSolver::addClause(SatClause& clause, bool removable)
84
{
85
9114
  for (const SatLiteral& lit : clause)
86
  {
87
6558
    d_solver->add(toCadicalLit(lit));
88
  }
89
2556
  d_solver->add(0);
90
2556
  ++d_statistics.d_numClauses;
91
2556
  return ClauseIdError;
92
}
93
94
ClauseId CadicalSolver::addXorClause(SatClause& clause,
95
                                     bool rhs,
96
                                     bool removable)
97
{
98
  Unreachable() << "CaDiCaL does not support adding XOR clauses.";
99
}
100
101
921
SatVariable CadicalSolver::newVar(bool isTheoryAtom,
102
                                  bool preRegister,
103
                                  bool canErase)
104
{
105
921
  ++d_statistics.d_numVariables;
106
921
  return d_nextVarIdx++;
107
}
108
109
3
SatVariable CadicalSolver::trueVar() { return d_true; }
110
111
SatVariable CadicalSolver::falseVar() { return d_false; }
112
113
SatValue CadicalSolver::solve()
114
{
115
  TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
116
  d_assumptions.clear();
117
  SatValue res = toSatValue(d_solver->solve());
118
  d_inSatMode = (res == SAT_VALUE_TRUE);
119
  ++d_statistics.d_numSatCalls;
120
  return res;
121
}
122
123
SatValue CadicalSolver::solve(long unsigned int&)
124
{
125
  Unimplemented() << "Setting limits for CaDiCaL not supported yet";
126
};
127
128
12
SatValue CadicalSolver::solve(const std::vector<SatLiteral>& assumptions)
129
{
130
24
  TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
131
12
  d_assumptions.clear();
132
21
  for (const SatLiteral& lit : assumptions)
133
  {
134
9
    d_solver->assume(toCadicalLit(lit));
135
9
    d_assumptions.push_back(lit);
136
  }
137
12
  SatValue res = toSatValue(d_solver->solve());
138
12
  d_inSatMode = (res == SAT_VALUE_TRUE);
139
12
  ++d_statistics.d_numSatCalls;
140
24
  return res;
141
}
142
143
bool CadicalSolver::setPropagateOnly()
144
{
145
  d_solver->limit("decisions", 0); /* Gets reset after next solve() call. */
146
  return true;
147
}
148
149
void CadicalSolver::getUnsatAssumptions(std::vector<SatLiteral>& assumptions)
150
{
151
  for (const SatLiteral& lit : d_assumptions)
152
  {
153
    if (d_solver->failed(toCadicalLit(lit)))
154
    {
155
      assumptions.push_back(lit);
156
    }
157
  }
158
}
159
160
void CadicalSolver::interrupt() { d_solver->terminate(); }
161
162
144
SatValue CadicalSolver::value(SatLiteral l)
163
{
164
144
  Assert(d_inSatMode);
165
144
  return toSatValueLit(d_solver->val(toCadicalLit(l)));
166
}
167
168
SatValue CadicalSolver::modelValue(SatLiteral l)
169
{
170
  Assert(d_inSatMode);
171
  return value(l);
172
}
173
174
unsigned CadicalSolver::getAssertionLevel() const
175
{
176
  Unreachable() << "CaDiCaL does not support assertion levels.";
177
}
178
179
bool CadicalSolver::ok() const { return d_inSatMode; }
180
181
3
CadicalSolver::Statistics::Statistics(StatisticsRegistry* registry,
182
3
                                      const std::string& prefix)
183
    : d_registry(registry),
184
6
      d_numSatCalls("theory::bv::" + prefix + "::cadical::calls_to_solve", 0),
185
6
      d_numVariables("theory::bv::" + prefix + "::cadical::variables", 0),
186
6
      d_numClauses("theory::bv::" + prefix + "::cadical::clauses", 0),
187
21
      d_solveTime("theory::bv::" + prefix + "::cadical::solve_time")
188
{
189
3
  d_registry->registerStat(&d_numSatCalls);
190
3
  d_registry->registerStat(&d_numVariables);
191
3
  d_registry->registerStat(&d_numClauses);
192
3
  d_registry->registerStat(&d_solveTime);
193
3
}
194
195
6
CadicalSolver::Statistics::~Statistics() {
196
3
  d_registry->unregisterStat(&d_numSatCalls);
197
3
  d_registry->unregisterStat(&d_numVariables);
198
3
  d_registry->unregisterStat(&d_numClauses);
199
3
  d_registry->unregisterStat(&d_solveTime);
200
3
}
201
202
}  // namespace prop
203
26685
}  // namespace CVC4
204
205
#endif  // CVC4_USE_CADICAL