1 /********************* */
2 /*! \file quant_conflict_find.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Tim King, Andres Noetzli
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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 Implements conflict-based instantiation (Reynolds et al FMCAD 2014)
13 **
14 **/
15
16 #include "theory/quantifiers/quant_conflict_find.h"
17
18 #include <vector>
19
20 #include "expr/node_algorithm.h"
21 #include "options/quantifiers_options.h"
22 #include "smt/smt_statistics_registry.h"
23 #include "theory/quantifiers/ematching/trigger.h"
24 #include "theory/quantifiers/first_order_model.h"
25 #include "theory/quantifiers/instantiate.h"
26 #include "theory/quantifiers/quant_util.h"
27 #include "theory/quantifiers/term_database.h"
28 #include "theory/quantifiers/term_util.h"
29 #include "theory/theory_engine.h"
30
31 using namespace CVC4::kind;
32 using namespace std;
33
34 namespace CVC4 {
35 namespace theory {
36 namespace quantifiers {
37
QuantInfo()38 QuantInfo::QuantInfo() : d_unassigned_nvar(0), d_una_index(0), d_mg(nullptr) {}
39
~QuantInfo()40 QuantInfo::~QuantInfo() {
41 delete d_mg;
42 for(std::map< int, MatchGen * >::iterator i = d_var_mg.begin(),
43 iend=d_var_mg.end(); i != iend; ++i) {
44 MatchGen* currentMatchGenerator = (*i).second;
45 delete currentMatchGenerator;
46 }
47 d_var_mg.clear();
48 }
49
50
initialize(QuantConflictFind * p,Node q,Node qn)51 void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) {
52 d_q = q;
53 d_extra_var.clear();
54 for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
55 d_match.push_back( TNode::null() );
56 d_match_term.push_back( TNode::null() );
57 }
58
59 //register the variables
60 for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
61 d_var_num[q[0][i]] = i;
62 d_vars.push_back( q[0][i] );
63 d_var_types.push_back( q[0][i].getType() );
64 }
65
66 registerNode( qn, true, true );
67
68
69 Trace("qcf-qregister") << "- Make match gen structure..." << std::endl;
70 d_mg = new MatchGen( this, qn );
71
72 if( d_mg->isValid() ){
73 /*
74 for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
75 if( d_inMatchConstraint.find( q[0][j] )==d_inMatchConstraint.end() ){
76 Trace("qcf-invalid") << "QCF invalid : variable " << q[0][j] << " does not exist in a matching constraint." << std::endl;
77 d_mg->setInvalid();
78 break;
79 }
80 }
81 */
82 for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){
83 if( d_vars[j].getKind()!=BOUND_VARIABLE ){
84 d_var_mg[j] = NULL;
85 bool is_tsym = false;
86 if( !MatchGen::isHandledUfTerm( d_vars[j] ) && d_vars[j].getKind()!=ITE ){
87 is_tsym = true;
88 d_tsym_vars.push_back( j );
89 }
90 if( !is_tsym || options::qcfTConstraint() ){
91 d_var_mg[j] = new MatchGen( this, d_vars[j], true );
92 }
93 if( !d_var_mg[j] || !d_var_mg[j]->isValid() ){
94 Trace("qcf-invalid") << "QCF invalid : cannot match for " << d_vars[j] << std::endl;
95 d_mg->setInvalid();
96 break;
97 }else{
98 std::vector< int > bvars;
99 d_var_mg[j]->determineVariableOrder( this, bvars );
100 }
101 }
102 }
103 if( d_mg->isValid() ){
104 std::vector< int > bvars;
105 d_mg->determineVariableOrder( this, bvars );
106 }
107 }else{
108 Trace("qcf-invalid") << "QCF invalid : body of formula cannot be processed." << std::endl;
109 }
110 Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl;
111
112 if( d_mg->isValid() && options::qcfEagerCheckRd() ){
113 //optimization : record variable argument positions for terms that must be matched
114 std::vector< TNode > vars;
115 //TODO: revisit this, makes QCF faster, but misses conflicts due to caring about paths that may not be relevant (starExec jobs 14136/14137)
116 if( options::qcfSkipRd() ){
117 for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){
118 vars.push_back( d_vars[j] );
119 }
120 }else{
121 //get all variables that are always relevant
122 std::map< TNode, bool > visited;
123 getPropagateVars( p, vars, q[1], false, visited );
124 }
125 for( unsigned j=0; j<vars.size(); j++ ){
126 Node v = vars[j];
127 TNode f = p->getTermDatabase()->getMatchOperator( v );
128 if( !f.isNull() ){
129 Trace("qcf-opt") << "Record variable argument positions in " << v << ", op=" << f << "..." << std::endl;
130 for( unsigned k=0; k<v.getNumChildren(); k++ ){
131 Node n = v[k];
132 std::map< TNode, int >::iterator itv = d_var_num.find( n );
133 if( itv!=d_var_num.end() ){
134 Trace("qcf-opt") << " arg " << k << " is var #" << itv->second << std::endl;
135 if( std::find( d_var_rel_dom[itv->second][f].begin(), d_var_rel_dom[itv->second][f].end(), k )==d_var_rel_dom[itv->second][f].end() ){
136 d_var_rel_dom[itv->second][f].push_back( k );
137 }
138 }
139 }
140 }
141 }
142 }
143 }
144
getPropagateVars(QuantConflictFind * p,std::vector<TNode> & vars,TNode n,bool pol,std::map<TNode,bool> & visited)145 void QuantInfo::getPropagateVars( QuantConflictFind * p, std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited ){
146 std::map< TNode, bool >::iterator itv = visited.find( n );
147 if( itv==visited.end() ){
148 visited[n] = true;
149 bool rec = true;
150 bool newPol = pol;
151 if( d_var_num.find( n )!=d_var_num.end() ){
152 Assert( std::find( vars.begin(), vars.end(), n )==vars.end() );
153 vars.push_back( n );
154 TNode f = p->getTermDatabase()->getMatchOperator( n );
155 if( !f.isNull() ){
156 if( std::find( p->d_func_rel_dom[f].begin(), p->d_func_rel_dom[f].end(), d_q )==p->d_func_rel_dom[f].end() ){
157 p->d_func_rel_dom[f].push_back( d_q );
158 }
159 }
160 }else if( MatchGen::isHandledBoolConnective( n ) ){
161 Assert( n.getKind()!=IMPLIES );
162 QuantPhaseReq::getEntailPolarity( n, 0, true, pol, rec, newPol );
163 }
164 Trace("qcf-opt-debug") << "getPropagateVars " << n << ", pol = " << pol << ", rec = " << rec << std::endl;
165 if( rec ){
166 for( unsigned i=0; i<n.getNumChildren(); i++ ){
167 getPropagateVars( p, vars, n[i], pol, visited );
168 }
169 }
170 }
171 }
172
isBaseMatchComplete()173 bool QuantInfo::isBaseMatchComplete() {
174 return d_vars_set.size()==(d_q[0].getNumChildren()+d_extra_var.size());
175 }
176
registerNode(Node n,bool hasPol,bool pol,bool beneathQuant)177 void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) {
178 Trace("qcf-qregister-debug2") << "Register : " << n << std::endl;
179 if( n.getKind()==FORALL ){
180 registerNode( n[1], hasPol, pol, true );
181 }else{
182 if( !MatchGen::isHandledBoolConnective( n ) ){
183 if (expr::hasBoundVar(n))
184 {
185 // literals
186 if (n.getKind() == EQUAL)
187 {
188 for (unsigned i = 0; i < n.getNumChildren(); i++)
189 {
190 flatten(n[i], beneathQuant);
191 }
192 }
193 else if (MatchGen::isHandledUfTerm(n))
194 {
195 flatten(n, beneathQuant);
196 }
197 else if (n.getKind() == ITE)
198 {
199 for (unsigned i = 1; i <= 2; i++)
200 {
201 flatten(n[i], beneathQuant);
202 }
203 registerNode(n[0], false, pol, beneathQuant);
204 }
205 else if (options::qcfTConstraint())
206 {
207 // a theory-specific predicate
208 for (unsigned i = 0; i < n.getNumChildren(); i++)
209 {
210 flatten(n[i], beneathQuant);
211 }
212 }
213 }
214 }else{
215 for( unsigned i=0; i<n.getNumChildren(); i++ ){
216 bool newHasPol;
217 bool newPol;
218 QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
219 //QcfNode * qcfc = new QcfNode( d_c );
220 //qcfc->d_parent = qcf;
221 //qcf->d_child[i] = qcfc;
222 registerNode( n[i], newHasPol, newPol, beneathQuant );
223 }
224 }
225 }
226 }
227
flatten(Node n,bool beneathQuant)228 void QuantInfo::flatten( Node n, bool beneathQuant ) {
229 Trace("qcf-qregister-debug2") << "Flatten : " << n << std::endl;
230 if (expr::hasBoundVar(n))
231 {
232 if( n.getKind()==BOUND_VARIABLE ){
233 d_inMatchConstraint[n] = true;
234 }
235 if( d_var_num.find( n )==d_var_num.end() ){
236 Trace("qcf-qregister-debug2") << "Add FLATTEN VAR : " << n << std::endl;
237 d_var_num[n] = d_vars.size();
238 d_vars.push_back( n );
239 d_var_types.push_back( n.getType() );
240 d_match.push_back( TNode::null() );
241 d_match_term.push_back( TNode::null() );
242 if( n.getKind()==ITE ){
243 registerNode( n, false, false );
244 }else if( n.getKind()==BOUND_VARIABLE ){
245 d_extra_var.push_back( n );
246 }else{
247 for( unsigned i=0; i<n.getNumChildren(); i++ ){
248 flatten( n[i], beneathQuant );
249 }
250 }
251 }else{
252 Trace("qcf-qregister-debug2") << "...already processed" << std::endl;
253 }
254 }else{
255 Trace("qcf-qregister-debug2") << "...is ground." << std::endl;
256 }
257 }
258
259
reset_round(QuantConflictFind * p)260 bool QuantInfo::reset_round( QuantConflictFind * p ) {
261 for( unsigned i=0; i<d_match.size(); i++ ){
262 d_match[i] = TNode::null();
263 d_match_term[i] = TNode::null();
264 }
265 d_vars_set.clear();
266 d_curr_var_deq.clear();
267 d_tconstraints.clear();
268
269 d_mg->reset_round( p );
270 for( std::map< int, MatchGen * >::iterator it = d_var_mg.begin(); it != d_var_mg.end(); ++it ){
271 if (!it->second->reset_round(p))
272 {
273 return false;
274 }
275 }
276 //now, reset for matching
277 d_mg->reset( p, false, this );
278 return true;
279 }
280
getCurrentRepVar(int v)281 int QuantInfo::getCurrentRepVar( int v ) {
282 if( v!=-1 && !d_match[v].isNull() ){
283 int vn = getVarNum( d_match[v] );
284 if( vn!=-1 ){
285 //int vr = getCurrentRepVar( vn );
286 //d_match[v] = d_vars[vr];
287 //return vr;
288 return getCurrentRepVar( vn );
289 }
290 }
291 return v;
292 }
293
getCurrentValue(TNode n)294 TNode QuantInfo::getCurrentValue( TNode n ) {
295 int v = getVarNum( n );
296 if( v==-1 ){
297 return n;
298 }else{
299 if( d_match[v].isNull() ){
300 return n;
301 }else{
302 Assert( getVarNum( d_match[v] )!=v );
303 return getCurrentValue( d_match[v] );
304 }
305 }
306 }
307
getCurrentExpValue(TNode n)308 TNode QuantInfo::getCurrentExpValue( TNode n ) {
309 int v = getVarNum( n );
310 if( v==-1 ){
311 return n;
312 }else{
313 if( d_match[v].isNull() ){
314 return n;
315 }else{
316 Assert( getVarNum( d_match[v] )!=v );
317 if( d_match_term[v].isNull() ){
318 return getCurrentValue( d_match[v] );
319 }else{
320 return d_match_term[v];
321 }
322 }
323 }
324 }
325
getCurrentCanBeEqual(QuantConflictFind * p,int v,TNode n,bool chDiseq)326 bool QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq ) {
327 //check disequalities
328 std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( v );
329 if( itd!=d_curr_var_deq.end() ){
330 for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){
331 Node cv = getCurrentValue( it->first );
332 Debug("qcf-ccbe") << "compare " << cv << " " << n << std::endl;
333 if( cv==n ){
334 return false;
335 }else if( chDiseq && !isVar( n ) && !isVar( cv ) ){
336 //they must actually be disequal if we are looking for conflicts
337 if( !p->areDisequal( n, cv ) ){
338 //TODO : check for entailed disequal
339
340 return false;
341 }
342 }
343 }
344 }
345 return true;
346 }
347
addConstraint(QuantConflictFind * p,int v,TNode n,bool polarity)348 int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, bool polarity ) {
349 v = getCurrentRepVar( v );
350 int vn = getVarNum( n );
351 vn = vn==-1 ? -1 : getCurrentRepVar( vn );
352 n = getCurrentValue( n );
353 return addConstraint( p, v, n, vn, polarity, false );
354 }
355
addConstraint(QuantConflictFind * p,int v,TNode n,int vn,bool polarity,bool doRemove)356 int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove ) {
357 //for handling equalities between variables, and disequalities involving variables
358 Debug("qcf-match-debug") << "- " << (doRemove ? "un" : "" ) << "constrain : " << v << " -> " << n << " (cv=" << getCurrentValue( n ) << ")";
359 Debug("qcf-match-debug") << ", (vn=" << vn << "), polarity = " << polarity << std::endl;
360 Assert( doRemove || n==getCurrentValue( n ) );
361 Assert( doRemove || v==getCurrentRepVar( v ) );
362 Assert( doRemove || vn==getCurrentRepVar( getVarNum( n ) ) );
363 if( polarity ){
364 if( vn!=v ){
365 if( doRemove ){
366 if( vn!=-1 ){
367 //if set to this in the opposite direction, clean up opposite instead
368 // std::map< int, TNode >::iterator itmn = d_match.find( vn );
369 if( d_match[vn]==d_vars[v] ){
370 return addConstraint( p, vn, d_vars[v], v, true, true );
371 }else{
372 //unsetting variables equal
373 std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( vn );
374 if( itd!=d_curr_var_deq.end() ){
375 //remove disequalities owned by this
376 std::vector< TNode > remDeq;
377 for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){
378 if( it->second==v ){
379 remDeq.push_back( it->first );
380 }
381 }
382 for( unsigned i=0; i<remDeq.size(); i++ ){
383 d_curr_var_deq[vn].erase( remDeq[i] );
384 }
385 }
386 }
387 }
388 unsetMatch( p, v );
389 return 1;
390 }else{
391 //std::map< int, TNode >::iterator itm = d_match.find( v );
392 bool isGroundRep = false;
393 bool isGround = false;
394 if( vn!=-1 ){
395 Debug("qcf-match-debug") << " ...Variable bound to variable" << std::endl;
396 //std::map< int, TNode >::iterator itmn = d_match.find( vn );
397 if( d_match[v].isNull() ){
398 //setting variables equal
399 bool alreadySet = false;
400 if( !d_match[vn].isNull() ){
401 alreadySet = true;
402 Assert( !isVar( d_match[vn] ) );
403 }
404
405 //copy or check disequalities
406 std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( v );
407 if( itd!=d_curr_var_deq.end() ){
408 for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){
409 Node dv = getCurrentValue( it->first );
410 if( !alreadySet ){
411 if( d_curr_var_deq[vn].find( dv )==d_curr_var_deq[vn].end() ){
412 d_curr_var_deq[vn][dv] = v;
413 }
414 }else{
415 if( !p->areMatchDisequal( d_match[vn], dv ) ){
416 Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl;
417 return -1;
418 }
419 }
420 }
421 }
422 if( alreadySet ){
423 n = getCurrentValue( n );
424 }
425 }else{
426 if( d_match[vn].isNull() ){
427 Debug("qcf-match-debug") << " ...Reverse direction" << std::endl;
428 //set the opposite direction
429 return addConstraint( p, vn, d_vars[v], v, true, false );
430 }else{
431 Debug("qcf-match-debug") << " -> Both variables bound, compare" << std::endl;
432 //are they currently equal
433 return p->areMatchEqual( d_match[v], d_match[vn] ) ? 0 : -1;
434 }
435 }
436 }else{
437 Debug("qcf-match-debug") << " ...Variable bound to ground" << std::endl;
438 if( d_match[v].isNull() ){
439 //isGroundRep = true; ??
440 isGround = true;
441 }else{
442 //compare ground values
443 Debug("qcf-match-debug") << " -> Ground value, compare " << d_match[v] << " "<< n << std::endl;
444 return p->areMatchEqual( d_match[v], n ) ? 0 : -1;
445 }
446 }
447 if( setMatch( p, v, n, isGroundRep, isGround ) ){
448 Debug("qcf-match-debug") << " -> success" << std::endl;
449 return 1;
450 }else{
451 Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl;
452 return -1;
453 }
454 }
455 }else{
456 Debug("qcf-match-debug") << " -> redundant, variable identity" << std::endl;
457 return 0;
458 }
459 }else{
460 if( vn==v ){
461 Debug("qcf-match-debug") << " -> fail, variable identity" << std::endl;
462 return -1;
463 }else{
464 if( doRemove ){
465 Assert( d_curr_var_deq[v].find( n )!=d_curr_var_deq[v].end() );
466 d_curr_var_deq[v].erase( n );
467 return 1;
468 }else{
469 if( d_curr_var_deq[v].find( n )==d_curr_var_deq[v].end() ){
470 //check if it respects equality
471 //std::map< int, TNode >::iterator itm = d_match.find( v );
472 if( !d_match[v].isNull() ){
473 TNode nv = getCurrentValue( n );
474 if( !p->areMatchDisequal( nv, d_match[v] ) ){
475 Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl;
476 return -1;
477 }
478 }
479 d_curr_var_deq[v][n] = v;
480 Debug("qcf-match-debug") << " -> success" << std::endl;
481 return 1;
482 }else{
483 Debug("qcf-match-debug") << " -> redundant disequality" << std::endl;
484 return 0;
485 }
486 }
487 }
488 }
489 }
490
isConstrainedVar(int v)491 bool QuantInfo::isConstrainedVar( int v ) {
492 if( d_curr_var_deq.find( v )!=d_curr_var_deq.end() && !d_curr_var_deq[v].empty() ){
493 return true;
494 }else{
495 Node vv = getVar( v );
496 //for( std::map< int, TNode >::iterator it = d_match.begin(); it != d_match.end(); ++it ){
497 for( unsigned i=0; i<d_match.size(); i++ ){
498 if( d_match[i]==vv ){
499 return true;
500 }
501 }
502 for( std::map< int, std::map< TNode, int > >::iterator it = d_curr_var_deq.begin(); it != d_curr_var_deq.end(); ++it ){
503 for( std::map< TNode, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
504 if( it2->first==vv ){
505 return true;
506 }
507 }
508 }
509 return false;
510 }
511 }
512
setMatch(QuantConflictFind * p,int v,TNode n,bool isGroundRep,bool isGround)513 bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n, bool isGroundRep, bool isGround ) {
514 if( getCurrentCanBeEqual( p, v, n ) ){
515 if( isGroundRep ){
516 //fail if n does not exist in the relevant domain of each of the argument positions
517 std::map< int, std::map< TNode, std::vector< unsigned > > >::iterator it = d_var_rel_dom.find( v );
518 if( it!=d_var_rel_dom.end() ){
519 for( std::map< TNode, std::vector< unsigned > >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
520 for( unsigned j=0; j<it2->second.size(); j++ ){
521 Debug("qcf-match-debug2") << n << " in relevant domain " << it2->first << "." << it2->second[j] << "?" << std::endl;
522 if( !p->getTermDatabase()->inRelevantDomain( it2->first, it2->second[j], n ) ){
523 Debug("qcf-match-debug") << " -> fail, since " << n << " is not in relevant domain of " << it2->first << "." << it2->second[j] << std::endl;
524 return false;
525 }
526 }
527 }
528 }
529 }
530 Debug("qcf-match-debug") << "-- bind : " << v << " -> " << n << ", checked " << d_curr_var_deq[v].size() << " disequalities" << std::endl;
531 if( isGround ){
532 if( d_vars[v].getKind()==BOUND_VARIABLE ){
533 d_vars_set[v] = true;
534 Debug("qcf-match-debug") << "---- now bound " << d_vars_set.size() << " / " << d_q[0].getNumChildren() << " base variables." << std::endl;
535 }
536 }
537 d_match[v] = n;
538 return true;
539 }else{
540 return false;
541 }
542 }
543
unsetMatch(QuantConflictFind * p,int v)544 void QuantInfo::unsetMatch( QuantConflictFind * p, int v ) {
545 Debug("qcf-match-debug") << "-- unbind : " << v << std::endl;
546 if( d_vars[v].getKind()==BOUND_VARIABLE && d_vars_set.find( v )!=d_vars_set.end() ){
547 d_vars_set.erase( v );
548 }
549 d_match[ v ] = TNode::null();
550 }
551
isMatchSpurious(QuantConflictFind * p)552 bool QuantInfo::isMatchSpurious( QuantConflictFind * p ) {
553 for( int i=0; i<getNumVars(); i++ ){
554 //std::map< int, TNode >::iterator it = d_match.find( i );
555 if( !d_match[i].isNull() ){
556 if (!getCurrentCanBeEqual(p, i, d_match[i], p->atConflictEffort())) {
557 return true;
558 }
559 }
560 }
561 return false;
562 }
563
isTConstraintSpurious(QuantConflictFind * p,std::vector<Node> & terms)564 bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms ) {
565 if( options::qcfEagerTest() ){
566 //check whether the instantiation evaluates as expected
567 if (p->atConflictEffort()) {
568 Trace("qcf-instance-check") << "Possible conflict instance for " << d_q << " : " << std::endl;
569 std::map< TNode, TNode > subs;
570 for( unsigned i=0; i<terms.size(); i++ ){
571 Trace("qcf-instance-check") << " " << terms[i] << std::endl;
572 subs[d_q[0][i]] = terms[i];
573 }
574 for( unsigned i=0; i<d_extra_var.size(); i++ ){
575 Node n = getCurrentExpValue( d_extra_var[i] );
576 Trace("qcf-instance-check") << " " << d_extra_var[i] << " -> " << n << std::endl;
577 subs[d_extra_var[i]] = n;
578 }
579 if( !p->getTermDatabase()->isEntailed( d_q[1], subs, false, false ) ){
580 Trace("qcf-instance-check") << "...not entailed to be false." << std::endl;
581 return true;
582 }
583 }else{
584 Node inst =
585 p->d_quantEngine->getInstantiate()->getInstantiation(d_q, terms);
586 Node inst_eval = p->getTermDatabase()->evaluateTerm( inst, NULL, options::qcfTConstraint() );
587 if( Trace.isOn("qcf-instance-check") ){
588 Trace("qcf-instance-check") << "Possible propagating instance for " << d_q << " : " << std::endl;
589 for( unsigned i=0; i<terms.size(); i++ ){
590 Trace("qcf-instance-check") << " " << terms[i] << std::endl;
591 }
592 Trace("qcf-instance-check") << "...evaluates to " << inst_eval << std::endl;
593 }
594 if( inst_eval.isNull() || inst_eval==p->getTermUtil()->d_true || !isPropagatingInstance( p, inst_eval ) ){
595 Trace("qcf-instance-check") << "...spurious." << std::endl;
596 return true;
597 }else{
598 Trace("qcf-instance-check") << "...not spurious." << std::endl;
599 }
600 }
601 }
602 if( !d_tconstraints.empty() ){
603 //check constraints
604 for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){
605 //apply substitution to the tconstraint
606 Node cons =
607 p->getTermUtil()->substituteBoundVariables(it->first, d_q, terms);
608 cons = it->second ? cons : cons.negate();
609 if (!entailmentTest(p, cons, p->atConflictEffort())) {
610 return true;
611 }
612 }
613 }
614 // spurious if quantifiers engine is in conflict
615 return p->d_quantEngine->inConflict();
616 }
617
isPropagatingInstance(QuantConflictFind * p,Node n)618 bool QuantInfo::isPropagatingInstance( QuantConflictFind * p, Node n ) {
619 if( n.getKind()==FORALL ){
620 //TODO?
621 return true;
622 }else if( n.getKind()==NOT || n.getKind()==AND || n.getKind()==OR || n.getKind()==EQUAL || n.getKind()==ITE ||
623 ( n.getKind()==EQUAL && n[0].getType().isBoolean() ) ){
624 for( unsigned i=0; i<n.getNumChildren(); i++ ){
625 if( !isPropagatingInstance( p, n[i] ) ){
626 return false;
627 }
628 }
629 return true;
630 }else{
631 if( p->getEqualityEngine()->hasTerm( n ) || isGroundSubterm( n ) ){
632 return true;
633 }
634 }
635 Trace("qcf-instance-check-debug") << "...not propagating instance because of " << n << std::endl;
636 return false;
637 }
638
entailmentTest(QuantConflictFind * p,Node lit,bool chEnt)639 bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) {
640 Trace("qcf-tconstraint-debug") << "Check : " << lit << std::endl;
641 Node rew = Rewriter::rewrite( lit );
642 if( rew==p->d_false ){
643 Trace("qcf-tconstraint-debug") << "...constraint " << lit << " is disentailed (rewrites to false)." << std::endl;
644 return false;
645 }else if( rew!=p->d_true ){
646 //if checking for conflicts, we must be sure that the (negation of) constraint is (not) entailed
647 if( !chEnt ){
648 rew = Rewriter::rewrite( rew.negate() );
649 }
650 //check if it is entailed
651 Trace("qcf-tconstraint-debug") << "Check entailment of " << rew << "..." << std::endl;
652 std::pair<bool, Node> et = p->getQuantifiersEngine()->getTheoryEngine()->entailmentCheck(THEORY_OF_TYPE_BASED, rew );
653 ++(p->d_statistics.d_entailment_checks);
654 Trace("qcf-tconstraint-debug") << "ET result : " << et.first << " " << et.second << std::endl;
655 if( !et.first ){
656 Trace("qcf-tconstraint-debug") << "...cannot show entailment of " << rew << "." << std::endl;
657 return !chEnt;
658 }else{
659 return chEnt;
660 }
661 }else{
662 Trace("qcf-tconstraint-debug") << "...rewrites to true." << std::endl;
663 return true;
664 }
665 }
666
completeMatch(QuantConflictFind * p,std::vector<int> & assigned,bool doContinue)667 bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue ) {
668 //assign values for variables that were unassigned (usually not necessary, but handles corner cases)
669 bool doFail = false;
670 bool success = true;
671 if( doContinue ){
672 doFail = true;
673 success = false;
674 }else{
675 if( isBaseMatchComplete() && options::qcfEagerTest() ){
676 return true;
677 }
678 //solve for interpreted symbol matches
679 // this breaks the invariant that all introduced constraints are over existing terms
680 for( int i=(int)(d_tsym_vars.size()-1); i>=0; i-- ){
681 int index = d_tsym_vars[i];
682 TNode v = getCurrentValue( d_vars[index] );
683 int slv_v = -1;
684 if( v==d_vars[index] ){
685 slv_v = index;
686 }
687 Trace("qcf-tconstraint-debug") << "Solve " << d_vars[index] << " = " << v << " " << d_vars[index].getKind() << std::endl;
688 if( d_vars[index].getKind()==PLUS || d_vars[index].getKind()==MULT ){
689 Kind k = d_vars[index].getKind();
690 std::vector< TNode > children;
691 for( unsigned j=0; j<d_vars[index].getNumChildren(); j++ ){
692 int vn = getVarNum( d_vars[index][j] );
693 if( vn!=-1 ){
694 TNode vv = getCurrentValue( d_vars[index][j] );
695 if( vv==d_vars[index][j] ){
696 //we will assign this
697 if( slv_v==-1 ){
698 Trace("qcf-tconstraint-debug") << "...will solve for var #" << vn << std::endl;
699 slv_v = vn;
700 if (!p->atConflictEffort()) {
701 break;
702 }
703 }else{
704 Node z = p->getZero( k );
705 if( !z.isNull() ){
706 Trace("qcf-tconstraint-debug") << "...set " << d_vars[vn] << " = " << z << std::endl;
707 assigned.push_back( vn );
708 if( !setMatch( p, vn, z, false, true ) ){
709 success = false;
710 break;
711 }
712 }
713 }
714 }else{
715 Trace("qcf-tconstraint-debug") << "...sum value " << vv << std::endl;
716 children.push_back( vv );
717 }
718 }else{
719 Trace("qcf-tconstraint-debug") << "...sum " << d_vars[index][j] << std::endl;
720 children.push_back( d_vars[index][j] );
721 }
722 }
723 if( success ){
724 if( slv_v!=-1 ){
725 Node lhs;
726 if( children.empty() ){
727 lhs = p->getZero( k );
728 }else if( children.size()==1 ){
729 lhs = children[0];
730 }else{
731 lhs = NodeManager::currentNM()->mkNode( k, children );
732 }
733 Node sum;
734 if( v==d_vars[index] ){
735 sum = lhs;
736 }else{
737 if (p->atConflictEffort()) {
738 Kind kn = k;
739 if( d_vars[index].getKind()==PLUS ){
740 kn = MINUS;
741 }
742 if( kn!=k ){
743 sum = NodeManager::currentNM()->mkNode( kn, v, lhs );
744 }
745 }
746 }
747 if( !sum.isNull() ){
748 assigned.push_back( slv_v );
749 Trace("qcf-tconstraint-debug") << "...set " << d_vars[slv_v] << " = " << sum << std::endl;
750 if( !setMatch( p, slv_v, sum, false, true ) ){
751 success = false;
752 }
753 p->d_tempCache.push_back( sum );
754 }
755 }else{
756 //must show that constraint is met
757 Node sum = NodeManager::currentNM()->mkNode( k, children );
758 Node eq = sum.eqNode( v );
759 if( !entailmentTest( p, eq ) ){
760 success = false;
761 }
762 p->d_tempCache.push_back( sum );
763 }
764 }
765 }
766
767 if( !success ){
768 break;
769 }
770 }
771 if( success ){
772 //check what is left to assign
773 d_unassigned.clear();
774 d_unassigned_tn.clear();
775 std::vector< int > unassigned[2];
776 std::vector< TypeNode > unassigned_tn[2];
777 for( int i=0; i<getNumVars(); i++ ){
778 if( d_match[i].isNull() ){
779 int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;
780 unassigned[rindex].push_back( i );
781 unassigned_tn[rindex].push_back( getVar( i ).getType() );
782 assigned.push_back( i );
783 }
784 }
785 d_unassigned_nvar = unassigned[0].size();
786 for( unsigned i=0; i<2; i++ ){
787 d_unassigned.insert( d_unassigned.end(), unassigned[i].begin(), unassigned[i].end() );
788 d_unassigned_tn.insert( d_unassigned_tn.end(), unassigned_tn[i].begin(), unassigned_tn[i].end() );
789 }
790 d_una_eqc_count.clear();
791 d_una_index = 0;
792 }
793 }
794
795 if( !d_unassigned.empty() && ( success || doContinue ) ){
796 Trace("qcf-check") << "Assign to unassigned (" << d_unassigned.size() << ")..." << std::endl;
797 do {
798 if( doFail ){
799 Trace("qcf-check-unassign") << "Failure, try again..." << std::endl;
800 }
801 bool invalidMatch = false;
802 while( ( d_una_index>=0 && (int)d_una_index<(int)d_unassigned.size() ) || invalidMatch || doFail ){
803 invalidMatch = false;
804 if( !doFail && d_una_index==(int)d_una_eqc_count.size() ){
805 //check if it has now been assigned
806 if( d_una_index<d_unassigned_nvar ){
807 if( !isConstrainedVar( d_unassigned[d_una_index] ) ){
808 d_una_eqc_count.push_back( -1 );
809 }else{
810 d_var_mg[ d_unassigned[d_una_index] ]->reset( p, true, this );
811 d_una_eqc_count.push_back( 0 );
812 }
813 }else{
814 d_una_eqc_count.push_back( 0 );
815 }
816 }else{
817 bool failed = false;
818 if( !doFail ){
819 if( d_una_index<d_unassigned_nvar ){
820 if( !isConstrainedVar( d_unassigned[d_una_index] ) ){
821 Trace("qcf-check-unassign") << "Succeeded, variable unconstrained at " << d_una_index << std::endl;
822 d_una_index++;
823 }else if( d_var_mg[d_unassigned[d_una_index]]->getNextMatch( p, this ) ){
824 Trace("qcf-check-unassign") << "Succeeded match with mg at " << d_una_index << std::endl;
825 d_una_index++;
826 }else{
827 failed = true;
828 Trace("qcf-check-unassign") << "Failed match with mg at " << d_una_index << std::endl;
829 }
830 }else{
831 Assert( doFail || d_una_index==(int)d_una_eqc_count.size()-1 );
832 if( d_una_eqc_count[d_una_index]<(int)p->d_eqcs[d_unassigned_tn[d_una_index]].size() ){
833 int currIndex = d_una_eqc_count[d_una_index];
834 d_una_eqc_count[d_una_index]++;
835 Trace("qcf-check-unassign") << d_unassigned[d_una_index] << "->" << p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex] << std::endl;
836 if( setMatch( p, d_unassigned[d_una_index], p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex], true, true ) ){
837 d_match_term[d_unassigned[d_una_index]] = TNode::null();
838 Trace("qcf-check-unassign") << "Succeeded match " << d_una_index << std::endl;
839 d_una_index++;
840 }else{
841 Trace("qcf-check-unassign") << "Failed match " << d_una_index << std::endl;
842 invalidMatch = true;
843 }
844 }else{
845 failed = true;
846 Trace("qcf-check-unassign") << "No more matches " << d_una_index << std::endl;
847 }
848 }
849 }
850 if( doFail || failed ){
851 do{
852 if( !doFail ){
853 d_una_eqc_count.pop_back();
854 }else{
855 doFail = false;
856 }
857 d_una_index--;
858 }while( d_una_index>=0 && d_una_eqc_count[d_una_index]==-1 );
859 }
860 }
861 }
862 success = d_una_index>=0;
863 if( success ){
864 doFail = true;
865 Trace("qcf-check-unassign") << " Try: " << std::endl;
866 for( unsigned i=0; i<d_unassigned.size(); i++ ){
867 int ui = d_unassigned[i];
868 if( !d_match[ui].isNull() ){
869 Trace("qcf-check-unassign") << " Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;
870 }
871 }
872 }
873 }while( success && isMatchSpurious( p ) );
874 Trace("qcf-check") << "done assigning." << std::endl;
875 }
876 if( success ){
877 for( unsigned i=0; i<d_unassigned.size(); i++ ){
878 int ui = d_unassigned[i];
879 if( !d_match[ui].isNull() ){
880 Trace("qcf-check") << " Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;
881 }
882 }
883 return true;
884 }else{
885 revertMatch( p, assigned );
886 assigned.clear();
887 return false;
888 }
889 }
890
getMatch(std::vector<Node> & terms)891 void QuantInfo::getMatch( std::vector< Node >& terms ){
892 for( unsigned i=0; i<d_q[0].getNumChildren(); i++ ){
893 //Node cv = qi->getCurrentValue( qi->d_match[i] );
894 int repVar = getCurrentRepVar( i );
895 Node cv;
896 //std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar );
897 if( !d_match_term[repVar].isNull() ){
898 cv = d_match_term[repVar];
899 }else{
900 cv = d_match[repVar];
901 }
902 Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << d_match[i] << std::endl;
903 terms.push_back( cv );
904 }
905 }
906
revertMatch(QuantConflictFind * p,std::vector<int> & assigned)907 void QuantInfo::revertMatch( QuantConflictFind * p, std::vector< int >& assigned ) {
908 for( unsigned i=0; i<assigned.size(); i++ ){
909 unsetMatch( p, assigned[i] );
910 }
911 }
912
debugPrintMatch(const char * c)913 void QuantInfo::debugPrintMatch( const char * c ) {
914 for( int i=0; i<getNumVars(); i++ ){
915 Trace(c) << " " << d_vars[i] << " -> ";
916 if( !d_match[i].isNull() ){
917 Trace(c) << d_match[i];
918 }else{
919 Trace(c) << "(unassigned) ";
920 }
921 if( !d_curr_var_deq[i].empty() ){
922 Trace(c) << ", DEQ{ ";
923 for( std::map< TNode, int >::iterator it = d_curr_var_deq[i].begin(); it != d_curr_var_deq[i].end(); ++it ){
924 Trace(c) << it->first << " ";
925 }
926 Trace(c) << "}";
927 }
928 if( !d_match_term[i].isNull() && d_match_term[i]!=d_match[i] ){
929 Trace(c) << ", EXP : " << d_match_term[i];
930 }
931 Trace(c) << std::endl;
932 }
933 if( !d_tconstraints.empty() ){
934 Trace(c) << "ADDITIONAL CONSTRAINTS : " << std::endl;
935 for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){
936 Trace(c) << " " << it->first << " -> " << it->second << std::endl;
937 }
938 }
939 }
940
MatchGen()941 MatchGen::MatchGen()
942 : d_matched_basis(),
943 d_binding(),
944 d_tgt(),
945 d_tgt_orig(),
946 d_wasSet(),
947 d_n(),
948 d_type( typ_invalid ),
949 d_type_not()
950 {
951 d_qni_size = 0;
952 d_child_counter = -1;
953 d_use_children = true;
954 }
955
956
MatchGen(QuantInfo * qi,Node n,bool isVar)957 MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar )
958 : d_matched_basis(),
959 d_binding(),
960 d_tgt(),
961 d_tgt_orig(),
962 d_wasSet(),
963 d_n(),
964 d_type(),
965 d_type_not()
966 {
967 //initialize temporary
968 d_child_counter = -1;
969 d_use_children = true;
970
971 Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << std::endl;
972 std::vector< Node > qni_apps;
973 d_qni_size = 0;
974 if( isVar ){
975 Assert( qi->d_var_num.find( n )!=qi->d_var_num.end() );
976 if( n.getKind()==ITE ){
977 d_type = typ_invalid;
978 }else{
979 d_type = isHandledUfTerm( n ) ? typ_var : typ_tsym;
980 d_qni_var_num[0] = qi->getVarNum( n );
981 d_qni_size++;
982 d_type_not = false;
983 d_n = n;
984 //Node f = getMatchOperator( n );
985 for( unsigned j=0; j<d_n.getNumChildren(); j++ ){
986 Node nn = d_n[j];
987 Trace("qcf-qregister-debug") << " " << d_qni_size;
988 if( qi->isVar( nn ) ){
989 int v = qi->d_var_num[nn];
990 Trace("qcf-qregister-debug") << " is var #" << v << std::endl;
991 d_qni_var_num[d_qni_size] = v;
992 //qi->addFuncParent( v, f, j );
993 }else{
994 Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;
995 d_qni_gterm[d_qni_size] = nn;
996 }
997 d_qni_size++;
998 }
999 }
1000 }else{
1001 if (expr::hasBoundVar(n))
1002 {
1003 d_type_not = false;
1004 d_n = n;
1005 if( d_n.getKind()==NOT ){
1006 d_n = d_n[0];
1007 d_type_not = !d_type_not;
1008 }
1009
1010 if( isHandledBoolConnective( d_n ) ){
1011 //non-literals
1012 d_type = typ_formula;
1013 for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
1014 if( d_n.getKind()!=FORALL || i==1 ){
1015 d_children.push_back( MatchGen( qi, d_n[i], false ) );
1016 if( !d_children[d_children.size()-1].isValid() ){
1017 setInvalid();
1018 break;
1019 }
1020 }
1021 }
1022 }else{
1023 d_type = typ_invalid;
1024 //literals
1025 if( isHandledUfTerm( d_n ) ){
1026 Assert( qi->isVar( d_n ) );
1027 d_type = typ_pred;
1028 }else if( d_n.getKind()==BOUND_VARIABLE ){
1029 Assert( d_n.getType().isBoolean() );
1030 d_type = typ_bool_var;
1031 }else if( d_n.getKind()==EQUAL || options::qcfTConstraint() ){
1032 for (unsigned i = 0; i < d_n.getNumChildren(); i++)
1033 {
1034 if (expr::hasBoundVar(d_n[i]))
1035 {
1036 if (!qi->isVar(d_n[i]))
1037 {
1038 Trace("qcf-qregister-debug")
1039 << "ERROR : not var " << d_n[i] << std::endl;
1040 }
1041 Assert(qi->isVar(d_n[i]));
1042 if (d_n.getKind() != EQUAL && qi->isVar(d_n[i]))
1043 {
1044 d_qni_var_num[i + 1] = qi->d_var_num[d_n[i]];
1045 }
1046 }
1047 else
1048 {
1049 d_qni_gterm[i] = d_n[i];
1050 qi->setGroundSubterm(d_n[i]);
1051 }
1052 }
1053 d_type = d_n.getKind() == EQUAL ? typ_eq : typ_tconstraint;
1054 Trace("qcf-tconstraint") << "T-Constraint : " << d_n << std::endl;
1055 }
1056 }
1057 }else{
1058 //we will just evaluate
1059 d_n = n;
1060 d_type = typ_ground;
1061 qi->setGroundSubterm( d_n );
1062 }
1063 }
1064 Trace("qcf-qregister-debug") << "Done make match gen " << n << ", type = ";
1065 debugPrintType( "qcf-qregister-debug", d_type, true );
1066 Trace("qcf-qregister-debug") << std::endl;
1067 //Assert( d_children.size()==d_children_order.size() );
1068
1069 }
1070
collectBoundVar(QuantInfo * qi,Node n,std::vector<int> & cbvars,std::map<Node,bool> & visited,bool & hasNested)1071 void MatchGen::collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbvars, std::map< Node, bool >& visited, bool& hasNested ) {
1072 if( visited.find( n )==visited.end() ){
1073 visited[n] = true;
1074 if( n.getKind()==FORALL ){
1075 hasNested = true;
1076 }
1077 int v = qi->getVarNum( n );
1078 if( v!=-1 && std::find( cbvars.begin(), cbvars.end(), v )==cbvars.end() ){
1079 cbvars.push_back( v );
1080 }
1081 for( unsigned i=0; i<n.getNumChildren(); i++ ){
1082 collectBoundVar( qi, n[i], cbvars, visited, hasNested );
1083 }
1084 }
1085 }
1086
determineVariableOrder(QuantInfo * qi,std::vector<int> & bvars)1087 void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars ) {
1088 Trace("qcf-qregister-debug") << "Determine variable order " << d_n << ", #bvars = " << bvars.size() << std::endl;
1089 bool isComm = d_type==typ_formula && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==EQUAL );
1090 if( isComm ){
1091 std::map< int, std::vector< int > > c_to_vars;
1092 std::map< int, std::vector< int > > vars_to_c;
1093 std::map< int, int > vb_count;
1094 std::map< int, int > vu_count;
1095 std::map< int, bool > has_nested;
1096 std::vector< bool > assigned;
1097 Trace("qcf-qregister-debug") << "Calculate bound variables..." << std::endl;
1098 for( unsigned i=0; i<d_children.size(); i++ ){
1099 std::map< Node, bool > visited;
1100 has_nested[i] = false;
1101 collectBoundVar( qi, d_children[i].d_n, c_to_vars[i], visited, has_nested[i] );
1102 assigned.push_back( false );
1103 vb_count[i] = 0;
1104 vu_count[i] = 0;
1105 for( unsigned j=0; j<c_to_vars[i].size(); j++ ){
1106 int v = c_to_vars[i][j];
1107 vars_to_c[v].push_back( i );
1108 if( std::find( bvars.begin(), bvars.end(), v )==bvars.end() ){
1109 vu_count[i]++;
1110 }else{
1111 vb_count[i]++;
1112 }
1113 }
1114 }
1115 //children that bind no unbound variable, then the most number of bound, unbound variables go first
1116 Trace("qcf-qregister-vo") << "Variable order for " << d_n << " : " << std::endl;
1117 do {
1118 int min_score0 = -1;
1119 int min_score = -1;
1120 int min_score_index = -1;
1121 for( unsigned i=0; i<d_children.size(); i++ ){
1122 if( !assigned[i] ){
1123 Trace("qcf-qregister-debug2") << "Child " << i << " has b/ub : " << vb_count[i] << "/" << vu_count[i] << std::endl;
1124 int score0 = 0;//has_nested[i] ? 0 : 1;
1125 int score;
1126 if( !options::qcfVoExp() ){
1127 score = vu_count[i];
1128 }else{
1129 score = vu_count[i]==0 ? 0 : ( 1 + qi->d_vars.size()*( qi->d_vars.size() - vb_count[i] ) + ( qi->d_vars.size() - vu_count[i] ) );
1130 }
1131 if( min_score==-1 || score0<min_score0 || ( score0==min_score0 && score<min_score ) ){
1132 min_score0 = score0;
1133 min_score = score;
1134 min_score_index = i;
1135 }
1136 }
1137 }
1138 Trace("qcf-qregister-vo") << " " << d_children_order.size()+1 << ": " << d_children[min_score_index].d_n << " : ";
1139 Trace("qcf-qregister-vo") << vu_count[min_score_index] << " " << vb_count[min_score_index] << " " << has_nested[min_score_index] << std::endl;
1140 Trace("qcf-qregister-debug") << "...assign child " << min_score_index << std::endl;
1141 Trace("qcf-qregister-debug") << "...score : " << min_score << std::endl;
1142 Assert( min_score_index!=-1 );
1143 //add to children order
1144 d_children_order.push_back( min_score_index );
1145 assigned[min_score_index] = true;
1146 //determine order internal to children
1147 d_children[min_score_index].determineVariableOrder( qi, bvars );
1148 Trace("qcf-qregister-debug") << "...bind variables" << std::endl;
1149 //now, make it a bound variable
1150 if( vu_count[min_score_index]>0 ){
1151 for( unsigned i=0; i<c_to_vars[min_score_index].size(); i++ ){
1152 int v = c_to_vars[min_score_index][i];
1153 if( std::find( bvars.begin(), bvars.end(), v )==bvars.end() ){
1154 for( unsigned j=0; j<vars_to_c[v].size(); j++ ){
1155 int vc = vars_to_c[v][j];
1156 vu_count[vc]--;
1157 vb_count[vc]++;
1158 }
1159 bvars.push_back( v );
1160 }
1161 }
1162 }
1163 Trace("qcf-qregister-debug") << "...done assign child " << min_score_index << std::endl;
1164 }while( d_children_order.size()!=d_children.size() );
1165 Trace("qcf-qregister-debug") << "Done assign variable ordering for " << d_n << std::endl;
1166 }else{
1167 for( unsigned i=0; i<d_children.size(); i++ ){
1168 d_children_order.push_back( i );
1169 d_children[i].determineVariableOrder( qi, bvars );
1170 //now add to bvars
1171 std::map< Node, bool > visited;
1172 std::vector< int > cvars;
1173 bool has_nested = false;
1174 collectBoundVar( qi, d_children[i].d_n, cvars, visited, has_nested );
1175 for( unsigned j=0; j<cvars.size(); j++ ){
1176 if( std::find( bvars.begin(), bvars.end(), cvars[j] )==bvars.end() ){
1177 bvars.push_back( cvars[j] );
1178 }
1179 }
1180 }
1181 }
1182 }
1183
reset_round(QuantConflictFind * p)1184 bool MatchGen::reset_round(QuantConflictFind* p)
1185 {
1186 d_wasSet = false;
1187 for( unsigned i=0; i<d_children.size(); i++ ){
1188 if (!d_children[i].reset_round(p))
1189 {
1190 return false;
1191 }
1192 }
1193 for( std::map< int, TNode >::iterator it = d_qni_gterm.begin(); it != d_qni_gterm.end(); ++it ){
1194 d_qni_gterm_rep[it->first] = p->getRepresentative( it->second );
1195 }
1196 if( d_type==typ_ground ){
1197 // int e = p->evaluate( d_n );
1198 // if( e==1 ){
1199 // d_ground_eval[0] = p->d_true;
1200 //}else if( e==-1 ){
1201 // d_ground_eval[0] = p->d_false;
1202 //}
1203 // modified
1204 TermDb* tdb = p->getTermDatabase();
1205 QuantifiersEngine* qe = p->getQuantifiersEngine();
1206 for (unsigned i = 0; i < 2; i++)
1207 {
1208 if (tdb->isEntailed(d_n, i == 0))
1209 {
1210 d_ground_eval[0] = i==0 ? p->d_true : p->d_false;
1211 }
1212 if (qe->inConflict())
1213 {
1214 return false;
1215 }
1216 }
1217 }else if( d_type==typ_eq ){
1218 TermDb* tdb = p->getTermDatabase();
1219 QuantifiersEngine* qe = p->getQuantifiersEngine();
1220 for (unsigned i = 0, size = d_n.getNumChildren(); i < size; i++)
1221 {
1222 if (!expr::hasBoundVar(d_n[i]))
1223 {
1224 TNode t = tdb->getEntailedTerm(d_n[i]);
1225 if (qe->inConflict())
1226 {
1227 return false;
1228 }
1229 if (t.isNull())
1230 {
1231 d_ground_eval[i] = d_n[i];
1232 }
1233 else
1234 {
1235 d_ground_eval[i] = t;
1236 }
1237 }
1238 }
1239 }
1240 d_qni_bound_cons.clear();
1241 d_qni_bound_cons_var.clear();
1242 d_qni_bound.clear();
1243 return true;
1244 }
1245
reset(QuantConflictFind * p,bool tgt,QuantInfo * qi)1246 void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
1247 d_tgt = d_type_not ? !tgt : tgt;
1248 Debug("qcf-match") << " Reset for : " << d_n << ", type : ";
1249 debugPrintType( "qcf-match", d_type );
1250 Debug("qcf-match") << ", tgt = " << d_tgt << ", children = " << d_children.size() << " " << d_children_order.size() << std::endl;
1251 d_qn.clear();
1252 d_qni.clear();
1253 d_qni_bound.clear();
1254 d_child_counter = -1;
1255 d_use_children = true;
1256 d_tgt_orig = d_tgt;
1257
1258 //set up processing matches
1259 if( d_type==typ_invalid ){
1260 d_use_children = false;
1261 }else if( d_type==typ_ground ){
1262 d_use_children = false;
1263 if( d_ground_eval[0]==( d_tgt ? p->d_true : p->d_false ) ){
1264 d_child_counter = 0;
1265 }
1266 }else if( qi->isBaseMatchComplete() && options::qcfEagerTest() ){
1267 d_use_children = false;
1268 d_child_counter = 0;
1269 }else if( d_type==typ_bool_var ){
1270 //get current value of the variable
1271 TNode n = qi->getCurrentValue( d_n );
1272 int vn = qi->getCurrentRepVar( qi->getVarNum( n ) );
1273 if( vn==-1 ){
1274 //evaluate the value, see if it is compatible
1275 //int e = p->evaluate( n );
1276 //if( ( e==1 && d_tgt ) || ( e==0 && !d_tgt ) ){
1277 // d_child_counter = 0;
1278 //}
1279 //modified
1280 if( p->getTermDatabase()->isEntailed( n, d_tgt ) ){
1281 d_child_counter = 0;
1282 }
1283 }else{
1284 //unassigned, set match to true/false
1285 d_qni_bound[0] = vn;
1286 qi->setMatch( p, vn, d_tgt ? p->d_true : p->d_false, false, true );
1287 d_child_counter = 0;
1288 }
1289 if( d_child_counter==0 ){
1290 d_qn.push_back( NULL );
1291 }
1292 }else if( d_type==typ_var ){
1293 Assert( isHandledUfTerm( d_n ) );
1294 TNode f = getMatchOperator( p, d_n );
1295 Debug("qcf-match-debug") << " reset: Var will match operators of " << f << std::endl;
1296 TNodeTrie* qni = p->getTermDatabase()->getTermArgTrie(Node::null(), f);
1297 if (qni == nullptr || qni->empty())
1298 {
1299 //inform irrelevant quantifiers
1300 p->setIrrelevantFunction( f );
1301 }
1302 else
1303 {
1304 d_qn.push_back(qni);
1305 }
1306 d_matched_basis = false;
1307 }else if( d_type==typ_tsym || d_type==typ_tconstraint ){
1308 for( std::map< int, int >::iterator it = d_qni_var_num.begin(); it != d_qni_var_num.end(); ++it ){
1309 int repVar = qi->getCurrentRepVar( it->second );
1310 if( qi->d_match[repVar].isNull() ){
1311 Debug("qcf-match-debug") << "Force matching on child #" << it->first << ", which is var #" << repVar << std::endl;
1312 d_qni_bound[it->first] = repVar;
1313 }
1314 }
1315 d_qn.push_back( NULL );
1316 }else if( d_type==typ_pred || d_type==typ_eq ){
1317 //add initial constraint
1318 Node nn[2];
1319 int vn[2];
1320 if( d_type==typ_pred ){
1321 nn[0] = qi->getCurrentValue( d_n );
1322 vn[0] = qi->getCurrentRepVar( qi->getVarNum( nn[0] ) );
1323 nn[1] = p->getRepresentative( d_tgt ? p->d_true : p->d_false );
1324 vn[1] = -1;
1325 d_tgt = true;
1326 }else{
1327 for( unsigned i=0; i<2; i++ ){
1328 TNode nc;
1329 std::map< int, TNode >::iterator it = d_qni_gterm_rep.find( i );
1330 if( it!=d_qni_gterm_rep.end() ){
1331 nc = it->second;
1332 }else{
1333 nc = d_n[i];
1334 }
1335 nn[i] = qi->getCurrentValue( nc );
1336 vn[i] = qi->getCurrentRepVar( qi->getVarNum( nn[i] ) );
1337 }
1338 }
1339 bool success;
1340 if( vn[0]==-1 && vn[1]==-1 ){
1341 //Trace("qcf-explain") << " reset : " << d_n << " check ground values " << nn[0] << " " << nn[1] << " (tgt=" << d_tgt << ")" << std::endl;
1342 Debug("qcf-match-debug") << " reset: check ground values " << nn[0] << " " << nn[1] << " (" << d_tgt << ")" << std::endl;
1343 //just compare values
1344 if( d_tgt ){
1345 success = p->areMatchEqual( nn[0], nn[1] );
1346 }else{
1347 if (p->atConflictEffort()) {
1348 success = p->areDisequal( nn[0], nn[1] );
1349 }else{
1350 success = p->areMatchDisequal( nn[0], nn[1] );
1351 }
1352 }
1353 }else{
1354 //otherwise, add a constraint to a variable TODO: this may be over-eager at effort > conflict, since equality may be a propagation
1355 if( vn[1]!=-1 && vn[0]==-1 ){
1356 //swap
1357 Node t = nn[1];
1358 nn[1] = nn[0];
1359 nn[0] = t;
1360 vn[0] = vn[1];
1361 vn[1] = -1;
1362 }
1363 Debug("qcf-match-debug") << " reset: add constraint " << vn[0] << " -> " << nn[1] << " (vn=" << vn[1] << ")" << std::endl;
1364 //add some constraint
1365 int addc = qi->addConstraint( p, vn[0], nn[1], vn[1], d_tgt, false );
1366 success = addc!=-1;
1367 //if successful and non-redundant, store that we need to cleanup this
1368 if( addc==1 ){
1369 //Trace("qcf-explain") << " reset: " << d_n << " add constraint " << vn[0] << " -> " << nn[1] << " (vn=" << vn[1] << ")" << ", d_tgt = " << d_tgt << std::endl;
1370 for( unsigned i=0; i<2; i++ ){
1371 if( vn[i]!=-1 && std::find( d_qni_bound_except.begin(), d_qni_bound_except.end(), i )==d_qni_bound_except.end() ){
1372 d_qni_bound[vn[i]] = vn[i];
1373 }
1374 }
1375 d_qni_bound_cons[vn[0]] = nn[1];
1376 d_qni_bound_cons_var[vn[0]] = vn[1];
1377 }
1378 }
1379 //if successful, we will bind values to variables
1380 if( success ){
1381 d_qn.push_back( NULL );
1382 }
1383 }else{
1384 if( d_children.empty() ){
1385 //add dummy
1386 d_qn.push_back( NULL );
1387 }else{
1388 if( d_tgt && d_n.getKind()==FORALL ){
1389 //fail
1390 } else if (d_n.getKind() == FORALL && p->atConflictEffort() &&
1391 !options::qcfNestedConflict()) {
1392 //fail
1393 }else{
1394 //reset the first child to d_tgt
1395 d_child_counter = 0;
1396 getChild( d_child_counter )->reset( p, d_tgt, qi );
1397 }
1398 }
1399 }
1400 d_binding = false;
1401 d_wasSet = true;
1402 Debug("qcf-match") << " reset: Finished reset for " << d_n << ", success = " << ( !d_qn.empty() || d_child_counter!=-1 ) << std::endl;
1403 }
1404
getNextMatch(QuantConflictFind * p,QuantInfo * qi)1405 bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
1406 Debug("qcf-match") << " Get next match for : " << d_n << ", type = ";
1407 debugPrintType( "qcf-match", d_type );
1408 Debug("qcf-match") << ", children = " << d_children.size() << ", binding = " << d_binding << std::endl;
1409 if( !d_use_children ){
1410 if( d_child_counter==0 ){
1411 d_child_counter = -1;
1412 return true;
1413 }else{
1414 d_wasSet = false;
1415 return false;
1416 }
1417 }else if( d_type==typ_var || d_type==typ_eq || d_type==typ_pred || d_type==typ_bool_var || d_type==typ_tconstraint || d_type==typ_tsym ){
1418 bool success = false;
1419 bool terminate = false;
1420 do {
1421 bool doReset = false;
1422 bool doFail = false;
1423 if( !d_binding ){
1424 if( doMatching( p, qi ) ){
1425 Debug("qcf-match-debug") << " - Matching succeeded" << std::endl;
1426 d_binding = true;
1427 d_binding_it = d_qni_bound.begin();
1428 doReset = true;
1429 //for tconstraint, add constraint
1430 if( d_type==typ_tconstraint ){
1431 std::map< Node, bool >::iterator it = qi->d_tconstraints.find( d_n );
1432 if( it==qi->d_tconstraints.end() ){
1433 qi->d_tconstraints[d_n] = d_tgt;
1434 //store that we added this constraint
1435 d_qni_bound_cons[0] = d_n;
1436 }else if( d_tgt!=it->second ){
1437 success = false;
1438 terminate = true;
1439 }
1440 }
1441 }else{
1442 Debug("qcf-match-debug") << " - Matching failed" << std::endl;
1443 success = false;
1444 terminate = true;
1445 }
1446 }else{
1447 doFail = true;
1448 }
1449 if( d_binding ){
1450 //also need to create match for each variable we bound
1451 success = true;
1452 Debug("qcf-match-debug") << " Produce matches for bound variables by " << d_n << ", type = ";
1453 debugPrintType( "qcf-match-debug", d_type );
1454 Debug("qcf-match-debug") << "..." << std::endl;
1455
1456 while( ( success && d_binding_it!=d_qni_bound.end() ) || doFail ){
1457 QuantInfo::VarMgMap::const_iterator itm;
1458 if( !doFail ){
1459 Debug("qcf-match-debug") << " check variable " << d_binding_it->second << std::endl;
1460 itm = qi->var_mg_find( d_binding_it->second );
1461 }
1462 if( doFail || ( d_binding_it->first!=0 && itm != qi->var_mg_end() ) ){
1463 Debug("qcf-match-debug") << " we had bound variable " << d_binding_it->second << ", reset = " << doReset << std::endl;
1464 if( doReset ){
1465 itm->second->reset( p, true, qi );
1466 }
1467 if( doFail || !itm->second->getNextMatch( p, qi ) ){
1468 do {
1469 if( d_binding_it==d_qni_bound.begin() ){
1470 Debug("qcf-match-debug") << " failed." << std::endl;
1471 success = false;
1472 }else{
1473 --d_binding_it;
1474 Debug("qcf-match-debug") << " decrement..." << std::endl;
1475 }
1476 }while( success &&
1477 ( d_binding_it->first==0 ||
1478 (!qi->containsVarMg(d_binding_it->second))));
1479 doReset = false;
1480 doFail = false;
1481 }else{
1482 Debug("qcf-match-debug") << " increment..." << std::endl;
1483 ++d_binding_it;
1484 doReset = true;
1485 }
1486 }else{
1487 Debug("qcf-match-debug") << " skip..." << d_binding_it->second << std::endl;
1488 ++d_binding_it;
1489 doReset = true;
1490 }
1491 }
1492 if( !success ){
1493 d_binding = false;
1494 }else{
1495 terminate = true;
1496 if( d_binding_it==d_qni_bound.begin() ){
1497 d_binding = false;
1498 }
1499 }
1500 }
1501 }while( !terminate );
1502 //if not successful, clean up the variables you bound
1503 if( !success ){
1504 if( d_type==typ_eq || d_type==typ_pred ){
1505 //clean up the constraints you added
1506 for( std::map< int, TNode >::iterator it = d_qni_bound_cons.begin(); it != d_qni_bound_cons.end(); ++it ){
1507 if( !it->second.isNull() ){
1508 Debug("qcf-match") << " Clean up bound var " << it->first << (d_tgt ? "!" : "") << " = " << it->second << std::endl;
1509 std::map< int, int >::iterator itb = d_qni_bound_cons_var.find( it->first );
1510 int vn = itb!=d_qni_bound_cons_var.end() ? itb->second : -1;
1511 //Trace("qcf-explain") << " cleanup: " << d_n << " remove constraint " << it->first << " -> " << it->second << " (vn=" << vn << ")" << ", d_tgt = " << d_tgt << std::endl;
1512 qi->addConstraint( p, it->first, it->second, vn, d_tgt, true );
1513 }
1514 }
1515 d_qni_bound_cons.clear();
1516 d_qni_bound_cons_var.clear();
1517 d_qni_bound.clear();
1518 }else{
1519 //clean up the matches you set
1520 for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){
1521 Debug("qcf-match") << " Clean up bound var " << it->second << std::endl;
1522 Assert( it->second<qi->getNumVars() );
1523 qi->unsetMatch( p, it->second );
1524 qi->d_match_term[ it->second ] = TNode::null();
1525 }
1526 d_qni_bound.clear();
1527 }
1528 if( d_type==typ_tconstraint ){
1529 //remove constraint if applicable
1530 if( d_qni_bound_cons.find( 0 )!=d_qni_bound_cons.end() ){
1531 qi->d_tconstraints.erase( d_n );
1532 d_qni_bound_cons.clear();
1533 }
1534 }
1535 }
1536 Debug("qcf-match") << " ...finished matching for " << d_n << ", success = " << success << std::endl;
1537 d_wasSet = success;
1538 return success;
1539 }
1540 else if (d_type == typ_formula)
1541 {
1542 bool success = false;
1543 if( d_child_counter<0 ){
1544 if( d_child_counter<-1 ){
1545 success = true;
1546 d_child_counter = -1;
1547 }
1548 }else{
1549 while( !success && d_child_counter>=0 ){
1550 //transition system based on d_child_counter
1551 if( d_n.getKind()==OR || d_n.getKind()==AND ){
1552 if( (d_n.getKind()==AND)==d_tgt ){
1553 //all children must match simultaneously
1554 if( getChild( d_child_counter )->getNextMatch( p, qi ) ){
1555 if( d_child_counter<(int)(getNumChildren()-1) ){
1556 d_child_counter++;
1557 Debug("qcf-match-debug") << " Reset child " << d_child_counter << " of " << d_n << std::endl;
1558 getChild( d_child_counter )->reset( p, d_tgt, qi );
1559 }else{
1560 success = true;
1561 }
1562 }else{
1563 //if( std::find( d_independent.begin(), d_independent.end(), d_child_counter )!=d_independent.end() ){
1564 // d_child_counter--;
1565 //}else{
1566 d_child_counter--;
1567 //}
1568 }
1569 }else{
1570 //one child must match
1571 if( !getChild( d_child_counter )->getNextMatch( p, qi ) ){
1572 if( d_child_counter<(int)(getNumChildren()-1) ){
1573 d_child_counter++;
1574 Debug("qcf-match-debug") << " Reset child " << d_child_counter << " of " << d_n << ", one match" << std::endl;
1575 getChild( d_child_counter )->reset( p, d_tgt, qi );
1576 }else{
1577 d_child_counter = -1;
1578 }
1579 }else{
1580 success = true;
1581 }
1582 }
1583 }else if( d_n.getKind()==EQUAL ){
1584 //construct match based on both children
1585 if( d_child_counter%2==0 ){
1586 if( getChild( 0 )->getNextMatch( p, qi ) ){
1587 d_child_counter++;
1588 getChild( 1 )->reset( p, d_child_counter==1, qi );
1589 }else{
1590 if( d_child_counter==0 ){
1591 d_child_counter = 2;
1592 getChild( 0 )->reset( p, !d_tgt, qi );
1593 }else{
1594 d_child_counter = -1;
1595 }
1596 }
1597 }
1598 if( d_child_counter>=0 && d_child_counter%2==1 ){
1599 if( getChild( 1 )->getNextMatch( p, qi ) ){
1600 success = true;
1601 }else{
1602 d_child_counter--;
1603 }
1604 }
1605 }else if( d_n.getKind()==ITE ){
1606 if( d_child_counter%2==0 ){
1607 int index1 = d_child_counter==4 ? 1 : 0;
1608 if( getChild( index1 )->getNextMatch( p, qi ) ){
1609 d_child_counter++;
1610 getChild( d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==1) ? 1 : 2) )->reset( p, d_tgt, qi );
1611 }else{
1612 if (d_child_counter == 4)
1613 {
1614 d_child_counter = -1;
1615 }else{
1616 d_child_counter +=2;
1617 getChild( d_child_counter==2 ? 0 : 1 )->reset( p, d_child_counter==2 ? !d_tgt : d_tgt, qi );
1618 }
1619 }
1620 }
1621 if( d_child_counter>=0 && d_child_counter%2==1 ){
1622 int index2 = d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==1) ? 1 : 2);
1623 if( getChild( index2 )->getNextMatch( p, qi ) ){
1624 success = true;
1625 }else{
1626 d_child_counter--;
1627 }
1628 }
1629 }else if( d_n.getKind()==FORALL ){
1630 if( getChild( d_child_counter )->getNextMatch( p, qi ) ){
1631 success = true;
1632 }else{
1633 d_child_counter = -1;
1634 }
1635 }
1636 }
1637 d_wasSet = success;
1638 Debug("qcf-match") << " ...finished construct match for " << d_n << ", success = " << success << std::endl;
1639 return success;
1640 }
1641 }
1642 Debug("qcf-match") << " ...already finished for " << d_n << std::endl;
1643 return false;
1644 }
1645
doMatching(QuantConflictFind * p,QuantInfo * qi)1646 bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
1647 if( !d_qn.empty() ){
1648 if( d_qn[0]==NULL ){
1649 d_qn.clear();
1650 return true;
1651 }else{
1652 Assert( d_type==typ_var );
1653 Assert( d_qni_size>0 );
1654 bool invalidMatch;
1655 do {
1656 invalidMatch = false;
1657 Debug("qcf-match-debug") << " Do matching " << d_n << " " << d_qn.size() << " " << d_qni.size() << std::endl;
1658 if( d_qn.size()==d_qni.size()+1 ) {
1659 int index = (int)d_qni.size();
1660 //initialize
1661 TNode val;
1662 std::map< int, int >::iterator itv = d_qni_var_num.find( index );
1663 if( itv!=d_qni_var_num.end() ){
1664 //get the representative variable this variable is equal to
1665 int repVar = qi->getCurrentRepVar( itv->second );
1666 Debug("qcf-match-debug") << " Match " << index << " is a variable " << itv->second << ", which is repVar " << repVar << std::endl;
1667 //get the value the rep variable
1668 //std::map< int, TNode >::iterator itm = qi->d_match.find( repVar );
1669 if( !qi->d_match[repVar].isNull() ){
1670 val = qi->d_match[repVar];
1671 Debug("qcf-match-debug") << " Variable is already bound to " << val << std::endl;
1672 }else{
1673 //binding a variable
1674 d_qni_bound[index] = repVar;
1675 std::map<TNode, TNodeTrie>::iterator it =
1676 d_qn[index]->d_data.begin();
1677 if( it != d_qn[index]->d_data.end() ) {
1678 d_qni.push_back( it );
1679 //set the match
1680 if( it->first.getType().isComparableTo( qi->d_var_types[repVar] ) && qi->setMatch( p, d_qni_bound[index], it->first, true, true ) ){
1681 Debug("qcf-match-debug") << " Binding variable" << std::endl;
1682 if( d_qn.size()<d_qni_size ){
1683 d_qn.push_back( &it->second );
1684 }
1685 }else{
1686 Debug("qcf-match") << " Binding variable, currently fail." << std::endl;
1687 invalidMatch = true;
1688 }
1689 }else{
1690 Debug("qcf-match-debug") << " Binding variable, fail, no more variables to bind" << std::endl;
1691 d_qn.pop_back();
1692 }
1693 }
1694 }else{
1695 Debug("qcf-match-debug") << " Match " << index << " is ground term" << std::endl;
1696 Assert( d_qni_gterm.find( index )!=d_qni_gterm.end() );
1697 Assert( d_qni_gterm_rep.find( index )!=d_qni_gterm_rep.end() );
1698 val = d_qni_gterm_rep[index];
1699 Assert( !val.isNull() );
1700 }
1701 if( !val.isNull() ){
1702 //constrained by val
1703 std::map<TNode, TNodeTrie>::iterator it =
1704 d_qn[index]->d_data.find(val);
1705 if( it!=d_qn[index]->d_data.end() ){
1706 Debug("qcf-match-debug") << " Match" << std::endl;
1707 d_qni.push_back( it );
1708 if( d_qn.size()<d_qni_size ){
1709 d_qn.push_back( &it->second );
1710 }
1711 }else{
1712 Debug("qcf-match-debug") << " Failed to match" << std::endl;
1713 d_qn.pop_back();
1714 }
1715 }
1716 }else{
1717 Assert( d_qn.size()==d_qni.size() );
1718 int index = d_qni.size()-1;
1719 //increment if binding this variable
1720 bool success = false;
1721 std::map< int, int >::iterator itb = d_qni_bound.find( index );
1722 if( itb!=d_qni_bound.end() ){
1723 d_qni[index]++;
1724 if( d_qni[index]!=d_qn[index]->d_data.end() ){
1725 success = true;
1726 if( qi->setMatch( p, itb->second, d_qni[index]->first, true, true ) ){
1727 Debug("qcf-match-debug") << " Bind next variable" << std::endl;
1728 if( d_qn.size()<d_qni_size ){
1729 d_qn.push_back( &d_qni[index]->second );
1730 }
1731 }else{
1732 Debug("qcf-match-debug") << " Bind next variable, currently fail" << std::endl;
1733 invalidMatch = true;
1734 }
1735 }else{
1736 qi->unsetMatch( p, itb->second );
1737 qi->d_match_term[ itb->second ] = TNode::null();
1738 Debug("qcf-match-debug") << " Bind next variable, no more variables to bind" << std::endl;
1739 }
1740 }else{
1741 //TODO : if it equal to something else, also try that
1742 }
1743 //if not incrementing, move to next
1744 if( !success ){
1745 d_qn.pop_back();
1746 d_qni.pop_back();
1747 }
1748 }
1749 }while( ( !d_qn.empty() && d_qni.size()!=d_qni_size ) || invalidMatch );
1750 if( d_qni.size()==d_qni_size ){
1751 //Assert( !d_qni[d_qni.size()-1]->second.d_data.empty() );
1752 //Debug("qcf-match-debug") << " We matched " << d_qni[d_qni.size()-1]->second.d_children.begin()->first << std::endl;
1753 Assert( !d_qni[d_qni.size()-1]->second.d_data.empty() );
1754 TNode t = d_qni[d_qni.size()-1]->second.d_data.begin()->first;
1755 Debug("qcf-match-debug") << " " << d_n << " matched " << t << std::endl;
1756 qi->d_match_term[d_qni_var_num[0]] = t;
1757 //set the match terms
1758 for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){
1759 Debug("qcf-match-debug") << " position " << it->first << " bounded " << it->second << " / " << qi->d_q[0].getNumChildren() << std::endl;
1760 //if( it->second<(int)qi->d_q[0].getNumChildren() ){ //if it is an actual variable, we are interested in knowing the actual term
1761 if( it->first>0 ){
1762 Assert( !qi->d_match[ it->second ].isNull() );
1763 Assert( p->areEqual( t[it->first-1], qi->d_match[ it->second ] ) );
1764 qi->d_match_term[it->second] = t[it->first-1];
1765 }
1766 //}
1767 }
1768 }
1769 }
1770 }
1771 return !d_qn.empty();
1772 }
1773
debugPrintType(const char * c,short typ,bool isTrace)1774 void MatchGen::debugPrintType( const char * c, short typ, bool isTrace ) {
1775 if( isTrace ){
1776 switch( typ ){
1777 case typ_invalid: Trace(c) << "invalid";break;
1778 case typ_ground: Trace(c) << "ground";break;
1779 case typ_eq: Trace(c) << "eq";break;
1780 case typ_pred: Trace(c) << "pred";break;
1781 case typ_formula: Trace(c) << "formula";break;
1782 case typ_var: Trace(c) << "var";break;
1783 case typ_bool_var: Trace(c) << "bool_var";break;
1784 }
1785 }else{
1786 switch( typ ){
1787 case typ_invalid: Debug(c) << "invalid";break;
1788 case typ_ground: Debug(c) << "ground";break;
1789 case typ_eq: Debug(c) << "eq";break;
1790 case typ_pred: Debug(c) << "pred";break;
1791 case typ_formula: Debug(c) << "formula";break;
1792 case typ_var: Debug(c) << "var";break;
1793 case typ_bool_var: Debug(c) << "bool_var";break;
1794 }
1795 }
1796 }
1797
setInvalid()1798 void MatchGen::setInvalid() {
1799 d_type = typ_invalid;
1800 d_children.clear();
1801 }
1802
isHandledBoolConnective(TNode n)1803 bool MatchGen::isHandledBoolConnective( TNode n ) {
1804 return TermUtil::isBoolConnectiveTerm( n ) && n.getKind()!=SEP_STAR;
1805 }
1806
isHandledUfTerm(TNode n)1807 bool MatchGen::isHandledUfTerm( TNode n ) {
1808 //return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT ||
1809 // n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;
1810 //TODO : treat APPLY_TESTER as a T-constraint instead of matching (currently leads to overabundance of instantiations)
1811 //return inst::Trigger::isAtomicTriggerKind( n.getKind() ) && ( !options::qcfTConstraint() || n.getKind()!=APPLY_TESTER );
1812 return inst::Trigger::isAtomicTriggerKind( n.getKind() );
1813 }
1814
getMatchOperator(QuantConflictFind * p,Node n)1815 Node MatchGen::getMatchOperator( QuantConflictFind * p, Node n ) {
1816 if( isHandledUfTerm( n ) ){
1817 return p->getTermDatabase()->getMatchOperator( n );
1818 }else{
1819 return Node::null();
1820 }
1821 }
1822
isHandled(TNode n)1823 bool MatchGen::isHandled( TNode n ) {
1824 if (n.getKind() != BOUND_VARIABLE && expr::hasBoundVar(n))
1825 {
1826 if( !isHandledBoolConnective( n ) && !isHandledUfTerm( n ) && n.getKind()!=EQUAL && n.getKind()!=ITE ){
1827 return false;
1828 }
1829 for( unsigned i=0; i<n.getNumChildren(); i++ ){
1830 if( !isHandled( n[i] ) ){
1831 return false;
1832 }
1833 }
1834 }
1835 return true;
1836 }
1837
QuantConflictFind(QuantifiersEngine * qe,context::Context * c)1838 QuantConflictFind::QuantConflictFind(QuantifiersEngine* qe, context::Context* c)
1839 : QuantifiersModule(qe),
1840 d_conflict(c, false),
1841 d_true(NodeManager::currentNM()->mkConst<bool>(true)),
1842 d_false(NodeManager::currentNM()->mkConst<bool>(false)),
1843 d_effort(EFFORT_INVALID),
1844 d_needs_computeRelEqr() {}
1845
1846 //-------------------------------------------------- registration
1847
registerQuantifier(Node q)1848 void QuantConflictFind::registerQuantifier( Node q ) {
1849 if( d_quantEngine->hasOwnership( q, this ) ){
1850 d_quants.push_back( q );
1851 d_quant_id[q] = d_quants.size();
1852 if( Trace.isOn("qcf-qregister") ){
1853 Trace("qcf-qregister") << "Register ";
1854 debugPrintQuant( "qcf-qregister", q );
1855 Trace("qcf-qregister") << " : " << q << std::endl;
1856 }
1857 //make QcfNode structure
1858 Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl;
1859 d_qinfo[q].initialize( this, q, q[1] );
1860
1861 //debug print
1862 if( Trace.isOn("qcf-qregister") ){
1863 Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;
1864 Trace("qcf-qregister") << " ";
1865 debugPrintQuantBody( "qcf-qregister", q, q[1] );
1866 Trace("qcf-qregister") << std::endl;
1867 if( d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){
1868 Trace("qcf-qregister") << " with additional constraints : " << std::endl;
1869 for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){
1870 Trace("qcf-qregister") << " ?x" << j << " = ";
1871 debugPrintQuantBody( "qcf-qregister", q, d_qinfo[q].d_vars[j], false );
1872 Trace("qcf-qregister") << std::endl;
1873 }
1874 }
1875 Trace("qcf-qregister") << "Done registering quantifier." << std::endl;
1876 }
1877 }
1878 }
1879
areMatchEqual(TNode n1,TNode n2)1880 bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) {
1881 //if( d_effort==QuantConflictFind::effort_mc ){
1882 // return n1==n2 || !areDisequal( n1, n2 );
1883 //}else{
1884 return n1==n2;
1885 //}
1886 }
1887
areMatchDisequal(TNode n1,TNode n2)1888 bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) {
1889 // if( d_effort==QuantConflictFind::Effort::Conflict ){
1890 // return areDisequal( n1, n2 );
1891 //}else{
1892 return n1!=n2;
1893 //}
1894 }
1895
1896 //-------------------------------------------------- check function
1897
needsCheck(Theory::Effort level)1898 bool QuantConflictFind::needsCheck( Theory::Effort level ) {
1899 bool performCheck = false;
1900 if( options::quantConflictFind() && !d_conflict ){
1901 if( level==Theory::EFFORT_LAST_CALL ){
1902 performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_LAST_CALL;
1903 }else if( level==Theory::EFFORT_FULL ){
1904 performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_DEFAULT;
1905 }else if( level==Theory::EFFORT_STANDARD ){
1906 performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_STD;
1907 }
1908 }
1909 return performCheck;
1910 }
1911
reset_round(Theory::Effort level)1912 void QuantConflictFind::reset_round( Theory::Effort level ) {
1913 d_needs_computeRelEqr = true;
1914 }
1915
setIrrelevantFunction(TNode f)1916 void QuantConflictFind::setIrrelevantFunction( TNode f ) {
1917 if( d_irr_func.find( f )==d_irr_func.end() ){
1918 d_irr_func[f] = true;
1919 std::map< TNode, std::vector< Node > >::iterator it = d_func_rel_dom.find( f );
1920 if( it != d_func_rel_dom.end()){
1921 for( unsigned j=0; j<it->second.size(); j++ ){
1922 d_irr_quant[it->second[j]] = true;
1923 }
1924 }
1925 }
1926 }
1927
1928 namespace {
1929
1930 // Returns the beginning of a range of efforts. The range can be iterated
1931 // through as unsigned using operator++.
QcfEffortStart()1932 inline QuantConflictFind::Effort QcfEffortStart() {
1933 return QuantConflictFind::EFFORT_CONFLICT;
1934 }
1935
1936 // Returns the beginning of a range of efforts. The value returned is included
1937 // in the range.
QcfEffortEnd()1938 inline QuantConflictFind::Effort QcfEffortEnd() {
1939 return options::qcfMode() == QCF_PROP_EQ ? QuantConflictFind::EFFORT_PROP_EQ
1940 : QuantConflictFind::EFFORT_CONFLICT;
1941 }
1942
1943 } // namespace
1944
1945 /** check */
check(Theory::Effort level,QEffort quant_e)1946 void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
1947 {
1948 CodeTimer codeTimer(d_quantEngine->d_statistics.d_qcf_time);
1949 if (quant_e == QEFFORT_CONFLICT)
1950 {
1951 Trace("qcf-check") << "QCF : check : " << level << std::endl;
1952 if( d_conflict ){
1953 Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;
1954 if( level>=Theory::EFFORT_FULL ){
1955 Trace("qcf-warn") << "ALREADY IN CONFLICT? " << level << std::endl;
1956 //Assert( false );
1957 }
1958 }else{
1959 int addedLemmas = 0;
1960 ++(d_statistics.d_inst_rounds);
1961 double clSet = 0;
1962 int prevEt = 0;
1963 if( Trace.isOn("qcf-engine") ){
1964 prevEt = d_statistics.d_entailment_checks.getData();
1965 clSet = double(clock())/double(CLOCKS_PER_SEC);
1966 Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level << "---" << std::endl;
1967 }
1968 computeRelevantEqr();
1969
1970 d_irr_func.clear();
1971 d_irr_quant.clear();
1972
1973 if( Trace.isOn("qcf-debug") ){
1974 Trace("qcf-debug") << std::endl;
1975 debugPrint("qcf-debug");
1976 Trace("qcf-debug") << std::endl;
1977 }
1978 bool isConflict = false;
1979 for (unsigned e = QcfEffortStart(), end = QcfEffortEnd(); e <= end; ++e) {
1980 d_effort = static_cast<Effort>(e);
1981 Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl;
1982 for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
1983 Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true );
1984 if( d_quantEngine->hasOwnership( q, this ) && d_irr_quant.find( q )==d_irr_quant.end() ){
1985 QuantInfo * qi = &d_qinfo[q];
1986
1987 Assert( d_qinfo.find( q )!=d_qinfo.end() );
1988 if( qi->matchGeneratorIsValid() ){
1989 Trace("qcf-check") << "Check quantified formula ";
1990 debugPrintQuant("qcf-check", q);
1991 Trace("qcf-check") << " : " << q << "..." << std::endl;
1992
1993 Trace("qcf-check-debug") << "Reset round..." << std::endl;
1994 if( qi->reset_round( this ) ){
1995 //try to make a matches making the body false
1996 Trace("qcf-check-debug") << "Get next match..." << std::endl;
1997 while( qi->getNextMatch( this ) ){
1998 if( d_quantEngine->inConflict() ){
1999 Trace("qcf-check") << " ... Quantifiers engine discovered conflict, ";
2000 Trace("qcf-check") << "probably related to disequal congruent terms in master equality engine" << std::endl;
2001 break;
2002 }else{
2003 Trace("qcf-inst") << "*** Produced match at effort " << e << " : " << std::endl;
2004 qi->debugPrintMatch("qcf-inst");
2005 Trace("qcf-inst") << std::endl;
2006 if( !qi->isMatchSpurious( this ) ){
2007 std::vector< int > assigned;
2008 if( qi->completeMatch( this, assigned ) ){
2009 std::vector< Node > terms;
2010 qi->getMatch( terms );
2011 bool tcs = qi->isTConstraintSpurious( this, terms );
2012 if( !tcs ){
2013 //for debugging
2014 if( Debug.isOn("qcf-check-inst") ){
2015 Node inst = d_quantEngine->getInstantiate()
2016 ->getInstantiation(q, terms);
2017 Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;
2018 Assert( !getTermDatabase()->isEntailed( inst, true ) );
2019 Assert(getTermDatabase()->isEntailed(inst, false) ||
2020 e > EFFORT_CONFLICT);
2021 }
2022 if (d_quantEngine->getInstantiate()->addInstantiation(
2023 q, terms))
2024 {
2025 Trace("qcf-check") << " ... Added instantiation" << std::endl;
2026 Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl;
2027 qi->debugPrintMatch("qcf-inst");
2028 Trace("qcf-inst") << std::endl;
2029 ++addedLemmas;
2030 if (e == EFFORT_CONFLICT) {
2031 d_quantEngine->markRelevant( q );
2032 ++(d_quantEngine->d_statistics.d_instantiations_qcf);
2033 if( options::qcfAllConflict() ){
2034 isConflict = true;
2035 }else{
2036 d_conflict.set( true );
2037 }
2038 break;
2039 } else if (e == EFFORT_PROP_EQ) {
2040 d_quantEngine->markRelevant( q );
2041 ++(d_quantEngine->d_statistics.d_instantiations_qcf);
2042 }
2043 }else{
2044 Trace("qcf-inst") << " ... Failed to add instantiation" << std::endl;
2045 //this should only happen if the algorithm generates the same propagating instance twice this round
2046 //in this case, break to avoid exponential behavior
2047 break;
2048 }
2049 }else{
2050 Trace("qcf-inst") << " ... Spurious instantiation (match is T-inconsistent)" << std::endl;
2051 }
2052 //clean up assigned
2053 qi->revertMatch( this, assigned );
2054 d_tempCache.clear();
2055 }else{
2056 Trace("qcf-inst") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
2057 }
2058 }else{
2059 Trace("qcf-inst") << " ... Spurious instantiation (match is inconsistent)" << std::endl;
2060 }
2061 }
2062 }
2063 Trace("qcf-check") << "Done, conflict = " << d_conflict << std::endl;
2064 }
2065 if (d_conflict || d_quantEngine->inConflict())
2066 {
2067 break;
2068 }
2069 }
2070 }
2071 }
2072 if( addedLemmas>0 || d_quantEngine->inConflict() ){
2073 break;
2074 }
2075 }
2076 if( isConflict ){
2077 d_conflict.set( true );
2078 }
2079 if( Trace.isOn("qcf-engine") ){
2080 double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
2081 Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet);
2082 if( addedLemmas>0 ){
2083 Trace("qcf-engine")
2084 << ", effort = "
2085 << (d_effort == EFFORT_CONFLICT
2086 ? "conflict"
2087 : (d_effort == EFFORT_PROP_EQ ? "prop_eq" : "mc"));
2088 Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;
2089 }
2090 Trace("qcf-engine") << std::endl;
2091 int currEt = d_statistics.d_entailment_checks.getData();
2092 if( currEt!=prevEt ){
2093 Trace("qcf-engine") << " Entailment checks = " << ( currEt - prevEt ) << std::endl;
2094 }
2095 }
2096 Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;
2097 }
2098 }
2099 }
2100
computeRelevantEqr()2101 void QuantConflictFind::computeRelevantEqr() {
2102 if( d_needs_computeRelEqr ){
2103 d_needs_computeRelEqr = false;
2104 Trace("qcf-check") << "Compute relevant equivalence classes..." << std::endl;
2105 d_eqcs.clear();
2106
2107 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );
2108 while( !eqcs_i.isFinished() ){
2109 Node r = (*eqcs_i);
2110 if( getTermDatabase()->hasTermCurrent( r ) ){
2111 TypeNode rtn = r.getType();
2112 if( !options::cbqi() || !TermUtil::hasInstConstAttr( r ) ){
2113 d_eqcs[rtn].push_back( r );
2114 }
2115 }
2116 ++eqcs_i;
2117 }
2118 }
2119 }
2120
2121
2122 //-------------------------------------------------- debugging
2123
2124
debugPrint(const char * c)2125 void QuantConflictFind::debugPrint( const char * c ) {
2126 //print the equivalance classes
2127 Trace(c) << "----------EQ classes" << std::endl;
2128 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );
2129 while( !eqcs_i.isFinished() ){
2130 Node n = (*eqcs_i);
2131 //if( !n.getType().isInteger() ){
2132 Trace(c) << " - " << n << " : {";
2133 eq::EqClassIterator eqc_i = eq::EqClassIterator( n, getEqualityEngine() );
2134 bool pr = false;
2135 while( !eqc_i.isFinished() ){
2136 Node nn = (*eqc_i);
2137 if( nn.getKind()!=EQUAL && nn!=n ){
2138 Trace(c) << (pr ? "," : "" ) << " " << nn;
2139 pr = true;
2140 }
2141 ++eqc_i;
2142 }
2143 Trace(c) << (pr ? " " : "" ) << "}" << std::endl;
2144 ++eqcs_i;
2145 }
2146 }
2147
debugPrintQuant(const char * c,Node q)2148 void QuantConflictFind::debugPrintQuant( const char * c, Node q ) {
2149 Trace(c) << "Q" << d_quant_id[q];
2150 }
2151
debugPrintQuantBody(const char * c,Node q,Node n,bool doVarNum)2152 void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, bool doVarNum ) {
2153 if( n.getNumChildren()==0 ){
2154 Trace(c) << n;
2155 }else if( doVarNum && d_qinfo[q].d_var_num.find( n )!=d_qinfo[q].d_var_num.end() ){
2156 Trace(c) << "?x" << d_qinfo[q].d_var_num[n];
2157 }else{
2158 Trace(c) << "(";
2159 if( n.getKind()==APPLY_UF ){
2160 Trace(c) << n.getOperator();
2161 }else{
2162 Trace(c) << n.getKind();
2163 }
2164 for( unsigned i=0; i<n.getNumChildren(); i++ ){
2165 Trace(c) << " ";
2166 debugPrintQuantBody( c, q, n[i] );
2167 }
2168 Trace(c) << ")";
2169 }
2170 }
2171
Statistics()2172 QuantConflictFind::Statistics::Statistics():
2173 d_inst_rounds("QuantConflictFind::Inst_Rounds", 0),
2174 d_entailment_checks("QuantConflictFind::Entailment_Checks",0)
2175 {
2176 smtStatisticsRegistry()->registerStat(&d_inst_rounds);
2177 smtStatisticsRegistry()->registerStat(&d_entailment_checks);
2178 }
2179
~Statistics()2180 QuantConflictFind::Statistics::~Statistics(){
2181 smtStatisticsRegistry()->unregisterStat(&d_inst_rounds);
2182 smtStatisticsRegistry()->unregisterStat(&d_entailment_checks);
2183 }
2184
getZero(Kind k)2185 TNode QuantConflictFind::getZero( Kind k ) {
2186 std::map< Kind, Node >::iterator it = d_zero.find( k );
2187 if( it==d_zero.end() ){
2188 Node nn;
2189 if( k==PLUS ){
2190 nn = NodeManager::currentNM()->mkConst( Rational(0) );
2191 }
2192 d_zero[k] = nn;
2193 return nn;
2194 }else{
2195 return it->second;
2196 }
2197 }
2198
operator <<(std::ostream & os,const QuantConflictFind::Effort & e)2199 std::ostream& operator<<(std::ostream& os, const QuantConflictFind::Effort& e) {
2200 switch (e) {
2201 case QuantConflictFind::EFFORT_INVALID:
2202 os << "Invalid";
2203 break;
2204 case QuantConflictFind::EFFORT_CONFLICT:
2205 os << "Conflict";
2206 break;
2207 case QuantConflictFind::EFFORT_PROP_EQ:
2208 os << "PropEq";
2209 break;
2210 }
2211 return os;
2212 }
2213
2214 } /* namespace CVC4::theory::quantifiers */
2215 } /* namespace CVC4::theory */
2216 } /* namespace CVC4 */
2217