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
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
|
/********************* */
/*! \file term_formula_removal.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds, Dejan Jovanovic, Morgan Deters
** 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 Removal of term formulas
**
** Removal of term formulas.
**/
#include "cvc4_private.h"
#pragma once
#include <unordered_set>
#include <vector>
#include "context/cdinsert_hashmap.h"
#include "context/context.h"
#include "expr/node.h"
#include "expr/term_context.h"
#include "theory/trust_node.h"
#include "util/hash.h"
namespace CVC5 {
class LazyCDProof;
class ProofNodeManager;
class TConvProofGenerator;
class RemoveTermFormulas {
public:
RemoveTermFormulas(context::UserContext* u, ProofNodeManager* pnm = nullptr);
~RemoveTermFormulas();
/**
* By introducing skolem variables, this function removes all occurrences of:
* (1) term ITEs,
* (2) terms of type Boolean that are not Boolean term variables,
* (3) lambdas, and
* (4) Hilbert choice expressions.
* from assertions.
* All additional assertions are pushed into assertions. iteSkolemMap
* contains a map from introduced skolem variables to the index in
* assertions containing the new definition created in conjunction
* with that skolem variable.
*
* As an example of (1):
* f( (ite C 0 1)) = 2
* becomes
* f( k ) = 2 ^ ite( C, k=0, k=1 )
*
* As an example of (2):
* g( (and C1 C2) ) = 3
* becomes
* g( k ) = 3 ^ ( k <=> (and C1 C2) )
*
* As an example of (3):
* (lambda x. t[x]) = f
* becomes
* (forall x. k(x) = t[x]) ^ k = f
* where k is a fresh skolem function.
* This is sometimes called "lambda lifting"
*
* As an example of (4):
* (witness x. P( x ) ) = t
* becomes
* P( k ) ^ k = t
* where k is a fresh skolem constant.
*
* With reportDeps true, report reasoning dependences to the proof
* manager (for unsat cores).
*
* @param assertion The assertion to remove term formulas from
* @param newAsserts The new assertions corresponding to axioms for newly
* introduced skolems.
* @param newSkolems The skolems corresponding to each of the newAsserts.
* @param fixedPoint Whether to run term formula removal on the lemmas in
* newAsserts. This adds new assertions to this vector until a fixed
* point is reached. When this option is true, all lemmas in newAsserts
* have all term formulas removed.
* @return a trust node of kind TrustNodeKind::REWRITE whose
* right hand side is assertion after removing term formulas, and the proof
* generator (if provided) that can prove the equivalence.
*/
theory::TrustNode run(TNode assertion,
std::vector<theory::TrustNode>& newAsserts,
std::vector<Node>& newSkolems,
bool fixedPoint = false);
/**
* Same as above, but does not track lemmas, and does not run to fixed point.
* The relevant lemmas can be extracted by the caller later using getSkolems
* and getLemmaForSkolem.
*/
theory::TrustNode run(TNode assertion);
/**
* Same as above, but transforms a lemma, returning a LEMMA trust node that
* proves the same formula as lem with term formulas removed.
*/
theory::TrustNode runLemma(theory::TrustNode lem,
std::vector<theory::TrustNode>& newAsserts,
std::vector<Node>& newSkolems,
bool fixedPoint = false);
/**
* Get proof generator that is responsible for all proofs for removing term
* formulas from nodes. When proofs are enabled, the returned trust node
* of the run method use this proof generator (the trust nodes in newAsserts
* do not use this generator).
*/
ProofGenerator* getTConvProofGenerator();
/**
* Get axiom for term n. This returns the axiom that this class uses to
* eliminate the term n, which is determined by its top-most symbol. For
* example, if n is (ite n1 n2 n3), this returns the formula:
* (ite n1 (= (ite n1 n2 n3) n2) (= (ite n1 n2 n3) n3))
*/
static Node getAxiomFor(Node n);
private:
typedef context::CDInsertHashMap<
std::pair<Node, uint32_t>,
Node,
PairHashFunction<Node, uint32_t, NodeHashFunction> >
TermFormulaCache;
/** term formula removal cache
*
* This stores the results of term formula removal for inputs to the run(...)
* function below, where the integer in the pair we hash on is the
* result of cacheVal below.
*/
TermFormulaCache d_tfCache;
/** skolem cache
*
* This is a cache that maps terms to the skolem we use to replace them.
*
* Notice that this cache is necessary in addition to d_tfCache, since
* we should use the same skolem to replace terms, regardless of the input
* arguments to run(...). For example:
*
* ite( G, a, b ) = c ^ forall x. P( ite( G, a, b ), x )
*
* should be processed to:
*
* k = c ^ forall x. P( k, x ) ^ ite( G, k=a, k=b )
*
* where notice
* d_skolem_cache[ite( G, a, b )] = k, and
* d_tfCache[<ite( G, a, b ),0>] = d_tfCache[<ite( G, a, b ),1>] = k.
*/
context::CDInsertHashMap<Node, Node, NodeHashFunction> d_skolem_cache;
/** gets the skolem for node
*
* This returns the d_skolem_cache value for node, if it exists as a key
* in the above map, or the null node otherwise.
*/
inline Node getSkolemForNode(Node node) const;
/** Pointer to a proof node manager */
ProofNodeManager* d_pnm;
/**
* A proof generator for the term conversion.
*/
std::unique_ptr<TConvProofGenerator> d_tpg;
/**
* A proof generator for skolems we introduce that are based on axioms that
* this class is responsible for.
*/
std::unique_ptr<LazyCDProof> d_lp;
/**
* The remove term formula context, which computes hash values for term
* contexts.
*/
RtfTermContext d_rtfc;
/**
* Removes terms of the forms described above from formula assertion.
* All additional assertions and skolems are pushed into newAsserts and
* newSkolems, which are always of the same length.
*
* This uses a term-context-sensitive stack to process assertion. It returns
* the version of assertion with all term formulas removed.
*/
Node runInternal(TNode assertion,
std::vector<theory::TrustNode>& newAsserts,
std::vector<Node>& newSkolems);
/**
* This is called on curr of the form (t, val) where t is a term and val is
* a term context identifier computed by RtfTermContext. If curr should be
* replaced by a skolem, this method returns this skolem k. If this was the
* first time that t was encountered, we set newLem to the lemma for the
* skolem that axiomatizes k.
*
* Otherwise, if t should not be replaced in the term context, this method
* returns the null node.
*/
Node runCurrent(std::pair<Node, uint32_t>& curr, theory::TrustNode& newLem);
/** Whether proofs are enabled */
bool isProofEnabled() const;
};/* class RemoveTTE */
} // namespace CVC5
|
