Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * CDCL(T) IPASIRUP propagator for CaDiCaL.
11 : : */
12 : : #include "prop/cadical/cdclt_propagator.h"
13 : :
14 : : namespace cvc5::internal::prop::cadical {
15 : :
16 : 79 : CadicalPropagator::CadicalPropagator(prop::TheoryProxy* proxy,
17 : : context::Context* context,
18 : : CaDiCaL::Solver& solver,
19 : 79 : StatisticsRegistry& stats)
20 : 79 : : d_proxy(proxy), d_context(*context), d_solver(solver), d_stats(stats)
21 : : {
22 : 79 : d_var_info.emplace_back(); // 0: Not used
23 : 79 : }
24 : :
25 : 37978 : void CadicalPropagator::notify_assignment(const std::vector<int>& lits)
26 : : {
27 [ + - ][ - + ]: 37978 : if (Trace("cadical::propagator").isConnected())
28 : : {
29 [ - - ]: 0 : Trace("cadical::propagator") << "notif::assignments: { ";
30 [ - - ]: 0 : for (auto lit : lits)
31 : : {
32 [ - - ]: 0 : Trace("cadical::propagator") << lit << " ";
33 : : }
34 [ - - ]: 0 : Trace("cadical::propagator") << "}" << std::endl;
35 : : }
36 : 37978 : ++d_stats.notifyAssignment;
37 : :
38 [ + + ]: 37978 : if (d_found_solution)
39 : : {
40 : 13 : return;
41 : : }
42 : :
43 [ + + ]: 99879 : for (const auto& lit : lits)
44 : : {
45 : 61914 : SatLiteral slit = toSatLiteral(lit);
46 : 61914 : SatVariable var = slit.getSatVariable();
47 [ - + ][ - + ]: 61914 : Assert(var < d_var_info.size());
[ - - ]
48 : :
49 : 61914 : auto& info = d_var_info[var];
50 : :
51 : : // Only consider active variables
52 [ - + ]: 61914 : if (!info.is_active)
53 : : {
54 : 0 : continue;
55 : : }
56 : :
57 : 61914 : bool is_decision = d_solver.is_decision(lit);
58 : :
59 [ + - ]: 123828 : Trace("cadical::propagator")
60 [ - - ]: 0 : << "notif::assignment: [" << (is_decision ? "d" : "p") << "] " << slit
61 : 0 : << " (level: " << d_decisions.size()
62 : 0 : << ", level_intro: " << info.level_intro
63 : 61914 : << ", level_user: " << current_user_level() << ")" << std::endl;
64 : :
65 : : // Save decision variables
66 [ + + ]: 61914 : if (is_decision)
67 : : {
68 : 10268 : d_decisions.back() = slit;
69 : : }
70 : :
71 [ + + ][ + - ]: 61914 : Assert(info.assignment == 0 || info.assignment == lit);
[ - + ][ - + ]
[ - - ]
72 : :
73 : : // Only notify theory proxy if variable was assigned a new value, not if
74 : : // it got fixed after assignment already happend.
75 [ + + ]: 61914 : if (info.assignment == 0)
76 : : {
77 : 60697 : info.assignment = lit;
78 : 60697 : d_assignments.push_back(slit);
79 [ + + ]: 60697 : if (info.is_theory_atom)
80 : : {
81 [ + - ]: 59486 : Trace("cadical::propagator") << "enqueue: " << slit << std::endl;
82 [ + - ]: 118972 : Trace("cadical::propagator")
83 [ - + ][ - - ]: 59486 : << "node: " << d_proxy->getNode(slit) << std::endl;
84 : 59486 : d_proxy->enqueueTheoryLiteral(slit);
85 : : }
86 : : }
87 : : }
88 : : }
89 : :
90 : 1243 : void CadicalPropagator::notify_fixed_assignment(int lit)
91 : : {
92 : 1243 : SatLiteral slit = toSatLiteral(lit);
93 : 1243 : SatVariable var = slit.getSatVariable();
94 : :
95 : : // We don't care about non-observed variables
96 [ - + ]: 1243 : if (var >= d_var_info.size())
97 : : {
98 : 51 : return;
99 : : }
100 : :
101 : 1243 : auto& info = d_var_info[var];
102 : : // Only consider active variables
103 [ + + ]: 1243 : if (!info.is_active)
104 : : {
105 : 51 : return;
106 : : }
107 : 1192 : ++d_stats.notifyFixedAssignment;
108 : :
109 [ + - ]: 2384 : Trace("cadical::propagator")
110 : 1192 : << "notif::fixed assignment: " << slit << std::endl;
111 : :
112 : : // Mark as fixed.
113 [ - + ][ - + ]: 1192 : Assert(!info.is_fixed);
[ - - ]
114 : 1192 : info.is_fixed = true;
115 : 1192 : info.level_fixed = current_user_level();
116 : : // Trigger actual assignment.
117 : 1192 : notify_assignment({lit});
118 : : }
119 : :
120 : 17033 : void CadicalPropagator::notify_new_decision_level()
121 : : {
122 : 17033 : d_context.push();
123 : 17033 : d_assignment_control.push_back(d_assignments.size());
124 : 17033 : d_decisions.emplace_back();
125 [ + - ]: 34066 : Trace("cadical::propagator")
126 : 17033 : << "notif::decision: new level " << d_decisions.size() << std::endl;
127 : 17033 : ++d_stats.notifyNewDecision;
128 : 17033 : }
129 : :
130 : 16196 : void CadicalPropagator::notify_backtrack(size_t level)
131 : : {
132 [ + - ]: 16196 : Trace("cadical::propagator") << "notif::backtrack: " << level << std::endl;
133 : :
134 : : // CaDiCaL may notify us about backtracks of decisions that we were not
135 : : // notified about. We can safely ignore them.
136 [ + + ]: 16196 : if (d_decisions.size() <= level)
137 : : {
138 [ - + ][ - + ]: 79 : Assert(d_decisions.size() == 0);
[ - - ]
139 : 79 : return;
140 : : }
141 : 16117 : d_found_solution = false;
142 : :
143 : : // Backtrack decisions
144 [ - + ][ - + ]: 16117 : Assert(d_decisions.size() > level);
[ - - ]
145 [ - + ][ - + ]: 16117 : Assert(d_context.getLevel() > level);
[ - - ]
146 [ + + ]: 33150 : for (size_t cur_level = d_decisions.size(); cur_level > level; --cur_level)
147 : : {
148 : 17033 : d_context.pop();
149 : 17033 : d_decisions.pop_back();
150 : : }
151 : :
152 : : // Backtrack assignments. Genuine decision-level assignments are undone,
153 : : // but fixed assignments are permanent (decision level 0): we keep them
154 : : // assigned and retain them in d_assignments so that the user_pop()
155 : : // renotification machinery still sees them (it relies on d_assignments
156 : : // holding exactly the fixed literals once we are back at decision level 0).
157 : : // The corresponding theory literals are re-enqueued below, after notifying
158 : : // the theory proxy about the backtrack.
159 [ - + ][ - + ]: 16117 : Assert(!d_assignment_control.empty());
[ - - ]
160 : 16117 : size_t pop_to = d_assignment_control[level];
161 : 16117 : d_assignment_control.resize(level);
162 : :
163 : 16117 : size_t keep = pop_to;
164 : 16117 : std::vector<SatLiteral> renotify;
165 [ + + ]: 75723 : for (size_t i = pop_to, n = d_assignments.size(); i < n; ++i)
166 : : {
167 : 59606 : SatLiteral lit = d_assignments[i];
168 : 59606 : SatVariable var = lit.getSatVariable();
169 : 59606 : auto& info = d_var_info[var];
170 [ + + ]: 59606 : if (info.is_fixed)
171 : : {
172 : : // Permanent assignment: keep it and retain it in d_assignments.
173 [ + - ]: 101 : Trace("cadical::propagator") << "keep fixed: " << var << std::endl;
174 : 101 : d_assignments[keep++] = lit;
175 [ + + ]: 101 : if (info.is_theory_atom)
176 : : {
177 : 65 : renotify.push_back(lit);
178 : : }
179 : : }
180 : : else
181 : : {
182 [ + - ]: 59505 : Trace("cadical::propagator") << "unassign: " << var << std::endl;
183 : 59505 : info.assignment = 0;
184 : : }
185 : : }
186 : 16117 : d_assignments.resize(keep);
187 : :
188 : : // Notify theory proxy about backtrack
189 : 16117 : d_proxy->notifyBacktrack();
190 : : // Re-enqueue fixed theory literals that got backtracked at the theory level
191 : : // but remain assigned at the SAT level. This must happen after
192 : : // notifyBacktrack(), otherwise the theory backtrack would discard them.
193 [ + + ]: 16182 : for (const SatLiteral& lit : renotify)
194 : : {
195 [ + - ]: 130 : Trace("cadical::propagator")
196 : 65 : << "re-enqueue (backtrack): " << lit << std::endl;
197 : 65 : d_proxy->enqueueTheoryLiteral(lit);
198 : : }
199 : : // Clear the propagations since they are not valid anymore.
200 : 16117 : d_propagations.clear();
201 : 16117 : ++d_stats.notifyBacktrack;
202 : :
203 [ + - ]: 16117 : Trace("cadical::propagator") << "notif::backtrack end" << std::endl;
204 : 16117 : }
205 : :
206 : 209 : bool CadicalPropagator::cb_check_found_model(
207 : : CVC5_UNUSED const std::vector<int>& model)
208 : : {
209 [ + - ]: 209 : Trace("cadical::propagator") << "cb::check_found_model" << std::endl;
210 : 209 : bool recheck = false;
211 : :
212 [ + + ]: 209 : if (d_found_solution)
213 : : {
214 : 7 : return true;
215 : : }
216 : :
217 : 202 : ++d_stats.cbCheckFoundModel;
218 : : // CaDiCaL may backtrack while importing clauses, which can result in some
219 : : // clauses not being processed. Make sure to add all clauses before
220 : : // checking the model.
221 [ + + ]: 202 : if (!d_new_clauses.empty())
222 : : {
223 [ + - ]: 18 : Trace("cadical::propagator") << "cb::check_found_model end: new "
224 : 0 : "variables added via theory decision"
225 : 9 : << std::endl;
226 : : // CaDiCaL expects us to be able to provide a reason for rejecting the
227 : : // model (it asserts that after this call, cb_has_external_clause()
228 : : // returns true). However, in this particular case, we want to force
229 : : // CaDiCaL to give us model values for the new variables that were
230 : : // introduced (to kick off the assignment notification machinery), we
231 : : // don't have a reason clause for rejecting the model. CaDiCaL's
232 : : // expectation will be weakened in the future to allow for this, but for
233 : : // now we simply add a tautology as reason to pacify CaDiCaL.
234 : 9 : d_new_clauses.push_back(1);
235 : 9 : d_new_clauses.push_back(-1);
236 : 9 : d_new_clauses.push_back(0);
237 : 9 : return false;
238 : : }
239 : :
240 : : // Check full model.
241 : : //
242 : : // First, we have to ensure that if the SAT solver determines sat without
243 : : // making any decisions, theory decisions are still requested until fixed
244 : : // point at least once since some modules, e.g., finite model finding, rely
245 : : // on this. Theory decisions may add new variables (while decisions
246 : : // requested by the decision engine will not). If new variables are added,
247 : : // we interrupt the check to force the SAT solver to extend the model with
248 : : // the new variables.
249 : 193 : size_t size = d_var_info.size();
250 : : bool requirePhase, stopSearch;
251 : 193 : d_proxy->getNextDecisionRequest(requirePhase, stopSearch);
252 [ - + ]: 193 : if (d_var_info.size() != size)
253 : : {
254 [ - - ]: 0 : Trace("cadical::propagator") << "cb::check_found_model end: new "
255 : 0 : "variables added via theory decision"
256 : 0 : << std::endl;
257 : 0 : return false;
258 : : }
259 : : // Theory engine may trigger a recheck, unless new variables were added
260 : : // during check. If so, we break out of the check and have the SAT solver
261 : : // extend the model with the new variables.
262 : : do
263 : : {
264 [ + - ]: 404 : Trace("cadical::propagator")
265 : 202 : << "full check (recheck: " << recheck << ")" << std::endl;
266 : 202 : d_proxy->theoryCheck(theory::Theory::Effort::EFFORT_FULL);
267 : 202 : theory_propagate();
268 [ + + ]: 266 : for (const SatLiteral& p : d_propagations)
269 : : {
270 [ + - ]: 128 : Trace("cadical::propagator")
271 : 64 : << "add propagation reason: " << p << std::endl;
272 : 64 : SatClause clause;
273 : 64 : d_proxy->explainPropagation(p, clause);
274 : 64 : add_clause(clause);
275 : 64 : }
276 : 202 : d_propagations.clear();
277 : :
278 [ + + ]: 202 : if (!d_new_clauses.empty())
279 : : {
280 : : // Will again call cb_check_found_model() after clauses were added.
281 : 166 : recheck = false;
282 : : }
283 : : else
284 : : {
285 : 36 : recheck = d_proxy->theoryNeedCheck();
286 : : }
287 [ + + ][ + + ]: 202 : } while (d_var_info.size() == size && recheck);
[ + + ]
288 : :
289 [ + + ]: 193 : if (d_var_info.size() != size)
290 : : {
291 [ + - ]: 282 : Trace("cadical::propagator") << "cb::check_found_model end: new "
292 : 0 : "variables added via theory check"
293 : 141 : << std::endl;
294 : : // Same as above, until CaDiCaL's assertion that we have to have
295 : : // a reason clause for rejecting the model is weakened, we need to
296 : : // pacify it with a tautology.
297 : 141 : d_new_clauses.push_back(1);
298 : 141 : d_new_clauses.push_back(-1);
299 : 141 : d_new_clauses.push_back(0);
300 : 141 : return false;
301 : : }
302 : 52 : bool res = done();
303 [ + - ]: 104 : Trace("cadical::propagator")
304 : 52 : << "cb::check_found_model end: done: " << res << std::endl;
305 : 52 : return res;
306 : : }
307 : :
308 : 16392 : int CadicalPropagator::cb_decide()
309 : : {
310 [ + - ]: 16392 : Trace("cadical::propagator") << "cb::decide" << std::endl;
311 [ + + ]: 16392 : if (d_found_solution)
312 : : {
313 : 6 : return 0;
314 : : }
315 : 16386 : ++d_stats.cbDecide;
316 : 16386 : bool stopSearch = false;
317 : 16386 : bool requirePhase = false;
318 : 16386 : SatLiteral lit = d_proxy->getNextDecisionRequest(requirePhase, stopSearch);
319 : : // We found a partial model, let's check it.
320 [ + + ]: 16386 : if (stopSearch)
321 : : {
322 : 92 : d_found_solution = cb_check_found_model({});
323 [ + + ]: 92 : if (d_found_solution)
324 : : {
325 [ + - ]: 7 : Trace("cadical::propagator") << "Found solution" << std::endl;
326 : 7 : d_found_solution = d_proxy->isDecisionEngineDone();
327 [ - + ]: 7 : if (!d_found_solution)
328 : : {
329 [ - - ]: 0 : Trace("cadical::propagator") << "Decision engine not done" << std::endl;
330 : 0 : lit = d_proxy->getNextDecisionRequest(requirePhase, stopSearch);
331 : : }
332 : : }
333 : : else
334 : : {
335 [ + - ]: 85 : Trace("cadical::propagator") << "No solution found yet" << std::endl;
336 : : }
337 : : }
338 [ + + ][ + + ]: 16386 : if (!stopSearch && lit != undefSatLiteral)
[ + + ]
339 : : {
340 [ + + ]: 16193 : if (!requirePhase)
341 : : {
342 : 16126 : int8_t phase = d_var_info[lit.getSatVariable()].phase;
343 [ - + ]: 16126 : if (phase != 0)
344 : : {
345 [ - - ]: 0 : if ((phase == -1 && !lit.isNegated())
346 [ - - ][ - - ]: 0 : || (phase == 1 && lit.isNegated()))
[ - - ][ - - ]
347 : : {
348 : 0 : lit = ~lit;
349 : : }
350 : : }
351 : : }
352 [ + - ]: 16193 : Trace("cadical::propagator") << "cb::decide: " << lit << std::endl;
353 : 16193 : return toCadicalLit(lit);
354 : : }
355 [ + - ]: 193 : Trace("cadical::propagator") << "cb::decide: 0" << std::endl;
356 : 193 : return 0;
357 : : }
358 : :
359 : 66293 : int CadicalPropagator::cb_propagate()
360 : : {
361 [ + + ]: 66293 : if (d_found_solution)
362 : : {
363 : 13 : return 0;
364 : : }
365 : 66280 : ++d_stats.cbPropagate;
366 [ + - ]: 66280 : Trace("cadical::propagator") << "cb::propagate" << std::endl;
367 [ + + ]: 66280 : if (d_propagations.empty())
368 : : {
369 : : // Only propagate if all activation literals are processed. Activation
370 : : // literals are always assumed first. If we don't do this, explanations
371 : : // for theory propagations may force activation literals to different
372 : : // values before they can get decided on.
373 [ + + ]: 36399 : if (d_decisions.size() < current_user_level())
374 : : {
375 : 42 : return 0;
376 : : }
377 : 36357 : d_proxy->theoryCheck(theory::Theory::Effort::EFFORT_STANDARD);
378 : 36357 : theory_propagate();
379 : : }
380 : 66238 : return next_propagation();
381 : : }
382 : :
383 : 21526 : int CadicalPropagator::cb_add_reason_clause_lit(int propagated_lit)
384 : : {
385 : 21526 : ++d_stats.cbAddReasonClauseLit;
386 : : // Get reason for propagated_lit.
387 [ + + ]: 21526 : if (!d_processing_reason)
388 : : {
389 [ - + ][ - + ]: 2209 : Assert(d_reason.empty());
[ - - ]
390 : 2209 : SatLiteral slit = toSatLiteral(propagated_lit);
391 : 2209 : SatClause clause;
392 : 2209 : d_proxy->explainPropagation(slit, clause);
393 [ - + ][ - + ]: 2209 : Assert(d_in_search);
[ - - ]
394 : : // Add activation literal of the clause's user level to the reason.
395 : 2209 : SatLiteral alit = activation_lit(clause_user_level(clause));
396 [ - + ]: 2209 : if (alit != undefSatLiteral)
397 : : {
398 : 0 : d_reason.push_back(alit);
399 : : }
400 : 2209 : d_reason.insert(d_reason.end(), clause.begin(), clause.end());
401 : 2209 : d_processing_reason = true;
402 [ + - ]: 4418 : Trace("cadical::propagator")
403 : 2209 : << "cb::reason: " << slit << ", size: " << d_reason.size() << std::endl;
404 : 2209 : }
405 : :
406 : : // We are done processing the reason for propagated_lit.
407 [ + + ]: 21526 : if (d_reason.empty())
408 : : {
409 : 2209 : d_processing_reason = false;
410 : 2209 : return 0;
411 : : }
412 : :
413 : : // Return next literal of the reason for propagated_lit.
414 [ + - ]: 38634 : Trace("cadical::propagator") << "cb::reason: " << toSatLiteral(propagated_lit)
415 : 19317 : << " " << d_reason.front() << std::endl;
416 : 19317 : int lit = toCadicalLit(d_reason.front());
417 : 19317 : d_reason.pop_front();
418 : 19317 : return lit;
419 : : }
420 : :
421 : 19369 : bool CadicalPropagator::cb_has_external_clause(bool& is_forgettable)
422 : : {
423 : 19369 : ++d_stats.cbHasExternalClause;
424 : 19369 : is_forgettable = false;
425 : 19369 : return !d_new_clauses.empty();
426 : : }
427 : :
428 : 7323 : int CadicalPropagator::cb_add_external_clause_lit()
429 : : {
430 : 7323 : ++d_stats.cbAddExternalClauseLit;
431 [ - + ][ - + ]: 7323 : Assert(!d_new_clauses.empty());
[ - - ]
432 : 7323 : CadicalLit lit = d_new_clauses.front();
433 : 7323 : d_new_clauses.pop_front();
434 [ + - ]: 14646 : Trace("cadical::propagator")
435 : 7323 : << "external_clause: " << toSatLiteral(lit) << std::endl;
436 : 7323 : return lit;
437 : : }
438 : :
439 : 130309 : SatValue CadicalPropagator::value(SatLiteral lit) const
440 : : {
441 : 130309 : SatVariable var = lit.getSatVariable();
442 : 130309 : SatValue val = SAT_VALUE_UNKNOWN;
443 : 130309 : int32_t assign = d_var_info[var].assignment;
444 [ + + ]: 130309 : if (assign != 0)
445 : : {
446 [ + + ]: 75563 : val = toSatValueLit(lit.isNegated() ? -assign : assign);
447 : : }
448 [ + - ]: 130309 : Trace("cadical::propagator") << "value: " << lit << ": " << val << std::endl;
449 : 130309 : return val;
450 : : }
451 : :
452 : 2657 : void CadicalPropagator::add_clause(const SatClause& clause)
453 : : {
454 : 2657 : std::vector<CadicalLit> lits;
455 : : // Note: Removable clauses can be added to lower user levels to avoid
456 : : // deleting them too eagerly. For example, conflicts may be learned
457 : : // at a user level N even though it only has literals of at most user
458 : : // level N - 2. In this case we can add the clause at N - 2 instead
459 : : // of deleting the clause when popping user level N, which would
460 : : // require us to relearn the clause again.
461 [ + + ]: 2657 : uint32_t max_user_level = d_in_search ? 0 : current_user_level();
462 [ + + ]: 9370 : for (const SatLiteral& lit : clause)
463 : : {
464 : 7045 : SatVariable var = lit.getSatVariable();
465 [ - + ][ - + ]: 7045 : Assert(var < d_var_info.size());
[ - - ]
466 : 7045 : const auto& info = d_var_info[var];
467 [ - + ][ - + ]: 7045 : Assert(info.is_active);
[ - - ]
468 [ + + ]: 7045 : if (info.is_fixed)
469 : : {
470 [ + + ]: 1296 : int32_t val = lit.isNegated() ? -info.assignment : info.assignment;
471 [ - + ][ - + ]: 1296 : Assert(val != 0);
[ - - ]
472 [ + + ]: 1296 : if (val > 0)
473 : : {
474 : : // Clause satisfied by fixed literal, no clause added
475 : 332 : return;
476 : : }
477 : : }
478 : 6713 : max_user_level = std::max(max_user_level, info.level_intro);
479 : 6713 : lits.push_back(toCadicalLit(lit));
480 : : }
481 [ + - ]: 2325 : if (!lits.empty())
482 : : {
483 : : // Determine activation literal based on max user level of clause.
484 : 2325 : SatLiteral alit = activation_lit(max_user_level);
485 [ + + ]: 2325 : if (alit != undefSatLiteral)
486 : : {
487 : 49 : lits.insert(lits.begin(), toCadicalLit(alit));
488 : : }
489 : : // Do not immediately add clauses added during search. We have to buffer
490 : : // them and add them during the cb_add_reason_clause_lit callback.
491 [ + + ]: 2325 : if (d_in_search)
492 : : {
493 : 1595 : d_new_clauses.insert(d_new_clauses.end(), lits.begin(), lits.end());
494 : 1595 : d_new_clauses.push_back(0);
495 : : }
496 : : else
497 : : {
498 [ + + ]: 2174 : for (const auto& lit : lits)
499 : : {
500 : 1444 : d_solver.add(lit);
501 : : }
502 : 730 : d_solver.add(0);
503 : : }
504 : : }
505 : : // // Add empty clause
506 : : // else if (num_false == clause.size())
507 : : // {
508 : : // d_solver.add(0);
509 : : // }
510 [ + + ]: 2657 : }
511 : :
512 : 2109 : void CadicalPropagator::add_new_var(const SatVariable& var, bool is_theory_atom)
513 : : {
514 : : // Since activation literals are not tracked here, we have to make sure to
515 : : // properly resize d_var_info.
516 [ - + ]: 2109 : if (var > d_var_info.size())
517 : : {
518 : 0 : d_var_info.resize(var);
519 : : }
520 [ - + ][ - + ]: 2109 : Assert(d_var_info.size() == var);
[ - - ]
521 : :
522 : : // Boolean variables are not theory atoms, but may still occur in
523 : : // lemmas/conflicts sent to the SAT solver. Hence, we have to observe them
524 : : // since CaDiCaL expects all literals sent back to be observed.
525 : 2109 : d_solver.add_observed_var(toCadicalVar(var));
526 : 2109 : d_active_vars.push_back(var);
527 [ + - ]: 4218 : Trace("cadical::propagator")
528 : 2109 : << "new var: " << var << " (level: " << current_user_level()
529 : 0 : << ", is_theory_atom: " << is_theory_atom
530 : 2109 : << ", in_search: " << d_in_search << ")" << std::endl;
531 : 2109 : auto& info = d_var_info.emplace_back();
532 : 2109 : info.level_intro = current_user_level();
533 : 2109 : info.is_theory_atom = is_theory_atom;
534 : 2109 : }
535 : :
536 : 79 : bool CadicalPropagator::done() const
537 : : {
538 [ + + ]: 79 : if (!d_new_clauses.empty())
539 : : {
540 [ + - ]: 25 : Trace("cadical::propagator") << "not done: pending clauses" << std::endl;
541 : 25 : return false;
542 : : }
543 [ - + ]: 54 : if (d_proxy->theoryNeedCheck())
544 : : {
545 [ - - ]: 0 : Trace("cadical::propagator") << "not done: theory need check" << std::endl;
546 : 0 : return false;
547 : : }
548 [ + + ]: 54 : if (d_found_solution)
549 : : {
550 [ + - ]: 7 : Trace("cadical::propagator") << "done: found partial solution" << std::endl;
551 : : }
552 : : else
553 : : {
554 [ + - ]: 94 : Trace("cadical::propagator")
555 : 47 : << "done: full assignment consistent" << std::endl;
556 : : }
557 : 54 : return true;
558 : : }
559 : :
560 : 46 : void CadicalPropagator::user_push()
561 : : {
562 [ + - ]: 46 : Trace("cadical::propagator") << "user push: " << d_active_vars_control.size();
563 : 46 : d_active_vars_control.push_back(d_active_vars.size());
564 [ + - ]: 92 : Trace("cadical::propagator")
565 : 46 : << " -> " << d_active_vars_control.size() << std::endl;
566 : 46 : }
567 : :
568 : 46 : void CadicalPropagator::set_activation_lit(SatVariable alit)
569 : : {
570 : 46 : d_activation_literals.push_back(SatLiteral(alit));
571 [ + - ]: 92 : Trace("cadical::propagator")
572 : 46 : << "enable activation lit: " << alit << std::endl;
573 : 46 : }
574 : :
575 : 32 : void CadicalPropagator::user_pop()
576 : : {
577 [ + - ]: 32 : Trace("cadical::propagator") << "user pop: " << d_active_vars_control.size();
578 : 32 : size_t pop_to = d_active_vars_control.back();
579 : 32 : d_active_vars_control.pop_back();
580 [ + - ]: 64 : Trace("cadical::propagator")
581 : 32 : << " -> " << d_active_vars_control.size() << std::endl;
582 : :
583 : : // Disable activation literal for popped user level. The activation literal
584 : : // will be set inactive below and is added as unit clause, which will satisfy
585 : : // all clauses added in this user level and get garbage collected in CaDiCal.
586 : 32 : SatLiteral alit = current_activation_lit();
587 [ + - ]: 64 : Trace("cadical::propagator")
588 : 32 : << "disable activation lit: " << alit << std::endl;
589 : 32 : d_activation_literals.pop_back();
590 : :
591 : 32 : size_t user_level = current_user_level();
592 : :
593 : : // Unregister popped variables so that CaDiCaL does not notify us anymore
594 : : // about assignments.
595 [ - + ][ - + ]: 32 : Assert(pop_to <= d_active_vars.size());
[ - - ]
596 : 32 : std::vector<SatVariable> fixed;
597 [ + + ]: 93 : while (d_active_vars.size() > pop_to)
598 : : {
599 : 61 : SatVariable var = d_active_vars.back();
600 : 61 : const auto& info = d_var_info[var];
601 : 61 : d_active_vars.pop_back();
602 : :
603 : : // We keep fixed literals that correspond to theory atoms introduced in
604 : : // lower user levels, since we have to renotify them before the next
605 : : // solve call.
606 [ + + ][ - + ]: 61 : if (info.is_fixed && info.is_theory_atom && info.level_intro <= user_level)
[ - - ]
607 : : {
608 : 0 : fixed.push_back(var);
609 : : }
610 : : else
611 : : {
612 [ + - ]: 61 : Trace("cadical::propagator") << "set inactive: " << var << std::endl;
613 : 61 : d_var_info[var].is_active = false;
614 : 61 : d_solver.remove_observed_var(toCadicalVar(var));
615 [ - + ][ - + ]: 61 : Assert(info.level_intro > user_level);
[ - - ]
616 : : // Fix value of inactive variables in order to avoid CaDiCaL from
617 : : // deciding on them again. This make a huge difference in performance
618 : : // for incremental problems with many check-sat calls.
619 : 61 : d_solver.add(toCadicalVar(var));
620 : 61 : d_solver.add(0);
621 : : }
622 : : }
623 : : // Re-add fixed active vars in the order they were added to d_active_vars.
624 : 32 : d_active_vars.insert(d_active_vars.end(), fixed.rbegin(), fixed.rend());
625 : :
626 : : // We are at decicion level 0 at this point.
627 [ - + ][ - + ]: 32 : Assert(d_decisions.empty());
[ - - ]
628 [ - + ][ - + ]: 32 : Assert(d_assignment_control.empty());
[ - - ]
629 : : // At this point, only fixed literals will be on d_assignments, now we have
630 : : // to determine which of these are still relevant in the current user
631 : : // level. If the variable is still active here, it means that it is still
632 : : // relevant for the current user level. If its assignment was fixed in a
633 : : // higher user level, we have to renotify the fixed literal in the current
634 : : // level (or in the user level of the next solve call). This happens by
635 : : // pushing the literal onto the d_renotify_fixed vector.
636 : 32 : auto it = d_assignments.begin();
637 [ + + ]: 174 : while (it != d_assignments.end())
638 : : {
639 : 142 : SatLiteral lit = *it;
640 : 142 : auto& info = d_var_info[lit.getSatVariable()];
641 [ - + ][ - + ]: 142 : Assert(info.is_fixed);
[ - - ]
642 : :
643 : : // Remove inactive variables from the assignment vector.
644 [ + + ]: 142 : if (!info.is_active)
645 : : {
646 : 8 : it = d_assignments.erase(it);
647 : 8 : continue;
648 : : }
649 : :
650 : : // Renotify fixed literals if it was fixed in a higher user level.
651 [ + + ][ + + ]: 134 : if (info.is_theory_atom && info.level_fixed > user_level)
652 : : {
653 [ + - ]: 32 : Trace("cadical::propagator")
654 : 0 : << "queue renotify: " << lit << " (level_intro: " << info.level_intro
655 : 16 : << ", level_fixed: " << info.level_fixed << ")" << std::endl;
656 : 16 : d_renotify_fixed.push_back(lit);
657 : : }
658 : 134 : ++it;
659 : : }
660 : 32 : }
661 : :
662 : 61 : void CadicalPropagator::phase(SatLiteral lit)
663 : : {
664 : 61 : d_solver.phase(toCadicalLit(lit));
665 [ - + ]: 61 : d_var_info[lit.getSatVariable()].phase = lit.isNegated() ? -1 : 1;
666 : 61 : }
667 : :
668 : 34 : const SatLiteral& CadicalPropagator::current_activation_lit() const
669 : : {
670 [ - + ]: 34 : if (d_activation_literals.empty())
671 : : {
672 : 0 : return undefSatLiteral;
673 : : }
674 : 34 : return d_activation_literals.back();
675 : : }
676 : :
677 : 4541 : const SatLiteral& CadicalPropagator::activation_lit(size_t user_level) const
678 : : {
679 : : // User level 0 has no activation literal.
680 [ + + ]: 4541 : if (user_level == 0)
681 : : {
682 : 4487 : return undefSatLiteral;
683 : : }
684 [ - + ][ - + ]: 54 : Assert(user_level <= d_activation_literals.size());
[ - - ]
685 : 54 : return d_activation_literals[user_level - 1];
686 : : }
687 : :
688 : 2215 : uint32_t CadicalPropagator::clause_user_level(const SatClause& clause) const
689 : : {
690 : 2215 : uint32_t max_user_level = 0;
691 [ + + ]: 21545 : for (const SatLiteral& lit : clause)
692 : : {
693 : 19330 : SatVariable var = lit.getSatVariable();
694 [ - + ][ - + ]: 19330 : Assert(var < d_var_info.size());
[ - - ]
695 : 19330 : max_user_level = std::max(max_user_level, d_var_info[var].level_intro);
696 : : }
697 : 2215 : return max_user_level;
698 : : }
699 : :
700 : 101 : void CadicalPropagator::renotify_fixed()
701 : : {
702 : 101 : ++d_stats.renotifyFixed;
703 [ + + ]: 117 : for (const auto& lit : d_renotify_fixed)
704 : : {
705 [ + - ]: 32 : Trace("cadical::propagator")
706 : 16 : << "re-enqueue (user pop): " << lit << std::endl;
707 : : // Re-enqueue fixed theory literal
708 : 16 : d_proxy->enqueueTheoryLiteral(lit);
709 : : // We are notifying fixed literals at the current user level, update the
710 : : // level at which the variable was fixed, so that it will be renotified,
711 : : // if needed in lower user levels.
712 : 16 : d_var_info[lit.getSatVariable()].level_fixed = current_user_level();
713 : 16 : ++d_stats.renotifyFixedLit;
714 : : }
715 : 101 : d_renotify_fixed.clear();
716 : 101 : }
717 : :
718 : 36559 : void CadicalPropagator::theory_propagate()
719 : : {
720 : 36559 : SatClause propagated_lits;
721 : 36559 : d_proxy->theoryPropagate(propagated_lits);
722 [ + - ]: 73118 : Trace("cadical::propagator")
723 : 36559 : << "new propagations: " << propagated_lits.size() << std::endl;
724 : :
725 [ + + ]: 85778 : for (const auto& lit : propagated_lits)
726 : : {
727 [ + - ]: 49219 : Trace("cadical::propagator") << "new propagation: " << lit << std::endl;
728 : 49219 : d_propagations.push_back(lit);
729 : : }
730 : 36559 : }
731 : :
732 : 66238 : int CadicalPropagator::next_propagation()
733 : : {
734 [ + + ]: 66238 : if (d_propagations.empty())
735 : : {
736 : 17657 : return 0;
737 : : }
738 : 48581 : SatLiteral next = d_propagations.front();
739 : 48581 : d_propagations.pop_front();
740 [ + - ]: 48581 : Trace("cadical::propagator") << "propagate: " << next << std::endl;
741 : 48581 : return toCadicalLit(next);
742 : : }
743 : :
744 : : } // namespace cvc5::internal::prop::cadical
|
