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 : : * Implementation of equality proof checker.
11 : : */
12 : :
13 : : #include "theory/builtin/proof_checker.h"
14 : :
15 : : #include "expr/aci_norm.h"
16 : : #include "expr/node_algorithm.h"
17 : : #include "expr/skolem_manager.h"
18 : : #include "rewriter/rewrite_db.h"
19 : : #include "rewriter/rewrite_db_term_process.h"
20 : : #include "rewriter/rewrite_proof_rule.h"
21 : : #include "smt/env.h"
22 : : #include "smt/term_formula_removal.h"
23 : : #include "theory/evaluator.h"
24 : : #include "theory/quantifiers/extended_rewrite.h"
25 : : #include "theory/rewriter.h"
26 : : #include "theory/substitutions.h"
27 : : #include "theory/theory.h"
28 : : #include "util/rational.h"
29 : :
30 : : using namespace cvc5::internal::kind;
31 : :
32 : : namespace cvc5::internal {
33 : : namespace theory {
34 : : namespace builtin {
35 : :
36 : 51214 : BuiltinProofRuleChecker::BuiltinProofRuleChecker(NodeManager* nm,
37 : : Rewriter* r,
38 : 51214 : Env& env)
39 : 51214 : : ProofRuleChecker(nm), d_rewriter(r), d_env(env), d_rdb(nullptr)
40 : : {
41 : 51214 : }
42 : :
43 : 19964 : void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
44 : : {
45 : 19964 : pc->registerChecker(ProofRule::ASSUME, this);
46 : 19964 : pc->registerChecker(ProofRule::SCOPE, this);
47 : 19964 : pc->registerChecker(ProofRule::SUBS, this);
48 : 19964 : pc->registerChecker(ProofRule::EVALUATE, this);
49 : 19964 : pc->registerChecker(ProofRule::DISTINCT_VALUES, this);
50 : 19964 : pc->registerChecker(ProofRule::ACI_NORM, this);
51 : 19964 : pc->registerChecker(ProofRule::ABSORB, this);
52 : 19964 : pc->registerChecker(ProofRule::ITE_EQ, this);
53 : 19964 : pc->registerChecker(ProofRule::ENCODE_EQ_INTRO, this);
54 : 19964 : pc->registerChecker(ProofRule::DSL_REWRITE, this);
55 : 19964 : pc->registerChecker(ProofRule::THEORY_REWRITE, this);
56 : : // rules depending on the rewriter
57 : 19964 : pc->registerTrustedChecker(ProofRule::MACRO_REWRITE, this, 4);
58 : 19964 : pc->registerTrustedChecker(ProofRule::MACRO_SR_EQ_INTRO, this, 4);
59 : 19964 : pc->registerTrustedChecker(ProofRule::MACRO_SR_PRED_INTRO, this, 4);
60 : 19964 : pc->registerTrustedChecker(ProofRule::MACRO_SR_PRED_ELIM, this, 4);
61 : 19964 : pc->registerTrustedChecker(ProofRule::MACRO_SR_PRED_TRANSFORM, this, 4);
62 : 19964 : pc->registerTrustedChecker(ProofRule::TRUST_THEORY_REWRITE, this, 4);
63 : : // trusted rules
64 : 19964 : pc->registerTrustedChecker(ProofRule::TRUST, this, 1);
65 : : // external proof rules
66 : 19964 : pc->registerChecker(ProofRule::LFSC_RULE, this);
67 : 19964 : pc->registerChecker(ProofRule::ALETHE_RULE, this);
68 : :
69 : 19964 : d_rdb = pc->getRewriteDatabase();
70 : 19964 : }
71 : :
72 : 278405 : Node BuiltinProofRuleChecker::applySubstitutionRewrite(
73 : : Node n,
74 : : const std::vector<Node>& exp,
75 : : MethodId ids,
76 : : MethodId ida,
77 : : MethodId idr)
78 : : {
79 : 278405 : Node nks = applySubstitution(n, exp, ids, ida);
80 [ + + ]: 278405 : if (nks.isNull())
81 : : {
82 : 40 : return nks;
83 : : }
84 : 278365 : return d_env.rewriteViaMethod(nks, idr);
85 : 278405 : }
86 : :
87 : 4937580 : bool BuiltinProofRuleChecker::getSubstitutionForLit(Node exp,
88 : : TNode& var,
89 : : TNode& subs,
90 : : MethodId ids)
91 : : {
92 : 4937580 : NodeManager* nm = exp.getNodeManager();
93 [ + + ]: 4937580 : if (ids == MethodId::SB_DEFAULT)
94 : : {
95 [ + + ]: 4936789 : if (exp.getKind() != Kind::EQUAL)
96 : : {
97 : 40 : return false;
98 : : }
99 : 4936749 : var = exp[0];
100 : 4936749 : subs = exp[1];
101 : : }
102 [ + + ]: 791 : else if (ids == MethodId::SB_LITERAL)
103 : : {
104 : 24 : bool polarity = exp.getKind() != Kind::NOT;
105 [ + - ]: 24 : var = polarity ? exp : exp[0];
106 : 24 : subs = nm->mkConst(polarity);
107 : : }
108 [ + - ]: 767 : else if (ids == MethodId::SB_FORMULA)
109 : : {
110 : 767 : var = exp;
111 : 767 : subs = nm->mkConst(true);
112 : : }
113 : : else
114 : : {
115 : 0 : DebugUnhandled() << "BuiltinProofRuleChecker::applySubstitution: no "
116 : 0 : "substitution for "
117 : 0 : << ids << std::endl;
118 : : return false;
119 : : }
120 : 4937540 : return true;
121 : : }
122 : :
123 : 91943 : bool BuiltinProofRuleChecker::getSubstitutionFor(Node exp,
124 : : std::vector<TNode>& vars,
125 : : std::vector<TNode>& subs,
126 : : std::vector<TNode>& from,
127 : : MethodId ids)
128 : : {
129 : 91943 : TNode v;
130 : 91943 : TNode s;
131 [ + + ][ + - ]: 91943 : if (exp.getKind() == Kind::AND && ids == MethodId::SB_DEFAULT)
[ + + ]
132 : : {
133 [ + + ]: 4921389 : for (const Node& ec : exp)
134 : : {
135 : : // non-recursive, do not use nested AND
136 [ - + ]: 4883513 : if (!getSubstitutionForLit(ec, v, s, ids))
137 : : {
138 : 0 : return false;
139 : : }
140 : 4883513 : vars.push_back(v);
141 : 4883513 : subs.push_back(s);
142 : 4883513 : from.push_back(ec);
143 [ + - ]: 4883513 : }
144 : 37876 : return true;
145 : : }
146 : 54067 : bool ret = getSubstitutionForLit(exp, v, s, ids);
147 : 54067 : vars.push_back(v);
148 : 54067 : subs.push_back(s);
149 : 54067 : from.push_back(exp);
150 : 54067 : return ret;
151 : 91943 : }
152 : :
153 : 0 : Node BuiltinProofRuleChecker::applySubstitution(Node n,
154 : : Node exp,
155 : : MethodId ids,
156 : : MethodId ida)
157 : : {
158 : 0 : std::vector<Node> expv{exp};
159 : 0 : return applySubstitution(n, expv, ids, ida);
160 : 0 : }
161 : :
162 : 321401 : Node BuiltinProofRuleChecker::applySubstitution(Node n,
163 : : const std::vector<Node>& exp,
164 : : MethodId ids,
165 : : MethodId ida)
166 : : {
167 : 321401 : std::vector<TNode> vars;
168 : 321401 : std::vector<TNode> subs;
169 : 321401 : std::vector<TNode> from;
170 [ + + ]: 394700 : for (size_t i = 0, nexp = exp.size(); i < nexp; i++)
171 : : {
172 [ - + ]: 73339 : if (exp[i].isNull())
173 : : {
174 : 0 : return Node::null();
175 : : }
176 [ + + ]: 73339 : if (!getSubstitutionFor(exp[i], vars, subs, from, ids))
177 : : {
178 : 40 : return Node::null();
179 : : }
180 : : }
181 [ - + ]: 321361 : if (ida == MethodId::SBA_SIMUL)
182 : : {
183 : : // simply apply the simultaneous substitution now
184 : 0 : return n.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
185 : : }
186 [ + + ]: 321361 : else if (ida == MethodId::SBA_FIXPOINT)
187 : : {
188 : 54831 : SubstitutionMap sm;
189 [ + + ]: 3880393 : for (size_t i = 0, nvars = vars.size(); i < nvars; i++)
190 : : {
191 : 3825562 : sm.addSubstitution(vars[i], subs[i]);
192 : : }
193 : 54831 : Node ns = sm.apply(n);
194 : 54831 : return ns;
195 : 54831 : }
196 [ - + ][ - + ]: 266530 : Assert(ida == MethodId::SBA_SEQUENTIAL);
[ - - ]
197 : : // we prefer n traversals of the term to n^2/2 traversals of range terms
198 : 266530 : Node ns = n;
199 [ + + ]: 304609 : for (size_t i = 0, nvars = vars.size(); i < nvars; i++)
200 : : {
201 : 38079 : TNode v = vars[(nvars - 1) - i];
202 : 38079 : TNode s = subs[(nvars - 1) - i];
203 : 38079 : ns = ns.substitute(v, s);
204 : 38079 : }
205 : 266530 : return ns;
206 : 321401 : }
207 : :
208 : 2643178 : Node BuiltinProofRuleChecker::checkInternal(ProofRule id,
209 : : const std::vector<Node>& children,
210 : : const std::vector<Node>& args)
211 : : {
212 : 2643178 : NodeManager* nm = nodeManager();
213 : : // compute what was proven
214 [ + + ]: 2643178 : if (id == ProofRule::ASSUME)
215 : : {
216 [ - + ][ - + ]: 65090 : Assert(children.empty());
[ - - ]
217 [ - + ][ - + ]: 65090 : Assert(args.size() == 1);
[ - - ]
218 [ - + ][ - + ]: 65090 : Assert(args[0].getType().isBoolean());
[ - - ]
219 : 65090 : return args[0];
220 : : }
221 [ + + ]: 2578088 : else if (id == ProofRule::SCOPE)
222 : : {
223 [ - + ][ - + ]: 760411 : Assert(children.size() == 1);
[ - - ]
224 [ + + ]: 760411 : if (args.empty())
225 : : {
226 : : // no antecedant
227 : 5943 : return children[0];
228 : : }
229 : 754468 : Node ant = nm->mkAnd(args);
230 : : // if the conclusion is false, its the negated antencedant only
231 [ + + ][ + + ]: 754468 : if (children[0].isConst() && !children[0].getConst<bool>())
[ + + ]
232 : : {
233 : 610172 : return ant.notNode();
234 : : }
235 : 144296 : return nm->mkNode(Kind::IMPLIES, ant, children[0]);
236 : 754468 : }
237 [ + + ]: 1817677 : else if (id == ProofRule::SUBS)
238 : : {
239 [ - + ][ - + ]: 80 : Assert(children.size() > 0);
[ - - ]
240 [ + - ][ + - ]: 80 : Assert(1 <= args.size() && args.size() <= 3) << "Args: " << args;
[ - + ][ - + ]
[ - - ]
241 : 80 : MethodId ids = MethodId::SB_DEFAULT;
242 [ - + ][ - - ]: 80 : if (args.size() >= 2 && !getMethodId(args[1], ids))
[ - + ][ - + ]
[ - - ]
243 : : {
244 : 0 : return Node::null();
245 : : }
246 : 80 : MethodId ida = MethodId::SBA_SEQUENTIAL;
247 [ - + ][ - - ]: 80 : if (args.size() >= 3 && !getMethodId(args[2], ida))
[ - + ][ - + ]
[ - - ]
248 : : {
249 : 0 : return Node::null();
250 : : }
251 : 80 : std::vector<Node> exp;
252 [ + + ]: 432 : for (size_t i = 0, nchild = children.size(); i < nchild; i++)
253 : : {
254 : 352 : exp.push_back(children[i]);
255 : : }
256 : 80 : Node res = applySubstitution(args[0], exp, ids, ida);
257 [ - + ]: 80 : if (res.isNull())
258 : : {
259 : 0 : return Node::null();
260 : : }
261 : 80 : return args[0].eqNode(res);
262 : 80 : }
263 [ + + ]: 1817597 : else if (id == ProofRule::MACRO_REWRITE)
264 : : {
265 [ - + ][ - + ]: 2034 : Assert(children.empty());
[ - - ]
266 [ + - ][ + - ]: 2034 : Assert(1 <= args.size() && args.size() <= 2);
[ - + ][ - + ]
[ - - ]
267 : 2034 : MethodId idr = MethodId::RW_REWRITE;
268 [ - + ][ - - ]: 2034 : if (args.size() == 2 && !getMethodId(args[1], idr))
[ - + ][ - + ]
[ - - ]
269 : : {
270 : 0 : return Node::null();
271 : : }
272 : 2034 : Node res = d_env.rewriteViaMethod(args[0], idr);
273 [ - + ]: 2034 : if (res.isNull())
274 : : {
275 : 0 : return Node::null();
276 : : }
277 : 2034 : return args[0].eqNode(res);
278 : 2034 : }
279 [ + + ]: 1815563 : else if (id == ProofRule::EVALUATE)
280 : : {
281 [ - + ][ - + ]: 718176 : Assert(children.empty());
[ - - ]
282 [ - + ][ - + ]: 718176 : Assert(args.size() == 1);
[ - - ]
283 : 718176 : Node res = d_env.rewriteViaMethod(args[0], MethodId::RW_EVALUATE);
284 [ + + ]: 718176 : if (res.isNull())
285 : : {
286 : 529227 : return Node::null();
287 : : }
288 : 188949 : return args[0].eqNode(res);
289 : 718176 : }
290 [ + + ]: 1097387 : else if (id == ProofRule::DISTINCT_VALUES)
291 : : {
292 [ - + ][ - + ]: 44 : Assert(children.empty());
[ - - ]
293 [ - + ][ - + ]: 44 : Assert(args.size() == 2);
[ - - ]
294 [ - + ][ - + ]: 132 : AssertEqual(args[0].getType(), args[1].getType());
[ - - ]
295 [ + - ][ + - ]: 44 : if (!args[0].isConst() || !args[1].isConst() || args[0] == args[1])
[ - + ][ - + ]
296 : : {
297 : 0 : return Node::null();
298 : : }
299 : : // note we don't check for illegal (non-first-class) types here
300 : 88 : return args[0].eqNode(args[1]).notNode();
301 : : }
302 [ + + ]: 1097343 : else if (id == ProofRule::ACI_NORM)
303 : : {
304 [ - + ][ - + ]: 28375 : Assert(children.empty());
[ - - ]
305 [ - + ][ - + ]: 28375 : Assert(args.size() == 1);
[ - - ]
306 [ - + ]: 28375 : if (args[0].getKind() != Kind::EQUAL)
307 : : {
308 : 0 : return Node::null();
309 : : }
310 [ - + ]: 28375 : if (!expr::isACINorm(args[0][0], args[0][1]))
311 : : {
312 : 0 : return Node::null();
313 : : }
314 : 28375 : return args[0];
315 : : }
316 [ + + ]: 1068968 : else if (id == ProofRule::ABSORB)
317 : : {
318 [ - + ][ - + ]: 4951 : Assert(children.empty());
[ - - ]
319 [ - + ][ - + ]: 4951 : Assert(args.size() == 1);
[ - - ]
320 [ - + ]: 4951 : if (args[0].getKind() != Kind::EQUAL)
321 : : {
322 : 0 : return Node::null();
323 : : }
324 : 9902 : if (expr::getZeroElement(nm, args[0][0].getKind(), args[0][0].getType())
325 [ - + ]: 14853 : != args[0][1])
326 : : {
327 : 0 : return Node::null();
328 : : }
329 [ - + ]: 4951 : if (!expr::isAbsorb(args[0][0], args[0][1]))
330 : : {
331 : 0 : return Node::null();
332 : : }
333 : 4951 : return args[0];
334 : : }
335 [ + + ]: 1064017 : else if (id == ProofRule::MACRO_SR_EQ_INTRO)
336 : : {
337 [ + - ][ + - ]: 35343 : Assert(1 <= args.size() && args.size() <= 4);
[ - + ][ - + ]
[ - - ]
338 : : MethodId ids, ida, idr;
339 [ - + ]: 35343 : if (!getMethodIds(args, ids, ida, idr, 1))
340 : : {
341 : 0 : return Node::null();
342 : : }
343 : 35343 : Node res = applySubstitutionRewrite(args[0], children, ids, ida, idr);
344 [ - + ]: 35343 : if (res.isNull())
345 : : {
346 : 0 : return Node::null();
347 : : }
348 : 35343 : return args[0].eqNode(res);
349 : 35343 : }
350 [ + + ]: 1028674 : else if (id == ProofRule::MACRO_SR_PRED_INTRO)
351 : : {
352 [ + - ]: 90550 : Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
353 : 45275 : << args[0] << std::endl;
354 [ + - ][ + - ]: 45275 : Assert(1 <= args.size() && args.size() <= 4);
[ - + ][ - + ]
[ - - ]
355 : : MethodId ids, ida, idr;
356 [ - + ]: 45275 : if (!getMethodIds(args, ids, ida, idr, 1))
357 : : {
358 : 0 : return Node::null();
359 : : }
360 : 45275 : Node res = applySubstitutionRewrite(args[0], children, ids, ida, idr);
361 [ - + ]: 45275 : if (res.isNull())
362 : : {
363 : 0 : return Node::null();
364 : : }
365 [ + - ]: 45275 : Trace("builtin-pfcheck") << "Result is " << res << std::endl;
366 [ + - ]: 90550 : Trace("builtin-pfcheck")
367 : 45275 : << "Witness form is " << SkolemManager::getOriginalForm(res)
368 : 45275 : << std::endl;
369 : : // **** NOTE: can rewrite the witness form here. This enables certain lemmas
370 : : // to be provable, e.g. (= k t) where k is a purification Skolem for t.
371 : 45275 : res = d_rewriter->rewrite(SkolemManager::getOriginalForm(res));
372 [ + + ][ + + ]: 45275 : if (!res.isConst() || !res.getConst<bool>())
[ + + ]
373 : : {
374 [ + - ]: 37760 : Trace("builtin-pfcheck")
375 : 18880 : << "Failed to rewrite to true, res=" << res << std::endl;
376 : 18880 : return Node::null();
377 : : }
378 [ + - ]: 26395 : Trace("builtin-pfcheck") << "...success" << std::endl;
379 : 26395 : return args[0];
380 : 45275 : }
381 [ + + ]: 983399 : else if (id == ProofRule::MACRO_SR_PRED_ELIM)
382 : : {
383 [ + - ]: 12002 : Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
384 : 6001 : << args.size() << std::endl;
385 [ - + ][ - + ]: 6001 : Assert(children.size() >= 1);
[ - - ]
386 [ - + ][ - + ]: 6001 : Assert(args.size() <= 3);
[ - - ]
387 : 6001 : std::vector<Node> exp;
388 : 6001 : exp.insert(exp.end(), children.begin() + 1, children.end());
389 : : MethodId ids, ida, idr;
390 [ - + ]: 6001 : if (!getMethodIds(args, ids, ida, idr, 0))
391 : : {
392 : 0 : return Node::null();
393 : : }
394 : 6001 : Node res1 = applySubstitutionRewrite(children[0], exp, ids, ida, idr);
395 [ + - ]: 6001 : Trace("builtin-pfcheck") << "Returned " << res1 << std::endl;
396 : 6001 : return res1;
397 : 6001 : }
398 [ + + ]: 977398 : else if (id == ProofRule::MACRO_SR_PRED_TRANSFORM)
399 : : {
400 [ + - ]: 191786 : Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
401 : 95893 : << args.size() << std::endl;
402 [ - + ][ - + ]: 95893 : Assert(children.size() >= 1);
[ - - ]
403 [ + - ][ + - ]: 95893 : Assert(1 <= args.size() && args.size() <= 4);
[ - + ][ - + ]
[ - - ]
404 [ - + ][ - + ]: 95893 : Assert(args[0].getType().isBoolean());
[ - - ]
405 : : MethodId ids, ida, idr;
406 [ - + ]: 95893 : if (!getMethodIds(args, ids, ida, idr, 1))
407 : : {
408 : 0 : return Node::null();
409 : : }
410 : 95893 : std::vector<Node> exp;
411 : 95893 : exp.insert(exp.end(), children.begin() + 1, children.end());
412 : 95893 : Node res1 = applySubstitutionRewrite(children[0], exp, ids, ida, idr);
413 : 95893 : Node res2 = applySubstitutionRewrite(args[0], exp, ids, ida, idr);
414 [ + + ][ - + ]: 95893 : if (res1.isNull() || res2.isNull())
[ + + ]
415 : : {
416 : 16 : return Node::null();
417 : : }
418 : : // if not already equal, do rewriting
419 [ + + ]: 95877 : if (res1 != res2)
420 : : {
421 [ + - ]: 7236 : Trace("builtin-pfcheck-debug")
422 : 0 : << "Failed to show " << res1 << " == " << res2
423 : 3618 : << ", resort to original forms..." << std::endl;
424 : : // can rewrite the witness forms
425 : 3618 : res1 = d_rewriter->rewrite(SkolemManager::getOriginalForm(res1));
426 : 3618 : res2 = d_rewriter->rewrite(SkolemManager::getOriginalForm(res2));
427 [ + - ][ + + ]: 3618 : if (res1.isNull() || res1 != res2)
[ + + ]
428 : : {
429 [ + - ]: 1219 : Trace("builtin-pfcheck") << "Failed to match results" << std::endl;
430 [ + - ]: 1219 : Trace("builtin-pfcheck-debug") << res1 << " vs " << res2 << std::endl;
431 : 1219 : return Node::null();
432 : : }
433 : : }
434 : 94658 : return args[0];
435 : 95893 : }
436 [ + + ]: 881505 : else if (id == ProofRule::ITE_EQ)
437 : : {
438 [ - + ][ - + ]: 5339 : Assert(children.empty());
[ - - ]
439 [ - + ][ - + ]: 5339 : Assert(args.size() == 1);
[ - - ]
440 : 5339 : return RemoveTermFormulas::getAxiomFor(args[0]);
441 : : }
442 [ + + ]: 876166 : else if (id == ProofRule::TRUST)
443 : : {
444 [ - + ][ - + ]: 69902 : Assert(args.size() >= 2);
[ - - ]
445 : 69902 : return args[1];
446 : : }
447 [ + + ]: 806264 : else if (id == ProofRule::TRUST_THEORY_REWRITE)
448 : : {
449 : : // "trusted" rules
450 [ - + ][ - + ]: 597969 : Assert(!args.empty());
[ - - ]
451 [ - + ][ - + ]: 597969 : Assert(args[0].getType().isBoolean());
[ - - ]
452 : 597969 : return args[0];
453 : : }
454 [ + + ][ - + ]: 208295 : else if (id == ProofRule::LFSC_RULE || id == ProofRule::ALETHE_RULE)
455 : : {
456 [ - + ][ - + ]: 43155 : Assert(args.size() > 1);
[ - - ]
457 [ - + ][ - + ]: 43155 : Assert(args[0].getType().isInteger());
[ - - ]
458 : 43155 : return args[1];
459 : : }
460 [ + + ]: 165140 : else if (id == ProofRule::ENCODE_EQ_INTRO)
461 : : {
462 [ - + ][ - + ]: 3370 : Assert(children.empty());
[ - - ]
463 [ - + ][ - + ]: 3370 : Assert(args.size() == 1);
[ - - ]
464 : 3370 : Node ac = getEncodeEqIntro(nodeManager(), args[0]);
465 : 3370 : return args[0].eqNode(ac);
466 : 3370 : }
467 [ + + ]: 161770 : else if (id == ProofRule::DSL_REWRITE)
468 : : {
469 : : // consult rewrite db, apply args[1]...args[n] as a substitution
470 : : // to variable list and prove equality between LHS and RHS.
471 [ - + ][ - + ]: 93235 : Assert(d_rdb != nullptr);
[ - - ]
472 : : ProofRewriteRule di;
473 [ - + ]: 93235 : if (!rewriter::getRewriteRule(args[0], di))
474 : : {
475 : 0 : return Node::null();
476 : : }
477 : 93235 : const rewriter::RewriteProofRule& rpr = d_rdb->getRule(di);
478 : 93235 : const std::vector<Node>& varList = rpr.getVarList();
479 : 93235 : const std::vector<Node>& conds = rpr.getConditions();
480 : 93235 : std::vector<Node> subs(args.begin() + 1, args.end());
481 [ - + ]: 93235 : if (varList.size() != subs.size())
482 : : {
483 : 0 : return Node::null();
484 : : }
485 : : // check whether child proof match
486 [ - + ]: 93235 : if (conds.size() != children.size())
487 : : {
488 : 0 : return Node::null();
489 : : }
490 [ + + ]: 97385 : for (size_t i = 0, nchildren = children.size(); i < nchildren; i++)
491 : : {
492 : 4150 : Node scond = expr::narySubstitute(conds[i], varList, subs);
493 [ - + ]: 4150 : if (scond != children[i])
494 : : {
495 : 0 : return Node::null();
496 : : }
497 [ + - ]: 4150 : }
498 : 93235 : return rpr.getConclusionFor(subs);
499 : 93235 : }
500 [ + - ]: 68535 : else if (id == ProofRule::THEORY_REWRITE)
501 : : {
502 [ - + ][ - + ]: 68535 : Assert(args.size() == 2);
[ - - ]
503 : : ProofRewriteRule di;
504 [ - + ]: 68535 : if (!rewriter::getRewriteRule(args[0], di))
505 : : {
506 : 0 : return Node::null();
507 : : }
508 [ - + ]: 68535 : if (args[1].getKind() != Kind::EQUAL)
509 : : {
510 : 0 : return Node::null();
511 : : }
512 : 68535 : Node rhs = d_rewriter->rewriteViaRule(di, args[1][0]);
513 [ + - ][ - + ]: 68535 : if (rhs.isNull() || rhs != args[1][1])
[ + - ][ - + ]
[ - - ]
514 : : {
515 : 0 : return Node::null();
516 : : }
517 : 68535 : return args[1];
518 : 68535 : }
519 : : // no rule
520 : 0 : return Node::null();
521 : : }
522 : :
523 : 3450 : Node BuiltinProofRuleChecker::getEncodeEqIntro(NodeManager* nm, const Node& n)
524 : : {
525 : 3450 : rewriter::RewriteDbNodeConverter rconv(nm);
526 : : // run a single (small) step conversion
527 : 6900 : return rconv.postConvert(n);
528 : 3450 : }
529 : :
530 : 504149 : bool BuiltinProofRuleChecker::getTheoryId(TNode n, TheoryId& tid)
531 : : {
532 : : uint32_t i;
533 [ - + ]: 504149 : if (!getUInt32(n, i))
534 : : {
535 : 0 : return false;
536 : : }
537 : 504149 : tid = static_cast<TheoryId>(i);
538 : 504149 : return true;
539 : : }
540 : :
541 : 1119103 : Node BuiltinProofRuleChecker::mkTheoryIdNode(NodeManager* nm, TheoryId tid)
542 : : {
543 : 2238206 : return nm->mkConstInt(Rational(static_cast<uint32_t>(tid)));
544 : : }
545 : :
546 : : } // namespace builtin
547 : : } // namespace theory
548 : : } // namespace cvc5::internal
|
