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