1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Aina Niemetz |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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 |
|
* The theory engine proof generator. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/theory_engine_proof_generator.h" |
17 |
|
|
18 |
|
#include <sstream> |
19 |
|
|
20 |
|
#include "proof/proof_node.h" |
21 |
|
|
22 |
|
using namespace cvc5::kind; |
23 |
|
|
24 |
|
namespace cvc5 { |
25 |
|
|
26 |
6271 |
TheoryEngineProofGenerator::TheoryEngineProofGenerator(ProofNodeManager* pnm, |
27 |
6271 |
context::UserContext* u) |
28 |
6271 |
: d_pnm(pnm), d_proofs(u) |
29 |
|
{ |
30 |
6271 |
d_false = NodeManager::currentNM()->mkConst(false); |
31 |
6271 |
} |
32 |
|
|
33 |
586 |
TrustNode TheoryEngineProofGenerator::mkTrustExplain( |
34 |
|
TNode lit, Node exp, std::shared_ptr<LazyCDProof> lpf) |
35 |
|
{ |
36 |
1172 |
Node p; |
37 |
586 |
TrustNode trn; |
38 |
586 |
if (lit == d_false) |
39 |
|
{ |
40 |
|
// propagation of false is a conflict |
41 |
|
trn = TrustNode::mkTrustConflict(exp, this); |
42 |
|
p = trn.getProven(); |
43 |
|
Assert(p.getKind() == NOT); |
44 |
|
} |
45 |
|
else |
46 |
|
{ |
47 |
586 |
trn = TrustNode::mkTrustPropExp(lit, exp, this); |
48 |
586 |
p = trn.getProven(); |
49 |
586 |
Assert(p.getKind() == IMPLIES && p.getNumChildren() == 2); |
50 |
|
} |
51 |
|
// should not already be proven |
52 |
586 |
NodeLazyCDProofMap::iterator it = d_proofs.find(p); |
53 |
586 |
if (it == d_proofs.end()) |
54 |
|
{ |
55 |
|
// we will prove the fact p using the proof from lpf. |
56 |
584 |
d_proofs.insert(p, lpf); |
57 |
|
} |
58 |
1172 |
return trn; |
59 |
|
} |
60 |
|
|
61 |
230 |
std::shared_ptr<ProofNode> TheoryEngineProofGenerator::getProofFor(Node f) |
62 |
|
{ |
63 |
460 |
Trace("tepg-debug") << "TheoryEngineProofGenerator::getProofFor: " << f |
64 |
230 |
<< std::endl; |
65 |
230 |
NodeLazyCDProofMap::iterator it = d_proofs.find(f); |
66 |
230 |
if (it == d_proofs.end()) |
67 |
|
{ |
68 |
|
Trace("tepg-debug") << "...null" << std::endl; |
69 |
|
return nullptr; |
70 |
|
} |
71 |
460 |
std::shared_ptr<LazyCDProof> lcp = (*it).second; |
72 |
|
// finalize it via scope |
73 |
460 |
std::vector<Node> scopeAssumps; |
74 |
|
// should only ask this generator for proofs of implications, or conflicts |
75 |
460 |
Node exp; |
76 |
460 |
Node conclusion; |
77 |
230 |
if (f.getKind() == IMPLIES && f.getNumChildren() == 2) |
78 |
|
{ |
79 |
230 |
exp = f[0]; |
80 |
230 |
conclusion = f[1]; |
81 |
|
} |
82 |
|
else if (f.getKind() == NOT) |
83 |
|
{ |
84 |
|
exp = f[0]; |
85 |
|
conclusion = d_false; |
86 |
|
} |
87 |
|
else |
88 |
|
{ |
89 |
|
Unhandled() << "TheoryEngineProofGenerator::getProofFor: unexpected fact " |
90 |
|
<< f << std::endl; |
91 |
|
return nullptr; |
92 |
|
} |
93 |
|
// get the assumptions to assume in a scope |
94 |
230 |
if (exp.getKind() == AND) |
95 |
|
{ |
96 |
1111 |
for (const Node& fc : exp) |
97 |
|
{ |
98 |
921 |
scopeAssumps.push_back(fc); |
99 |
|
} |
100 |
|
} |
101 |
|
else |
102 |
|
{ |
103 |
40 |
scopeAssumps.push_back(exp); |
104 |
|
} |
105 |
230 |
Trace("tepg-debug") << "...get proof body" << std::endl; |
106 |
|
// get the proof for conclusion |
107 |
460 |
std::shared_ptr<ProofNode> pfb = lcp->getProofFor(conclusion); |
108 |
230 |
Trace("tepg-debug") << "...mkScope" << std::endl; |
109 |
|
// call the scope method of proof node manager |
110 |
460 |
std::shared_ptr<ProofNode> pf = d_pnm->mkScope(pfb, scopeAssumps); |
111 |
|
|
112 |
230 |
if (pf->getResult() != f) |
113 |
|
{ |
114 |
|
std::stringstream serr; |
115 |
|
serr << "TheoryEngineProofGenerator::getProofFor: Proof: " << std::endl; |
116 |
|
serr << *pf << std::endl; |
117 |
|
serr << "TheoryEngineProofGenerator::getProofFor: unexpected return proof" |
118 |
|
<< std::endl; |
119 |
|
serr << " Expected: " << f << std::endl; |
120 |
|
serr << " Got: " << pf->getResult() << std::endl; |
121 |
|
Unhandled() << serr.str(); |
122 |
|
} |
123 |
230 |
Trace("tepg-debug") << "...finished" << std::endl; |
124 |
230 |
return pf; |
125 |
|
} |
126 |
|
|
127 |
1530 |
std::string TheoryEngineProofGenerator::identify() const |
128 |
|
{ |
129 |
1530 |
return "TheoryEngineProofGenerator"; |
130 |
|
} |
131 |
|
|
132 |
22746 |
} // namespace cvc5 |