1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Paul Meng, Morgan Deters |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Implementation of QuantifiersAttributes class. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/quantifiers/quantifiers_attributes.h" |
17 |
|
|
18 |
|
#include "options/quantifiers_options.h" |
19 |
|
#include "theory/arith/arith_msum.h" |
20 |
|
#include "theory/quantifiers/fmf/bounded_integers.h" |
21 |
|
#include "theory/quantifiers/sygus/synth_engine.h" |
22 |
|
#include "theory/quantifiers/term_util.h" |
23 |
|
#include "util/rational.h" |
24 |
|
#include "util/string.h" |
25 |
|
|
26 |
|
using namespace std; |
27 |
|
using namespace cvc5::kind; |
28 |
|
using namespace cvc5::context; |
29 |
|
|
30 |
|
namespace cvc5 { |
31 |
|
namespace theory { |
32 |
|
namespace quantifiers { |
33 |
|
|
34 |
1012163 |
bool QAttributes::isStandard() const |
35 |
|
{ |
36 |
1012163 |
return !d_sygus && !d_quant_elim && !isFunDef() && !d_isQuantBounded; |
37 |
|
} |
38 |
|
|
39 |
15272 |
QuantAttributes::QuantAttributes() {} |
40 |
|
|
41 |
3141 |
void QuantAttributes::setUserAttribute(const std::string& attr, |
42 |
|
TNode n, |
43 |
|
const std::vector<Node>& nodeValues) |
44 |
|
{ |
45 |
3141 |
Trace("quant-attr-debug") << "Set " << attr << " " << n << std::endl; |
46 |
3141 |
if (attr == "fun-def") |
47 |
|
{ |
48 |
|
Trace("quant-attr-debug") << "Set function definition " << n << std::endl; |
49 |
|
FunDefAttribute fda; |
50 |
|
n.setAttribute( fda, true ); |
51 |
|
} |
52 |
3141 |
else if (attr == "qid") |
53 |
|
{ |
54 |
|
// using z3 syntax "qid" |
55 |
2985 |
Trace("quant-attr-debug") << "Set quant-name " << n << std::endl; |
56 |
|
QuantNameAttribute qna; |
57 |
2985 |
n.setAttribute(qna, true); |
58 |
156 |
}else if( attr=="quant-inst-max-level" ){ |
59 |
|
Assert(nodeValues.size() == 1); |
60 |
|
uint64_t lvl = nodeValues[0].getConst<Rational>().getNumerator().getLong(); |
61 |
|
Trace("quant-attr-debug") << "Set instantiation level " << n << " to " << lvl << std::endl; |
62 |
|
QuantInstLevelAttribute qila; |
63 |
|
n.setAttribute( qila, lvl ); |
64 |
156 |
}else if( attr=="quant-elim" ){ |
65 |
138 |
Trace("quant-attr-debug") << "Set quantifier elimination " << n << std::endl; |
66 |
|
QuantElimAttribute qea; |
67 |
138 |
n.setAttribute( qea, true ); |
68 |
18 |
}else if( attr=="quant-elim-partial" ){ |
69 |
17 |
Trace("quant-attr-debug") << "Set partial quantifier elimination " << n << std::endl; |
70 |
|
QuantElimPartialAttribute qepa; |
71 |
17 |
n.setAttribute( qepa, true ); |
72 |
|
} |
73 |
3141 |
} |
74 |
|
|
75 |
|
bool QuantAttributes::checkFunDef( Node q ) { |
76 |
|
return !getFunDefHead( q ).isNull(); |
77 |
|
} |
78 |
|
|
79 |
|
bool QuantAttributes::checkFunDefAnnotation( Node ipl ) { |
80 |
|
if( !ipl.isNull() ){ |
81 |
|
for( unsigned i=0; i<ipl.getNumChildren(); i++ ){ |
82 |
|
if( ipl[i].getKind()==INST_ATTRIBUTE ){ |
83 |
|
if( ipl[i][0].getAttribute(FunDefAttribute()) ){ |
84 |
|
return true; |
85 |
|
} |
86 |
|
} |
87 |
|
} |
88 |
|
} |
89 |
|
return false; |
90 |
|
} |
91 |
|
|
92 |
630 |
Node QuantAttributes::getFunDefHead( Node q ) { |
93 |
|
//&& q[1].getKind()==EQUAL && q[1][0].getKind()==APPLY_UF && |
94 |
630 |
if( q.getKind()==FORALL && q.getNumChildren()==3 ){ |
95 |
250 |
Node ipl = q[2]; |
96 |
250 |
for (unsigned i = 0; i < ipl.getNumChildren(); i++) |
97 |
|
{ |
98 |
744 |
if (ipl[i].getKind() == INST_ATTRIBUTE |
99 |
744 |
&& ipl[i][0].getAttribute(FunDefAttribute())) |
100 |
|
{ |
101 |
246 |
return ipl[i][0]; |
102 |
|
} |
103 |
|
} |
104 |
|
} |
105 |
384 |
return Node::null(); |
106 |
|
} |
107 |
123 |
Node QuantAttributes::getFunDefBody( Node q ) { |
108 |
246 |
Node h = getFunDefHead( q ); |
109 |
123 |
if( !h.isNull() ){ |
110 |
123 |
if( q[1].getKind()==EQUAL ){ |
111 |
119 |
if( q[1][0]==h ){ |
112 |
66 |
return q[1][1]; |
113 |
53 |
}else if( q[1][1]==h ){ |
114 |
52 |
return q[1][0]; |
115 |
|
} |
116 |
1 |
else if (q[1][0].getType().isReal()) |
117 |
|
{ |
118 |
|
// solve for h in the equality |
119 |
1 |
std::map<Node, Node> msum; |
120 |
1 |
if (ArithMSum::getMonomialSumLit(q[1], msum)) |
121 |
|
{ |
122 |
1 |
Node veq; |
123 |
1 |
int res = ArithMSum::isolate(h, msum, veq, EQUAL); |
124 |
1 |
if (res != 0) |
125 |
|
{ |
126 |
1 |
Assert(veq.getKind() == EQUAL); |
127 |
1 |
return res == 1 ? veq[1] : veq[0]; |
128 |
|
} |
129 |
|
} |
130 |
|
} |
131 |
|
}else{ |
132 |
4 |
Node atom = q[1].getKind()==NOT ? q[1][0] : q[1]; |
133 |
4 |
bool pol = q[1].getKind()!=NOT; |
134 |
4 |
if( atom==h ){ |
135 |
4 |
return NodeManager::currentNM()->mkConst( pol ); |
136 |
|
} |
137 |
|
} |
138 |
|
} |
139 |
|
return Node::null(); |
140 |
|
} |
141 |
|
|
142 |
3798 |
bool QuantAttributes::checkSygusConjecture( Node q ) { |
143 |
3798 |
return ( q.getKind()==FORALL && q.getNumChildren()==3 ) ? checkSygusConjectureAnnotation( q[2] ) : false; |
144 |
|
} |
145 |
|
|
146 |
658 |
bool QuantAttributes::checkSygusConjectureAnnotation( Node ipl ){ |
147 |
658 |
if( !ipl.isNull() ){ |
148 |
772 |
for( unsigned i=0; i<ipl.getNumChildren(); i++ ){ |
149 |
658 |
if( ipl[i].getKind()==INST_ATTRIBUTE ){ |
150 |
772 |
Node avar = ipl[i][0]; |
151 |
658 |
if( avar.getAttribute(SygusAttribute()) ){ |
152 |
544 |
return true; |
153 |
|
} |
154 |
|
} |
155 |
|
} |
156 |
|
} |
157 |
114 |
return false; |
158 |
|
} |
159 |
|
|
160 |
|
bool QuantAttributes::checkQuantElimAnnotation( Node ipl ) { |
161 |
|
if( !ipl.isNull() ){ |
162 |
|
for( unsigned i=0; i<ipl.getNumChildren(); i++ ){ |
163 |
|
if( ipl[i].getKind()==INST_ATTRIBUTE ){ |
164 |
|
Node avar = ipl[i][0]; |
165 |
|
if( avar.getAttribute(QuantElimAttribute()) ){ |
166 |
|
return true; |
167 |
|
} |
168 |
|
} |
169 |
|
} |
170 |
|
} |
171 |
|
return false; |
172 |
|
} |
173 |
|
|
174 |
2335 |
bool QuantAttributes::hasPattern(Node q) |
175 |
|
{ |
176 |
2335 |
Assert(q.getKind() == FORALL); |
177 |
2335 |
if (q.getNumChildren() != 3) |
178 |
|
{ |
179 |
2161 |
return false; |
180 |
|
} |
181 |
199 |
for (const Node& qc : q[2]) |
182 |
|
{ |
183 |
183 |
if (qc.getKind() == INST_PATTERN || qc.getKind() == INST_NO_PATTERN) |
184 |
|
{ |
185 |
158 |
return true; |
186 |
|
} |
187 |
|
} |
188 |
16 |
return false; |
189 |
|
} |
190 |
|
|
191 |
26124 |
void QuantAttributes::computeAttributes( Node q ) { |
192 |
26124 |
computeQuantAttributes( q, d_qattr[q] ); |
193 |
26124 |
QAttributes& qa = d_qattr[q]; |
194 |
26124 |
if (qa.isFunDef()) |
195 |
|
{ |
196 |
332 |
Node f = qa.d_fundef_f; |
197 |
166 |
if( d_fun_defs.find( f )!=d_fun_defs.end() ){ |
198 |
|
CVC5Message() << "Cannot define function " << f << " more than once." |
199 |
|
<< std::endl; |
200 |
|
AlwaysAssert(false); |
201 |
|
} |
202 |
166 |
d_fun_defs[f] = true; |
203 |
|
} |
204 |
26124 |
} |
205 |
|
|
206 |
202801 |
void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){ |
207 |
202801 |
Trace("quant-attr-debug") << "Compute attributes for " << q << std::endl; |
208 |
202801 |
if( q.getNumChildren()==3 ){ |
209 |
36517 |
NodeManager* nm = NodeManager::currentNM(); |
210 |
36517 |
qa.d_ipl = q[2]; |
211 |
76766 |
for( unsigned i=0; i<q[2].getNumChildren(); i++ ){ |
212 |
40249 |
Kind k = q[2][i].getKind(); |
213 |
80498 |
Trace("quant-attr-debug") |
214 |
40249 |
<< "Check : " << q[2][i] << " " << k << std::endl; |
215 |
40249 |
if (k == INST_PATTERN || k == INST_NO_PATTERN) |
216 |
|
{ |
217 |
27399 |
qa.d_hasPattern = true; |
218 |
|
} |
219 |
12850 |
else if (k == INST_POOL || k == INST_ADD_TO_POOL |
220 |
12794 |
|| k == SKOLEM_ADD_TO_POOL) |
221 |
|
{ |
222 |
112 |
qa.d_hasPool = true; |
223 |
|
} |
224 |
12738 |
else if (k == INST_ATTRIBUTE) |
225 |
|
{ |
226 |
25476 |
Node avar; |
227 |
|
// We support two use cases of INST_ATTRIBUTE: |
228 |
|
// (1) where the user constructs a term of the form |
229 |
|
// (INST_ATTRIBUTE "keyword" [nodeValues]) |
230 |
|
// (2) where we internally generate nodes of the form |
231 |
|
// (INST_ATTRIBUTE v) where v has an internal attribute set on it. |
232 |
|
// We distinguish these two cases by checking the kind of the first |
233 |
|
// child. |
234 |
12738 |
if (q[2][i][0].getKind() == CONST_STRING) |
235 |
|
{ |
236 |
|
// make a dummy variable to be used below |
237 |
3141 |
avar = nm->mkBoundVar(nm->booleanType()); |
238 |
6282 |
std::vector<Node> nodeValues(q[2][i].begin() + 1, q[2][i].end()); |
239 |
|
// set user attribute on the dummy variable |
240 |
9423 |
setUserAttribute( |
241 |
6282 |
q[2][i][0].getConst<String>().toString(), avar, nodeValues); |
242 |
|
} |
243 |
|
else |
244 |
|
{ |
245 |
|
// assume the dummy variable has already had its attributes set |
246 |
9597 |
avar = q[2][i][0]; |
247 |
|
} |
248 |
12738 |
if( avar.getAttribute(FunDefAttribute()) ){ |
249 |
1180 |
Trace("quant-attr") << "Attribute : function definition : " << q << std::endl; |
250 |
|
//get operator directly from pattern |
251 |
1180 |
qa.d_fundef_f = q[2][i][0].getOperator(); |
252 |
|
} |
253 |
12738 |
if( avar.getAttribute(SygusAttribute()) ){ |
254 |
|
//not necessarily nested existential |
255 |
|
//Assert( q[1].getKind()==NOT ); |
256 |
|
//Assert( q[1][0].getKind()==FORALL ); |
257 |
4070 |
Trace("quant-attr") << "Attribute : sygus : " << q << std::endl; |
258 |
4070 |
qa.d_sygus = true; |
259 |
|
} |
260 |
12738 |
if (avar.hasAttribute(SygusSideConditionAttribute())) |
261 |
|
{ |
262 |
342 |
qa.d_sygusSideCondition = |
263 |
684 |
avar.getAttribute(SygusSideConditionAttribute()); |
264 |
684 |
Trace("quant-attr") |
265 |
342 |
<< "Attribute : sygus side condition : " |
266 |
342 |
<< qa.d_sygusSideCondition << " : " << q << std::endl; |
267 |
|
} |
268 |
12738 |
if (avar.getAttribute(QuantNameAttribute())) |
269 |
|
{ |
270 |
|
// only set the name if there is a value |
271 |
2985 |
if (q[2][i].getNumChildren() > 1) |
272 |
|
{ |
273 |
5970 |
Trace("quant-attr") << "Attribute : quantifier name : " |
274 |
5970 |
<< q[2][i][1].getConst<String>().toString() |
275 |
2985 |
<< " for " << q << std::endl; |
276 |
|
// assign the name to a variable with the given name (to avoid |
277 |
|
// enclosing the name in quotes) |
278 |
5970 |
qa.d_name = nm->mkBoundVar(q[2][i][1].getConst<String>().toString(), |
279 |
8955 |
nm->booleanType()); |
280 |
|
} |
281 |
|
else |
282 |
|
{ |
283 |
|
Warning() << "Missing name for qid attribute"; |
284 |
|
} |
285 |
|
} |
286 |
12738 |
if( avar.hasAttribute(QuantInstLevelAttribute()) ){ |
287 |
|
qa.d_qinstLevel = avar.getAttribute(QuantInstLevelAttribute()); |
288 |
|
Trace("quant-attr") << "Attribute : quant inst level " << qa.d_qinstLevel << " : " << q << std::endl; |
289 |
|
} |
290 |
12738 |
if( avar.getAttribute(QuantElimAttribute()) ){ |
291 |
501 |
Trace("quant-attr") << "Attribute : quantifier elimination : " << q << std::endl; |
292 |
501 |
qa.d_quant_elim = true; |
293 |
|
//don't set owner, should happen naturally |
294 |
|
} |
295 |
12738 |
if( avar.getAttribute(QuantElimPartialAttribute()) ){ |
296 |
17 |
Trace("quant-attr") << "Attribute : quantifier elimination partial : " << q << std::endl; |
297 |
17 |
qa.d_quant_elim = true; |
298 |
17 |
qa.d_quant_elim_partial = true; |
299 |
|
//don't set owner, should happen naturally |
300 |
|
} |
301 |
12738 |
if (BoundedIntegers::isBoundedForallAttribute(avar)) |
302 |
|
{ |
303 |
6720 |
Trace("quant-attr") |
304 |
3360 |
<< "Attribute : bounded quantifiers : " << q << std::endl; |
305 |
3360 |
qa.d_isQuantBounded = true; |
306 |
|
} |
307 |
12738 |
if( avar.hasAttribute(QuantIdNumAttribute()) ){ |
308 |
|
qa.d_qid_num = avar; |
309 |
|
Trace("quant-attr") << "Attribute : id number " << qa.d_qid_num.getAttribute(QuantIdNumAttribute()) << " : " << q << std::endl; |
310 |
|
} |
311 |
|
} |
312 |
|
} |
313 |
|
} |
314 |
202801 |
} |
315 |
|
|
316 |
1299 |
bool QuantAttributes::isFunDef( Node q ) { |
317 |
1299 |
std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); |
318 |
1299 |
if( it==d_qattr.end() ){ |
319 |
|
return false; |
320 |
|
}else{ |
321 |
1299 |
return it->second.isFunDef(); |
322 |
|
} |
323 |
|
} |
324 |
|
|
325 |
1803 |
bool QuantAttributes::isSygus( Node q ) { |
326 |
1803 |
std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); |
327 |
1803 |
if( it==d_qattr.end() ){ |
328 |
|
return false; |
329 |
|
}else{ |
330 |
1803 |
return it->second.d_sygus; |
331 |
|
} |
332 |
|
} |
333 |
|
|
334 |
970 |
int64_t QuantAttributes::getQuantInstLevel(Node q) |
335 |
|
{ |
336 |
970 |
std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); |
337 |
970 |
if( it==d_qattr.end() ){ |
338 |
|
return -1; |
339 |
|
}else{ |
340 |
970 |
return it->second.d_qinstLevel; |
341 |
|
} |
342 |
|
} |
343 |
|
|
344 |
|
bool QuantAttributes::isQuantElim( Node q ) { |
345 |
|
std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); |
346 |
|
if( it==d_qattr.end() ){ |
347 |
|
return false; |
348 |
|
}else{ |
349 |
|
return it->second.d_quant_elim; |
350 |
|
} |
351 |
|
} |
352 |
|
|
353 |
5952 |
bool QuantAttributes::isQuantElimPartial( Node q ) { |
354 |
5952 |
std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); |
355 |
5952 |
if( it==d_qattr.end() ){ |
356 |
|
return false; |
357 |
|
}else{ |
358 |
5952 |
return it->second.d_quant_elim_partial; |
359 |
|
} |
360 |
|
} |
361 |
|
|
362 |
69606 |
bool QuantAttributes::isQuantBounded(Node q) const |
363 |
|
{ |
364 |
69606 |
std::map<Node, QAttributes>::const_iterator it = d_qattr.find(q); |
365 |
69606 |
if (it != d_qattr.end()) |
366 |
|
{ |
367 |
69606 |
return it->second.d_isQuantBounded; |
368 |
|
} |
369 |
|
return false; |
370 |
|
} |
371 |
|
|
372 |
34 |
Node QuantAttributes::getQuantName(Node q) const |
373 |
|
{ |
374 |
34 |
std::map<Node, QAttributes>::const_iterator it = d_qattr.find(q); |
375 |
34 |
if (it != d_qattr.end()) |
376 |
|
{ |
377 |
34 |
return it->second.d_name; |
378 |
|
} |
379 |
|
return Node::null(); |
380 |
|
} |
381 |
|
|
382 |
|
std::string QuantAttributes::quantToString(Node q) const |
383 |
|
{ |
384 |
|
std::stringstream ss; |
385 |
|
Node name = getQuantName(q); |
386 |
|
ss << (name.isNull() ? q : name); |
387 |
|
return ss.str(); |
388 |
|
} |
389 |
|
|
390 |
|
int QuantAttributes::getQuantIdNum( Node q ) { |
391 |
|
std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); |
392 |
|
if( it!=d_qattr.end() ){ |
393 |
|
if( !it->second.d_qid_num.isNull() ){ |
394 |
|
return it->second.d_qid_num.getAttribute(QuantIdNumAttribute()); |
395 |
|
} |
396 |
|
} |
397 |
|
return -1; |
398 |
|
} |
399 |
|
|
400 |
|
Node QuantAttributes::getQuantIdNumNode( Node q ) { |
401 |
|
std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); |
402 |
|
if( it==d_qattr.end() ){ |
403 |
|
return Node::null(); |
404 |
|
}else{ |
405 |
|
return it->second.d_qid_num; |
406 |
|
} |
407 |
|
} |
408 |
|
|
409 |
2835 |
void QuantAttributes::setInstantiationLevelAttr(Node n, Node qn, uint64_t level) |
410 |
|
{ |
411 |
5670 |
Trace("inst-level-debug2") << "IL : " << n << " " << qn << " " << level |
412 |
2835 |
<< std::endl; |
413 |
|
// if not from the vector of terms we instantiatied |
414 |
2835 |
if (qn.getKind() != BOUND_VARIABLE && n != qn) |
415 |
|
{ |
416 |
|
// if this is a new term, without an instantiation level |
417 |
2078 |
if (!n.hasAttribute(InstLevelAttribute())) |
418 |
|
{ |
419 |
|
InstLevelAttribute ila; |
420 |
1188 |
n.setAttribute(ila, level); |
421 |
2376 |
Trace("inst-level-debug") << "Set instantiation level " << n << " to " |
422 |
1188 |
<< level << std::endl; |
423 |
1188 |
Assert(n.getNumChildren() == qn.getNumChildren()); |
424 |
3677 |
for (unsigned i = 0; i < n.getNumChildren(); i++) |
425 |
|
{ |
426 |
2489 |
setInstantiationLevelAttr(n[i], qn[i], level); |
427 |
|
} |
428 |
|
} |
429 |
|
} |
430 |
2835 |
} |
431 |
|
|
432 |
2099 |
void QuantAttributes::setInstantiationLevelAttr(Node n, uint64_t level) |
433 |
|
{ |
434 |
2099 |
if (!n.hasAttribute(InstLevelAttribute())) |
435 |
|
{ |
436 |
|
InstLevelAttribute ila; |
437 |
1104 |
n.setAttribute(ila, level); |
438 |
2208 |
Trace("inst-level-debug") << "Set instantiation level " << n << " to " |
439 |
1104 |
<< level << std::endl; |
440 |
2973 |
for (unsigned i = 0; i < n.getNumChildren(); i++) |
441 |
|
{ |
442 |
1869 |
setInstantiationLevelAttr(n[i], level); |
443 |
|
} |
444 |
|
} |
445 |
2099 |
} |
446 |
|
|
447 |
|
} // namespace quantifiers |
448 |
|
} // namespace theory |
449 |
31137 |
} // namespace cvc5 |