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