Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Hans-Joerg Schurr, Hanna Lachnitt
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 : : * Implementation of equality proof checker.
14 : : */
15 : :
16 : : #include "theory/builtin/proof_checker.h"
17 : :
18 : : #include "expr/nary_term_util.h"
19 : : #include "expr/skolem_manager.h"
20 : : #include "rewriter/rewrite_db.h"
21 : : #include "rewriter/rewrite_db_term_process.h"
22 : : #include "rewriter/rewrite_proof_rule.h"
23 : : #include "smt/env.h"
24 : : #include "smt/term_formula_removal.h"
25 : : #include "theory/evaluator.h"
26 : : #include "theory/quantifiers/extended_rewrite.h"
27 : : #include "theory/rewriter.h"
28 : : #include "theory/substitutions.h"
29 : : #include "theory/theory.h"
30 : : #include "util/rational.h"
31 : :
32 : : using namespace cvc5::internal::kind;
33 : :
34 : : namespace cvc5::internal {
35 : : namespace theory {
36 : : namespace builtin {
37 : :
38 : 49838 : BuiltinProofRuleChecker::BuiltinProofRuleChecker(NodeManager* nm,
39 : : Rewriter* r,
40 : 49838 : Env& env)
41 : 49838 : : ProofRuleChecker(nm), d_rewriter(r), d_env(env), d_rdb(nullptr)
42 : : {
43 : 49838 : }
44 : :
45 : 19204 : void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
46 : : {
47 : 19204 : pc->registerChecker(ProofRule::ASSUME, this);
48 : 19204 : pc->registerChecker(ProofRule::SCOPE, this);
49 : 19204 : pc->registerChecker(ProofRule::SUBS, this);
50 : 19204 : pc->registerChecker(ProofRule::EVALUATE, this);
51 : 19204 : pc->registerChecker(ProofRule::ACI_NORM, this);
52 : 19204 : pc->registerChecker(ProofRule::ITE_EQ, this);
53 : 19204 : pc->registerChecker(ProofRule::ENCODE_EQ_INTRO, this);
54 : 19204 : pc->registerChecker(ProofRule::DSL_REWRITE, this);
55 : 19204 : pc->registerChecker(ProofRule::THEORY_REWRITE, this);
56 : : // rules depending on the rewriter
57 : 19204 : pc->registerTrustedChecker(ProofRule::MACRO_REWRITE, this, 4);
58 : 19204 : pc->registerTrustedChecker(ProofRule::MACRO_SR_EQ_INTRO, this, 4);
59 : 19204 : pc->registerTrustedChecker(ProofRule::MACRO_SR_PRED_INTRO, this, 4);
60 : 19204 : pc->registerTrustedChecker(ProofRule::MACRO_SR_PRED_ELIM, this, 4);
61 : 19204 : pc->registerTrustedChecker(ProofRule::MACRO_SR_PRED_TRANSFORM, this, 4);
62 : 19204 : pc->registerTrustedChecker(ProofRule::TRUST_THEORY_REWRITE, this, 4);
63 : : // trusted rules
64 : 19204 : pc->registerTrustedChecker(ProofRule::TRUST, this, 1);
65 : : // external proof rules
66 : 19204 : pc->registerChecker(ProofRule::LFSC_RULE, this);
67 : 19204 : pc->registerChecker(ProofRule::ALETHE_RULE, this);
68 : :
69 : 19204 : d_rdb = pc->getRewriteDatabase();
70 : 19204 : }
71 : :
72 : 2513550 : Node BuiltinProofRuleChecker::applySubstitutionRewrite(
73 : : Node n,
74 : : const std::vector<Node>& exp,
75 : : MethodId ids,
76 : : MethodId ida,
77 : : MethodId idr)
78 : : {
79 : 2513550 : Node nks = applySubstitution(n, exp, ids, ida);
80 : 5027100 : return d_env.rewriteViaMethod(nks, idr);
81 : : }
82 : :
83 : 8907560 : bool BuiltinProofRuleChecker::getSubstitutionForLit(Node exp,
84 : : TNode& var,
85 : : TNode& subs,
86 : : MethodId ids)
87 : : {
88 [ + + ]: 8907560 : if (ids == MethodId::SB_DEFAULT)
89 : : {
90 [ - + ]: 8906660 : if (exp.getKind() != Kind::EQUAL)
91 : : {
92 : 0 : return false;
93 : : }
94 : 8906660 : var = exp[0];
95 : 8906660 : subs = exp[1];
96 : : }
97 [ - + ]: 896 : else if (ids == MethodId::SB_LITERAL)
98 : : {
99 : 0 : bool polarity = exp.getKind() != Kind::NOT;
100 [ - - ]: 0 : var = polarity ? exp : exp[0];
101 : 0 : subs = NodeManager::currentNM()->mkConst(polarity);
102 : : }
103 [ + - ]: 896 : else if (ids == MethodId::SB_FORMULA)
104 : : {
105 : 896 : var = exp;
106 : 896 : subs = NodeManager::currentNM()->mkConst(true);
107 : : }
108 : : else
109 : : {
110 : 0 : Assert(false) << "BuiltinProofRuleChecker::applySubstitution: no "
111 : 0 : "substitution for "
112 : 0 : << ids << std::endl;
113 : : return false;
114 : : }
115 : 8907560 : return true;
116 : : }
117 : :
118 : 150039 : bool BuiltinProofRuleChecker::getSubstitutionFor(Node exp,
119 : : std::vector<TNode>& vars,
120 : : std::vector<TNode>& subs,
121 : : std::vector<TNode>& from,
122 : : MethodId ids)
123 : : {
124 : 300078 : TNode v;
125 : 300078 : TNode s;
126 [ + + ][ + - ]: 150039 : if (exp.getKind() == Kind::AND && ids == MethodId::SB_DEFAULT)
[ + + ]
127 : : {
128 [ + + ]: 8903560 : for (const Node& ec : exp)
129 : : {
130 : : // non-recursive, do not use nested AND
131 [ - + ]: 8830540 : if (!getSubstitutionForLit(ec, v, s, ids))
132 : : {
133 : 0 : return false;
134 : : }
135 : 8830540 : vars.push_back(v);
136 : 8830540 : subs.push_back(s);
137 : 8830540 : from.push_back(ec);
138 : : }
139 : 73022 : return true;
140 : : }
141 : 77017 : bool ret = getSubstitutionForLit(exp, v, s, ids);
142 : 77017 : vars.push_back(v);
143 : 77017 : subs.push_back(s);
144 : 77017 : from.push_back(exp);
145 : 77017 : return ret;
146 : : }
147 : :
148 : 0 : Node BuiltinProofRuleChecker::applySubstitution(Node n,
149 : : Node exp,
150 : : MethodId ids,
151 : : MethodId ida)
152 : : {
153 : 0 : std::vector<Node> expv{exp};
154 : 0 : return applySubstitution(n, expv, ids, ida);
155 : : }
156 : :
157 : 2580150 : Node BuiltinProofRuleChecker::applySubstitution(Node n,
158 : : const std::vector<Node>& exp,
159 : : MethodId ids,
160 : : MethodId ida)
161 : : {
162 : 5160290 : std::vector<TNode> vars;
163 : 5160290 : std::vector<TNode> subs;
164 : 5160290 : std::vector<TNode> from;
165 [ + + ]: 2695360 : for (size_t i = 0, nexp = exp.size(); i < nexp; i++)
166 : : {
167 [ - + ]: 115211 : if (exp[i].isNull())
168 : : {
169 : 0 : return Node::null();
170 : : }
171 [ - + ]: 115211 : if (!getSubstitutionFor(exp[i], vars, subs, from, ids))
172 : : {
173 : 0 : return Node::null();
174 : : }
175 : : }
176 [ - + ]: 2580150 : if (ida == MethodId::SBA_SIMUL)
177 : : {
178 : : // simply apply the simultaneous substitution now
179 : 0 : return n.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
180 : : }
181 [ + + ]: 2580150 : else if (ida == MethodId::SBA_FIXPOINT)
182 : : {
183 : 185814 : SubstitutionMap sm;
184 [ + + ]: 6829770 : for (size_t i = 0, nvars = vars.size(); i < nvars; i++)
185 : : {
186 : 6736870 : sm.addSubstitution(vars[i], subs[i]);
187 : : }
188 : 185814 : Node ns = sm.apply(n);
189 : 92907 : return ns;
190 : : }
191 [ - + ][ - + ]: 2487240 : Assert(ida == MethodId::SBA_SEQUENTIAL);
[ - - ]
192 : : // we prefer n traversals of the term to n^2/2 traversals of range terms
193 : 4974480 : Node ns = n;
194 [ + + ]: 2540810 : for (size_t i = 0, nvars = vars.size(); i < nvars; i++)
195 : : {
196 : 107140 : TNode v = vars[(nvars - 1) - i];
197 : 53570 : TNode s = subs[(nvars - 1) - i];
198 : 53570 : ns = ns.substitute(v, s);
199 : : }
200 : 2487240 : return ns;
201 : : }
202 : :
203 : 3513390 : Node BuiltinProofRuleChecker::checkInternal(ProofRule id,
204 : : const std::vector<Node>& children,
205 : : const std::vector<Node>& args)
206 : : {
207 : 3513390 : NodeManager* nm = nodeManager();
208 : : // compute what was proven
209 [ + + ]: 3513390 : if (id == ProofRule::ASSUME)
210 : : {
211 [ - + ][ - + ]: 6 : Assert(children.empty());
[ - - ]
212 [ - + ][ - + ]: 6 : Assert(args.size() == 1);
[ - - ]
213 [ - + ][ - + ]: 6 : Assert(args[0].getType().isBoolean());
[ - - ]
214 : 6 : return args[0];
215 : : }
216 [ + + ]: 3513380 : else if (id == ProofRule::SCOPE)
217 : : {
218 [ - + ][ - + ]: 816084 : Assert(children.size() == 1);
[ - - ]
219 [ + + ]: 816084 : if (args.empty())
220 : : {
221 : : // no antecedant
222 : 4989 : return children[0];
223 : : }
224 : 1622190 : Node ant = nm->mkAnd(args);
225 : : // if the conclusion is false, its the negated antencedant only
226 [ + + ][ + + ]: 811095 : if (children[0].isConst() && !children[0].getConst<bool>())
[ + + ]
227 : : {
228 : 652944 : return ant.notNode();
229 : : }
230 : 158151 : return nm->mkNode(Kind::IMPLIES, ant, children[0]);
231 : : }
232 [ - + ]: 2697300 : else if (id == ProofRule::SUBS)
233 : : {
234 : 0 : Assert(children.size() > 0);
235 : 0 : Assert(1 <= args.size() && args.size() <= 3) << "Args: " << args;
236 : 0 : MethodId ids = MethodId::SB_DEFAULT;
237 : 0 : if (args.size() >= 2 && !getMethodId(args[1], ids))
238 : : {
239 : 0 : return Node::null();
240 : : }
241 : 0 : MethodId ida = MethodId::SBA_SEQUENTIAL;
242 : 0 : if (args.size() >= 3 && !getMethodId(args[2], ida))
243 : : {
244 : 0 : return Node::null();
245 : : }
246 : 0 : std::vector<Node> exp;
247 [ - - ]: 0 : for (size_t i = 0, nchild = children.size(); i < nchild; i++)
248 : : {
249 : 0 : exp.push_back(children[i]);
250 : : }
251 : 0 : Node res = applySubstitution(args[0], exp, ids, ida);
252 [ - - ]: 0 : if (res.isNull())
253 : : {
254 : 0 : return Node::null();
255 : : }
256 : 0 : return args[0].eqNode(res);
257 : : }
258 [ + + ]: 2697300 : else if (id == ProofRule::MACRO_REWRITE)
259 : : {
260 [ - + ][ - + ]: 743 : Assert(children.empty());
[ - - ]
261 [ + - ][ + - ]: 1486 : Assert(1 <= args.size() && args.size() <= 2);
[ - + ][ - - ]
262 : 743 : MethodId idr = MethodId::RW_REWRITE;
263 [ - + ][ - - ]: 743 : if (args.size() == 2 && !getMethodId(args[1], idr))
[ - + ][ - + ]
[ - - ]
264 : : {
265 : 0 : return Node::null();
266 : : }
267 : 1486 : Node res = d_env.rewriteViaMethod(args[0], idr);
268 [ - + ]: 743 : if (res.isNull())
269 : : {
270 : 0 : return Node::null();
271 : : }
272 : 743 : return args[0].eqNode(res);
273 : : }
274 [ + + ]: 2696560 : else if (id == ProofRule::EVALUATE)
275 : : {
276 [ - + ][ - + ]: 443971 : Assert(children.empty());
[ - - ]
277 [ - + ][ - + ]: 443971 : Assert(args.size() == 1);
[ - - ]
278 : 887942 : Node res = d_env.rewriteViaMethod(args[0], MethodId::RW_EVALUATE);
279 [ + + ]: 443971 : if (res.isNull())
280 : : {
281 : 291413 : return Node::null();
282 : : }
283 : 152558 : return args[0].eqNode(res);
284 : : }
285 [ + + ]: 2252580 : else if (id == ProofRule::ACI_NORM)
286 : : {
287 [ - + ][ - + ]: 17674 : Assert(children.empty());
[ - - ]
288 [ - + ][ - + ]: 17674 : Assert(args.size() == 1);
[ - - ]
289 [ - + ]: 17674 : if (args[0].getKind() != Kind::EQUAL)
290 : : {
291 : 0 : return Node::null();
292 : : }
293 [ - + ]: 17674 : if (!expr::isACINorm(args[0][0], args[0][1]))
294 : : {
295 : 0 : return Node::null();
296 : : }
297 : 17674 : return args[0];
298 : : }
299 [ + + ]: 2234910 : else if (id == ProofRule::MACRO_SR_EQ_INTRO)
300 : : {
301 [ + - ][ + - ]: 110024 : Assert(1 <= args.size() && args.size() <= 4);
[ - + ][ - - ]
302 : : MethodId ids, ida, idr;
303 [ - + ]: 55012 : if (!getMethodIds(args, ids, ida, idr, 1))
304 : : {
305 : 0 : return Node::null();
306 : : }
307 : 110024 : Node res = applySubstitutionRewrite(args[0], children, ids, ida, idr);
308 [ - + ]: 55012 : if (res.isNull())
309 : : {
310 : 0 : return Node::null();
311 : : }
312 : 55012 : return args[0].eqNode(res);
313 : : }
314 [ + + ]: 2179900 : else if (id == ProofRule::MACRO_SR_PRED_INTRO)
315 : : {
316 [ + - ]: 88530 : Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
317 : 44265 : << args[0] << std::endl;
318 [ + - ][ + - ]: 88530 : Assert(1 <= args.size() && args.size() <= 4);
[ - + ][ - - ]
319 : : MethodId ids, ida, idr;
320 [ - + ]: 44265 : if (!getMethodIds(args, ids, ida, idr, 1))
321 : : {
322 : 0 : return Node::null();
323 : : }
324 : 88530 : Node res = applySubstitutionRewrite(args[0], children, ids, ida, idr);
325 [ - + ]: 44265 : if (res.isNull())
326 : : {
327 : 0 : return Node::null();
328 : : }
329 [ + - ]: 44265 : Trace("builtin-pfcheck") << "Result is " << res << std::endl;
330 [ + - ]: 88530 : Trace("builtin-pfcheck") << "Witness form is "
331 : 44265 : << SkolemManager::getOriginalForm(res) << std::endl;
332 : : // **** NOTE: can rewrite the witness form here. This enables certain lemmas
333 : : // to be provable, e.g. (= k t) where k is a purification Skolem for t.
334 : 44265 : res = d_rewriter->rewrite(SkolemManager::getOriginalForm(res));
335 [ + + ][ + + ]: 44265 : if (!res.isConst() || !res.getConst<bool>())
[ + + ]
336 : : {
337 [ + - ]: 41758 : Trace("builtin-pfcheck")
338 : 20879 : << "Failed to rewrite to true, res=" << res << std::endl;
339 : 20879 : return Node::null();
340 : : }
341 [ + - ]: 23386 : Trace("builtin-pfcheck") << "...success" << std::endl;
342 : 23386 : return args[0];
343 : : }
344 [ + + ]: 2135630 : else if (id == ProofRule::MACRO_SR_PRED_ELIM)
345 : : {
346 [ + - ]: 10222 : Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
347 : 5111 : << args.size() << std::endl;
348 [ - + ][ - + ]: 5111 : Assert(children.size() >= 1);
[ - - ]
349 [ - + ][ - + ]: 5111 : Assert(args.size() <= 3);
[ - - ]
350 : 10222 : std::vector<Node> exp;
351 : 5111 : exp.insert(exp.end(), children.begin() + 1, children.end());
352 : : MethodId ids, ida, idr;
353 [ - + ]: 5111 : if (!getMethodIds(args, ids, ida, idr, 0))
354 : : {
355 : 0 : return Node::null();
356 : : }
357 : 10222 : Node res1 = applySubstitutionRewrite(children[0], exp, ids, ida, idr);
358 [ + - ]: 5111 : Trace("builtin-pfcheck") << "Returned " << res1 << std::endl;
359 : 5111 : return res1;
360 : : }
361 [ + + ]: 2130520 : else if (id == ProofRule::MACRO_SR_PRED_TRANSFORM)
362 : : {
363 [ + - ]: 2409160 : Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
364 : 1204580 : << args.size() << std::endl;
365 [ - + ][ - + ]: 1204580 : Assert(children.size() >= 1);
[ - - ]
366 [ + - ][ + - ]: 2409160 : Assert(1 <= args.size() && args.size() <= 4);
[ - + ][ - - ]
367 [ - + ][ - + ]: 1204580 : Assert(args[0].getType().isBoolean());
[ - - ]
368 : : MethodId ids, ida, idr;
369 [ - + ]: 1204580 : if (!getMethodIds(args, ids, ida, idr, 1))
370 : : {
371 : 0 : return Node::null();
372 : : }
373 : 2409160 : std::vector<Node> exp;
374 : 1204580 : exp.insert(exp.end(), children.begin() + 1, children.end());
375 : 2409160 : Node res1 = applySubstitutionRewrite(children[0], exp, ids, ida, idr);
376 : 2409160 : Node res2 = applySubstitutionRewrite(args[0], exp, ids, ida, idr);
377 : : // if not already equal, do rewriting
378 [ + + ]: 1204580 : if (res1 != res2)
379 : : {
380 [ + - ]: 14128 : Trace("builtin-pfcheck-debug")
381 : 0 : << "Failed to show " << res1 << " == " << res2
382 : 7064 : << ", resort to original forms..." << std::endl;
383 : : // can rewrite the witness forms
384 : 7064 : res1 = d_rewriter->rewrite(SkolemManager::getOriginalForm(res1));
385 : 7064 : res2 = d_rewriter->rewrite(SkolemManager::getOriginalForm(res2));
386 [ + + ][ + + ]: 7064 : if (res1.isNull() || res1 != res2)
[ + + ]
387 : : {
388 [ + - ]: 1113 : Trace("builtin-pfcheck") << "Failed to match results" << std::endl;
389 [ + - ]: 1113 : Trace("builtin-pfcheck-debug") << res1 << " vs " << res2 << std::endl;
390 : 1113 : return Node::null();
391 : : }
392 : : }
393 : 1203470 : return args[0];
394 : : }
395 [ + + ]: 925943 : else if (id == ProofRule::ITE_EQ)
396 : : {
397 [ - + ][ - + ]: 7786 : Assert(children.empty());
[ - - ]
398 [ - + ][ - + ]: 7786 : Assert(args.size() == 1);
[ - - ]
399 : 7786 : return RemoveTermFormulas::getAxiomFor(args[0]);
400 : : }
401 [ + + ]: 918157 : else if (id == ProofRule::TRUST)
402 : : {
403 [ - + ][ - + ]: 51542 : Assert(args.size() >= 2);
[ - - ]
404 : 51542 : return args[1];
405 : : }
406 [ + + ]: 866615 : else if (id == ProofRule::TRUST_THEORY_REWRITE)
407 : : {
408 : : // "trusted" rules
409 [ - + ][ - + ]: 706156 : Assert(!args.empty());
[ - - ]
410 [ - + ][ - + ]: 706156 : Assert(args[0].getType().isBoolean());
[ - - ]
411 : 706156 : return args[0];
412 : : }
413 [ + + ][ - + ]: 160459 : else if (id == ProofRule::LFSC_RULE || id == ProofRule::ALETHE_RULE)
414 : : {
415 [ - + ][ - + ]: 49522 : Assert(args.size() > 1);
[ - - ]
416 [ - + ][ - + ]: 49522 : Assert(args[0].getType().isInteger());
[ - - ]
417 : 49522 : return args[1];
418 : : }
419 [ + + ]: 110937 : else if (id == ProofRule::ENCODE_EQ_INTRO)
420 : : {
421 [ - + ][ - + ]: 6212 : Assert(children.empty());
[ - - ]
422 [ - + ][ - + ]: 6212 : Assert(args.size() == 1);
[ - - ]
423 : 12424 : rewriter::RewriteDbNodeConverter rconv(nodeManager());
424 : : // run a single (small) step conversion
425 : 12424 : Node ac = rconv.postConvert(args[0]);
426 : 6212 : return args[0].eqNode(ac);
427 : : }
428 [ + + ]: 104725 : else if (id == ProofRule::DSL_REWRITE)
429 : : {
430 : : // consult rewrite db, apply args[1]...args[n] as a substitution
431 : : // to variable list and prove equality between LHS and RHS.
432 [ - + ][ - + ]: 95384 : Assert(d_rdb != nullptr);
[ - - ]
433 : : ProofRewriteRule di;
434 [ - + ]: 95384 : if (!rewriter::getRewriteRule(args[0], di))
435 : : {
436 : 0 : return Node::null();
437 : : }
438 : 95384 : const rewriter::RewriteProofRule& rpr = d_rdb->getRule(di);
439 : 95384 : const std::vector<Node>& varList = rpr.getVarList();
440 : 95384 : const std::vector<Node>& conds = rpr.getConditions();
441 : 190768 : std::vector<Node> subs(args.begin() + 1, args.end());
442 [ - + ]: 95384 : if (varList.size() != subs.size())
443 : : {
444 : 0 : return Node::null();
445 : : }
446 : : // check whether child proof match
447 [ - + ]: 95384 : if (conds.size() != children.size())
448 : : {
449 : 0 : return Node::null();
450 : : }
451 [ + + ]: 97713 : for (size_t i = 0, nchildren = children.size(); i < nchildren; i++)
452 : : {
453 : 2329 : Node scond = expr::narySubstitute(conds[i], varList, subs);
454 [ - + ]: 2329 : if (scond != children[i])
455 : : {
456 : 0 : return Node::null();
457 : : }
458 : : }
459 : 95384 : return rpr.getConclusionFor(subs);
460 : : }
461 [ + - ]: 9341 : else if (id == ProofRule::THEORY_REWRITE)
462 : : {
463 [ - + ][ - + ]: 9341 : Assert(args.size() == 2);
[ - - ]
464 : : ProofRewriteRule di;
465 [ - + ]: 9341 : if (!rewriter::getRewriteRule(args[0], di))
466 : : {
467 : 0 : return Node::null();
468 : : }
469 [ - + ]: 9341 : if (args[1].getKind() != Kind::EQUAL)
470 : : {
471 : 0 : return Node::null();
472 : : }
473 : 18682 : Node rhs = d_rewriter->rewriteViaRule(di, args[1][0]);
474 [ + - ][ - + ]: 9341 : if (rhs.isNull() || rhs != args[1][1])
[ + - ][ - + ]
[ - - ]
475 : : {
476 : 0 : return Node::null();
477 : : }
478 : 9341 : return args[1];
479 : : }
480 : : // no rule
481 : 0 : return Node::null();
482 : : }
483 : :
484 : 779018 : bool BuiltinProofRuleChecker::getTheoryId(TNode n, TheoryId& tid)
485 : : {
486 : : uint32_t i;
487 [ - + ]: 779018 : if (!getUInt32(n, i))
488 : : {
489 : 0 : return false;
490 : : }
491 : 779018 : tid = static_cast<TheoryId>(i);
492 : 779018 : return true;
493 : : }
494 : :
495 : 1337930 : Node BuiltinProofRuleChecker::mkTheoryIdNode(TheoryId tid)
496 : : {
497 : : return NodeManager::currentNM()->mkConstInt(
498 : 2675870 : Rational(static_cast<uint32_t>(tid)));
499 : : }
500 : :
501 : : } // namespace builtin
502 : : } // namespace theory
503 : : } // namespace cvc5::internal
|
