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 : : * CaDiCaL proof tracer.
11 : : *
12 : : * Implementation of a CaDiCaL proof tracer.
13 : : */
14 : :
15 : : #include "prop/cadical/proof_tracer.h"
16 : :
17 : : #include <unordered_set>
18 : :
19 : : #include "proof/proof_node.h"
20 : : #include "prop/cadical/cadical.h"
21 : : #include "prop/cadical/cdclt_propagator.h"
22 : :
23 : : namespace cvc5::internal::prop::cadical {
24 : :
25 : : namespace {
26 : :
27 : 8180 : Node toNode(NodeManager* nm, TheoryProxy* proxy, const SatClause& clause)
28 : : {
29 [ + + ]: 8180 : if (clause.empty())
30 : : {
31 : 40 : return nm->mkConst(false);
32 : : }
33 : 8160 : std::vector<Node> lits;
34 [ + + ]: 54928 : for (const auto& lit : clause)
35 : : {
36 : 46768 : lits.push_back(proxy->getNode(lit));
37 : : }
38 : : // Sat clause is sorted by literal id. Ensure that node-level clause is
39 : : // sorted by node ids. Also factor duplicate literals to match the
40 : : // normalization done by PropPfManager when registering CNF clause proofs.
41 : 8160 : std::sort(lits.begin(), lits.end());
42 : 8160 : lits.erase(std::unique(lits.begin(), lits.end()), lits.end());
43 [ + + ]: 8160 : return lits.size() == 1 ? lits[0] : nm->mkNode(Kind::OR, lits);
44 : 8160 : }
45 : :
46 : : /**
47 : : * Normalize a unary CaDiCaL derivation to a proof of conclusion.
48 : : *
49 : : * CaDiCaL's LRUP trace can contain derived clauses with exactly one
50 : : * antecedent. These steps are not resolution chains; they typically remove
51 : : * duplicate literals from the antecedent and may leave the node-level clause
52 : : * order different from the normalized conclusion expected by cvc5.
53 : : *
54 : : * Since CHAIN_M_RESOLUTION needs at least two premises, this builds the proof
55 : : * with the smaller Boolean proof rules instead:
56 : : * - reuse the child if it already proves conclusion,
57 : : * - use FACTORING when duplicate literals are removed,
58 : : * - add REORDERING when the factored clause has the right literals in a
59 : : * different order,
60 : : * - or use REORDERING directly if no factoring is required.
61 : : */
62 : 8 : std::shared_ptr<ProofNode> normalizeDerivedClause(
63 : : ProofNodeManager* pnm,
64 : : const std::shared_ptr<ProofNode>& child,
65 : : const Node& conclusion)
66 : : {
67 : 8 : Node childConclusion = child->getResult();
68 [ + - ]: 8 : if (childConclusion == conclusion)
69 : : {
70 : 8 : return child;
71 : : }
72 : :
73 : 0 : std::vector<std::shared_ptr<ProofNode>> children{child};
74 : : std::shared_ptr<ProofNode> factored =
75 : 0 : pnm->mkNode(ProofRule::FACTORING, children, {}, conclusion);
76 [ - - ]: 0 : if (factored != nullptr)
77 : : {
78 : 0 : return factored;
79 : : }
80 : :
81 : 0 : factored = pnm->mkNode(ProofRule::FACTORING, children, {});
82 [ - - ]: 0 : if (factored != nullptr)
83 : : {
84 [ - - ]: 0 : if (factored->getResult() == conclusion)
85 : : {
86 : 0 : return factored;
87 : : }
88 : 0 : return pnm->mkNode(
89 : 0 : ProofRule::REORDERING, {factored}, {conclusion}, conclusion);
90 : : }
91 : :
92 : 0 : return pnm->mkNode(ProofRule::REORDERING, children, {conclusion}, conclusion);
93 : 8 : }
94 : :
95 : : } // namespace
96 : :
97 : 20 : ProofTracer::ProofTracer(const CadicalPropagator& propagator)
98 : 20 : : d_propagator(propagator)
99 : : {
100 : 20 : }
101 : :
102 : 2404 : void ProofTracer::add_original_clause(uint64_t clause_id,
103 : : CVC5_UNUSED bool redundant,
104 : : const std::vector<int>& clause,
105 : : CVC5_UNUSED bool restored)
106 : : {
107 : : ClauseType ctype =
108 [ + + ]: 2404 : d_propagator.in_search() ? ClauseType::THEORY : ClauseType::INPUT;
109 : 2404 : d_clauses.emplace(clause_id, ClauseInfo(clause_id, ctype, clause));
110 [ + - ]: 2404 : Trace("cadical::prooftracer") << d_clauses.at(clause_id) << std::endl;
111 : 2404 : }
112 : :
113 : 11380 : void ProofTracer::add_derived_clause(CVC5_UNUSED uint64_t clause_id,
114 : : bool redundant,
115 : : const std::vector<int>& clause,
116 : : const std::vector<uint64_t>& antecedents)
117 : : {
118 : : (void)redundant;
119 : 11380 : d_clauses.emplace(
120 : : clause_id,
121 : 22760 : ClauseInfo(clause_id, ClauseType::DERIVED, clause, antecedents));
122 [ + - ]: 11380 : Trace("cadical::prooftracer") << d_clauses.at(clause_id) << std::endl;
123 : 11380 : }
124 : :
125 : 0 : void ProofTracer::add_assumption_clause(
126 : : uint64_t clause_id,
127 : : const std::vector<int>& clause,
128 : : const std::vector<uint64_t>& antecedents)
129 : : {
130 : : // Assumption clauses are the negation of the core of failed/unsat
131 : : // assumptions.
132 : 0 : d_clauses.emplace(
133 : : clause_id,
134 : 0 : ClauseInfo(clause_id, ClauseType::ASSUMPTION, clause, antecedents));
135 [ - - ]: 0 : Trace("cadical::prooftracer") << d_clauses.at(clause_id) << std::endl;
136 : 0 : }
137 : :
138 : 20 : void ProofTracer::conclude_unsat(CVC5_UNUSED CaDiCaL::ConclusionType type,
139 : : const std::vector<uint64_t>& clause_ids)
140 : : {
141 : : // Store final clause ids that concluded unsat.
142 : 20 : d_final_clauses = clause_ids;
143 : 20 : }
144 : :
145 : 20 : void ProofTracer::compute_proof_core(std::vector<uint64_t>& core) const
146 : : {
147 : 20 : std::vector<uint64_t> visit{d_final_clauses};
148 : 20 : std::unordered_set<uint64_t> visited;
149 : :
150 : : // Trace back from final clause ids (empty clause) to original clauses.
151 [ + + ]: 53272 : while (!visit.empty())
152 : : {
153 : 53252 : const uint64_t clause_id = visit.back();
154 : 53252 : visit.pop_back();
155 : :
156 [ + + ]: 53252 : if (visited.insert(clause_id).second)
157 : : {
158 : 8180 : core.push_back(clause_id);
159 : 8180 : const auto& antecedents = d_clauses.at(clause_id).antecedents;
160 : 8180 : visit.insert(visit.end(), antecedents.begin(), antecedents.end());
161 : : }
162 : : }
163 : :
164 [ - + ]: 20 : if (TraceIsOn("cadical::prooftracer"))
165 : : {
166 [ - - ]: 0 : Trace("cadical::prooftracer") << "proof core:" << std::endl;
167 [ - - ]: 0 : for (const auto& cid : core)
168 : : {
169 : 0 : const auto& clause = d_clauses.at(cid);
170 [ - - ]: 0 : Trace("cadical::prooftracer") << clause << std::endl;
171 : : }
172 : : }
173 : 20 : }
174 : :
175 : 20 : std::shared_ptr<ProofNode> ProofTracer::get_chain_resolution_proof(
176 : : ProofNodeManager* pnm, NodeManager* nm, TheoryProxy* proxy)
177 : : {
178 : 20 : std::vector<uint64_t> core;
179 : 20 : compute_proof_core(core);
180 : : // Sort core clause ids in ascending order to construct proof steps
181 : : // starting from the original clauses.
182 : 20 : std::sort(core.begin(), core.end());
183 : :
184 : 20 : std::unordered_set<int64_t> alits;
185 [ - + ]: 20 : for (const auto& lit : d_propagator.activation_literals())
186 : : {
187 : 0 : alits.insert(lit.getSatVariable());
188 : : }
189 : :
190 : 20 : std::unordered_map<uint64_t, std::shared_ptr<ProofNode>> steps;
191 [ + + ]: 8200 : for (const uint64_t cid : core)
192 : : {
193 : 8180 : const auto& clause = d_clauses.at(cid);
194 [ + + ]: 8180 : if (clause.type == ClauseType::DERIVED)
195 : : {
196 [ - + ][ - + ]: 6596 : Assert(!clause.antecedents.empty());
[ - - ]
197 : 6596 : steps.emplace(cid,
198 : 13192 : chain_resolution_step(cid, proxy, pnm, nm, steps, alits));
199 : : }
200 : : else
201 : : {
202 : 1584 : SatClause sat_clause = toSatClause(alits, clause.literals);
203 [ - + ]: 1584 : if (clause.type == ClauseType::ASSUMPTION)
204 : : {
205 : 0 : Assert(cid == core.back());
206 : 0 : Assert(sat_clause.empty());
207 : : // Empty antecedents for assumption clauses only happen with constraint
208 : : // feature (CaDiCaL's constrain method), which we don't use. The main
209 : : // application is model checking.
210 : 0 : Assert(!clause.antecedents.empty());
211 : 0 : steps.emplace(cid, steps.at(core[core.size() - 2]));
212 : : }
213 : : else
214 : : {
215 : 1584 : Node assump = toNode(nm, proxy, sat_clause);
216 : 1584 : steps.emplace(cid, pnm->mkAssume(assump));
217 : 1584 : }
218 : 1584 : }
219 : : }
220 : : // Last clause id corresponds to empty clause.
221 : 20 : auto pf = steps.at(core.back());
222 : 40 : return pf;
223 : 20 : }
224 : :
225 : 219028 : bool ProofTracer::mark_var(std::unordered_map<int32_t, uint8_t>& marked_vars,
226 : : int32_t lit)
227 : : {
228 : 219028 : int32_t var = std::abs(lit);
229 [ + + ]: 219028 : uint8_t mask = (lit < 0) ? 2 : 1;
230 : 219028 : uint8_t marked = marked_vars[var];
231 [ + + ]: 219028 : if (!(marked & mask))
232 : : {
233 : 129400 : marked_vars[var] |= mask;
234 : : }
235 : 219028 : return marked & ~mask;
236 : : }
237 : :
238 : 6596 : std::shared_ptr<ProofNode> ProofTracer::chain_resolution_step(
239 : : uint64_t cid,
240 : : TheoryProxy* proxy,
241 : : ProofNodeManager* pnm,
242 : : NodeManager* nm,
243 : : const std::unordered_map<uint64_t, std::shared_ptr<ProofNode>>& steps,
244 : : const std::unordered_set<int64_t>& activation_literals)
245 : : {
246 : 6596 : const auto& cl = d_clauses.at(cid);
247 : 6596 : SatClause expected_cl = toSatClause(activation_literals, cl.literals);
248 : 6596 : Node conclusion = toNode(nm, proxy, expected_cl);
249 : 6596 : const auto& antecedents = cl.antecedents;
250 : : // Handle unary derivations separately; see normalizeDerivedClause.
251 [ + + ]: 6596 : if (antecedents.size() == 1)
252 : : {
253 : 8 : auto it = steps.find(antecedents[0]);
254 [ - + ][ - + ]: 8 : Assert(it != steps.end());
[ - - ]
255 : 8 : return normalizeDerivedClause(pnm, it->second, conclusion);
256 : : }
257 : 6588 : std::vector<std::shared_ptr<ProofNode>> children;
258 : 6588 : std::vector<Node> polarities, literals;
259 : 6588 : std::unordered_map<int32_t, uint8_t> marked_vars;
260 : : // Create chain resolution step for each derived clause
261 [ + + ]: 59812 : for (size_t i = 0, size = antecedents.size(); i < size; ++i)
262 : : {
263 : : // Antecedants are stored in the order they were resolved. Thus, we have
264 : : // to process them in reverse order, starting from the last id.
265 : 53224 : size_t idx = size - i - 1;
266 : 53224 : uint64_t aid = antecedents[idx];
267 : 53224 : const auto& clause = d_clauses.at(aid);
268 [ + + ]: 272252 : for (int32_t lit : clause.literals)
269 : : {
270 [ + + ]: 219028 : if (!mark_var(marked_vars, lit))
271 : : {
272 : 172392 : continue;
273 : : }
274 : : // Found pivot literal
275 : 46636 : literals.push_back(proxy->getNode(toSatLiteral(std::abs(lit))));
276 : : // Polarity of pivot literal in this antecedent
277 : 46636 : polarities.push_back(nm->mkConst(!(lit > 0)));
278 : : }
279 : :
280 : 53224 : auto it = steps.find(aid);
281 [ - + ][ - + ]: 53224 : Assert(it != steps.end());
[ - - ]
282 : 53224 : children.push_back(it->second);
283 : : }
284 : 19764 : std::vector<Node> args{conclusion};
285 : 6588 : args.push_back(nm->mkNode(Kind::SEXPR, polarities));
286 : 6588 : args.push_back(nm->mkNode(Kind::SEXPR, literals));
287 : 6588 : return pnm->mkNode(ProofRule::CHAIN_M_RESOLUTION, children, args);
288 : 6596 : }
289 : :
290 : 0 : std::ostream& operator<<(std::ostream& os, const ProofTracer::ClauseInfo& ci)
291 : : {
292 : 0 : char ct = ' ';
293 [ - - ][ - - ]: 0 : switch (ci.type)
[ - ]
294 : : {
295 : 0 : case ProofTracer::ClauseType::DERIVED: ct = 'd'; break;
296 : 0 : case ProofTracer::ClauseType::INPUT: ct = 'i'; break;
297 : 0 : case ProofTracer::ClauseType::THEORY: ct = 't'; break;
298 : 0 : case ProofTracer::ClauseType::ASSUMPTION: ct = 'a'; break;
299 : : }
300 : :
301 : 0 : os << ci.clause_id << " " << ct << ": ( ";
302 [ - - ]: 0 : for (const auto lit : ci.literals)
303 : : {
304 : 0 : os << lit << " ";
305 : : }
306 : 0 : os << ")";
307 : 0 : os << " [ ";
308 [ - - ]: 0 : for (const auto lit : ci.antecedents)
309 : : {
310 : 0 : os << lit << " ";
311 : : }
312 : 0 : os << "] ";
313 : 0 : return os;
314 : : }
315 : :
316 : : } // namespace cvc5::internal::prop::cadical
|
