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
|
/********************* */
/*! \file tconv_seq_proof_generator.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds, Gereon Kremer
** This file is part of the CVC4 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.\endverbatim
**
** \brief Term conversion sequence proof generator utility
**/
#include "cvc4_private.h"
#ifndef CVC4__EXPR__TCONV_SEQ_PROOF_GENERATOR_H
#define CVC4__EXPR__TCONV_SEQ_PROOF_GENERATOR_H
#include "context/cdhashmap.h"
#include "expr/node.h"
#include "expr/proof_generator.h"
#include "theory/trust_node.h"
namespace CVC4 {
class ProofNodeManager;
/**
* The term conversion sequence proof generator. This is used for maintaining
* a fixed sequence of proof generators that provide proofs for rewrites
* (equalities). We call these the "component generators" of this sequence,
* which are typically TConvProofGenerator.
*/
class TConvSeqProofGenerator : public ProofGenerator
{
public:
/**
* @param pnm The proof node manager for constructing ProofNode objects.
* @param ts The list of component term conversion generators that are
* applied in sequence
* @param c The context that this class depends on. If none is provided,
* this class is context-independent.
* @param name The name of this generator (for debugging).
*/
TConvSeqProofGenerator(ProofNodeManager* pnm,
const std::vector<ProofGenerator*>& ts,
context::Context* c = nullptr,
std::string name = "TConvSeqProofGenerator");
~TConvSeqProofGenerator();
/**
* Indicate that the index^th proof generator converts term t to s. This
* should be called for a unique s for each (t, index). It must be the
* case that d_tconv[index] can provide a proof for t = s in the remainder
* of the context maintained by this class.
*/
void registerConvertedTerm(Node t, Node s, size_t index);
/**
* Get the proof for formula f. It should be the case that f is of the form
* t_0 = t_n, where it must be the case that t_n is obtained by the following:
* For each i=0, ... n, let t_{i+1} be the term such that
* registerConvertedTerm(t_i, t_{i+1}, i)
* was called. Otherwise t_{i+1} = t_i.
* In other words, t_n is obtained by converting t_0, in order, based on the
* calls to registerConvertedTerm.
*
* @param f The equality fact to get the proof for.
* @return The proof for f.
*/
std::shared_ptr<ProofNode> getProofFor(Node f) override;
/**
* Get subsequence proof for f, with given start and end steps (inclusive).
*/
std::shared_ptr<ProofNode> getSubsequenceProofFor(Node f,
size_t start,
size_t end);
/** Identify this generator (for debugging, etc..) */
std::string identify() const override;
/**
* Make trust node from a sequence of converted terms. The number of
* terms in cterms should be 1 + the number of component proof generators
* maintained by this class. This selects a proof generator that is capable
* of proving cterms[0] = cterms[cterms.size()-1], which is either this
* generator, or one of the component proof generators, if only one step
* rewrote. In the former case, all steps are registered to this class.
* Using a component generator is an optimization that saves having to
* save the conversion steps or use this class. For example, if we have 2
* term conversion components, and call this method on:
* { a, b, c }
* then this method calls:
* registerConvertedTerm( a, b, 0 )
* registerConvertedTerm( b, c, 1 )
* and returns a trust node proving (= a c) with this class as the proof
* generator. On the other hand, if we call this method on:
* { d, d, e }
* then we return a trust node proving (= d e) with the 2nd component proof
* generator, as it alone is capable of proving this equality.
*/
theory::TrustNode mkTrustRewriteSequence(const std::vector<Node>& cterms);
protected:
using NodeIndexPairHashFunction =
PairHashFunction<Node, size_t, NodeHashFunction>;
typedef context::
CDHashMap<std::pair<Node, size_t>, Node, NodeIndexPairHashFunction>
NodeIndexNodeMap;
/** The proof node manager */
ProofNodeManager* d_pnm;
/** The term conversion generators */
std::vector<ProofGenerator*> d_tconvs;
/** the set of converted terms */
NodeIndexNodeMap d_converted;
/** Name identifier */
std::string d_name;
};
} // namespace CVC4
#endif /* CVC4__EXPR__TCONV_SEQ_PROOF_GENERATOR_H */
|
