GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/skolem_manager.h Lines: 2 2 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file skolem_manager.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Skolem manager utility
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__EXPR__SKOLEM_MANAGER_H
18
#define CVC4__EXPR__SKOLEM_MANAGER_H
19
20
#include <string>
21
22
#include "expr/node.h"
23
24
namespace CVC4 {
25
26
class ProofGenerator;
27
28
/**
29
 * A manager for skolems that can be used in proofs. This is designed to be
30
 * a trusted interface to NodeManager::mkSkolem, where one
31
 * must provide a definition for the skolem they create in terms of a
32
 * predicate that the introduced variable is intended to witness.
33
 *
34
 * It is implemented by mapping terms to an attribute corresponding to their
35
 * "original form" and "witness form" as described below. Hence, this class does
36
 * not impact the reference counting of skolem variables which may be deleted if
37
 * they are not used.
38
 *
39
 * We distinguish two kinds of mappings between terms and skolems:
40
 *
41
 * (1) "Original form", which associates skolems with the terms they purify.
42
 * This is used in mkPurifySkolem below.
43
 *
44
 * (2) "Witness form", which associates skolems with their formal definition
45
 * as a witness term. This is used in mkSkolem below.
46
 *
47
 * It is possible to unify these so that purification skolems for t are skolems
48
 * whose witness form is (witness ((x T)) (= x t)). However, there are
49
 * motivations not to do so. In particular, witness terms in most contexts
50
 * should be seen as black boxes, converting something to witness form may have
51
 * unintended consequences e.g. variable shadowing. In contrast, converting to
52
 * original form does not have these complications. Furthermore, having original
53
 * form greatly simplifies reasoning in the proof, in particular, it avoids the
54
 * need to reason about identifiers for introduced variables x.
55
 *
56
 * Furthermore, note that original form and witness form may share skolems
57
 * in the rare case that a witness term is purified. This is currently only the
58
 * case for algorithms that introduce witness, e.g. BV/set instantiation.
59
 */
60
class SkolemManager
61
{
62
 public:
63
7167
  SkolemManager() {}
64
7146
  ~SkolemManager() {}
65
  /**
66
   * This makes a skolem of same type as bound variable v, (say its type is T),
67
   * whose definition is (witness ((v T)) pred). This definition is maintained
68
   * by this class.
69
   *
70
   * Notice that (exists ((v T)) pred) should be a valid formula. This fact
71
   * captures the reason for why the returned Skolem was introduced.
72
   *
73
   * Take as an example extensionality in arrays:
74
   *
75
   * (declare-fun a () (Array Int Int))
76
   * (declare-fun b () (Array Int Int))
77
   * (assert (not (= a b)))
78
   *
79
   * To witness the index where the arrays a and b are disequal, it is intended
80
   * we call this method on:
81
   *   Node k = mkSkolem( x, F )
82
   * where F is:
83
   *   (=> (not (= a b)) (not (= (select a x) (select b x))))
84
   * and x is a fresh bound variable of integer type. Internally, this will map
85
   * k to the term:
86
   *   (witness ((x Int)) (=> (not (= a b))
87
   *                          (not (= (select a x) (select b x)))))
88
   * A lemma generated by the array solver for extensionality may safely use
89
   * the skolem k in the standard way:
90
   *   (=> (not (= a b)) (not (= (select a k) (select b k))))
91
   * Furthermore, notice that the following lemma does not involve fresh
92
   * skolem variables and is valid according to the theory of arrays extended
93
   * with support for witness:
94
   *   (let ((w (witness ((x Int)) (=> (not (= a b))
95
   *                                   (not (= (select a x) (select b x)))))))
96
   *     (=> (not (= a b)) (not (= (select a w) (select b w)))))
97
   * This version of the lemma, which requires no explicit tracking of free
98
   * Skolem variables, can be obtained by a call to getWitnessForm(...)
99
   * below. We call this the "witness form" of the lemma above.
100
   *
101
   * @param v The bound variable of the same type of the Skolem to create.
102
   * @param pred The desired property of the Skolem to create, in terms of bound
103
   * variable v.
104
   * @param prefix The prefix of the name of the Skolem
105
   * @param comment Debug information about the Skolem
106
   * @param flags The flags for the Skolem (see NodeManager::mkSkolem)
107
   * @param pg The proof generator for this skolem. If non-null, this proof
108
   * generator must respond to a call to getProofFor(exists v. pred) during
109
   * the lifetime of the current node manager.
110
   * @return The skolem whose witness form is registered by this class.
111
   */
112
  Node mkSkolem(Node v,
113
                Node pred,
114
                const std::string& prefix,
115
                const std::string& comment = "",
116
                int flags = NodeManager::SKOLEM_DEFAULT,
117
                ProofGenerator* pg = nullptr);
118
  /**
119
   * Make skolemized form of existentially quantified formula q, and store its
120
   * Skolems into the argument skolems.
121
   *
122
   * For example, calling this method on:
123
   *   (exists ((x Int) (y Int)) (P x y))
124
   * returns:
125
   *   (P w1 w2)
126
   * where w1 and w2 are skolems with witness forms:
127
   *   (witness ((x Int)) (exists ((y Int)) (P x y)))
128
   *   (witness ((y Int)) (P w1 y))
129
   * respectively. Additionally, this method will add { w1, w2 } to skolems.
130
   * Notice that y is *not* renamed in the witness form of w1. This is not
131
   * necessary since w1 is skolem. Although its witness form contains
132
   * quantification on y, we never construct a term where the witness form
133
   * of w1 is expanded in the witness form of w2. This avoids variable
134
   * shadowing.
135
   *
136
   * In contrast to mkSkolem, the proof generator is for the *entire*
137
   * existentially quantified formula q, which may have multiple variables in
138
   * its prefix.
139
   *
140
   * @param q The existentially quantified formula to skolemize,
141
   * @param skolems Vector to add Skolems of q to,
142
   * @param prefix The prefix of the name of each of the Skolems
143
   * @param comment Debug information about each of the Skolems
144
   * @param flags The flags for the Skolem (see NodeManager::mkSkolem)
145
   * @param pg The proof generator for this skolem. If non-null, this proof
146
   * generator must respond to a call to getProofFor(q) during
147
   * the lifetime of the current node manager.
148
   * @return The skolemized form of q.
149
   */
150
  Node mkSkolemize(Node q,
151
                   std::vector<Node>& skolems,
152
                   const std::string& prefix,
153
                   const std::string& comment = "",
154
                   int flags = NodeManager::SKOLEM_DEFAULT,
155
                   ProofGenerator* pg = nullptr);
156
  /**
157
   * Same as above, but for special case of (witness ((x T)) (= x t))
158
   * where T is the type of t. This skolem is unique for each t, which we
159
   * implement via an attribute on t. This attribute is used to ensure to
160
   * associate a unique skolem for each t.
161
   *
162
   * Notice that a purification skolem is trivial to justify, and hence it
163
   * does not require a proof generator.
164
   *
165
   * Notice that in very rare cases, two different terms may have the
166
   * same purification skolem. For example, let k be the skolem introduced to
167
   * eliminate (ite A B C). Then, the pair of terms:
168
   *  (ite (ite A B C) D E) and (ite k D E)
169
   * have the same purification skolem. In the implementation, this is a result
170
   * of the fact that the above terms have the same original form. It is sound
171
   * to use the same skolem to purify these two terms, since they are
172
   * definitionally equivalent.
173
   */
174
  Node mkPurifySkolem(Node t,
175
                      const std::string& prefix,
176
                      const std::string& comment = "",
177
                      int flags = NodeManager::SKOLEM_DEFAULT);
178
  /**
179
   * Make Boolean term variable for term t. This is a special case of
180
   * mkPurifySkolem above, where the returned term has kind
181
   * BOOLEAN_TERM_VARIABLE.
182
   */
183
  Node mkBooleanTermVariable(Node t);
184
  /**
185
   * Get proof generator for existentially quantified formula q. This returns
186
   * the proof generator that was provided in a call to mkSkolem above.
187
   */
188
  ProofGenerator* getProofGenerator(Node q) const;
189
  /**
190
   * Convert to witness form, which gets the witness form of a skolem k.
191
   * Notice this method is *not* recursive, instead, it is a simple attribute
192
   * lookup.
193
   *
194
   * @param k The variable to convert to witness form described above
195
   * @return k in witness form.
196
   */
197
  static Node getWitnessForm(Node k);
198
  /**
199
   * Convert to original form, which recursively replaces all skolems terms in n
200
   * by the term they purify.
201
   *
202
   * @param n The term or formula to convert to original form described above
203
   * @return n in original form.
204
   */
205
  static Node getOriginalForm(Node n);
206
207
 private:
208
  /**
209
   * Mapping from witness terms to proof generators.
210
   */
211
  std::map<Node, ProofGenerator*> d_gens;
212
  /** Get or make skolem attribute for term w, which may be a witness term */
213
  static Node mkSkolemInternal(Node w,
214
                               const std::string& prefix,
215
                               const std::string& comment,
216
                               int flags);
217
  /**
218
   * Skolemize the first variable of existentially quantified formula q.
219
   * For example, calling this method on:
220
   *   (exists ((x Int) (y Int)) (P x y))
221
   * will return:
222
   *   (witness ((x Int)) (exists ((y Int)) (P x y)))
223
   * If q is not an existentially quantified formula, then null is
224
   * returned and an assertion failure is thrown.
225
   *
226
   * This method additionally updates qskolem to be the skolemized form of q.
227
   * In the above example, this is set to:
228
   *   (exists ((y Int)) (P (witness ((x Int)) (exists ((y' Int)) (P x y'))) y))
229
   */
230
  Node skolemize(Node q,
231
                 Node& qskolem,
232
                 const std::string& prefix,
233
                 const std::string& comment = "",
234
                 int flags = NodeManager::SKOLEM_DEFAULT);
235
};
236
237
}  // namespace CVC4
238
239
#endif /* CVC4__EXPR__PROOF_SKOLEM_CACHE_H */