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
104
105
106
107
108
109
110
111
|
/******************************************************************************
* Top contributors (to current version):
* Andrew Reynolds, Gereon Kremer
*
* 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.
* ****************************************************************************
*
* Lazy proof utility.
*/
#include "cvc4_private.h"
#ifndef CVC5__EXPR__LAZY_PROOF_H
#define CVC5__EXPR__LAZY_PROOF_H
#include "expr/proof.h"
namespace cvc5 {
class ProofGenerator;
class ProofNodeManager;
/**
* A (context-dependent) lazy proof. This class is an extension of CDProof
* that additionally maps facts to proof generators in a context-dependent
* manner. It extends CDProof with an additional method, addLazyStep for adding
* steps to a proof via a given proof generator.
*/
class LazyCDProof : public CDProof
{
public:
/** Constructor
*
* @param pnm The proof node manager for constructing ProofNode objects.
* @param dpg The (optional) default proof generator, which is called
* for facts that have no explicitly provided generator.
* @param c The context that this class depends on. If none is provided,
* this class is context-independent.
*/
LazyCDProof(ProofNodeManager* pnm,
ProofGenerator* dpg = nullptr,
context::Context* c = nullptr,
std::string name = "LazyCDProof");
~LazyCDProof();
/**
* Get lazy proof for fact, or nullptr if it does not exist. This may
* additionally call proof generators to generate proofs for ASSUME nodes that
* don't yet have a concrete proof.
*/
std::shared_ptr<ProofNode> getProofFor(Node fact) override;
/** Add step by generator
*
* This method stores that expected can be proven by proof generator pg if
* it is required to do so. This mapping is maintained in the remainder of
* the current context (according to the context c provided to this class).
*
* It is important to note that pg is asked to provide a proof for expected
* only when no other call for the fact expected is provided via the addStep
* method of this class. In particular, pg is asked to prove expected when it
* appears as the conclusion of an ASSUME leaf within CDProof::getProofFor.
*
* @param expected The fact that can be proven.
* @param pg The generator that can proof expected.
* @param trustId If a null proof generator is provided, we add a step to
* the proof that has trustId as the rule and expected as the sole argument.
* We do this only if trustId is not PfRule::ASSUME. This is primarily used
* for identifying the kind of hole when a proof generator is not given.
* @param isClosed Whether to expect that pg can provide a closed proof for
* this fact.
* @param ctx The context we are in (for debugging).
* @param forceOverwrite If this flag is true, then this call overwrites
* an existing proof generator provided for expected, if one was provided
* via a previous call to addLazyStep in the current context.
*/
void addLazyStep(Node expected,
ProofGenerator* pg,
PfRule trustId = PfRule::ASSUME,
bool isClosed = false,
const char* ctx = "LazyCDProof::addLazyStep",
bool forceOverwrite = false);
/**
* Does this have any proof generators? This method always returns true
* if the default is non-null.
*/
bool hasGenerators() const;
/** Does the given fact have an explicitly provided generator? */
bool hasGenerator(Node fact) const;
protected:
typedef context::CDHashMap<Node, ProofGenerator*, NodeHashFunction>
NodeProofGeneratorMap;
/** Maps facts that can be proven to generators */
NodeProofGeneratorMap d_gens;
/** The default proof generator */
ProofGenerator* d_defaultGen;
/**
* Get generator for fact, or nullptr if it doesnt exist. This method is
* robust to symmetry of (dis)equality. It updates isSym to true if a
* proof generator for the symmetric form of fact was provided.
*/
ProofGenerator* getGeneratorFor(Node fact, bool& isSym);
};
} // namespace cvc5
#endif /* CVC5__EXPR__LAZY_PROOF_H */
|
