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
155
156
157
158
159
160
161
162
163
164
165
166
|
/********************* */
/*! \file infer_proof_cons.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2019 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.\endverbatim
**
** \brief Inference to proof conversion
**/
#include "cvc4_private.h"
#ifndef CVC4__THEORY__STRINGS__INFER_PROOF_CONS_H
#define CVC4__THEORY__STRINGS__INFER_PROOF_CONS_H
#include <vector>
#include "expr/node.h"
#include "expr/proof_checker.h"
#include "expr/proof_rule.h"
#include "expr/proof_step_buffer.h"
#include "theory/builtin/proof_checker.h"
#include "theory/strings/infer_info.h"
#include "theory/strings/sequences_stats.h"
#include "theory/uf/proof_equality_engine.h"
namespace CVC4 {
namespace theory {
namespace strings {
/**
* Converts between the strings-specific (untrustworthy) InferInfo class and
* information about how to construct a trustworthy proof step, e.g.
* (PfRule, children, args).
*
* It also may act as a (lazy) proof generator.
*/
class InferProofCons : public ProofGenerator
{
typedef context::CDHashMap<Node, std::shared_ptr<InferInfo>, NodeHashFunction>
NodeInferInfoMap;
public:
InferProofCons(context::Context* c,
ProofNodeManager* pnm,
SequencesStatistics& statistics,
bool pfEnabled);
~InferProofCons() {}
/**
* This is called to notify that ii is an inference that may need a proof
* in the future.
*
* In detail, this class should be prepared to respond to a call to:
* addProofTo(ii.d_conc, ...)
* in the remainder of the SAT context. This method copies ii and stores it
* in the context-dependent map d_lazyFactMap below.
*
* This is used for lazy proof construction, where proofs are constructed
* only for facts that are explained.
*/
void notifyFact(const InferInfo& ii);
/** convert
*
* This method is called when the theory of strings makes an inference
* described by an inference info ii, which is of the form:
* (<conclusion>, <Inference_id>, <antecendant>).
*
* This method converts this call to instructions on what the proof rule
* step(s) are for concluding the conclusion of the inference. This
* information is stored in the argument ps, which consists of:
* (1) A proof rule identifier (d_rule).
* (2) The premises of the proof step (d_children).
* (3) Arguments to the proof step (d_args).
*
* NOTE: if the proof for the inference cannot be captured by a single
* step, then the d_rule field of ps is not set, and useBuffer is set to
* true. In this case, the ProofStepBuffer of this class contains (multiple)
* steps for how to construct a proof for the inference. This buffer can be
* obtained by getBuffer() below.
*
* This method returns the conclusion of ii.
*/
Node convert(const InferInfo& ii, ProofStep& ps, bool& useBuffer);
/**
* Internal version of above, where the fields of ii have been expanded
* into separate arguments.
*/
Node convert(Inference infer,
bool isRev,
Node conc,
const std::vector<Node>& exp,
ProofStep& ps,
bool& useBuffer);
/** Get the proof step buffer */
ProofStepBuffer* getBuffer();
/** Get the proof for formula f */
std::shared_ptr<ProofNode> getProofFor(Node f) override;
/**
* This adds the proof steps for fact to proof pf with the given overwrite
* policy. This is required for using this class as a lazy proof generator.
*
* It should be the case that a call was made to convert(...), where conc
* was fact, in the current SAT context.
*/
bool addProofTo(Node fact, CDProof* pf, bool forceOverwrite = false) override;
/** Identify this generator (for debugging, etc..) */
virtual std::string identify() const override;
private:
/**
* Convert length proof. If this method returns true, it adds proof step(s)
* to the buffer that conclude lenReq from premises lenExp.
*/
bool convertLengthPf(Node lenReq, const std::vector<Node>& lenExp);
/**
* Apply macro transform. If this method returns true, it adds proof step(s)
* to the buffer that conclude tgt from premises src, exp. In particular,
* it may attempt to apply MACRO_SR_PRED_TRANSFORM. This method should be
* applied when src and tgt are equivalent formulas assuming exp.
*/
bool convertPredTransform(Node src,
Node tgt,
const std::vector<Node>& exp,
MethodId ids = MethodId::SB_DEFAULT,
MethodId idr = MethodId::RW_REWRITE);
/**
*/
bool convertPredIntro(Node tgt,
const std::vector<Node>& exp,
MethodId ids = MethodId::SB_DEFAULT,
MethodId idr = MethodId::RW_REWRITE);
/**
*/
Node convertPredElim(Node src,
const std::vector<Node>& exp,
MethodId ids = MethodId::SB_DEFAULT,
MethodId idr = MethodId::RW_REWRITE);
/** Add method ids */
void addMethodIds(std::vector<Node>& args, MethodId ids, MethodId idr);
/**
*/
Node convertTrans(Node eqa, Node eqb);
/** Is symm */
static bool isSymm(Node src, Node tgt);
/** the proof node manager */
ProofNodeManager* d_pnm;
/** The lazy fact map */
NodeInferInfoMap d_lazyFactMap;
/** The proof step buffer */
ProofStepBuffer d_psb;
/** Reference to the statistics for the theory of strings/sequences. */
SequencesStatistics& d_statistics;
/** Whether proofs are enabled */
bool d_pfEnabled;
};
} // namespace strings
} // namespace theory
} // namespace CVC4
#endif /* CVC4__THEORY__STRINGS__INFER_PROOF_CONS_H */
|
