1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Haniel Barbosa |
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 |
|
* Implementation of a proof generator for buffered proof steps. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "proof/buffered_proof_generator.h" |
17 |
|
|
18 |
|
#include "proof/proof.h" |
19 |
|
#include "proof/proof_node_manager.h" |
20 |
|
|
21 |
|
namespace cvc5 { |
22 |
|
|
23 |
722 |
BufferedProofGenerator::BufferedProofGenerator(context::Context* c, |
24 |
722 |
ProofNodeManager* pnm) |
25 |
722 |
: ProofGenerator(), d_facts(c), d_pnm(pnm) |
26 |
|
{ |
27 |
722 |
} |
28 |
|
|
29 |
231 |
bool BufferedProofGenerator::addStep(Node fact, |
30 |
|
ProofStep ps, |
31 |
|
CDPOverwrite opolicy) |
32 |
|
{ |
33 |
|
// check duplicates if we are not always overwriting |
34 |
231 |
if (opolicy != CDPOverwrite::ALWAYS) |
35 |
|
{ |
36 |
231 |
if (d_facts.find(fact) != d_facts.end()) |
37 |
|
{ |
38 |
|
// duplicate |
39 |
|
return false; |
40 |
|
} |
41 |
462 |
Node symFact = CDProof::getSymmFact(fact); |
42 |
231 |
if (!symFact.isNull()) |
43 |
|
{ |
44 |
140 |
if (d_facts.find(symFact) != d_facts.end()) |
45 |
|
{ |
46 |
|
// duplicate due to symmetry |
47 |
|
return false; |
48 |
|
} |
49 |
|
} |
50 |
|
} |
51 |
|
// note that this replaces the value fact is mapped to if there is already one |
52 |
231 |
d_facts.insert(fact, std::make_shared<ProofStep>(ps)); |
53 |
231 |
return true; |
54 |
|
} |
55 |
|
|
56 |
60 |
std::shared_ptr<ProofNode> BufferedProofGenerator::getProofFor(Node fact) |
57 |
|
{ |
58 |
120 |
Trace("pfee-fact-gen") << "BufferedProofGenerator::getProofFor: " << fact |
59 |
60 |
<< std::endl; |
60 |
60 |
NodeProofStepMap::iterator it = d_facts.find(fact); |
61 |
60 |
if (it == d_facts.end()) |
62 |
|
{ |
63 |
|
Node symFact = CDProof::getSymmFact(fact); |
64 |
|
if (symFact.isNull()) |
65 |
|
{ |
66 |
|
Trace("pfee-fact-gen") << "...cannot find step" << std::endl; |
67 |
|
Assert(false); |
68 |
|
return nullptr; |
69 |
|
} |
70 |
|
it = d_facts.find(symFact); |
71 |
|
if (it == d_facts.end()) |
72 |
|
{ |
73 |
|
Assert(false); |
74 |
|
Trace("pfee-fact-gen") << "...cannot find step (no sym)" << std::endl; |
75 |
|
return nullptr; |
76 |
|
} |
77 |
|
} |
78 |
60 |
Trace("pfee-fact-gen") << "...return via step " << *(*it).second << std::endl; |
79 |
120 |
CDProof cdp(d_pnm); |
80 |
60 |
cdp.addStep(fact, *(*it).second); |
81 |
60 |
return cdp.getProofFor(fact); |
82 |
|
} |
83 |
|
|
84 |
47 |
bool BufferedProofGenerator::hasProofFor(Node f) |
85 |
|
{ |
86 |
47 |
NodeProofStepMap::iterator it = d_facts.find(f); |
87 |
47 |
if (it == d_facts.end()) |
88 |
|
{ |
89 |
46 |
Node symFact = CDProof::getSymmFact(f); |
90 |
46 |
if (symFact.isNull()) |
91 |
|
{ |
92 |
36 |
return false; |
93 |
|
} |
94 |
10 |
it = d_facts.find(symFact); |
95 |
10 |
if (it == d_facts.end()) |
96 |
|
{ |
97 |
10 |
return false; |
98 |
|
} |
99 |
|
} |
100 |
1 |
return true; |
101 |
|
} |
102 |
|
|
103 |
22746 |
} // namespace cvc5 |