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
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
|
/******************************************************************************
* Top contributors (to current version):
* Haniel Barbosa, 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 chain utility.
*/
#include "cvc4_private.h"
#ifndef CVC5__EXPR__LAZY_PROOF_CHAIN_H
#define CVC5__EXPR__LAZY_PROOF_CHAIN_H
#include <vector>
#include "context/cdhashmap.h"
#include "expr/proof_generator.h"
namespace cvc5 {
class ProofNodeManager;
/**
* A (context-dependent) lazy generator for proof chains. This class is an
* extension of ProofGenerator that additionally that maps facts to proof
* generators in a context-dependent manner. The map is built with the addition
* of lazy steps mapping facts to proof generators. More importantly, its
* getProofFor method expands the proof generators registered to this class by
* connecting, for the proof generated to one fact, assumptions to the proofs
* generated for those assumptinos that are registered in the chain.
*/
class LazyCDProofChain : public ProofGenerator
{
public:
/** Constructor
*
* @param pnm The proof node manager for constructing ProofNode objects.
* @param cyclic Whether this instance is robust to cycles in the chain.
* @param c The context that this class depends on. If none is provided,
* this class is context-independent.
* @param defGen The default generator to be used if no generator exists
* for a step.
* @param defRec Whether this instance expands proofs from defGen recursively.
*/
LazyCDProofChain(ProofNodeManager* pnm,
bool cyclic = true,
context::Context* c = nullptr,
ProofGenerator* defGen = nullptr,
bool defRec = true);
~LazyCDProofChain();
/**
* Get lazy proof for fact, or nullptr if it does not exist, by connecting the
* proof nodes generated for each intermediate relevant fact registered in the
* chain (i.e., in the domain of d_gens).
*
* For example, if d_gens consists of the following pairs
*
* --- (A, PG1)
* --- (B, PG2)
* --- (C, PG3)
*
* and getProofFor(A) is called, with PG1 generating a proof with assumptions
* B and D, then B is expanded, with its assumption proof node being updated
* to the expanded proof node, while D is not. Assuming PG2 provides a proof
* with assumptions C and E, then C is expanded and E is not. Suppose PG3
* gives a closed proof, thus the call getProofFor(A) produces a proof node
*
* A : ( ... B : ( ... C : (...), ... ASSUME( E ) ), ... ASSUME( D ) )
*
* Note that the expansions are done directly on the proof nodes produced by
* the generators.
*
* If this instance has been set to be robust to cyclic proofs (i.e., d_cyclic
* is true), then the construction of the proof chain checks that there are no
* cycles, i.e., a given fact would have itself as an assumption when
* connecting the chain links. If such a cycle were to be detected then the
* fact will be marked as an assumption and not expanded in the final proof
* node. The method does not fail.
*/
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).
*
* Moreover the lazy steps of this class are expected to fulfill the
* requirement that pg.getProofFor(expected) generates a proof node closed
* with relation to
* (1) a fixed set F1, ..., Fn,
* (2) formulas in the current domain of d_gens.
*
* This is so that we only add links to the chain that depend on a fixed set
* of assumptions or in other links.
*
* @param expected The fact that can be proven.
* @param pg The generator that can proof expected.
* @param assumptions The fixed set of assumptions with relation to which the
* chain, now augmented with expect, must be closed.
* @param ctx The context we are in (for debugging).
*/
void addLazyStep(Node expected,
ProofGenerator* pg,
const std::vector<Node>& assumptions,
const char* ctx = "LazyCDProofChain::addLazyStep");
/** As above but does not do the closedness check. */
void addLazyStep(Node expected, ProofGenerator* pg);
/** Does the given fact have an explicitly provided generator? */
bool hasGenerator(Node fact) const;
/**
* Get generator for fact, or nullptr if it doesnt exist.
*/
ProofGenerator* getGeneratorFor(Node fact);
/** identify */
std::string identify() const override;
/** Retrieve, for each fact in d_gens, it mapped to the proof node generated
* by its generator in d_gens. */
const std::map<Node, std::shared_ptr<ProofNode>> getLinks() const;
private:
/**
* Get generator for fact, or nullptr if it doesnt exist. Updates rec to
* true if we should recurse on its proof.
*/
ProofGenerator* getGeneratorForInternal(Node fact, bool& rec);
/** The proof manager, used for allocating new ProofNode objects */
ProofNodeManager* d_manager;
/** Whether this instance is robust to cycles in the chain. */
bool d_cyclic;
/** Whether we expand recursively (for the default generator) */
bool d_defRec;
/** A dummy context used by this class if none is provided */
context::Context d_context;
/** Maps facts that can be proven to generators */
context::CDHashMap<Node, ProofGenerator*, NodeHashFunction> d_gens;
/** The default proof generator (if one exists) */
ProofGenerator* d_defGen;
};
} // namespace cvc5
#endif /* CVC5__EXPR__LAZY_PROOF_CHAIN_H */
|
