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