1 /******************************************************************************
2 * Top contributors (to current version):
3 * Andrew Reynolds, Aina Niemetz
5 * This file is part of the cvc5 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.
11 * ****************************************************************************
13 * Implementation of skolem manager class.
16 #include "expr/skolem_manager.h"
20 #include "expr/attribute.h"
21 #include "expr/bound_var_manager.h"
22 #include "expr/node_algorithm.h"
24 using namespace cvc5::kind
;
28 // Attributes are global maps from Nodes to data. Thus, note that these could
29 // be implemented as internal maps in SkolemManager.
30 struct WitnessFormAttributeId
33 typedef expr::Attribute
<WitnessFormAttributeId
, Node
> WitnessFormAttribute
;
35 struct SkolemFormAttributeId
38 typedef expr::Attribute
<SkolemFormAttributeId
, Node
> SkolemFormAttribute
;
40 struct OriginalFormAttributeId
43 typedef expr::Attribute
<OriginalFormAttributeId
, Node
> OriginalFormAttribute
;
45 const char* toString(SkolemFunId id
)
49 case SkolemFunId::DIV_BY_ZERO
: return "DIV_BY_ZERO";
50 case SkolemFunId::INT_DIV_BY_ZERO
: return "INT_DIV_BY_ZERO";
51 case SkolemFunId::MOD_BY_ZERO
: return "MOD_BY_ZERO";
52 case SkolemFunId::SQRT
: return "SQRT";
53 case SkolemFunId::SELECTOR_WRONG
: return "SELECTOR_WRONG";
54 case SkolemFunId::SHARED_SELECTOR
: return "SHARED_SELECTOR";
55 case SkolemFunId::SEQ_NTH_OOB
: return "SEQ_NTH_OOB";
56 case SkolemFunId::RE_UNFOLD_POS_COMPONENT
: return "RE_UNFOLD_POS_COMPONENT";
61 std::ostream
& operator<<(std::ostream
& out
, SkolemFunId id
)
67 Node
SkolemManager::mkSkolem(Node v
,
69 const std::string
& prefix
,
70 const std::string
& comment
,
74 // We do not currently insist that pred does not contain witness terms
75 Assert(v
.getKind() == BOUND_VARIABLE
);
76 // make the witness term
77 NodeManager
* nm
= NodeManager::currentNM();
78 Node bvl
= nm
->mkNode(BOUND_VAR_LIST
, v
);
79 // Make the witness term, where notice that pred may contain skolems. We do
80 // not recursively convert pred to witness form, since witness terms should
81 // be treated as opaque. Moreover, the use of witness forms leads to
82 // variable shadowing issues in e.g. skolemization.
83 Node w
= nm
->mkNode(WITNESS
, bvl
, pred
);
84 // store the mapping to proof generator if it exists
87 // We cache based on the existential of the original predicate
88 Node q
= nm
->mkNode(EXISTS
, bvl
, pred
);
89 // Notice this may overwrite an existing proof generator. This does not
90 // matter since either should be able to prove q.
93 Node k
= mkSkolemInternal(w
, prefix
, comment
, flags
);
94 // set witness form attribute for k
95 WitnessFormAttribute wfa
;
96 k
.setAttribute(wfa
, w
);
97 Trace("sk-manager-skolem")
98 << "skolem: " << k
<< " witness " << w
<< std::endl
;
102 Node
SkolemManager::mkSkolemize(Node q
,
103 std::vector
<Node
>& skolems
,
104 const std::string
& prefix
,
105 const std::string
& comment
,
109 Trace("sk-manager-debug") << "mkSkolemize " << q
<< std::endl
;
110 Assert(q
.getKind() == EXISTS
);
112 for (const Node
& av
: q
[0])
114 Assert(currQ
.getKind() == EXISTS
&& av
== currQ
[0][0]);
115 // currQ is updated to the result of skolemizing its first variable in
117 Node sk
= skolemize(currQ
, currQ
, prefix
, comment
, flags
);
118 Trace("sk-manager-debug")
119 << "made skolem " << sk
<< " for " << av
<< std::endl
;
120 skolems
.push_back(sk
);
124 // Same as above, this may overwrite an existing proof generator
127 Trace("sk-manager-debug") << "...mkSkolemize returns " << currQ
<< std::endl
;
131 Node
SkolemManager::skolemize(Node q
,
133 const std::string
& prefix
,
134 const std::string
& comment
,
137 Assert(q
.getKind() == EXISTS
);
139 std::vector
<Node
> ovars
;
140 Trace("sk-manager-debug") << "mkSkolemize..." << std::endl
;
141 NodeManager
* nm
= NodeManager::currentNM();
142 for (const Node
& av
: q
[0])
152 // make the predicate with one variable stripped off
154 Trace("sk-manager-debug") << "make exists predicate" << std::endl
;
157 // keeps the same variables
158 Node bvl
= nm
->mkNode(BOUND_VAR_LIST
, ovars
);
159 // update the predicate
160 pred
= nm
->mkNode(EXISTS
, bvl
, pred
);
162 Trace("sk-manager-debug") << "call sub mkSkolem" << std::endl
;
163 // don't use a proof generator, since this may be an intermediate, partially
164 // skolemized formula.
165 Node k
= mkSkolem(v
, pred
, prefix
, comment
, flags
, nullptr);
166 Assert(k
.getType() == v
.getType());
169 Trace("sk-manager-debug")
170 << "qskolem apply " << tv
<< " -> " << tk
<< " to " << pred
<< std::endl
;
171 // the quantified formula with one step of skolemization
172 qskolem
= pred
.substitute(tv
, tk
);
173 Trace("sk-manager-debug") << "qskolem done substitution" << std::endl
;
177 Node
SkolemManager::mkPurifySkolem(Node t
,
178 const std::string
& prefix
,
179 const std::string
& comment
,
182 Node to
= getOriginalForm(t
);
183 // We do not currently insist that to does not contain witness terms
185 Node k
= mkSkolemInternal(to
, prefix
, comment
, flags
);
186 // set original form attribute for k
187 OriginalFormAttribute ofa
;
188 k
.setAttribute(ofa
, to
);
190 Trace("sk-manager-skolem")
191 << "skolem: " << k
<< " purify " << to
<< std::endl
;
195 Node
SkolemManager::mkSkolemFunction(SkolemFunId id
,
200 std::tuple
<SkolemFunId
, TypeNode
, Node
> key(id
, tn
, cacheVal
);
201 std::map
<std::tuple
<SkolemFunId
, TypeNode
, Node
>, Node
>::iterator it
=
202 d_skolemFuns
.find(key
);
203 if (it
== d_skolemFuns
.end())
205 NodeManager
* nm
= NodeManager::currentNM();
206 std::stringstream ss
;
207 ss
<< "SKOLEM_FUN_" << id
;
208 Node k
= nm
->mkSkolem(ss
.str(), tn
, "an internal skolem function", flags
);
209 d_skolemFuns
[key
] = k
;
210 d_skolemFunMap
[k
] = key
;
216 Node
SkolemManager::mkSkolemFunction(SkolemFunId id
,
218 const std::vector
<Node
>& cacheVals
,
221 Assert(cacheVals
.size() > 1);
222 Node cacheVal
= NodeManager::currentNM()->mkNode(SEXPR
, cacheVals
);
223 return mkSkolemFunction(id
, tn
, cacheVal
, flags
);
226 bool SkolemManager::isSkolemFunction(Node k
,
228 Node
& cacheVal
) const
230 std::map
<Node
, std::tuple
<SkolemFunId
, TypeNode
, Node
>>::const_iterator it
=
231 d_skolemFunMap
.find(k
);
232 if (it
== d_skolemFunMap
.end())
236 id
= std::get
<0>(it
->second
);
237 cacheVal
= std::get
<2>(it
->second
);
241 Node
SkolemManager::mkDummySkolem(const std::string
& prefix
,
242 const TypeNode
& type
,
243 const std::string
& comment
,
246 return NodeManager::currentNM()->mkSkolem(prefix
, type
, comment
, flags
);
249 ProofGenerator
* SkolemManager::getProofGenerator(Node t
) const
251 std::map
<Node
, ProofGenerator
*>::const_iterator it
= d_gens
.find(t
);
252 if (it
!= d_gens
.end())
259 Node
SkolemManager::getWitnessForm(Node k
)
261 Assert(k
.getKind() == SKOLEM
);
262 // simply look up the witness form for k via an attribute
263 WitnessFormAttribute wfa
;
264 return k
.getAttribute(wfa
);
267 Node
SkolemManager::getOriginalForm(Node n
)
273 Trace("sk-manager-debug")
274 << "SkolemManager::getOriginalForm " << n
<< std::endl
;
275 OriginalFormAttribute ofa
;
276 NodeManager
* nm
= NodeManager::currentNM();
277 std::unordered_map
<TNode
, Node
> visited
;
278 std::unordered_map
<TNode
, Node
>::iterator it
;
279 std::vector
<TNode
> visit
;
286 it
= visited
.find(cur
);
288 if (it
== visited
.end())
290 if (cur
.hasAttribute(ofa
))
292 visited
[cur
] = cur
.getAttribute(ofa
);
296 visited
[cur
] = Node::null();
297 visit
.push_back(cur
);
298 if (cur
.getMetaKind() == metakind::PARAMETERIZED
)
300 visit
.push_back(cur
.getOperator());
302 for (const Node
& cn
: cur
)
308 else if (it
->second
.isNull())
311 bool childChanged
= false;
312 std::vector
<Node
> children
;
313 if (cur
.getMetaKind() == metakind::PARAMETERIZED
)
315 it
= visited
.find(cur
.getOperator());
316 Assert(it
!= visited
.end());
317 Assert(!it
->second
.isNull());
318 childChanged
= childChanged
|| cur
.getOperator() != it
->second
;
319 children
.push_back(it
->second
);
321 for (const Node
& cn
: cur
)
323 it
= visited
.find(cn
);
324 Assert(it
!= visited
.end());
325 Assert(!it
->second
.isNull());
326 childChanged
= childChanged
|| cn
!= it
->second
;
327 children
.push_back(it
->second
);
331 ret
= nm
->mkNode(cur
.getKind(), children
);
333 cur
.setAttribute(ofa
, ret
);
336 } while (!visit
.empty());
337 Assert(visited
.find(n
) != visited
.end());
338 Assert(!visited
.find(n
)->second
.isNull());
339 Trace("sk-manager-debug") << "..return " << visited
[n
] << std::endl
;
343 Node
SkolemManager::mkSkolemInternal(Node w
,
344 const std::string
& prefix
,
345 const std::string
& comment
,
348 // note that witness, original forms are independent, but share skolems
349 NodeManager
* nm
= NodeManager::currentNM();
350 // w is not necessarily a witness term
351 SkolemFormAttribute sfa
;
353 // could already have a skolem if we used w already
354 if (w
.hasAttribute(sfa
))
356 return w
.getAttribute(sfa
);
358 // make the new skolem
359 if (flags
& NodeManager::SKOLEM_BOOL_TERM_VAR
)
361 Assert (w
.getType().isBoolean());
362 k
= nm
->mkBooleanTermVariable();
366 k
= nm
->mkSkolem(prefix
, w
.getType(), comment
, flags
);
368 // set skolem form attribute for w
369 w
.setAttribute(sfa
, k
);
370 Trace("sk-manager") << "SkolemManager::mkSkolem: " << k
<< " : " << w