Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Mathias Preiner, Aina Niemetz, Andrew Reynolds
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 : : #include <deque>
21 : :
22 : : #include "base/check.h"
23 : : #include "options/base_options.h"
24 : : #include "options/main_options.h"
25 : : #include "options/proof_options.h"
26 : : #include "prop/theory_proxy.h"
27 : : #include "util/resource_manager.h"
28 : : #include "util/statistics_registry.h"
29 : : #include "util/string.h"
30 : :
31 : : namespace cvc5::internal {
32 : : namespace prop {
33 : :
34 : : /* -------------------------------------------------------------------------- */
35 : :
36 : : using CadicalLit = int;
37 : : using CadicalVar = int;
38 : :
39 : : // helper functions
40 : : namespace {
41 : :
42 : 68903 : SatValue toSatValue(int result)
43 : : {
44 [ + + ]: 68903 : if (result == 10) return SAT_VALUE_TRUE;
45 [ + - ]: 20093 : if (result == 20) return SAT_VALUE_FALSE;
46 : 0 : Assert(result == 0);
47 : 0 : return SAT_VALUE_UNKNOWN;
48 : : }
49 : :
50 : : // Note: CaDiCaL returns lit/-lit for true/false. Older versions returned 1/-1.
51 : 553144 : SatValue toSatValueLit(int value)
52 : : {
53 [ + + ]: 553144 : if (value > 0) return SAT_VALUE_TRUE;
54 [ - + ][ - + ]: 341759 : Assert(value < 0);
[ - - ]
55 : 341759 : return SAT_VALUE_FALSE;
56 : : }
57 : :
58 : 30964500 : CadicalLit toCadicalLit(const SatLiteral lit)
59 : : {
60 [ + + ]: 30964500 : return lit.isNegated() ? -lit.getSatVariable() : lit.getSatVariable();
61 : : }
62 : :
63 : 469 : SatLiteral toSatLiteral(CadicalLit lit)
64 : : {
65 : 469 : return SatLiteral(std::abs(lit), lit < 0);
66 : : }
67 : :
68 : 80391 : CadicalVar toCadicalVar(SatVariable var) { return var; }
69 : :
70 : : } // namespace helper functions
71 : :
72 : : class CadicalPropagator : public CaDiCaL::ExternalPropagator,
73 : : public CaDiCaL::FixedAssignmentListener
74 : : {
75 : : public:
76 : 15 : CadicalPropagator(prop::TheoryProxy* proxy,
77 : : context::Context* context,
78 : : CaDiCaL::Solver& solver,
79 : : StatisticsRegistry& stats)
80 : 15 : : d_proxy(proxy), d_context(*context), d_solver(solver), d_stats(stats)
81 : : {
82 : 15 : d_var_info.emplace_back(); // 0: Not used
83 : 15 : }
84 : :
85 : : /**
86 : : * Notification from the SAT solver on assignment of a new literal.
87 : : *
88 : : * Saves assignment for notified literal, enqueues corresponding theory
89 : : * literal in theory proxy.
90 : : *
91 : : * @param lit The CaDiCaL literal that was assigned.
92 : : */
93 : 239 : void notify_assignment(const std::vector<int>& lits) override
94 : : {
95 [ + - ][ - + ]: 239 : if (Trace("cadical::propagator").isConnected())
96 : : {
97 [ - - ]: 0 : Trace("cadical::propagator") << "notif::assignments: { ";
98 [ - - ]: 0 : for (auto lit : lits)
99 : : {
100 [ - - ]: 0 : Trace("cadical::propagator") << lit << " ";
101 : : }
102 [ - - ]: 0 : Trace("cadical::propagator") << "}" << std::endl;
103 : : }
104 : 239 : ++d_stats.notifyAssignment;
105 : :
106 [ + + ]: 239 : if (d_found_solution)
107 : : {
108 : 2 : return;
109 : : }
110 : :
111 [ + + ]: 555 : for (const auto& lit : lits)
112 : : {
113 : 318 : SatLiteral slit = toSatLiteral(lit);
114 : 318 : SatVariable var = slit.getSatVariable();
115 [ - + ][ - + ]: 318 : Assert(var < d_var_info.size());
[ - - ]
116 : :
117 : 318 : auto& info = d_var_info[var];
118 : :
119 : : // Only consider active variables
120 [ - + ]: 318 : if (!info.is_active)
121 : : {
122 : 0 : continue;
123 : : }
124 : :
125 : 318 : bool is_decision = d_solver.is_decision(lit);
126 : :
127 [ + - ]: 636 : Trace("cadical::propagator")
128 [ - - ]: 0 : << "notif::assignment: [" << (is_decision ? "d" : "p") << "] " << slit
129 : 0 : << " (level: " << d_decisions.size()
130 : 0 : << ", level_intro: " << info.level_intro
131 : 318 : << ", level_user: " << current_user_level() << ")" << std::endl;
132 : :
133 : : // Save decision variables
134 [ + + ]: 318 : if (is_decision)
135 : : {
136 : 38 : d_decisions.back() = slit;
137 : : }
138 : :
139 [ + + ][ - + ]: 318 : Assert(info.assignment == 0 || info.assignment == lit);
[ - + ][ - - ]
140 : :
141 : : // Only notify theory proxy if variable was assigned a new value, not if
142 : : // it got fixed after assignment already happend.
143 [ + + ]: 318 : if (info.assignment == 0)
144 : : {
145 : 213 : info.assignment = lit;
146 : 213 : d_assignments.push_back(slit);
147 [ + + ]: 213 : if (info.is_theory_atom)
148 : : {
149 [ + - ]: 130 : Trace("cadical::propagator") << "enqueue: " << slit << std::endl;
150 [ + - ]: 260 : Trace("cadical::propagator")
151 [ - + ][ - - ]: 130 : << "node: " << d_proxy->getNode(slit) << std::endl;
152 : 130 : d_proxy->enqueueTheoryLiteral(slit);
153 : : }
154 : : }
155 : : }
156 : : }
157 : :
158 : : /**
159 : : * Notification from the SAT solver on fixed assignment of a literal.
160 : : *
161 : : * Notifications on fixed assignment are sent during the search, while
162 : : * regular assignment notifications are sent batch-wise, before the first
163 : : * callback is issued. This thus calls notify_assignment() to trigger what
164 : : * needs to be done on assignment. Already notified fixed assignments are
165 : : * then skipped in notify_assignment().
166 : : *
167 : : * @param lit The CaDiCaL literal that was fixed.
168 : : */
169 : 139 : void notify_fixed_assignment(int lit) override
170 : : {
171 : 139 : SatLiteral slit = toSatLiteral(lit);
172 : 139 : SatVariable var = slit.getSatVariable();
173 : :
174 : : // We don't care about non-observed variables
175 [ - + ]: 139 : if (var >= d_var_info.size())
176 : : {
177 : 32 : return;
178 : : }
179 : :
180 : 139 : auto& info = d_var_info[var];
181 : : // Only consider active variables
182 [ + + ]: 139 : if (!info.is_active)
183 : : {
184 : 32 : return;
185 : : }
186 : 107 : ++d_stats.notifyFixedAssignment;
187 : :
188 [ + - ]: 214 : Trace("cadical::propagator")
189 : 107 : << "notif::fixed assignment: " << slit << std::endl;
190 : :
191 : : // Mark as fixed.
192 [ - + ][ - + ]: 107 : Assert(!info.is_fixed);
[ - - ]
193 : 107 : info.is_fixed = true;
194 : 107 : info.level_fixed = current_user_level();
195 : : // Trigger actual assignment.
196 : 107 : notify_assignment({lit});
197 : : }
198 : :
199 : : /**
200 : : * Notification from the SAT solver when it makes a decision.
201 : : * Pushes new SAT context level.
202 : : */
203 : 40 : void notify_new_decision_level() override
204 : : {
205 : 40 : d_context.push();
206 : 40 : d_assignment_control.push_back(d_assignments.size());
207 : 40 : d_decisions.emplace_back();
208 [ + - ]: 80 : Trace("cadical::propagator")
209 : 40 : << "notif::decision: new level " << d_decisions.size() << std::endl;
210 : 40 : ++d_stats.notifyNewDecision;
211 : 40 : }
212 : :
213 : : /**
214 : : * Notification from the SAT solver on backtrack to the given level.
215 : : *
216 : : * This will automatically backtrack decisions and assignments to the
217 : : * specified level. Fixed assignments that get backtracked will be
218 : : * re-assigned at `level` and the corresponding theory literals are
219 : : * re-enqueued in the theory proxy.
220 : : *
221 : : * @param level The level the SAT solver backtracked to.
222 : : */
223 : 62 : void notify_backtrack(size_t level) override
224 : : {
225 [ + - ]: 62 : Trace("cadical::propagator") << "notif::backtrack: " << level << std::endl;
226 : :
227 : : // CaDiCaL may notify us about backtracks of decisions that we were not
228 : : // notified about. We can safely ignore them.
229 [ + + ]: 62 : if (d_decisions.size() <= level)
230 : : {
231 [ - + ][ - + ]: 30 : Assert(d_decisions.size() == 0);
[ - - ]
232 : 30 : return;
233 : : }
234 : 32 : d_found_solution = false;
235 : :
236 : : // Backtrack decisions
237 [ - + ][ - + ]: 32 : Assert(d_decisions.size() > level);
[ - - ]
238 [ - + ][ - + ]: 32 : Assert(d_context.getLevel() > level);
[ - - ]
239 [ + + ]: 72 : for (size_t cur_level = d_decisions.size(); cur_level > level; --cur_level)
240 : : {
241 : 40 : d_context.pop();
242 : 40 : d_decisions.pop_back();
243 : : }
244 : :
245 : : // Backtrack assignments, resend fixed theory literals that got backtracked
246 [ - + ][ - + ]: 32 : Assert(!d_assignment_control.empty());
[ - - ]
247 : 32 : size_t pop_to = d_assignment_control[level];
248 : 32 : d_assignment_control.resize(level);
249 : :
250 [ + + ]: 138 : while (pop_to < d_assignments.size())
251 : : {
252 : 106 : SatLiteral lit = d_assignments.back();
253 : 106 : d_assignments.pop_back();
254 : 106 : SatVariable var = lit.getSatVariable();
255 : 106 : auto& info = d_var_info[var];
256 [ + - ]: 106 : Trace("cadical::propagator") << "unassign: " << var << std::endl;
257 : 106 : info.assignment = 0;
258 : : }
259 : :
260 : : // Notify theory proxy about backtrack
261 : 32 : d_proxy->notifyBacktrack();
262 : : // Clear the propgations since they are not valid anymore.
263 : 32 : d_propagations.clear();
264 : 32 : ++d_stats.notifyBacktrack;
265 : :
266 [ + - ]: 32 : Trace("cadical::propagator") << "notif::backtrack end" << std::endl;
267 : : }
268 : :
269 : : /**
270 : : * Callback of the SAT solver on finding a full sat assignment.
271 : : *
272 : : * Checks whether current model is consistent with the theories, performs a
273 : : * full effort check and theory propgations.
274 : : *
275 : : * @param model The full assignment.
276 : : * @return true If the current model is not in conflict with the theories.
277 : : */
278 : 55 : bool cb_check_found_model(const std::vector<int>& model) override
279 : : {
280 [ + - ]: 55 : Trace("cadical::propagator") << "cb::check_found_model" << std::endl;
281 : 55 : bool recheck = false;
282 : :
283 [ + + ]: 55 : if (d_found_solution)
284 : : {
285 : 2 : return true;
286 : : }
287 : :
288 : 53 : ++d_stats.cbCheckFoundModel;
289 : : // CaDiCaL may backtrack while importing clauses, which can result in some
290 : : // clauses not being processed. Make sure to add all clauses before
291 : : // checking the model.
292 [ + + ]: 53 : if (!d_new_clauses.empty())
293 : : {
294 [ + - ]: 8 : Trace("cadical::propagator") << "cb::check_found_model end: new "
295 : 0 : "variables added via theory decision"
296 : 4 : << std::endl;
297 : : // CaDiCaL expects us to be able to provide a reason for rejecting the
298 : : // model (it asserts that after this call, cb_has_external_clause()
299 : : // returns true). However, in this particular case, we want to force
300 : : // CaDiCaL to give us model values for the new variables that were
301 : : // introduced (to kick off the assignment notification machinery), we
302 : : // don't have a reason clause for rejecting the model. CaDiCaL's
303 : : // expectation will be weakened in the future to allow for this, but for
304 : : // now we simply add a tautology as reason to pacify CaDiCaL.
305 : 4 : d_new_clauses.push_back(1);
306 : 4 : d_new_clauses.push_back(-1);
307 : 4 : d_new_clauses.push_back(0);
308 : 4 : return false;
309 : : }
310 : :
311 : : // Check full model.
312 : : //
313 : : // First, we have to ensure that if the SAT solver determines sat without
314 : : // making any decisions, theory decisions are still requested until fixed
315 : : // point at least once since some modules, e.g., finite model finding, rely
316 : : // on this. Theory decisions may add new variables (while decisions
317 : : // requested by the decision engine will not). If new variables are added,
318 : : // we interrupt the check to force the SAT solver to extend the model with
319 : : // the new variables.
320 : 49 : size_t size = d_var_info.size();
321 : : bool requirePhase, stopSearch;
322 : 49 : d_proxy->getNextDecisionRequest(requirePhase, stopSearch);
323 [ - + ]: 49 : if (d_var_info.size() != size)
324 : : {
325 [ - - ]: 0 : Trace("cadical::propagator") << "cb::check_found_model end: new "
326 : 0 : "variables added via theory decision"
327 : 0 : << std::endl;
328 : 0 : return false;
329 : : }
330 : : // Theory engine may trigger a recheck, unless new variables were added
331 : : // during check. If so, we break out of the check and have the SAT solver
332 : : // extend the model with the new variables.
333 : 2 : do
334 : : {
335 [ + - ]: 102 : Trace("cadical::propagator")
336 : 51 : << "full check (recheck: " << recheck << ")" << std::endl;
337 : 51 : d_proxy->theoryCheck(theory::Theory::Effort::EFFORT_FULL);
338 : 51 : theory_propagate();
339 [ + + ]: 59 : for (const SatLiteral& p : d_propagations)
340 : : {
341 [ + - ]: 16 : Trace("cadical::propagator")
342 : 8 : << "add propagation reason: " << p << std::endl;
343 : 16 : SatClause clause;
344 : 8 : d_proxy->explainPropagation(p, clause);
345 : 8 : add_clause(clause);
346 : : }
347 : 51 : d_propagations.clear();
348 : :
349 [ + + ]: 51 : if (!d_new_clauses.empty())
350 : : {
351 : : // Will again call cb_check_found_model() after clauses were added.
352 : 33 : recheck = false;
353 : : }
354 : : else
355 : : {
356 : 18 : recheck = d_proxy->theoryNeedCheck();
357 : : }
358 [ + + ][ + + ]: 51 : } while (d_var_info.size() == size && recheck);
[ + + ]
359 : :
360 [ + + ]: 49 : if (d_var_info.size() != size)
361 : : {
362 [ + - ]: 36 : Trace("cadical::propagator") << "cb::check_found_model end: new "
363 : 0 : "variables added via theory check"
364 : 18 : << std::endl;
365 : : // Same as above, until CaDiCaL's assertion that we have to have
366 : : // a reason clause for rejecting the model is weakened, we need to
367 : : // pacify it with a tautology.
368 : 18 : d_new_clauses.push_back(1);
369 : 18 : d_new_clauses.push_back(-1);
370 : 18 : d_new_clauses.push_back(0);
371 : 18 : return false;
372 : : }
373 : 31 : bool res = done();
374 [ + - ]: 62 : Trace("cadical::propagator")
375 : 31 : << "cb::check_found_model end: done: " << res << std::endl;
376 : 31 : return res;
377 : : }
378 : :
379 : : /**
380 : : * Callback of the SAT solver before making a new decision.
381 : : *
382 : : * Processes decision requests from the theory proxy.
383 : : *
384 : : * @note This may call cb_check_found_model() in case the decision engine
385 : : * determines that we have a partial model, i.e., stopSearch is true.
386 : : *
387 : : * @return The next decision.
388 : : */
389 : 26 : int cb_decide() override
390 : : {
391 [ + - ]: 26 : Trace("cadical::propagator") << "cb::decide" << std::endl;
392 [ - + ]: 26 : if (d_found_solution)
393 : : {
394 : 0 : return 0;
395 : : }
396 : 26 : ++d_stats.cbDecide;
397 : 26 : bool stopSearch = false;
398 : 26 : bool requirePhase = false;
399 : 26 : SatLiteral lit = d_proxy->getNextDecisionRequest(requirePhase, stopSearch);
400 : : // We found a partial model, let's check it.
401 [ + + ]: 26 : if (stopSearch)
402 : : {
403 : 12 : d_found_solution = cb_check_found_model({});
404 [ + + ]: 12 : if (d_found_solution)
405 : : {
406 [ + - ]: 2 : Trace("cadical::propagator") << "Found solution" << std::endl;
407 : 2 : d_found_solution = d_proxy->isDecisionEngineDone();
408 [ - + ]: 2 : if (!d_found_solution)
409 : : {
410 [ - - ]: 0 : Trace("cadical::propagator")
411 : 0 : << "Decision engine not done" << std::endl;
412 : 0 : lit = d_proxy->getNextDecisionRequest(requirePhase, stopSearch);
413 : : }
414 : : }
415 : : else
416 : : {
417 [ + - ]: 10 : Trace("cadical::propagator") << "No solution found yet" << std::endl;
418 : : }
419 : : }
420 [ + + ][ + - ]: 26 : if (!stopSearch && lit != undefSatLiteral)
[ + + ]
421 : : {
422 [ + + ]: 14 : if (!requirePhase)
423 : : {
424 : 8 : int8_t phase = d_var_info[lit.getSatVariable()].phase;
425 [ - + ]: 8 : if (phase != 0)
426 : : {
427 [ - - ]: 0 : if ((phase == -1 && !lit.isNegated())
428 [ - - ][ - - ]: 0 : || (phase == 1 && lit.isNegated()))
[ - - ][ - - ]
429 : : {
430 : 0 : lit = ~lit;
431 : : }
432 : : }
433 : : }
434 [ + - ]: 14 : Trace("cadical::propagator") << "cb::decide: " << lit << std::endl;
435 : 14 : return toCadicalLit(lit);
436 : : }
437 [ + - ]: 12 : Trace("cadical::propagator") << "cb::decide: 0" << std::endl;
438 : 12 : return 0;
439 : : }
440 : :
441 : : /**
442 : : * Callback of the SAT solver after BCP.
443 : : *
444 : : * Performs standard theory check and theory propagations.
445 : : *
446 : : * If we don't have any theory propagations queued in d_propagations, we
447 : : * perform an EFFORT_STANDARD check in combination with theory_propagate() to
448 : : * populate d_propagations.
449 : : *
450 : : * @return The next theory propagation.
451 : : */
452 : 158 : int cb_propagate() override
453 : : {
454 [ + + ]: 158 : if (d_found_solution)
455 : : {
456 : 2 : return 0;
457 : : }
458 : 156 : ++d_stats.cbPropagate;
459 [ + - ]: 156 : Trace("cadical::propagator") << "cb::propagate" << std::endl;
460 [ + + ]: 156 : if (d_propagations.empty())
461 : : {
462 : : // Only propagate if all activation literals are processed. Activation
463 : : // literals are always assumed first. If we don't do this, explanations
464 : : // for theory propgations may force activation literals to different
465 : : // values before they can get decided on.
466 [ + + ]: 135 : if (d_decisions.size() < current_user_level())
467 : : {
468 : 26 : return 0;
469 : : }
470 : 109 : d_proxy->theoryCheck(theory::Theory::Effort::EFFORT_STANDARD);
471 : 109 : theory_propagate();
472 : : }
473 : 130 : return next_propagation();
474 : : }
475 : :
476 : : /**
477 : : * Callback of the SAT solver asking for the explanation of a theory literal.
478 : : * @note This is called on `propagated_lit` until the reason clause is
479 : : * fully processed.
480 : : * @param propagated_lit The theory literal.
481 : : * @return The next literal of the reason clause, 0 to terminate the clause.
482 : : */
483 : 41 : int cb_add_reason_clause_lit(int propagated_lit) override
484 : : {
485 : 41 : ++d_stats.cbAddReasonClauseLit;
486 : : // Get reason for propagated_lit.
487 [ + + ]: 41 : if (!d_processing_reason)
488 : : {
489 [ - + ][ - + ]: 11 : Assert(d_reason.empty());
[ - - ]
490 : 11 : SatLiteral slit = toSatLiteral(propagated_lit);
491 : 11 : SatClause clause;
492 : 11 : d_proxy->explainPropagation(slit, clause);
493 : : // Add activation literal to reason
494 : 11 : SatLiteral alit = current_activation_lit();
495 [ + + ]: 11 : if (alit != undefSatLiteral)
496 : : {
497 : 4 : d_reason.push_back(alit);
498 : : }
499 : 11 : d_reason.insert(d_reason.end(), clause.begin(), clause.end());
500 : 11 : d_processing_reason = true;
501 [ + - ]: 22 : Trace("cadical::propagator")
502 : 11 : << "cb::reason: " << slit << ", size: " << d_reason.size()
503 : 11 : << std::endl;
504 : : }
505 : :
506 : : // We are done processing the reason for propagated_lit.
507 [ + + ]: 41 : if (d_reason.empty())
508 : : {
509 : 11 : d_processing_reason = false;
510 : 11 : return 0;
511 : : }
512 : :
513 : : // Return next literal of the reason for propagated_lit.
514 [ + - ]: 60 : Trace("cadical::propagator")
515 : 30 : << "cb::reason: " << toSatLiteral(propagated_lit) << " "
516 : 30 : << d_reason.front() << std::endl;
517 : 30 : int lit = toCadicalLit(d_reason.front());
518 : 30 : d_reason.pop_front();
519 : 30 : return lit;
520 : : }
521 : :
522 : : /**
523 : : * Callback of the SAT solver to determine if we have a new clause to add.
524 : : * @param forgettable True if clause is not irredundant.
525 : : * @return True to indicate that we have clauses to add.
526 : : */
527 : 178 : bool cb_has_external_clause(bool& is_forgettable) override
528 : : {
529 : 178 : ++d_stats.cbHasExternalClause;
530 : 178 : is_forgettable = false;
531 : 178 : return !d_new_clauses.empty();
532 : : }
533 : :
534 : : /**
535 : : * Callback of the SAT solver to add a new clause.
536 : : * @note This is called consecutively until the full clause is processed.
537 : : * @note Clauses are terminated with 0 in d_new_clauses.
538 : : * @return The next literal of the clause, 0 to terminate the clause.
539 : : */
540 : 251 : int cb_add_external_clause_lit() override
541 : : {
542 : 251 : ++d_stats.cbAddExternalClauseLit;
543 [ - + ][ - + ]: 251 : Assert(!d_new_clauses.empty());
[ - - ]
544 : 251 : CadicalLit lit = d_new_clauses.front();
545 : 251 : d_new_clauses.pop_front();
546 [ + - ]: 502 : Trace("cadical::propagator")
547 : 251 : << "external_clause: " << toSatLiteral(lit) << std::endl;
548 : 251 : return lit;
549 : : }
550 : :
551 : : /**
552 : : * Get the current trail of decisions.
553 : : * @return The trail of decisions.
554 : : */
555 : 0 : const std::vector<SatLiteral>& get_decisions() const { return d_decisions; }
556 : :
557 : : /**
558 : : * Get the current assignment of lit.
559 : : *
560 : : * Note: This does not query d_solver->val() since this can only be queried
561 : : * if the SAT solver is in a SAT state, which is not the case during solving.
562 : : *
563 : : * @param lit SatLiteral to be queried.
564 : : * @return Current value of given literal on the trail.
565 : : */
566 : 401 : SatValue value(SatLiteral lit) const
567 : : {
568 : 401 : SatVariable var = lit.getSatVariable();
569 : 401 : SatValue val = SAT_VALUE_UNKNOWN;
570 : 401 : int32_t assign = d_var_info[var].assignment;
571 [ + + ]: 401 : if (assign != 0)
572 : : {
573 [ + + ]: 258 : val = toSatValueLit(lit.isNegated() ? -assign : assign);
574 : : }
575 [ + - ]: 802 : Trace("cadical::propagator")
576 : 401 : << "value: " << lit << ": " << val << std::endl;
577 : 401 : return val;
578 : : }
579 : :
580 : : /**
581 : : * Adds a new clause to the propagator.
582 : : *
583 : : * The clause will not immediately added to the SAT solver, but instead
584 : : * will be added through the `cb_add_external_clause_lit` callback.
585 : : *
586 : : * Note: Filters out clauses satisfied by fixed literals.
587 : : *
588 : : * @param clause The clause to add.
589 : : */
590 : 215 : void add_clause(const SatClause& clause)
591 : : {
592 : 215 : std::vector<CadicalLit> lits;
593 [ + + ]: 424 : for (const SatLiteral& lit : clause)
594 : : {
595 : 302 : SatVariable var = lit.getSatVariable();
596 [ - + ][ - + ]: 302 : Assert(var < d_var_info.size());
[ - - ]
597 : 302 : const auto& info = d_var_info[var];
598 [ - + ][ - + ]: 302 : Assert(info.is_active);
[ - - ]
599 [ + + ]: 302 : if (info.is_fixed)
600 : : {
601 [ + + ]: 138 : int32_t val = lit.isNegated() ? -info.assignment : info.assignment;
602 [ - + ][ - + ]: 138 : Assert(val != 0);
[ - - ]
603 [ + + ]: 138 : if (val > 0)
604 : : {
605 : : // Clause satisfied by fixed literal, no clause added
606 : 93 : return;
607 : : }
608 : : }
609 : 209 : lits.push_back(toCadicalLit(lit));
610 : : }
611 [ + - ]: 122 : if (!lits.empty())
612 : : {
613 : : // Add activation literal to clause if we are in user level > 0
614 : 122 : SatLiteral alit = current_activation_lit();
615 [ + + ]: 122 : if (alit != undefSatLiteral)
616 : : {
617 : 38 : lits.insert(lits.begin(), toCadicalLit(alit));
618 : : }
619 : : // Do not immediately add clauses added during search. We have to buffer
620 : : // them and add them during the cb_add_reason_clause_lit callback.
621 [ + + ]: 122 : if (d_in_search)
622 : : {
623 : 55 : d_new_clauses.insert(d_new_clauses.end(), lits.begin(), lits.end());
624 : 55 : d_new_clauses.push_back(0);
625 : : }
626 : : else
627 : : {
628 [ + + ]: 168 : for (const auto& lit : lits)
629 : : {
630 : 101 : d_solver.add(lit);
631 : : }
632 : 67 : d_solver.add(0);
633 : : }
634 : : }
635 : : }
636 : :
637 : : /**
638 : : * Add new CaDiCaL variable.
639 : : * @param var The variable to add.
640 : : * @param level The current user assertion level.
641 : : * @param is_theory_atom True if variable is a theory atom.
642 : : * @param in_search True if SAT solver is currently in search().
643 : : */
644 : 150 : void add_new_var(const SatVariable& var, bool is_theory_atom)
645 : : {
646 : : // Since activation literals are not tracked here, we have to make sure to
647 : : // properly resize d_var_info.
648 [ - + ]: 150 : if (var > d_var_info.size())
649 : : {
650 : 0 : d_var_info.resize(var);
651 : : }
652 [ - + ][ - + ]: 150 : Assert(d_var_info.size() == var);
[ - - ]
653 : :
654 : : // Boolean variables are not theory atoms, but may still occur in
655 : : // lemmas/conflicts sent to the SAT solver. Hence, we have to observe them
656 : : // since CaDiCaL expects all literals sent back to be observed.
657 : 150 : d_solver.add_observed_var(toCadicalVar(var));
658 : 150 : d_active_vars.push_back(var);
659 [ + - ]: 300 : Trace("cadical::propagator")
660 : 150 : << "new var: " << var << " (level: " << current_user_level()
661 : 0 : << ", is_theory_atom: " << is_theory_atom
662 : 150 : << ", in_search: " << d_in_search << ")" << std::endl;
663 : 150 : auto& info = d_var_info.emplace_back();
664 : 150 : info.level_intro = current_user_level();
665 : 150 : info.is_theory_atom = is_theory_atom;
666 : 150 : }
667 : :
668 : : /**
669 : : * Checks whether the theory engine is done, no new clauses need to be added
670 : : * and the current model is consistent.
671 : : */
672 : 47 : bool done() const
673 : : {
674 [ + + ]: 47 : if (!d_new_clauses.empty())
675 : : {
676 [ + - ]: 15 : Trace("cadical::propagator") << "not done: pending clauses" << std::endl;
677 : 15 : return false;
678 : : }
679 [ - + ]: 32 : if (d_proxy->theoryNeedCheck())
680 : : {
681 [ - - ]: 0 : Trace("cadical::propagator")
682 : 0 : << "not done: theory need check" << std::endl;
683 : 0 : return false;
684 : : }
685 [ + + ]: 32 : if (d_found_solution)
686 : : {
687 [ + - ]: 4 : Trace("cadical::propagator")
688 : 2 : << "done: found partial solution" << std::endl;
689 : : }
690 : : else
691 : : {
692 [ + - ]: 60 : Trace("cadical::propagator")
693 : 30 : << "done: full assignment consistent" << std::endl;
694 : : }
695 : 32 : return true;
696 : : }
697 : :
698 : : /**
699 : : * Push user assertion level.
700 : : */
701 : 20 : void user_push()
702 : : {
703 [ + - ]: 40 : Trace("cadical::propagator")
704 : 20 : << "user push: " << d_active_vars_control.size();
705 : 20 : d_active_vars_control.push_back(d_active_vars.size());
706 [ + - ]: 40 : Trace("cadical::propagator")
707 : 20 : << " -> " << d_active_vars_control.size() << std::endl;
708 : 20 : }
709 : :
710 : : /**
711 : : * Set the activation literal for the current user assertion level.
712 : : *
713 : : * @param alit The activation literal for the current user assertion level.
714 : : */
715 : 20 : void set_activation_lit(SatVariable& alit)
716 : : {
717 : 20 : d_activation_literals.push_back(alit);
718 [ + - ]: 40 : Trace("cadical::propagator")
719 : 20 : << "enable activation lit: " << alit << std::endl;
720 : 20 : }
721 : :
722 : : /**
723 : : * Pop user assertion level.
724 : : */
725 : 20 : void user_pop()
726 : : {
727 [ + - ]: 40 : Trace("cadical::propagator")
728 : 20 : << "user pop: " << d_active_vars_control.size();
729 : 20 : size_t pop_to = d_active_vars_control.back();
730 : 20 : d_active_vars_control.pop_back();
731 [ + - ]: 40 : Trace("cadical::propagator")
732 : 20 : << " -> " << d_active_vars_control.size() << std::endl;
733 : :
734 : : // Disable activation literal for popped user level. The activation literal
735 : : // is added as unit clause, which will satisfy all clauses added in this
736 : : // user level and get garbage collected in the SAT solver.
737 : 20 : SatLiteral alit = current_activation_lit();
738 [ + - ]: 40 : Trace("cadical::propagator")
739 : 20 : << "disable activation lit: " << alit << std::endl;
740 : 20 : d_activation_literals.pop_back();
741 : :
742 : 20 : size_t user_level = current_user_level();
743 : :
744 : : // Unregister popped variables so that CaDiCaL does not notify us anymore
745 : : // about assignments.
746 [ - + ][ - + ]: 20 : Assert(pop_to <= d_active_vars.size());
[ - - ]
747 : 40 : std::vector<SatVariable> fixed;
748 [ + + ]: 61 : while (d_active_vars.size() > pop_to)
749 : : {
750 : 41 : SatVariable var = d_active_vars.back();
751 : 41 : const auto& info = d_var_info[var];
752 : 41 : d_active_vars.pop_back();
753 : :
754 : : // We keep fixed literals that correspond to theory atoms introduced in
755 : : // lower user levels, since we have to renotify them before the next
756 : : // solve call.
757 [ + + ][ - + ]: 41 : if (info.is_fixed && info.is_theory_atom
758 [ - - ]: 0 : && info.level_intro <= user_level)
759 : : {
760 : 0 : fixed.push_back(var);
761 : : }
762 : : else
763 : : {
764 [ + - ]: 41 : Trace("cadical::propagator") << "set inactive: " << var << std::endl;
765 : 41 : d_var_info[var].is_active = false;
766 : 41 : d_solver.remove_observed_var(toCadicalVar(var));
767 [ - + ][ - + ]: 41 : Assert(info.level_intro > user_level);
[ - - ]
768 : : // Fix value of inactive variables in order to avoid CaDiCaL from
769 : : // deciding on them again. This make a huge difference in performance
770 : : // for incremental problems with many check-sat calls.
771 : 41 : d_solver.add(toCadicalLit(var));
772 : 41 : d_solver.add(0);
773 : : }
774 : : }
775 : : // Re-add fixed active vars in the order they were added to d_active_vars.
776 : 20 : d_active_vars.insert(d_active_vars.end(), fixed.rbegin(), fixed.rend());
777 : :
778 : : // We are at decicion level 0 at this point.
779 [ - + ][ - + ]: 20 : Assert(d_decisions.empty());
[ - - ]
780 [ - + ][ - + ]: 20 : Assert(d_assignment_control.empty());
[ - - ]
781 : : // At this point, only fixed literals will be on d_assignments, now we have
782 : : // to determine which of these are still relevant in the current user
783 : : // level. If the variable is still active here, it means that it is still
784 : : // relevant for the current user level. If its assignment was fixed in a
785 : : // higher user level, we have to renotify the fixed literal in the current
786 : : // level (or in the user level of the next solve call). This happens by
787 : : // pushing the literal onto the d_renotify_fixed vector.
788 : 20 : auto it = d_assignments.begin();
789 [ + + ]: 112 : while (it != d_assignments.end())
790 : : {
791 : 92 : SatLiteral lit = *it;
792 : 92 : auto& info = d_var_info[lit.getSatVariable()];
793 [ - + ][ - + ]: 92 : Assert(info.is_fixed);
[ - - ]
794 : :
795 : : // Remove inactive variables from the assignment vector.
796 [ + + ]: 92 : if (!info.is_active)
797 : : {
798 : 9 : it = d_assignments.erase(it);
799 : 9 : continue;
800 : : }
801 : :
802 : : // Renotify fixed literals if it was fixed in a higher user level.
803 [ + + ][ - + ]: 83 : if (info.is_theory_atom && info.level_fixed > user_level)
804 : : {
805 [ - - ]: 0 : Trace("cadical::propagator")
806 : 0 : << "queue renotify: " << lit
807 : 0 : << " (level_intro: " << info.level_intro
808 : 0 : << ", level_fixed: " << info.level_fixed << ")" << std::endl;
809 : 0 : d_renotify_fixed.push_back(lit);
810 : : }
811 : 83 : ++it;
812 : : }
813 : 20 : }
814 : :
815 : 0 : bool is_fixed(SatVariable var) const { return d_var_info[var].is_fixed; }
816 : :
817 : : /**
818 : : * Configure and record preferred phase of variable.
819 : : * @param lit The literal.
820 : : */
821 : 2 : void phase(SatLiteral lit)
822 : : {
823 : 2 : d_solver.phase(toCadicalLit(lit));
824 [ - + ]: 2 : d_var_info[lit.getSatVariable()].phase = lit.isNegated() ? -1 : 1;
825 : 2 : }
826 : :
827 : : /**
828 : : * Return the activation literal for the current user level.
829 : : *
830 : : * Note: Returns undefSatLiteral at user level 0.
831 : : */
832 : 153 : const SatLiteral& current_activation_lit()
833 : : {
834 [ + + ]: 153 : if (d_activation_literals.empty())
835 : : {
836 : 91 : return undefSatLiteral;
837 : : }
838 : 62 : return d_activation_literals.back();
839 : : }
840 : :
841 : : /** Return the current user (assertion) level. */
842 : 427 : size_t current_user_level() const { return d_active_vars_control.size(); }
843 : :
844 : : /** Return the current list of activation literals. */
845 : 33 : const std::vector<SatLiteral>& activation_literals()
846 : : {
847 : 33 : return d_activation_literals;
848 : : }
849 : :
850 : : /**
851 : : * Renotify fixed literals in the current user level.
852 : : *
853 : : * This is done prior to a new solve() call and ensures that fixed literals
854 : : * are enqueued in the theory proxy. This is needed since the SAT solver does
855 : : * not re-notify us about fixed literals.
856 : : */
857 : 33 : void renotify_fixed()
858 : : {
859 : 33 : ++d_stats.renotifyFixed;
860 [ - + ]: 33 : for (const auto& lit : d_renotify_fixed)
861 : : {
862 [ - - ]: 0 : Trace("cadical::propagator")
863 : 0 : << "re-enqueue (user pop): " << lit << std::endl;
864 : : // Make sure to pre-register the re-enqueued theory literal
865 : 0 : d_proxy->notifySatLiteral(d_proxy->getNode(lit));
866 : : // Re-enqueue fixed theory literal
867 : 0 : d_proxy->enqueueTheoryLiteral(lit);
868 : : // We are notifying fixed literals at the current user level, update the
869 : : // level at which the variable was fixed, so that it will be renotified,
870 : : // if needed in lower user levels.
871 : 0 : d_var_info[lit.getSatVariable()].level_fixed = current_user_level();
872 : 0 : ++d_stats.renotifyFixedLit;
873 : : }
874 : 33 : d_renotify_fixed.clear();
875 : 33 : }
876 : :
877 : : /** Set d_in_search flag to indicate whether solver is currently in search. */
878 : 66 : void in_search(bool flag) { d_in_search = flag; }
879 : :
880 : : private:
881 : : /** Retrieve theory propagations and add them to the propagations list. */
882 : 160 : void theory_propagate()
883 : : {
884 : 320 : SatClause propagated_lits;
885 : 160 : d_proxy->theoryPropagate(propagated_lits);
886 [ + - ]: 320 : Trace("cadical::propagator")
887 : 160 : << "new propagations: " << propagated_lits.size() << std::endl;
888 : :
889 [ + + ]: 221 : for (const auto& lit : propagated_lits)
890 : : {
891 [ + - ]: 61 : Trace("cadical::propagator") << "new propagation: " << lit << std::endl;
892 : 61 : d_propagations.push_back(lit);
893 : : }
894 : 160 : }
895 : :
896 : : /**
897 : : * Get next propagation.
898 : : *
899 : : * @return Return next propagation queued in d_propagations.
900 : : */
901 : 130 : int next_propagation()
902 : : {
903 [ + + ]: 130 : if (d_propagations.empty())
904 : : {
905 : 79 : return 0;
906 : : }
907 : 51 : SatLiteral next = d_propagations.front();
908 : 51 : d_propagations.pop_front();
909 [ + - ]: 51 : Trace("cadical::propagator") << "propagate: " << next << std::endl;
910 : 51 : return toCadicalLit(next);
911 : : }
912 : :
913 : : /** The associated theory proxy. */
914 : : prop::TheoryProxy* d_proxy = nullptr;
915 : :
916 : : /** The SAT context. */
917 : : context::Context& d_context;
918 : : CaDiCaL::Solver& d_solver;
919 : :
920 : : /** Struct to store information on variables. */
921 : : struct VarInfo
922 : : {
923 : : uint32_t level_intro = 0; // user level at which variable was created
924 : : uint32_t level_fixed = 0; // user level at which variable was fixed
925 : : bool is_theory_atom = false; // is variable a theory atom
926 : : bool is_fixed = false; // has variable fixed assignment
927 : : bool is_active = true; // is variable active
928 : : int32_t assignment = 0; // current variable assignment
929 : : int8_t phase = 0; // preferred phase
930 : : };
931 : : /** Maps SatVariable to corresponding info struct. */
932 : : std::vector<VarInfo> d_var_info;
933 : :
934 : : /**
935 : : * Currently active variables, can get inactive on user pops.
936 : : * Dependent on user context.
937 : : */
938 : : std::vector<SatVariable> d_active_vars;
939 : : /**
940 : : * Control stack to mananage d_active_vars on user pop.
941 : : *
942 : : * Note: We do not use a User-context-dependent CDList here, since we neeed
943 : : * to know which variables are popped and thus become inactive.
944 : : */
945 : : std::vector<size_t> d_active_vars_control;
946 : :
947 : : /**
948 : : * Current activation literals.
949 : : *
950 : : * For each user level, we push a fresh activation literal to the vector (in
951 : : * user_pop()). Activation literals get removed and disabled in user_pop().
952 : : * The size of the vector corresponds to the current user level.
953 : : *
954 : : * The activation literals corrsponding to the current user level gets
955 : : * automtically added to each clause added in this user level. With
956 : : * activation literals we can simulate push/pop of clauses in the SAT solver.
957 : : */
958 : : std::vector<SatLiteral> d_activation_literals;
959 : :
960 : : /** List of fixed literals to be re-notified in lower user level. */
961 : : std::vector<SatLiteral> d_renotify_fixed;
962 : :
963 : : /**
964 : : * Variable assignment notifications.
965 : : *
966 : : * Used to unassign variables on backtrack.
967 : : */
968 : : std::vector<SatLiteral> d_assignments;
969 : : /**
970 : : * Control stack to manage d_assignments when backtracking on SAT level.
971 : : *
972 : : * Note: We do not use a SAT-context-depenent CDList for d_assignments, since
973 : : * we need to know which non-fixed variables are unassigned on
974 : : * backtrack.
975 : : */
976 : : std::vector<size_t> d_assignment_control;
977 : :
978 : : /**
979 : : * Stores all observed decision variables.
980 : : *
981 : : * Note: May contain undefSatLiteral for unobserved decision variables.
982 : : */
983 : : std::vector<SatLiteral> d_decisions;
984 : :
985 : : /** Used by cb_propagate() to return propagated literals. */
986 : : std::deque<SatLiteral> d_propagations;
987 : :
988 : : /**
989 : : * Used by add_clause() to buffer added clauses, which will be added via
990 : : * cb_add_reason_clause_lit().
991 : : */
992 : : std::deque<CadicalLit> d_new_clauses;
993 : :
994 : : /**
995 : : * Flag indicating whether cb_add_reason_clause_lit() is currently
996 : : * processing a reason.
997 : : */
998 : : bool d_processing_reason = false;
999 : : /** Reason storage to process current reason in cb_add_reason_clause_lit(). */
1000 : : std::deque<SatLiteral> d_reason;
1001 : :
1002 : : bool d_found_solution = false;
1003 : :
1004 : : /** Flag indicating if SAT solver is in search(). */
1005 : : bool d_in_search = false;
1006 : :
1007 : : struct Statistics
1008 : : {
1009 : 15 : Statistics(StatisticsRegistry& stats)
1010 : 15 : : renotifyFixed(
1011 : 15 : stats.registerInt("cadical::propagator::renotify_fixed")),
1012 : : renotifyFixedLit(
1013 : 15 : stats.registerInt("cadical::propagator::renotify_fixed_lit")),
1014 : : notifyAssignment(
1015 : 15 : stats.registerInt("cadical::propagator::notify_assignment")),
1016 : : notifyFixedAssignment(stats.registerInt(
1017 : 15 : "cadical::propagator::notify_fixed_assignment")),
1018 : : notifyNewDecision(
1019 : 15 : stats.registerInt("cadical::propagator::notify_new_decision")),
1020 : : notifyBacktrack(
1021 : 15 : stats.registerInt("cadical::propagator::notify_backtrack")),
1022 : : cbCheckFoundModel(
1023 : 15 : stats.registerInt("cadical::propagator::cb_check_found_model")),
1024 : 15 : cbDecide(stats.registerInt("cadical::propagator::cb_decide")),
1025 : 15 : cbPropagate(stats.registerInt("cadical::propagator::cb_propagate")),
1026 : : cbAddReasonClauseLit(stats.registerInt(
1027 : 15 : "cadical::propagator::cb_add_reason_clause_lit")),
1028 : : cbHasExternalClause(
1029 : 15 : stats.registerInt("cadical::propagator::cb_has_external_clause")),
1030 : : cbAddExternalClauseLit(stats.registerInt(
1031 : 15 : "cadical::propagator::cb_add_external_clause_lit"))
1032 : : {
1033 : 15 : }
1034 : : IntStat renotifyFixed;
1035 : : IntStat renotifyFixedLit;
1036 : : IntStat notifyAssignment;
1037 : : IntStat notifyFixedAssignment;
1038 : : IntStat notifyNewDecision;
1039 : : IntStat notifyBacktrack;
1040 : : IntStat cbCheckFoundModel;
1041 : : IntStat cbDecide;
1042 : : IntStat cbPropagate;
1043 : : IntStat cbAddReasonClauseLit;
1044 : : IntStat cbHasExternalClause;
1045 : : IntStat cbAddExternalClauseLit;
1046 : : } d_stats;
1047 : : };
1048 : :
1049 : : class ClauseLearner : public CaDiCaL::Learner
1050 : : {
1051 : : public:
1052 : 1 : ClauseLearner(TheoryProxy& proxy, int32_t clause_size)
1053 : 1 : : d_proxy(proxy), d_max_clause_size(clause_size)
1054 : : {
1055 : 1 : }
1056 : 2 : ~ClauseLearner() override {}
1057 : :
1058 : 1 : bool learning(int size) override
1059 : : {
1060 [ - + ][ - - ]: 1 : return d_max_clause_size == 0 || size <= d_max_clause_size;
1061 : : }
1062 : :
1063 : 2 : void learn(int lit) override
1064 : : {
1065 [ + + ]: 2 : if (lit)
1066 : : {
1067 : 1 : SatLiteral slit = toSatLiteral(lit);
1068 : 1 : d_clause.push_back(slit);
1069 : : }
1070 : : else
1071 : : {
1072 : 1 : d_proxy.notifySatClause(d_clause);
1073 : 1 : d_clause.clear();
1074 : : }
1075 : 2 : }
1076 : :
1077 : : private:
1078 : : TheoryProxy& d_proxy;
1079 : : /** Intermediate literals buffer. */
1080 : : std::vector<SatLiteral> d_clause;
1081 : : /** Maximum size of clauses to get notified about. */
1082 : : int32_t d_max_clause_size;
1083 : : };
1084 : :
1085 : 40099 : CadicalSolver::CadicalSolver(Env& env,
1086 : : StatisticsRegistry& registry,
1087 : 40099 : const std::string& name)
1088 : : : EnvObj(env),
1089 : 40099 : d_solver(new CaDiCaL::Solver()),
1090 : 40099 : d_context(context()),
1091 : : // Note: CaDiCaL variables start with index 1 rather than 0 since negated
1092 : : // literals are represented as the negation of the index.
1093 : : d_nextVarIdx(1),
1094 : : d_inSatMode(false),
1095 : 120297 : d_statistics(registry, name)
1096 : : {
1097 : 40099 : }
1098 : :
1099 : 40099 : void CadicalSolver::init()
1100 : : {
1101 : 40099 : d_solver->set("quiet", 1); // CaDiCaL is verbose by default
1102 : :
1103 : : // walk and lucky phase do not use the external propagator, disable for now
1104 [ + + ]: 40099 : if (d_propagator)
1105 : : {
1106 : 15 : d_solver->set("walk", 0);
1107 : 15 : d_solver->set("lucky", 0);
1108 : : // ilb currently does not play well with user propagators
1109 : 15 : d_solver->set("ilb", 0);
1110 : 15 : d_solver->set("ilbassumptions", 0);
1111 [ + - ]: 15 : d_solver->connect_fixed_listener(d_propagator.get());
1112 : 15 : d_solver->connect_external_propagator(d_propagator.get());
1113 : : }
1114 : :
1115 : 40099 : d_true = newVar();
1116 : 40099 : d_false = newVar();
1117 : 40099 : d_solver->add(toCadicalVar(d_true));
1118 : 40099 : d_solver->add(0);
1119 : 40099 : d_solver->add(-toCadicalVar(d_false));
1120 : 40099 : d_solver->add(0);
1121 : :
1122 : 40099 : bool logProofs = false;
1123 : : // TODO (wishue #154): determine how to initialize the proofs for CaDiCaL
1124 : : // here based on d_env.isSatProofProducing and options().proof.propProofMode.
1125 : : // The latter should be extended to include modes DRAT and LRAT based on
1126 : : // what is available here.
1127 [ - + ]: 40099 : if (logProofs)
1128 : : {
1129 : 0 : d_pfFile = options().driver.filename + ".drat_proof.txt";
1130 [ - - ]: 0 : if (!options().proof.dratBinaryFormat)
1131 : : {
1132 : 0 : d_solver->set("binary", 0);
1133 : : }
1134 : 0 : d_solver->set("inprocessing", 0);
1135 : 0 : d_solver->trace_proof(d_pfFile.c_str());
1136 : : }
1137 : 40099 : }
1138 : :
1139 : 79702 : CadicalSolver::~CadicalSolver() {}
1140 : :
1141 : : /**
1142 : : * Terminator class that notifies CaDiCaL to terminate when the resource limit
1143 : : * is reached (used for resource limits specified via --rlimit or --tlimit).
1144 : : */
1145 : : class ResourceLimitTerminator : public CaDiCaL::Terminator
1146 : : {
1147 : : public:
1148 : 40099 : ResourceLimitTerminator(ResourceManager& resmgr) : d_resmgr(resmgr){};
1149 : :
1150 : 829916 : bool terminate() override
1151 : : {
1152 : 829916 : d_resmgr.spendResource(Resource::BvSatStep);
1153 : 829916 : return d_resmgr.out();
1154 : : }
1155 : :
1156 : : private:
1157 : : ResourceManager& d_resmgr;
1158 : : };
1159 : :
1160 : 40099 : void CadicalSolver::setResourceLimit(ResourceManager* resmgr)
1161 : : {
1162 : 40099 : d_terminator.reset(new ResourceLimitTerminator(*resmgr));
1163 : 40099 : d_solver->connect_terminator(d_terminator.get());
1164 : 40099 : }
1165 : :
1166 : 68903 : SatValue CadicalSolver::_solve(const std::vector<SatLiteral>& assumptions)
1167 : : {
1168 [ + + ]: 68903 : if (d_propagator)
1169 : : {
1170 [ + - ]: 33 : Trace("cadical::propagator") << "solve start" << std::endl;
1171 : 33 : d_propagator->renotify_fixed();
1172 : : }
1173 : 68903 : TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
1174 : 68903 : d_assumptions.clear();
1175 [ + + ]: 68903 : if (d_propagator)
1176 : : {
1177 : : // Assume activation literals for all active user levels.
1178 [ + + ]: 53 : for (const auto& lit : d_propagator->activation_literals())
1179 : : {
1180 [ + - ]: 40 : Trace("cadical::propagator")
1181 : 20 : << "assume activation lit: " << ~lit << std::endl;
1182 : 20 : d_solver->assume(toCadicalLit(~lit));
1183 : : }
1184 : : }
1185 : : SatValue res;
1186 [ + + ]: 7767900 : for (const SatLiteral& lit : assumptions)
1187 : : {
1188 [ - + ]: 7699000 : if (d_propagator)
1189 : : {
1190 [ - - ]: 0 : Trace("cadical::propagator") << "assume: " << lit << std::endl;
1191 : : }
1192 : 7699000 : d_solver->assume(toCadicalLit(lit));
1193 : 7699000 : d_assumptions.push_back(lit);
1194 : : }
1195 [ + + ]: 68903 : if (d_propagator)
1196 : : {
1197 : 33 : d_propagator->in_search(true);
1198 : : }
1199 : 68903 : res = toSatValue(d_solver->solve());
1200 [ + + ]: 68903 : if (d_propagator)
1201 : : {
1202 [ + + ][ - + ]: 33 : Assert(res != SAT_VALUE_TRUE || d_propagator->done());
[ - + ][ - - ]
1203 [ + - ]: 33 : Trace("cadical::propagator") << "solve done: " << res << std::endl;
1204 : 33 : d_propagator->in_search(false);
1205 : : }
1206 : 68903 : ++d_statistics.d_numSatCalls;
1207 : 68903 : d_inSatMode = (res == SAT_VALUE_TRUE);
1208 : 137806 : return res;
1209 : : }
1210 : :
1211 : : /* SatSolver Interface ------------------------------------------------------ */
1212 : :
1213 : 5588920 : ClauseId CadicalSolver::addClause(SatClause& clause, bool removable)
1214 : : {
1215 : 5588920 : if (d_propagator && TraceIsOn("cadical::propagator"))
1216 : : {
1217 [ - - ]: 0 : Trace("cadical::propagator") << "addClause (" << removable << "):";
1218 : 0 : SatLiteral alit = d_propagator->current_activation_lit();
1219 [ - - ]: 0 : if (alit != undefSatLiteral)
1220 : : {
1221 [ - - ]: 0 : Trace("cadical::propagator") << " " << alit;
1222 : : }
1223 [ - - ]: 0 : for (const SatLiteral& lit : clause)
1224 : : {
1225 [ - - ]: 0 : Trace("cadical::propagator") << " " << lit;
1226 : : }
1227 [ - - ]: 0 : Trace("cadical::propagator") << " 0" << std::endl;
1228 : : }
1229 : : // If we are currently in search, add clauses through the propagator.
1230 [ + + ]: 5588920 : if (d_propagator)
1231 : : {
1232 : 207 : d_propagator->add_clause(clause);
1233 : : }
1234 : : else
1235 : : {
1236 [ + + ]: 20807100 : for (const SatLiteral& lit : clause)
1237 : : {
1238 : 15218400 : d_solver->add(toCadicalLit(lit));
1239 : : }
1240 : 5588720 : d_solver->add(0);
1241 : : }
1242 : 5588920 : ++d_statistics.d_numClauses;
1243 : 5588920 : return ClauseIdError;
1244 : : }
1245 : :
1246 : 0 : ClauseId CadicalSolver::addXorClause(SatClause& clause,
1247 : : bool rhs,
1248 : : bool removable)
1249 : : {
1250 : 0 : Unreachable() << "CaDiCaL does not support adding XOR clauses.";
1251 : : return 0;
1252 : : }
1253 : :
1254 : 1507890 : SatVariable CadicalSolver::newVar(bool isTheoryAtom, bool canErase)
1255 : : {
1256 : 1507890 : ++d_statistics.d_numVariables;
1257 [ + + ]: 1507890 : if (d_propagator)
1258 : : {
1259 : 150 : d_propagator->add_new_var(d_nextVarIdx, isTheoryAtom);
1260 : : }
1261 : 1507890 : return d_nextVarIdx++;
1262 : : }
1263 : :
1264 : 111 : SatVariable CadicalSolver::trueVar() { return d_true; }
1265 : :
1266 : 237 : SatVariable CadicalSolver::falseVar() { return d_false; }
1267 : :
1268 : 33 : SatValue CadicalSolver::solve() { return _solve({}); }
1269 : :
1270 : 0 : SatValue CadicalSolver::solve(long unsigned int&)
1271 : : {
1272 : 0 : Unimplemented() << "Setting limits for CaDiCaL not supported yet";
1273 : : return SatValue::SAT_VALUE_UNKNOWN;
1274 : : };
1275 : :
1276 : 68870 : SatValue CadicalSolver::solve(const std::vector<SatLiteral>& assumptions)
1277 : : {
1278 : 68870 : return _solve(assumptions);
1279 : : }
1280 : :
1281 : 0 : bool CadicalSolver::setPropagateOnly()
1282 : : {
1283 : 0 : d_solver->limit("decisions", 0); /* Gets reset after next solve() call. */
1284 : 0 : return true;
1285 : : }
1286 : :
1287 : 20076 : void CadicalSolver::getUnsatAssumptions(std::vector<SatLiteral>& assumptions)
1288 : : {
1289 [ + + ]: 7513920 : for (const SatLiteral& lit : d_assumptions)
1290 : : {
1291 [ + + ]: 7493840 : if (d_solver->failed(toCadicalLit(lit)))
1292 : : {
1293 : 153603 : assumptions.push_back(lit);
1294 : : }
1295 : : }
1296 : 20076 : }
1297 : :
1298 : 0 : void CadicalSolver::interrupt() { d_solver->terminate(); }
1299 : :
1300 : 401 : SatValue CadicalSolver::value(SatLiteral l) { return d_propagator->value(l); }
1301 : :
1302 : 552886 : SatValue CadicalSolver::modelValue(SatLiteral l)
1303 : : {
1304 [ - + ][ - + ]: 552886 : Assert(d_inSatMode);
[ - - ]
1305 : 552886 : auto val = d_solver->val(toCadicalLit(l.getSatVariable()));
1306 [ + + ]: 552886 : return toSatValueLit(l.isNegated() ? -val : val);
1307 : : }
1308 : :
1309 : 15 : uint32_t CadicalSolver::getAssertionLevel() const
1310 : : {
1311 [ - + ][ - + ]: 15 : Assert(d_propagator);
[ - - ]
1312 : 15 : return d_propagator->current_user_level();
1313 : : }
1314 : :
1315 : 0 : bool CadicalSolver::ok() const { return d_inSatMode; }
1316 : :
1317 : 40099 : CadicalSolver::Statistics::Statistics(StatisticsRegistry& registry,
1318 : 40099 : const std::string& prefix)
1319 : 40099 : : d_numSatCalls(registry.registerInt(prefix + "cadical::calls_to_solve")),
1320 : 40099 : d_numVariables(registry.registerInt(prefix + "cadical::variables")),
1321 : 40099 : d_numClauses(registry.registerInt(prefix + "cadical::clauses")),
1322 : 40099 : d_solveTime(registry.registerTimer(prefix + "cadical::solve_time"))
1323 : : {
1324 : 40099 : }
1325 : :
1326 : : /* CDCLTSatSolver Interface ------------------------------------------------- */
1327 : :
1328 : 15 : void CadicalSolver::initialize(prop::TheoryProxy* theoryProxy,
1329 : : PropPfManager* ppm)
1330 : : {
1331 : 15 : d_proxy = theoryProxy;
1332 : 15 : d_propagator.reset(new CadicalPropagator(
1333 : 15 : theoryProxy, d_context, *d_solver, statisticsRegistry()));
1334 [ + + ]: 15 : if (!d_env.getPlugins().empty())
1335 : : {
1336 : 1 : d_clause_learner.reset(new ClauseLearner(*theoryProxy, 0));
1337 : 1 : d_solver->connect_learner(d_clause_learner.get());
1338 : : }
1339 : :
1340 : 15 : init();
1341 : 15 : }
1342 : :
1343 : 20 : void CadicalSolver::push()
1344 : : {
1345 : 20 : d_context->push(); // SAT context for cvc5
1346 : : // Push new user level
1347 : 20 : d_propagator->user_push();
1348 : : // Set new activation literal for pushed user level
1349 : : // Note: This happens after the push to ensure that the activation literal's
1350 : : // introduction level is the current user level.
1351 : 20 : SatVariable alit = newVar(false);
1352 : 20 : d_propagator->set_activation_lit(alit);
1353 : 20 : }
1354 : :
1355 : 20 : void CadicalSolver::pop()
1356 : : {
1357 : 20 : d_context->pop(); // SAT context for cvc5
1358 : 20 : d_propagator->user_pop();
1359 : : // CaDiCaL issues notify_backtrack(0) when done, we don't have to call this
1360 : : // explicitly here
1361 : 20 : }
1362 : :
1363 : 33 : void CadicalSolver::resetTrail()
1364 : : {
1365 : : // Reset SAT context to decision level 0
1366 : 33 : d_propagator->notify_backtrack(0);
1367 : 33 : }
1368 : :
1369 : 2 : void CadicalSolver::preferPhase(SatLiteral lit)
1370 : : {
1371 [ + - ]: 2 : Trace("cadical::propagator") << "phase: " << lit << std::endl;
1372 : 2 : d_propagator->phase(lit);
1373 : 2 : }
1374 : :
1375 : 2 : bool CadicalSolver::isDecision(SatVariable var) const
1376 : : {
1377 : 2 : return d_solver->is_decision(toCadicalVar(var));
1378 : : }
1379 : :
1380 : 0 : bool CadicalSolver::isFixed(SatVariable var) const
1381 : : {
1382 [ - - ]: 0 : if (d_propagator)
1383 : : {
1384 : 0 : return d_propagator->is_fixed(var);
1385 : : }
1386 : 0 : return d_solver->fixed(toCadicalVar(var));
1387 : : }
1388 : :
1389 : 0 : std::vector<SatLiteral> CadicalSolver::getDecisions() const
1390 : : {
1391 : 0 : std::vector<SatLiteral> decisions;
1392 [ - - ]: 0 : for (SatLiteral lit : d_propagator->get_decisions())
1393 : : {
1394 [ - - ]: 0 : if (lit != 0)
1395 : : {
1396 : 0 : decisions.push_back(lit);
1397 : : }
1398 : : }
1399 : 0 : return decisions;
1400 : : }
1401 : :
1402 : 0 : std::vector<Node> CadicalSolver::getOrderHeap() const { return {}; }
1403 : :
1404 : 0 : std::shared_ptr<ProofNode> CadicalSolver::getProof()
1405 : : {
1406 : : // NOTE: we could return a DRAT_REFUTATION or LRAT_REFUTATION proof node
1407 : : // consisting of a single step, referencing the files for the DIMACS + proof.
1408 : : // do not throw an exception, since we test whether the proof is available
1409 : : // by comparing it to nullptr.
1410 : 0 : return nullptr;
1411 : : }
1412 : :
1413 : : /* -------------------------------------------------------------------------- */
1414 : : } // namespace prop
1415 : : } // namespace cvc5::internal
|
