GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/skolem_manager.h Lines: 2 2 100.0 %
Date: 2021-03-22 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
7165
  SkolemManager() {}
64
7144
  ~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
  Node mkPurifySkolem(Node t,
166
                      const std::string& prefix,
167
                      const std::string& comment = "",
168
                      int flags = NodeManager::SKOLEM_DEFAULT);
169
  /**
170
   * Make Boolean term variable for term t. This is a special case of
171
   * mkPurifySkolem above, where the returned term has kind
172
   * BOOLEAN_TERM_VARIABLE.
173
   */
174
  Node mkBooleanTermVariable(Node t);
175
  /**
176
   * Get proof generator for existentially quantified formula q. This returns
177
   * the proof generator that was provided in a call to mkSkolem above.
178
   */
179
  ProofGenerator* getProofGenerator(Node q) const;
180
  /**
181
   * Convert to witness form, which gets the witness form of a skolem k.
182
   * Notice this method is *not* recursive, instead, it is a simple attribute
183
   * lookup.
184
   *
185
   * @param k The variable to convert to witness form described above
186
   * @return k in witness form.
187
   */
188
  static Node getWitnessForm(Node k);
189
  /**
190
   * Convert to original form, which recursively replaces all skolems terms in n
191
   * by the term they purify.
192
   *
193
   * @param n The term or formula to convert to original form described above
194
   * @return n in original form.
195
   */
196
  static Node getOriginalForm(Node n);
197
198
 private:
199
  /**
200
   * Mapping from witness terms to proof generators.
201
   */
202
  std::map<Node, ProofGenerator*> d_gens;
203
  /** Get or make skolem attribute for term w, which may be a witness term */
204
  static Node mkSkolemInternal(Node w,
205
                               const std::string& prefix,
206
                               const std::string& comment,
207
                               int flags);
208
  /**
209
   * Skolemize the first variable of existentially quantified formula q.
210
   * For example, calling this method on:
211
   *   (exists ((x Int) (y Int)) (P x y))
212
   * will return:
213
   *   (witness ((x Int)) (exists ((y Int)) (P x y)))
214
   * If q is not an existentially quantified formula, then null is
215
   * returned and an assertion failure is thrown.
216
   *
217
   * This method additionally updates qskolem to be the skolemized form of q.
218
   * In the above example, this is set to:
219
   *   (exists ((y Int)) (P (witness ((x Int)) (exists ((y' Int)) (P x y'))) y))
220
   */
221
  Node skolemize(Node q,
222
                 Node& qskolem,
223
                 const std::string& prefix,
224
                 const std::string& comment = "",
225
                 int flags = NodeManager::SKOLEM_DEFAULT);
226
};
227
228
}  // namespace CVC4
229
230
#endif /* CVC4__EXPR__PROOF_SKOLEM_CACHE_H */