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