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
|
/******************************************************************************
* 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.
* ****************************************************************************
*
* Trust substitutions.
*/
#include "cvc5_private.h"
#ifndef CVC5__THEORY__TRUST_SUBSTITUTIONS_H
#define CVC5__THEORY__TRUST_SUBSTITUTIONS_H
#include "context/cdhashmap.h"
#include "context/cdlist.h"
#include "context/context.h"
#include "expr/lazy_proof.h"
#include "expr/proof_node_manager.h"
#include "expr/proof_set.h"
#include "expr/term_conversion_proof_generator.h"
#include "theory/eager_proof_generator.h"
#include "theory/substitutions.h"
#include "theory/theory_proof_step_buffer.h"
#include "theory/trust_node.h"
namespace cvc5 {
namespace theory {
/**
* A layer on top of SubstitutionMap that tracks proofs.
*/
class TrustSubstitutionMap : public ProofGenerator
{
using NodeUIntMap = context::CDHashMap<Node, size_t>;
public:
TrustSubstitutionMap(context::Context* c,
ProofNodeManager* pnm = nullptr,
std::string name = "TrustSubstitutionMap",
PfRule trustId = PfRule::PREPROCESS_LEMMA,
MethodId ids = MethodId::SB_DEFAULT);
/** Set proof node manager */
void setProofNodeManager(ProofNodeManager* pnm);
/** Gets a reference to the underlying substitution map */
SubstitutionMap& get();
/**
* Add substitution x -> t, where pg can provide a closed proof of (= x t)
* in the remainder of this user context.
*/
void addSubstitution(TNode x, TNode t, ProofGenerator* pg = nullptr);
/**
* Add substitution x -> t from a single proof step with rule id, no children
* and arguments args.
*/
void addSubstitution(TNode x,
TNode t,
PfRule id,
const std::vector<Node>& children,
const std::vector<Node>& args);
/**
* Add substitution x -> t, which was derived from the proven field of
* trust node tn. In other words, (= x t) is the solved form of
* tn.getProven(). This method is a helper function for methods (e.g.
* ppAssert) that put literals into solved form. It should be the case
* that (= x t) and tn.getProven() can be shown equivalent by rewriting.
*
* This ensures that we add a substitution with a proof
* based on transforming the tn.getProven() to (= x t) if tn has a
* non-null proof generator; otherwise if tn has no proof generator
* we simply add the substitution.
*
* @return The proof generator that can prove (= x t).
*/
ProofGenerator* addSubstitutionSolved(TNode x, TNode t, TrustNode tn);
/**
* Add substitutions from trust substitution map t. This adds all
* substitutions from the map t and carries over its information about proofs.
*/
void addSubstitutions(TrustSubstitutionMap& t);
/**
* Apply substitutions in this class to node n. Returns a trust node
* proving n = n*sigma, where the proof generator is provided by this class
* (when proofs are enabled).
*/
TrustNode applyTrusted(Node n, bool doRewrite = true);
/** Same as above, without proofs */
Node apply(Node n, bool doRewrite = true);
/** Get the proof for formula f */
std::shared_ptr<ProofNode> getProofFor(Node f) override;
/** Identify */
std::string identify() const override;
private:
/** Are proofs enabled? */
bool isProofEnabled() const;
/**
* Get the substitution up to index
*/
Node getSubstitution(size_t index);
/** The context used here */
context::Context* d_ctx;
/** The substitution map */
SubstitutionMap d_subs;
/** A context-dependent list of trust nodes */
context::CDList<TrustNode> d_tsubs;
/** Theory proof step buffer */
std::unique_ptr<TheoryProofStepBuffer> d_tspb;
/** A lazy proof for substitution steps */
std::unique_ptr<LazyCDProof> d_subsPg;
/** A lazy proof for apply steps */
std::unique_ptr<LazyCDProof> d_applyPg;
/**
* A context-dependent list of LazyCDProof, allocated for internal steps.
*/
std::unique_ptr<CDProofSet<LazyCDProof>> d_helperPf;
/** Name for debugging */
std::string d_name;
/**
* The placeholder trusted PfRule identifier for calls to addSubstitution
* that are not given proof generators.
*/
PfRule d_trustId;
/** The method id for which form of substitution to apply */
MethodId d_ids;
/**
* Map from solved equalities to the size of d_tsubs at the time they
* were concluded. Notice this is required so that we can reconstruct
* proofs for substitutions after they have become invalidated by later
* calls to addSubstitution. For example, if we call:
* addSubstitution x -> y
* addSubstitution z -> w
* apply f(x), returns f(y)
* addSubstitution y -> w
* We map (= (f x) (f y)) to index 2, since we only should apply the first
* two substitutions but not the third when asked to prove this equality.
*/
NodeUIntMap d_eqtIndex;
};
} // namespace theory
} // namespace cvc5
#endif /* CVC5__THEORY__TRUST_SUBSTITUTIONS_H */
|
