2f210cc20f67c8d3cae30db3efc2200d3a05608b
1 /********************* */
2 /*! \file skolemize.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 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
12 ** \brief Implementation of skolemization utility
15 #include "theory/quantifiers/skolemize.h"
17 #include "options/quantifiers_options.h"
18 #include "theory/quantifiers/term_util.h"
19 #include "theory/quantifiers_engine.h"
20 #include "theory/sort_inference.h"
21 #include "theory/theory_engine.h"
23 using namespace CVC4::kind
;
27 namespace quantifiers
{
29 Skolemize::Skolemize(QuantifiersEngine
* qe
, context::UserContext
* u
)
30 : d_quantEngine(qe
), d_skolemized(u
)
34 Node
Skolemize::process(Node q
)
37 if (d_skolemized
.find(q
) == d_skolemized
.end())
39 Node body
= getSkolemizedBody(q
);
40 NodeBuilder
<> nb(kind::OR
);
41 nb
<< q
<< body
.notNode();
43 d_skolemized
[q
] = lem
;
49 bool Skolemize::getSkolemConstants(Node q
, std::vector
<Node
>& skolems
)
51 std::unordered_map
<Node
, std::vector
<Node
>, NodeHashFunction
>::iterator it
=
52 d_skolem_constants
.find(q
);
53 if (it
!= d_skolem_constants
.end())
55 skolems
.insert(skolems
.end(), it
->second
.begin(), it
->second
.end());
61 Node
Skolemize::getSkolemConstant(Node q
, unsigned i
)
63 std::unordered_map
<Node
, std::vector
<Node
>, NodeHashFunction
>::iterator it
=
64 d_skolem_constants
.find(q
);
65 if (it
!= d_skolem_constants
.end())
67 if (i
< it
->second
.size())
75 void Skolemize::getSelfSel(const Datatype
& dt
,
76 const DatatypeConstructor
& dc
,
79 std::vector
<Node
>& selfSel
)
82 if (dt
.isParametric())
84 tspec
= TypeNode::fromType(
85 dc
.getSpecializedConstructorType(n
.getType().toType()));
86 Trace("sk-ind-debug") << "Specialized constructor type : " << tspec
88 Assert(tspec
.getNumChildren() == dc
.getNumArgs());
90 Trace("sk-ind-debug") << "Check self sel " << dc
.getName() << " "
91 << dt
.getName() << std::endl
;
92 for (unsigned j
= 0; j
< dc
.getNumArgs(); j
++)
94 std::vector
<Node
> ssc
;
95 if (dt
.isParametric())
97 Trace("sk-ind-debug") << "Compare " << tspec
[j
] << " " << ntn
106 TypeNode tn
= TypeNode::fromType(dc
[j
].getRangeType());
107 Trace("sk-ind-debug") << "Compare " << tn
<< " " << ntn
<< std::endl
;
113 /* TODO: more than weak structural induction
114 else if( tn.isDatatype() && std::find( visited.begin(), visited.end(), tn
116 visited.push_back( tn );
118 ((DatatypeType)(subs[0].getType()).toType()).getDatatype();
119 std::vector< Node > disj;
120 for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
121 getSelfSel( dt[i], n, ntn, ssc );
126 for (unsigned k
= 0; k
< ssc
.size(); k
++)
128 Node ss
= NodeManager::currentNM()->mkNode(
129 APPLY_SELECTOR_TOTAL
,
130 dc
.getSelectorInternal(n
.getType().toType(), j
),
132 if (std::find(selfSel
.begin(), selfSel
.end(), ss
) == selfSel
.end())
134 selfSel
.push_back(ss
);
140 Node
Skolemize::mkSkolemizedBody(Node f
,
142 std::vector
<TypeNode
>& argTypes
,
143 std::vector
<TNode
>& fvs
,
144 std::vector
<Node
>& sk
,
146 std::vector
<unsigned>& sub_vars
)
148 Assert(sk
.empty() || sk
.size() == f
[0].getNumChildren());
149 // calculate the variables and substitution
150 std::vector
<TNode
> ind_vars
;
151 std::vector
<unsigned> ind_var_indicies
;
152 std::vector
<TNode
> vars
;
153 std::vector
<unsigned> var_indicies
;
154 for (unsigned i
= 0; i
< f
[0].getNumChildren(); i
++)
156 if (isInductionTerm(f
[0][i
]))
158 ind_vars
.push_back(f
[0][i
]);
159 ind_var_indicies
.push_back(i
);
163 vars
.push_back(f
[0][i
]);
164 var_indicies
.push_back(i
);
167 // make the new function symbol or use existing
170 if (argTypes
.empty())
172 s
= NodeManager::currentNM()->mkSkolem(
173 "skv", f
[0][i
].getType(), "created during skolemization");
177 TypeNode typ
= NodeManager::currentNM()->mkFunctionType(
178 argTypes
, f
[0][i
].getType());
179 Node op
= NodeManager::currentNM()->mkSkolem(
180 "skop", typ
, "op created during pre-skolemization");
181 // DOTHIS: set attribute on op, marking that it should not be selected
183 std::vector
<Node
> funcArgs
;
184 funcArgs
.push_back(op
);
185 funcArgs
.insert(funcArgs
.end(), fvs
.begin(), fvs
.end());
186 s
= NodeManager::currentNM()->mkNode(kind::APPLY_UF
, funcArgs
);
192 Assert(sk
[i
].getType() == f
[0][i
].getType());
202 std::vector
<Node
> var_sk
;
203 for (unsigned i
= 0; i
< var_indicies
.size(); i
++)
205 var_sk
.push_back(sk
[var_indicies
[i
]]);
207 Assert(vars
.size() == var_sk
.size());
208 ret
= n
.substitute(vars
.begin(), vars
.end(), var_sk
.begin(), var_sk
.end());
210 if (!ind_vars
.empty())
212 Trace("sk-ind") << "Ind strengthen : (not " << f
<< ")" << std::endl
;
213 Trace("sk-ind") << "Skolemized is : " << ret
<< std::endl
;
215 TypeNode tn
= ind_vars
[0].getType();
216 Node k
= sk
[ind_var_indicies
[0]];
217 Node nret
= ret
.substitute(ind_vars
[0], k
);
218 // note : everything is under a negation
219 // the following constructs ~( R( x, k ) => ~P( x ) )
220 if (options::dtStcInduction() && tn
.isDatatype())
222 const Datatype
& dt
= ((DatatypeType
)(tn
).toType()).getDatatype();
223 std::vector
<Node
> disj
;
224 for (unsigned i
= 0; i
< dt
.getNumConstructors(); i
++)
226 std::vector
<Node
> selfSel
;
227 getSelfSel(dt
, dt
[i
], k
, tn
, selfSel
);
228 std::vector
<Node
> conj
;
230 NodeManager::currentNM()
231 ->mkNode(APPLY_TESTER
, Node::fromExpr(dt
[i
].getTester()), k
)
233 for (unsigned j
= 0; j
< selfSel
.size(); j
++)
235 conj
.push_back(ret
.substitute(ind_vars
[0], selfSel
[j
]).negate());
237 disj
.push_back(conj
.size() == 1
239 : NodeManager::currentNM()->mkNode(OR
, conj
));
241 Assert(!disj
.empty());
242 n_str_ind
= disj
.size() == 1
244 : NodeManager::currentNM()->mkNode(AND
, disj
);
246 else if (options::intWfInduction() && tn
.isInteger())
248 Node icond
= NodeManager::currentNM()->mkNode(
249 GEQ
, k
, NodeManager::currentNM()->mkConst(Rational(0)));
253 NodeManager::currentNM()->mkNode(
254 MINUS
, k
, NodeManager::currentNM()->mkConst(Rational(1))))
256 n_str_ind
= NodeManager::currentNM()->mkNode(OR
, icond
.negate(), iret
);
257 n_str_ind
= NodeManager::currentNM()->mkNode(AND
, icond
, n_str_ind
);
261 Trace("sk-ind") << "Unknown induction for term : " << ind_vars
[0]
262 << ", type = " << tn
<< std::endl
;
265 Trace("sk-ind") << "Strengthening is : " << n_str_ind
<< std::endl
;
267 std::vector
<Node
> rem_ind_vars
;
269 rem_ind_vars
.end(), ind_vars
.begin() + 1, ind_vars
.end());
270 if (!rem_ind_vars
.empty())
272 Node bvl
= NodeManager::currentNM()->mkNode(BOUND_VAR_LIST
, rem_ind_vars
);
273 nret
= NodeManager::currentNM()->mkNode(FORALL
, bvl
, nret
);
274 nret
= Rewriter::rewrite(nret
);
277 sub_vars
.end(), ind_var_indicies
.begin() + 1, ind_var_indicies
.end());
278 n_str_ind
= NodeManager::currentNM()
279 ->mkNode(FORALL
, bvl
, n_str_ind
.negate())
282 ret
= NodeManager::currentNM()->mkNode(OR
, nret
, n_str_ind
);
284 Trace("quantifiers-sk-debug") << "mkSkolem body for " << f
285 << " returns : " << ret
<< std::endl
;
286 // if it has an instantiation level, set the skolemized body to that level
287 if (f
.hasAttribute(InstLevelAttribute()))
289 theory::QuantifiersEngine::setInstantiationLevelAttr(
290 ret
, f
.getAttribute(InstLevelAttribute()));
293 if (Trace
.isOn("quantifiers-sk"))
295 Trace("quantifiers-sk") << "Skolemize : ";
296 for (unsigned i
= 0; i
< sk
.size(); i
++)
298 Trace("quantifiers-sk") << sk
[i
] << " ";
300 Trace("quantifiers-sk") << "for " << std::endl
;
301 Trace("quantifiers-sk") << " " << f
<< std::endl
;
307 Node
Skolemize::getSkolemizedBody(Node f
)
309 Assert(f
.getKind() == FORALL
);
310 if (d_skolem_body
.find(f
) == d_skolem_body
.end())
312 std::vector
<TypeNode
> fvTypes
;
313 std::vector
<TNode
> fvs
;
315 std::vector
<unsigned> sub_vars
;
316 d_skolem_body
[f
] = mkSkolemizedBody(
317 f
, f
[1], fvTypes
, fvs
, d_skolem_constants
[f
], sub
, sub_vars
);
318 // store sub quantifier information
321 // if we are skolemizing one at a time, we already know the skolem
322 // constants of the sub-quantified formula, store them
323 Assert(d_skolem_constants
[sub
].empty());
324 for (unsigned i
= 0; i
< sub_vars
.size(); i
++)
326 d_skolem_constants
[sub
].push_back(d_skolem_constants
[f
][sub_vars
[i
]]);
329 Assert(d_skolem_constants
[f
].size() == f
[0].getNumChildren());
330 if (options::sortInference())
332 for (unsigned i
= 0; i
< d_skolem_constants
[f
].size(); i
++)
334 // carry information for sort inference
335 d_quantEngine
->getTheoryEngine()->getSortInference()->setSkolemVar(
336 f
, f
[0][i
], d_skolem_constants
[f
][i
]);
340 return d_skolem_body
[f
];
343 bool Skolemize::isInductionTerm(Node n
)
345 TypeNode tn
= n
.getType();
346 if (options::dtStcInduction() && tn
.isDatatype())
348 const Datatype
& dt
= ((DatatypeType
)(tn
).toType()).getDatatype();
349 return !dt
.isCodatatype();
351 if (options::intWfInduction() && n
.getType().isInteger())
358 bool Skolemize::printSkolemization(std::ostream
& out
)
360 bool printed
= false;
361 for (NodeNodeMap::iterator it
= d_skolemized
.begin();
362 it
!= d_skolemized
.end();
365 Node q
= (*it
).first
;
367 out
<< "(skolem " << q
<< std::endl
;
369 for (unsigned i
= 0; i
< d_skolem_constants
[q
].size(); i
++)
375 out
<< d_skolem_constants
[q
][i
];
377 out
<< " )" << std::endl
;
378 out
<< ")" << std::endl
;
383 } /* CVC4::theory::quantifiers namespace */
384 } /* CVC4::theory namespace */
385 } /* CVC4 namespace */