1 /********************* */
2 /*! \file trigger.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Morgan Deters, Tim King
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 Implementation of trigger class
13 **/
14
15 #include "theory/quantifiers/ematching/trigger.h"
16
17 #include "expr/node_algorithm.h"
18 #include "theory/arith/arith_msum.h"
19 #include "theory/quantifiers/ematching/candidate_generator.h"
20 #include "theory/quantifiers/ematching/ho_trigger.h"
21 #include "theory/quantifiers/ematching/inst_match_generator.h"
22 #include "theory/quantifiers/instantiate.h"
23 #include "theory/quantifiers/term_database.h"
24 #include "theory/quantifiers/term_util.h"
25 #include "theory/quantifiers_engine.h"
26 #include "theory/theory_engine.h"
27 #include "theory/uf/equality_engine.h"
28 #include "util/hash.h"
29
30 using namespace std;
31 using namespace CVC4::kind;
32 using namespace CVC4::context;
33
34 namespace CVC4 {
35 namespace theory {
36 namespace inst {
37
init(Node q,Node n,int reqPol,Node reqPolEq)38 void TriggerTermInfo::init( Node q, Node n, int reqPol, Node reqPolEq ){
39 if( d_fv.empty() ){
40 quantifiers::TermUtil::computeInstConstContainsForQuant(q, n, d_fv);
41 }
42 if( d_reqPol==0 ){
43 d_reqPol = reqPol;
44 d_reqPolEq = reqPolEq;
45 }else{
46 //determined a ground (dis)equality must hold or else q is a tautology?
47 }
48 d_weight = Trigger::getTriggerWeight(n);
49 }
50
51 /** trigger class constructor */
Trigger(QuantifiersEngine * qe,Node q,std::vector<Node> & nodes)52 Trigger::Trigger(QuantifiersEngine* qe, Node q, std::vector<Node>& nodes)
53 : d_quantEngine(qe), d_quant(q)
54 {
55 d_nodes.insert( d_nodes.begin(), nodes.begin(), nodes.end() );
56 Trace("trigger") << "Trigger for " << q << ": " << std::endl;
57 for( unsigned i=0; i<d_nodes.size(); i++ ){
58 Trace("trigger") << " " << d_nodes[i] << std::endl;
59 }
60 if( d_nodes.size()==1 ){
61 if( isSimpleTrigger( d_nodes[0] ) ){
62 d_mg = new InstMatchGeneratorSimple(q, d_nodes[0], qe);
63 }else{
64 d_mg = InstMatchGenerator::mkInstMatchGenerator(q, d_nodes[0], qe);
65 }
66 }else{
67 if( options::multiTriggerCache() ){
68 d_mg = new InstMatchGeneratorMulti(q, d_nodes, qe);
69 }else{
70 d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti(q, d_nodes, qe);
71 }
72 }
73 if( d_nodes.size()==1 ){
74 if( isSimpleTrigger( d_nodes[0] ) ){
75 ++(qe->d_statistics.d_triggers);
76 }else{
77 ++(qe->d_statistics.d_simple_triggers);
78 }
79 }else{
80 Trace("multi-trigger") << "Trigger for " << q << ": " << std::endl;
81 for( unsigned i=0; i<d_nodes.size(); i++ ){
82 Trace("multi-trigger") << " " << d_nodes[i] << std::endl;
83 }
84 ++(qe->d_statistics.d_multi_triggers);
85 }
86
87 // Notice() << "Trigger : " << (*this) << " for " << q << std::endl;
88 Trace("trigger-debug") << "Finished making trigger." << std::endl;
89 }
90
~Trigger()91 Trigger::~Trigger() {
92 delete d_mg;
93 }
94
resetInstantiationRound()95 void Trigger::resetInstantiationRound(){
96 d_mg->resetInstantiationRound( d_quantEngine );
97 }
98
reset(Node eqc)99 void Trigger::reset( Node eqc ){
100 d_mg->reset( eqc, d_quantEngine );
101 }
102
getInstPattern()103 Node Trigger::getInstPattern(){
104 return NodeManager::currentNM()->mkNode( INST_PATTERN, d_nodes );
105 }
106
addInstantiations()107 int Trigger::addInstantiations()
108 {
109 int addedLemmas = d_mg->addInstantiations(d_quant, d_quantEngine, this);
110 if( addedLemmas>0 ){
111 if (Debug.isOn("inst-trigger"))
112 {
113 Debug("inst-trigger") << "Added " << addedLemmas
114 << " lemmas, trigger was ";
115 for (unsigned i = 0; i < d_nodes.size(); i++)
116 {
117 Debug("inst-trigger") << d_nodes[i] << " ";
118 }
119 Debug("inst-trigger") << std::endl;
120 }
121 }
122 return addedLemmas;
123 }
124
sendInstantiation(InstMatch & m)125 bool Trigger::sendInstantiation(InstMatch& m)
126 {
127 return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m);
128 }
129
mkTriggerTerms(Node q,std::vector<Node> & nodes,unsigned n_vars,std::vector<Node> & trNodes)130 bool Trigger::mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_vars, std::vector< Node >& trNodes ) {
131 //only take nodes that contribute variables to the trigger when added
132 std::vector< Node > temp;
133 temp.insert( temp.begin(), nodes.begin(), nodes.end() );
134 std::map< Node, bool > vars;
135 std::map< Node, std::vector< Node > > patterns;
136 size_t varCount = 0;
137 std::map< Node, std::vector< Node > > varContains;
138 for (const Node& pat : temp)
139 {
140 quantifiers::TermUtil::computeInstConstContainsForQuant(
141 q, pat, varContains[pat]);
142 }
143 for( unsigned i=0; i<temp.size(); i++ ){
144 bool foundVar = false;
145 for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){
146 Node v = varContains[ temp[i] ][j];
147 Assert( quantifiers::TermUtil::getInstConstAttr(v)==q );
148 if( vars.find( v )==vars.end() ){
149 varCount++;
150 vars[ v ] = true;
151 foundVar = true;
152 }
153 }
154 if( foundVar ){
155 trNodes.push_back( temp[i] );
156 for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){
157 Node v = varContains[ temp[i] ][j];
158 patterns[ v ].push_back( temp[i] );
159 }
160 }
161 if( varCount==n_vars ){
162 break;
163 }
164 }
165 if( varCount<n_vars ){
166 Trace("trigger-debug") << "Don't consider trigger since it does not contain specified number of variables." << std::endl;
167 for( unsigned i=0; i<nodes.size(); i++) {
168 Trace("trigger-debug") << nodes[i] << " ";
169 }
170 Trace("trigger-debug") << std::endl;
171
172 //do not generate multi-trigger if it does not contain all variables
173 return false;
174 }else{
175 //now, minimize the trigger
176 for( unsigned i=0; i<trNodes.size(); i++ ){
177 bool keepPattern = false;
178 Node n = trNodes[i];
179 for( unsigned j=0; j<varContains[ n ].size(); j++ ){
180 Node v = varContains[ n ][j];
181 if( patterns[v].size()==1 ){
182 keepPattern = true;
183 break;
184 }
185 }
186 if( !keepPattern ){
187 //remove from pattern vector
188 for( unsigned j=0; j<varContains[ n ].size(); j++ ){
189 Node v = varContains[ n ][j];
190 for( unsigned k=0; k<patterns[v].size(); k++ ){
191 if( patterns[v][k]==n ){
192 patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 );
193 break;
194 }
195 }
196 }
197 //remove from trigger nodes
198 trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 );
199 i--;
200 }
201 }
202 }
203 return true;
204 }
205
mkTrigger(QuantifiersEngine * qe,Node f,std::vector<Node> & nodes,bool keepAll,int trOption,unsigned use_n_vars)206 Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, bool keepAll, int trOption, unsigned use_n_vars ){
207 std::vector< Node > trNodes;
208 if( !keepAll ){
209 unsigned n_vars = use_n_vars==0 ? f[0].getNumChildren() : use_n_vars;
210 if( !mkTriggerTerms( f, nodes, n_vars, trNodes ) ){
211 return NULL;
212 }
213 }else{
214 trNodes.insert( trNodes.begin(), nodes.begin(), nodes.end() );
215 }
216
217 //check for duplicate?
218 if( trOption!=TR_MAKE_NEW ){
219 Trigger* t = qe->getTriggerDatabase()->getTrigger( trNodes );
220 if( t ){
221 if( trOption==TR_GET_OLD ){
222 //just return old trigger
223 return t;
224 }else{
225 return NULL;
226 }
227 }
228 }
229
230 // check if higher-order
231 Trace("trigger-debug") << "Collect higher-order variable triggers..."
232 << std::endl;
233 std::map<Node, std::vector<Node> > ho_apps;
234 HigherOrderTrigger::collectHoVarApplyTerms(f, trNodes, ho_apps);
235 Trace("trigger") << "...got " << ho_apps.size()
236 << " higher-order applications." << std::endl;
237 Trigger* t;
238 if (!ho_apps.empty())
239 {
240 t = new HigherOrderTrigger(qe, f, trNodes, ho_apps);
241 }
242 else
243 {
244 t = new Trigger(qe, f, trNodes);
245 }
246
247 qe->getTriggerDatabase()->addTrigger( trNodes, t );
248 return t;
249 }
250
mkTrigger(QuantifiersEngine * qe,Node f,Node n,bool keepAll,int trOption,unsigned use_n_vars)251 Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, bool keepAll, int trOption, unsigned use_n_vars ){
252 std::vector< Node > nodes;
253 nodes.push_back( n );
254 return mkTrigger( qe, f, nodes, keepAll, trOption, use_n_vars );
255 }
256
isUsable(Node n,Node q)257 bool Trigger::isUsable( Node n, Node q ){
258 if( quantifiers::TermUtil::getInstConstAttr(n)==q ){
259 if( isAtomicTrigger( n ) ){
260 for( unsigned i=0; i<n.getNumChildren(); i++ ){
261 if( !isUsable( n[i], q ) ){
262 return false;
263 }
264 }
265 return true;
266 }else if( n.getKind()==INST_CONSTANT ){
267 return true;
268 }else{
269 std::map< Node, Node > coeffs;
270 if (options::purifyTriggers())
271 {
272 Node x = getInversionVariable( n );
273 if( !x.isNull() ){
274 return true;
275 }
276 }
277 }
278 return false;
279 }else{
280 return true;
281 }
282 }
283
getIsUsableEq(Node q,Node n)284 Node Trigger::getIsUsableEq( Node q, Node n ) {
285 Assert( isRelationalTrigger( n ) );
286 for( unsigned i=0; i<2; i++) {
287 if( isUsableEqTerms( q, n[i], n[1-i] ) ){
288 if( i==1 && n.getKind()==EQUAL && !quantifiers::TermUtil::hasInstConstAttr(n[0]) ){
289 return NodeManager::currentNM()->mkNode( n.getKind(), n[1], n[0] );
290 }else{
291 return n;
292 }
293 }
294 }
295 return Node::null();
296 }
297
isUsableEqTerms(Node q,Node n1,Node n2)298 bool Trigger::isUsableEqTerms( Node q, Node n1, Node n2 ) {
299 if( n1.getKind()==INST_CONSTANT ){
300 if( options::relationalTriggers() ){
301 if( !quantifiers::TermUtil::hasInstConstAttr(n2) ){
302 return true;
303 }else if( n2.getKind()==INST_CONSTANT ){
304 return true;
305 }
306 }
307 }else if( isUsableAtomicTrigger( n1, q ) ){
308 if (options::relationalTriggers() && n2.getKind() == INST_CONSTANT
309 && !expr::hasSubterm(n1, n2))
310 {
311 return true;
312 }
313 else if (!quantifiers::TermUtil::hasInstConstAttr(n2))
314 {
315 return true;
316 }
317 }
318 return false;
319 }
320
getIsUsableTrigger(Node n,Node q)321 Node Trigger::getIsUsableTrigger( Node n, Node q ) {
322 bool pol = true;
323 Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl;
324 if( n.getKind()==NOT ){
325 pol = !pol;
326 n = n[0];
327 }
328 if( n.getKind()==INST_CONSTANT ){
329 return pol ? n : NodeManager::currentNM()->mkNode( EQUAL, n, NodeManager::currentNM()->mkConst( true ) ).notNode();
330 }else if( isRelationalTrigger( n ) ){
331 Node rtr = getIsUsableEq( q, n );
332 if( rtr.isNull() && n[0].getType().isReal() ){
333 //try to solve relation
334 std::map< Node, Node > m;
335 if (ArithMSum::getMonomialSumLit(n, m))
336 {
337 for( std::map< Node, Node >::iterator it = m.begin(); it!=m.end(); ++it ){
338 bool trySolve = false;
339 if( !it->first.isNull() ){
340 if( it->first.getKind()==INST_CONSTANT ){
341 trySolve = options::relationalTriggers();
342 }else if( isUsableTrigger( it->first, q ) ){
343 trySolve = true;
344 }
345 }
346 if( trySolve ){
347 Trace("trigger-debug") << "Try to solve for " << it->first << std::endl;
348 Node veq;
349 if (ArithMSum::isolate(it->first, m, veq, n.getKind()) != 0)
350 {
351 rtr = getIsUsableEq( q, veq );
352 }
353 //either all solves will succeed or all solves will fail
354 break;
355 }
356 }
357 }
358 }
359 if( !rtr.isNull() ){
360 Trace("relational-trigger") << "Relational trigger : " << std::endl;
361 Trace("relational-trigger") << " " << rtr << " (from " << n << ")" << std::endl;
362 Trace("relational-trigger") << " in quantifier " << q << std::endl;
363 Node rtr2 = pol ? rtr : rtr.negate();
364 Trace("relational-trigger") << " return : " << rtr2 << std::endl;
365 return rtr2;
366 }
367 }else{
368 Trace("trigger-debug") << n << " usable : " << ( quantifiers::TermUtil::getInstConstAttr(n)==q ) << " " << isAtomicTrigger( n ) << " " << isUsable( n, q ) << std::endl;
369 if( isUsableAtomicTrigger( n, q ) ){
370 return pol ? n : NodeManager::currentNM()->mkNode( EQUAL, n, NodeManager::currentNM()->mkConst( true ) ).notNode();
371 }
372 }
373 return Node::null();
374 }
375
isUsableAtomicTrigger(Node n,Node q)376 bool Trigger::isUsableAtomicTrigger( Node n, Node q ) {
377 return quantifiers::TermUtil::getInstConstAttr( n )==q && isAtomicTrigger( n ) && isUsable( n, q );
378 }
379
isUsableTrigger(Node n,Node q)380 bool Trigger::isUsableTrigger( Node n, Node q ){
381 Node nu = getIsUsableTrigger( n, q );
382 return !nu.isNull();
383 }
384
isAtomicTrigger(Node n)385 bool Trigger::isAtomicTrigger( Node n ){
386 return isAtomicTriggerKind( n.getKind() );
387 }
388
isAtomicTriggerKind(Kind k)389 bool Trigger::isAtomicTriggerKind( Kind k ) {
390 return k == APPLY_UF || k == SELECT || k == STORE || k == APPLY_CONSTRUCTOR
391 || k == APPLY_SELECTOR_TOTAL || k == APPLY_TESTER || k == UNION
392 || k == INTERSECTION || k == SUBSET || k == SETMINUS || k == MEMBER
393 || k == SINGLETON || k == SEP_PTO || k == BITVECTOR_TO_NAT
394 || k == INT_TO_BITVECTOR || k == HO_APPLY;
395 }
396
isRelationalTrigger(Node n)397 bool Trigger::isRelationalTrigger( Node n ) {
398 return isRelationalTriggerKind( n.getKind() );
399 }
400
isRelationalTriggerKind(Kind k)401 bool Trigger::isRelationalTriggerKind( Kind k ) {
402 return k==EQUAL || k==GEQ;
403 }
404
isSimpleTrigger(Node n)405 bool Trigger::isSimpleTrigger( Node n ){
406 Node t = n.getKind()==NOT ? n[0] : n;
407 if( t.getKind()==EQUAL ){
408 if( !quantifiers::TermUtil::hasInstConstAttr( t[1] ) ){
409 t = t[0];
410 }
411 }
412 if( isAtomicTrigger( t ) ){
413 for( unsigned i=0; i<t.getNumChildren(); i++ ){
414 if( t[i].getKind()!=INST_CONSTANT && quantifiers::TermUtil::hasInstConstAttr(t[i]) ){
415 return false;
416 }
417 }
418 if( options::purifyDtTriggers() && t.getKind()==APPLY_SELECTOR_TOTAL ){
419 return false;
420 }
421 if (t.getKind() == HO_APPLY && t[0].getKind() == INST_CONSTANT)
422 {
423 return false;
424 }
425 return true;
426 }else{
427 return false;
428 }
429 }
430
431 //store triggers in reqPol, indicating their polarity (if any) they must appear to falsify the quantified formula
collectPatTerms2(Node q,Node n,std::map<Node,std::vector<Node>> & visited,std::map<Node,TriggerTermInfo> & tinfo,quantifiers::TriggerSelMode tstrt,std::vector<Node> & exclude,std::vector<Node> & added,bool pol,bool hasPol,bool epol,bool hasEPol,bool knowIsUsable)432 void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Node > >& visited, std::map< Node, TriggerTermInfo >& tinfo,
433 quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added,
434 bool pol, bool hasPol, bool epol, bool hasEPol, bool knowIsUsable ){
435 std::map< Node, std::vector< Node > >::iterator itv = visited.find( n );
436 if( itv==visited.end() ){
437 visited[ n ].clear();
438 Trace("auto-gen-trigger-debug2") << "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol << " " << hasEPol << std::endl;
439 if( n.getKind()!=FORALL && n.getKind()!=INST_CONSTANT ){
440 Node nu;
441 bool nu_single = false;
442 if( knowIsUsable ){
443 nu = n;
444 }else if( n.getKind()!=NOT && std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){
445 nu = getIsUsableTrigger( n, q );
446 if( !nu.isNull() && nu!=n ){
447 collectPatTerms2( q, nu, visited, tinfo, tstrt, exclude, added, pol, hasPol, epol, hasEPol, true );
448 // copy to n
449 visited[n].insert( visited[n].end(), added.begin(), added.end() );
450 return;
451 }
452 }
453 if( !nu.isNull() ){
454 Assert( nu==n );
455 Assert( nu.getKind()!=NOT );
456 Trace("auto-gen-trigger-debug2") << "...found usable trigger : " << nu << std::endl;
457 Node reqEq;
458 if( nu.getKind()==EQUAL ){
459 if( isAtomicTrigger( nu[0] ) && !quantifiers::TermUtil::hasInstConstAttr(nu[1]) ){
460 if( hasPol ){
461 reqEq = nu[1];
462 }
463 nu = nu[0];
464 }
465 }
466 Assert( reqEq.isNull() || !quantifiers::TermUtil::hasInstConstAttr( reqEq ) );
467 Assert( isUsableTrigger( nu, q ) );
468 //tinfo.find( nu )==tinfo.end()
469 Trace("auto-gen-trigger-debug2") << "...add usable trigger : " << nu << std::endl;
470 tinfo[ nu ].init( q, nu, hasEPol ? ( epol ? 1 : -1 ) : 0, reqEq );
471 nu_single = tinfo[ nu ].d_fv.size()==q[0].getNumChildren();
472 }
473 Node nrec = nu.isNull() ? n : nu;
474 std::vector< Node > added2;
475 for( unsigned i=0; i<nrec.getNumChildren(); i++ ){
476 bool newHasPol, newPol;
477 bool newHasEPol, newEPol;
478 QuantPhaseReq::getPolarity( nrec, i, hasPol, pol, newHasPol, newPol );
479 QuantPhaseReq::getEntailPolarity( nrec, i, hasEPol, epol, newHasEPol, newEPol );
480 collectPatTerms2( q, nrec[i], visited, tinfo, tstrt, exclude, added2, newPol, newHasPol, newEPol, newHasEPol );
481 }
482 // if this is not a usable trigger, don't worry about caching the results, since triggers do not contain non-usable subterms
483 if( !nu.isNull() ){
484 bool rm_nu = false;
485 for( unsigned i=0; i<added2.size(); i++ ){
486 Trace("auto-gen-trigger-debug2") << "..." << nu << " added child " << i << " : " << added2[i] << std::endl;
487 Assert( added2[i]!=nu );
488 // if child was not already removed
489 if( tinfo.find( added2[i] )!=tinfo.end() ){
490 if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){
491 //discard all subterms
492 Trace("auto-gen-trigger-debug2") << "......remove it." << std::endl;
493 visited[ added2[i] ].clear();
494 tinfo.erase( added2[i] );
495 }else{
496 if( tinfo[ nu ].d_fv.size()==tinfo[ added2[i] ].d_fv.size() ){
497 if (tinfo[nu].d_weight >= tinfo[added2[i]].d_weight)
498 {
499 // discard if we added a subterm as a trigger with all
500 // variables that nu has
501 Trace("auto-gen-trigger-debug2")
502 << "......subsumes parent " << tinfo[nu].d_weight << " "
503 << tinfo[added2[i]].d_weight << "." << std::endl;
504 rm_nu = true;
505 }
506 }
507 if( std::find( added.begin(), added.end(), added2[i] )==added.end() ){
508 added.push_back( added2[i] );
509 }
510 }
511 }
512 }
513 if( rm_nu && ( tstrt==quantifiers::TRIGGER_SEL_MIN || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL && nu_single ) ) ){
514 tinfo.erase( nu );
515 }else{
516 if( std::find( added.begin(), added.end(), nu )==added.end() ){
517 added.push_back( nu );
518 }
519 }
520 visited[n].insert( visited[n].end(), added.begin(), added.end() );
521 }
522 }
523 }else{
524 for( unsigned i=0; i<itv->second.size(); ++i ){
525 Node t = itv->second[i];
526 if( std::find( added.begin(), added.end(), t )==added.end() ){
527 added.push_back( t );
528 }
529 }
530 }
531 }
532
isPureTheoryTrigger(Node n)533 bool Trigger::isPureTheoryTrigger( Node n ) {
534 if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){ //|| !quantifiers::TermUtil::hasInstConstAttr( n ) ){
535 return false;
536 }else{
537 for( unsigned i=0; i<n.getNumChildren(); i++ ){
538 if( !isPureTheoryTrigger( n[i] ) ){
539 return false;
540 }
541 }
542 return true;
543 }
544 }
545
getTriggerWeight(Node n)546 int Trigger::getTriggerWeight( Node n ) {
547 if (n.getKind() == APPLY_UF)
548 {
549 return 0;
550 }
551 else if (isAtomicTrigger(n))
552 {
553 return 1;
554 }else{
555 if( options::relationalTriggers() ){
556 if( isRelationalTrigger( n ) ){
557 for( unsigned i=0; i<2; i++ ){
558 if( n[i].getKind()==INST_CONSTANT && !quantifiers::TermUtil::hasInstConstAttr( n[1-i] ) ){
559 return 0;
560 }
561 }
562 }
563 }
564 return 2;
565 }
566 }
567
isLocalTheoryExt(Node n,std::vector<Node> & vars,std::vector<Node> & patTerms)568 bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< Node >& patTerms ) {
569 if( !n.getType().isBoolean() && n.getKind()==APPLY_UF ){
570 if( std::find( patTerms.begin(), patTerms.end(), n )==patTerms.end() ){
571 bool hasVar = false;
572 for( unsigned i=0; i<n.getNumChildren(); i++ ){
573 if( n[i].getKind()==INST_CONSTANT ){
574 hasVar = true;
575 if( std::find( vars.begin(), vars.end(), n[i] )==vars.end() ){
576 vars.push_back( n[i] );
577 }else{
578 //do not allow duplicate variables
579 return false;
580 }
581 }else{
582 //do not allow nested function applications
583 return false;
584 }
585 }
586 if( hasVar ){
587 patTerms.push_back( n );
588 }
589 }
590 }else{
591 for( unsigned i=0; i<n.getNumChildren(); i++ ){
592 if( !isLocalTheoryExt( n[i], vars, patTerms ) ){
593 return false;
594 }
595 }
596 }
597 return true;
598 }
599
collectPatTerms(Node q,Node n,std::vector<Node> & patTerms,quantifiers::TriggerSelMode tstrt,std::vector<Node> & exclude,std::map<Node,TriggerTermInfo> & tinfo,bool filterInst)600 void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude,
601 std::map< Node, TriggerTermInfo >& tinfo, bool filterInst ){
602 std::map< Node, std::vector< Node > > visited;
603 if( filterInst ){
604 //immediately do not consider any term t for which another term is an instance of t
605 std::vector< Node > patTerms2;
606 std::map< Node, TriggerTermInfo > tinfo2;
607 collectPatTerms( q, n, patTerms2, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo2, false );
608 std::vector< Node > temp;
609 temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() );
610 filterTriggerInstances(temp);
611 if (Trace.isOn("trigger-filter-instance"))
612 {
613 if (temp.size() != patTerms2.size())
614 {
615 Trace("trigger-filter-instance") << "Filtered an instance: "
616 << std::endl;
617 Trace("trigger-filter-instance") << "Old: ";
618 for (unsigned i = 0; i < patTerms2.size(); i++)
619 {
620 Trace("trigger-filter-instance") << patTerms2[i] << " ";
621 }
622 Trace("trigger-filter-instance") << std::endl << "New: ";
623 for (unsigned i = 0; i < temp.size(); i++)
624 {
625 Trace("trigger-filter-instance") << temp[i] << " ";
626 }
627 Trace("trigger-filter-instance") << std::endl;
628 }
629 }
630 if( tstrt==quantifiers::TRIGGER_SEL_ALL ){
631 for( unsigned i=0; i<temp.size(); i++ ){
632 //copy information
633 tinfo[temp[i]].d_fv.insert( tinfo[temp[i]].d_fv.end(), tinfo2[temp[i]].d_fv.begin(), tinfo2[temp[i]].d_fv.end() );
634 tinfo[temp[i]].d_reqPol = tinfo2[temp[i]].d_reqPol;
635 tinfo[temp[i]].d_reqPolEq = tinfo2[temp[i]].d_reqPolEq;
636 patTerms.push_back( temp[i] );
637 }
638 return;
639 }else{
640 //do not consider terms that have instances
641 for( unsigned i=0; i<patTerms2.size(); i++ ){
642 if( std::find( temp.begin(), temp.end(), patTerms2[i] )==temp.end() ){
643 visited[ patTerms2[i] ].clear();
644 }
645 }
646 }
647 }
648 std::vector< Node > added;
649 collectPatTerms2( q, n, visited, tinfo, tstrt, exclude, added, true, true, false, true );
650 for( std::map< Node, TriggerTermInfo >::iterator it = tinfo.begin(); it != tinfo.end(); ++it ){
651 patTerms.push_back( it->first );
652 }
653 }
654
isTriggerInstanceOf(Node n1,Node n2,std::vector<Node> & fv1,std::vector<Node> & fv2)655 int Trigger::isTriggerInstanceOf(Node n1,
656 Node n2,
657 std::vector<Node>& fv1,
658 std::vector<Node>& fv2)
659 {
660 Assert(n1 != n2);
661 int status = 0;
662 std::unordered_set<TNode, TNodeHashFunction> subs_vars;
663 std::unordered_set<std::pair<TNode, TNode>,
664 PairHashFunction<TNode,
665 TNode,
666 TNodeHashFunction,
667 TNodeHashFunction> >
668 visited;
669 std::vector<std::pair<TNode, TNode> > visit;
670 std::pair<TNode, TNode> cur;
671 TNode cur1;
672 TNode cur2;
673 visit.push_back(std::pair<TNode, TNode>(n1, n2));
674 do
675 {
676 cur = visit.back();
677 visit.pop_back();
678 if (visited.find(cur) == visited.end())
679 {
680 visited.insert(cur);
681 cur1 = cur.first;
682 cur2 = cur.second;
683 Assert(cur1 != cur2);
684 // recurse if they have the same operator
685 if (cur1.hasOperator() && cur2.hasOperator()
686 && cur1.getNumChildren() == cur2.getNumChildren()
687 && cur1.getOperator() == cur2.getOperator()
688 && cur1.getOperator().getKind()!=INST_CONSTANT)
689 {
690 visit.push_back(std::pair<TNode, TNode>(cur1, cur2));
691 for (unsigned i = 0, size = cur1.getNumChildren(); i < size; i++)
692 {
693 if (cur1[i] != cur2[i])
694 {
695 visit.push_back(std::pair<TNode, TNode>(cur1[i], cur2[i]));
696 }
697 else if (cur1[i].getKind() == INST_CONSTANT)
698 {
699 if (subs_vars.find(cur1[i]) != subs_vars.end())
700 {
701 return 0;
702 }
703 // the variable must map to itself in the substitution
704 subs_vars.insert(cur1[i]);
705 }
706 }
707 }
708 else
709 {
710 bool success = false;
711 // check if we are in a unifiable instance case
712 // must be only this case
713 for (unsigned r = 0; r < 2; r++)
714 {
715 if (status == 0 || ((status == 1) == (r == 0)))
716 {
717 TNode curi = r == 0 ? cur1 : cur2;
718 if (curi.getKind() == INST_CONSTANT
719 && subs_vars.find(curi) == subs_vars.end())
720 {
721 TNode curj = r == 0 ? cur2 : cur1;
722 // RHS must be a simple trigger
723 if (getTriggerWeight(curj) == 0)
724 {
725 // must occur in the free variables in the other
726 std::vector<Node>& free_vars = r == 0 ? fv2 : fv1;
727 if (std::find(free_vars.begin(), free_vars.end(), curi)
728 != free_vars.end())
729 {
730 status = r == 0 ? 1 : -1;
731 subs_vars.insert(curi);
732 success = true;
733 break;
734 }
735 }
736 }
737 }
738 }
739 if (!success)
740 {
741 return 0;
742 }
743 }
744 }
745 } while (!visit.empty());
746 return status;
747 }
748
filterTriggerInstances(std::vector<Node> & nodes)749 void Trigger::filterTriggerInstances(std::vector<Node>& nodes)
750 {
751 std::map<unsigned, std::vector<Node> > fvs;
752 for (unsigned i = 0, size = nodes.size(); i < size; i++)
753 {
754 quantifiers::TermUtil::computeInstConstContains(nodes[i], fvs[i]);
755 }
756 std::vector<bool> active;
757 active.resize(nodes.size(), true);
758 for (unsigned i = 0, size = nodes.size(); i < size; i++)
759 {
760 std::vector<Node>& fvsi = fvs[i];
761 if (active[i])
762 {
763 for (unsigned j = i + 1, size2 = nodes.size(); j < size2; j++)
764 {
765 if (active[j])
766 {
767 int result = isTriggerInstanceOf(nodes[i], nodes[j], fvsi, fvs[j]);
768 if (result == 1)
769 {
770 Trace("filter-instances") << nodes[j] << " is an instance of "
771 << nodes[i] << std::endl;
772 active[i] = false;
773 break;
774 }
775 else if (result == -1)
776 {
777 Trace("filter-instances") << nodes[i] << " is an instance of "
778 << nodes[j] << std::endl;
779 active[j] = false;
780 }
781 }
782 }
783 }
784 }
785 std::vector<Node> temp;
786 for (unsigned i = 0; i < nodes.size(); i++)
787 {
788 if (active[i])
789 {
790 temp.push_back(nodes[i]);
791 }
792 }
793 nodes.clear();
794 nodes.insert(nodes.begin(), temp.begin(), temp.end());
795 }
796
getInversionVariable(Node n)797 Node Trigger::getInversionVariable( Node n ) {
798 if( n.getKind()==INST_CONSTANT ){
799 return n;
800 }else if( n.getKind()==PLUS || n.getKind()==MULT ){
801 Node ret;
802 for( unsigned i=0; i<n.getNumChildren(); i++ ){
803 if( quantifiers::TermUtil::hasInstConstAttr(n[i]) ){
804 if( ret.isNull() ){
805 ret = getInversionVariable( n[i] );
806 if( ret.isNull() ){
807 Trace("var-trigger-debug") << "No : multiple variables " << n << std::endl;
808 return Node::null();
809 }
810 }else{
811 return Node::null();
812 }
813 }else if( n.getKind()==MULT ){
814 if( !n[i].isConst() ){
815 Trace("var-trigger-debug") << "No : non-linear coefficient " << n << std::endl;
816 return Node::null();
817 }
818 /*
819 else if( n.getType().isInteger() ){
820 Rational r = n[i].getConst<Rational>();
821 if( r!=Rational(-1) && r!=Rational(1) ){
822 Trace("var-trigger-debug") << "No : not integer coefficient " << n << std::endl;
823 return Node::null();
824 }
825 }
826 */
827 }
828 }
829 return ret;
830 }else{
831 Trace("var-trigger-debug") << "No : unsupported operator " << n << "." << std::endl;
832 }
833 return Node::null();
834 }
835
getInversion(Node n,Node x)836 Node Trigger::getInversion( Node n, Node x ) {
837 if( n.getKind()==INST_CONSTANT ){
838 return x;
839 }else if( n.getKind()==PLUS || n.getKind()==MULT ){
840 int cindex = -1;
841 bool cindexSet = false;
842 for( unsigned i=0; i<n.getNumChildren(); i++ ){
843 if( !quantifiers::TermUtil::hasInstConstAttr(n[i]) ){
844 if( n.getKind()==PLUS ){
845 x = NodeManager::currentNM()->mkNode( MINUS, x, n[i] );
846 }else if( n.getKind()==MULT ){
847 Assert( n[i].isConst() );
848 if( x.getType().isInteger() ){
849 Node coeff = NodeManager::currentNM()->mkConst( n[i].getConst<Rational>().abs() );
850 if( !n[i].getConst<Rational>().abs().isOne() ){
851 x = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, x, coeff );
852 }
853 if( n[i].getConst<Rational>().sgn()<0 ){
854 x = NodeManager::currentNM()->mkNode( UMINUS, x );
855 }
856 }else{
857 Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / n[i].getConst<Rational>() );
858 x = NodeManager::currentNM()->mkNode( MULT, x, coeff );
859 }
860 }
861 x = Rewriter::rewrite( x );
862 }else{
863 Assert(!cindexSet);
864 cindex = i;
865 cindexSet = true;
866 }
867 }
868 if (cindexSet)
869 {
870 return getInversion(n[cindex], x);
871 }
872 }
873 return Node::null();
874 }
875
getTriggerVariables(Node n,Node q,std::vector<Node> & t_vars)876 void Trigger::getTriggerVariables(Node n, Node q, std::vector<Node>& t_vars)
877 {
878 std::vector< Node > patTerms;
879 std::map< Node, TriggerTermInfo > tinfo;
880 // collect all patterns from n
881 std::vector< Node > exclude;
882 collectPatTerms(q, n, patTerms, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo);
883 //collect all variables from all patterns in patTerms, add to t_vars
884 for (const Node& pat : patTerms)
885 {
886 quantifiers::TermUtil::computeInstConstContainsForQuant(q, pat, t_vars);
887 }
888 }
889
getActiveScore()890 int Trigger::getActiveScore() {
891 return d_mg->getActiveScore( d_quantEngine );
892 }
893
TriggerTrie()894 TriggerTrie::TriggerTrie()
895 {}
896
~TriggerTrie()897 TriggerTrie::~TriggerTrie() {
898 for(std::map< TNode, TriggerTrie* >::iterator i = d_children.begin(), iend = d_children.end();
899 i != iend; ++i) {
900 TriggerTrie* current = (*i).second;
901 delete current;
902 }
903 d_children.clear();
904
905 for( unsigned i=0; i<d_tr.size(); i++ ){
906 delete d_tr[i];
907 }
908 }
909
getTrigger(std::vector<Node> & nodes)910 inst::Trigger* TriggerTrie::getTrigger(std::vector<Node>& nodes)
911 {
912 std::vector<Node> temp;
913 temp.insert(temp.begin(), nodes.begin(), nodes.end());
914 std::sort(temp.begin(), temp.end());
915 TriggerTrie* tt = this;
916 for (const Node& n : temp)
917 {
918 std::map<TNode, TriggerTrie*>::iterator itt = tt->d_children.find(n);
919 if (itt == tt->d_children.end())
920 {
921 return NULL;
922 }
923 else
924 {
925 tt = itt->second;
926 }
927 }
928 return tt->d_tr.empty() ? NULL : tt->d_tr[0];
929 }
930
addTrigger(std::vector<Node> & nodes,inst::Trigger * t)931 void TriggerTrie::addTrigger(std::vector<Node>& nodes, inst::Trigger* t)
932 {
933 std::vector<Node> temp;
934 temp.insert(temp.begin(), nodes.begin(), nodes.end());
935 std::sort(temp.begin(), temp.end());
936 TriggerTrie* tt = this;
937 for (const Node& n : temp)
938 {
939 std::map<TNode, TriggerTrie*>::iterator itt = tt->d_children.find(n);
940 if (itt == tt->d_children.end())
941 {
942 TriggerTrie* ttn = new TriggerTrie;
943 tt->d_children[n] = ttn;
944 tt = ttn;
945 }
946 else
947 {
948 tt = itt->second;
949 }
950 }
951 tt->d_tr.push_back(t);
952 }
953
954 }/* CVC4::theory::inst namespace */
955 }/* CVC4::theory namespace */
956 }/* CVC4 namespace */
957