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) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel 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 

* (declarefun a () (Array Int Int)) 
76 

* (declarefun 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 nonnull, 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 nonnull, 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 */ 