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 the abstract proof generator class.
11 : : */
12 : :
13 : : #include "proof/eager_proof_generator.h"
14 : :
15 : : #include "proof/proof.h"
16 : : #include "proof/proof_node.h"
17 : : #include "proof/proof_node_manager.h"
18 : : #include "rewriter/rewrites.h"
19 : : #include "smt/env.h"
20 : :
21 : : namespace cvc5::internal {
22 : :
23 : 478418 : EagerProofGenerator::EagerProofGenerator(Env& env,
24 : : context::Context* c,
25 : 478418 : std::string name)
26 [ + + ]: 478418 : : EnvObj(env), d_name(name), d_proofs(c == nullptr ? &d_context : c)
27 : : {
28 : 478418 : }
29 : :
30 : 3174553 : void EagerProofGenerator::setProofFor(Node f, std::shared_ptr<ProofNode> pf)
31 : : {
32 : : // pf should prove f
33 [ - + ][ - - ]: 6349106 : Assert(pf->getResult() == f)
34 : 0 : << "EagerProofGenerator::setProofFor: unexpected result" << std::endl
35 [ - + ][ - - ]: 3174553 : << "Expected: " << f << std::endl
36 : 3174553 : << "Actual: " << pf->getResult() << std::endl;
37 : 3174553 : d_proofs[f] = pf;
38 : 3174553 : }
39 : 71060 : void EagerProofGenerator::setProofForConflict(Node conf,
40 : : std::shared_ptr<ProofNode> pf)
41 : : {
42 : : // Normalize based on key
43 : 71060 : Node ckey = TrustNode::getConflictProven(conf);
44 : 71060 : setProofFor(ckey, pf);
45 : 71060 : }
46 : :
47 : 2383013 : void EagerProofGenerator::setProofForLemma(Node lem,
48 : : std::shared_ptr<ProofNode> pf)
49 : : {
50 : : // Normalize based on key
51 : 2383013 : Node lkey = TrustNode::getLemmaProven(lem);
52 : 2383013 : setProofFor(lkey, pf);
53 : 2383013 : }
54 : :
55 : 370083 : void EagerProofGenerator::setProofForPropExp(TNode lit,
56 : : Node exp,
57 : : std::shared_ptr<ProofNode> pf)
58 : : {
59 : : // Normalize based on key
60 : 740166 : Node pekey = TrustNode::getPropExpProven(lit, exp);
61 : 370083 : setProofFor(pekey, pf);
62 : 370083 : }
63 : :
64 : 414534 : std::shared_ptr<ProofNode> EagerProofGenerator::getProofFor(Node f)
65 : : {
66 : 414534 : NodeProofNodeMap::iterator it = d_proofs.find(f);
67 [ + + ]: 414534 : if (it == d_proofs.end())
68 : : {
69 : 9415 : return nullptr;
70 : : }
71 : 405119 : return (*it).second;
72 : : }
73 : :
74 : 7904086 : bool EagerProofGenerator::hasProofFor(Node f)
75 : : {
76 : 7904086 : return d_proofs.find(f) != d_proofs.end();
77 : : }
78 : :
79 : 2414796 : TrustNode EagerProofGenerator::mkTrustNode(Node n,
80 : : std::shared_ptr<ProofNode> pf,
81 : : bool isConflict)
82 : : {
83 [ - + ]: 2414796 : if (pf == nullptr)
84 : : {
85 : 0 : return TrustNode::null();
86 : : }
87 [ + + ]: 2414796 : if (isConflict)
88 : : {
89 : : // this shouldnt modify the key
90 : 52688 : setProofForConflict(n, pf);
91 : : // we can now return the trust node
92 : 52688 : return TrustNode::mkTrustConflict(n, this);
93 : : }
94 : : // this shouldnt modify the key
95 : 2362108 : setProofForLemma(n, pf);
96 : : // we can now return the trust node
97 : 2362108 : return TrustNode::mkTrustLemma(n, this);
98 : : }
99 : :
100 : 33711 : TrustNode EagerProofGenerator::mkTrustNode(Node conc,
101 : : ProofRule id,
102 : : const std::vector<Node>& exp,
103 : : const std::vector<Node>& args,
104 : : bool isConflict)
105 : : {
106 : 33711 : ProofNodeManager* pnm = d_env.getProofNodeManager();
107 : : // if no children, its easy
108 [ + + ]: 33711 : if (exp.empty())
109 : : {
110 : : // do not use "conc" as expected here, instead this will be checked
111 : : // later in setProofFor, where conc may be negated if isConflict is true
112 : 60686 : std::shared_ptr<ProofNode> pf = pnm->mkNode(id, {}, args);
113 : 30343 : return mkTrustNode(conc, pf, isConflict);
114 : 30343 : }
115 : : // otherwise, we use CDProof + SCOPE
116 : 6736 : CDProof cdp(d_env);
117 : 3368 : cdp.addStep(conc, id, exp, args);
118 : 3368 : std::shared_ptr<ProofNode> pf = cdp.getProofFor(conc);
119 : : // We use mkNode instead of mkScope, since there is no reason to check
120 : : // whether the free assumptions of pf are in exp, since they are by the
121 : : // construction above.
122 : 13472 : std::shared_ptr<ProofNode> pfs = pnm->mkNode(ProofRule::SCOPE, {pf}, exp);
123 : 6736 : return mkTrustNode(pfs->getResult(), pfs, isConflict);
124 : 3368 : }
125 : :
126 : 1138 : TrustNode EagerProofGenerator::mkTrustNodeTrusted(Node conc,
127 : : TrustId id,
128 : : const std::vector<Node>& exp,
129 : : const std::vector<Node>& args,
130 : : bool isConflict)
131 : : {
132 : 1138 : std::vector<Node> targs;
133 : 1138 : targs.push_back(mkTrustId(nodeManager(), id));
134 [ + - ]: 1138 : targs.push_back(isConflict ? conc.notNode() : conc);
135 : 1138 : targs.insert(targs.end(), args.begin(), args.end());
136 : 2276 : return mkTrustNode(conc, ProofRule::TRUST, exp, targs, isConflict);
137 : 1138 : }
138 : :
139 : 0 : TrustNode EagerProofGenerator::mkTrustNodeRewrite(const Node& a,
140 : : const Node& b,
141 : : ProofRewriteRule id)
142 : : {
143 : 0 : std::vector<Node> args;
144 : 0 : args.push_back(rewriter::mkRewriteRuleNode(nodeManager(), id));
145 : 0 : args.push_back(a.eqNode(b));
146 : 0 : return mkTrustedRewrite(a, b, ProofRule::THEORY_REWRITE, args);
147 : 0 : }
148 : :
149 : 27405 : TrustNode EagerProofGenerator::mkTrustedRewrite(Node a,
150 : : Node b,
151 : : std::shared_ptr<ProofNode> pf)
152 : : {
153 [ - + ]: 27405 : if (pf == nullptr)
154 : : {
155 : 0 : return TrustNode::null();
156 : : }
157 : 27405 : Node eq = a.eqNode(b);
158 : 27405 : setProofFor(eq, pf);
159 : 27405 : return TrustNode::mkTrustRewrite(a, b, this);
160 : 27405 : }
161 : :
162 : 240 : TrustNode EagerProofGenerator::mkTrustedRewrite(Node a,
163 : : Node b,
164 : : ProofRule id,
165 : : const std::vector<Node>& args)
166 : : {
167 : 240 : Node eq = a.eqNode(b);
168 : 480 : CDProof cdp(d_env);
169 : 240 : cdp.addStep(eq, id, {}, args);
170 : 240 : std::shared_ptr<ProofNode> pf = cdp.getProofFor(eq);
171 : 480 : return mkTrustedRewrite(a, b, pf);
172 : 240 : }
173 : :
174 : 18124 : TrustNode EagerProofGenerator::mkTrustedPropagation(
175 : : Node n, Node exp, std::shared_ptr<ProofNode> pf)
176 : : {
177 [ - + ]: 18124 : if (pf == nullptr)
178 : : {
179 : 0 : return TrustNode::null();
180 : : }
181 : 18124 : setProofForPropExp(n, exp, pf);
182 : 18124 : return TrustNode::mkTrustPropExp(n, exp, this);
183 : : }
184 : :
185 : 4040 : TrustNode EagerProofGenerator::mkTrustNodeSplit(Node f)
186 : : {
187 : : // make the lemma
188 : 4040 : Node lem = f.orNode(f.notNode());
189 : 12120 : return mkTrustNode(lem, ProofRule::SPLIT, {}, {f}, false);
190 : 4040 : }
191 : :
192 : 7527 : std::string EagerProofGenerator::identify() const { return d_name; }
193 : :
194 : : } // namespace cvc5::internal
|
