1 /********************* */
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-2017 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief Implementation of trigger class
15 #include "theory/quantifiers/trigger.h"
16 #include "theory/quantifiers/candidate_generator.h"
17 #include "theory/quantifiers/ho_trigger.h"
18 #include "theory/quantifiers/inst_match_generator.h"
19 #include "theory/quantifiers/term_database.h"
20 #include "theory/quantifiers/term_util.h"
21 #include "theory/quantifiers_engine.h"
22 #include "theory/theory_engine.h"
23 #include "theory/uf/equality_engine.h"
24 #include "util/hash.h"
27 using namespace CVC4::kind
;
28 using namespace CVC4::context
;
34 void TriggerTermInfo::init( Node q
, Node n
, int reqPol
, Node reqPolEq
){
36 quantifiers::TermUtil::getVarContainsNode( q
, n
, d_fv
);
40 d_reqPolEq
= reqPolEq
;
42 //determined a ground (dis)equality must hold or else q is a tautology?
46 /** trigger class constructor */
47 Trigger::Trigger( QuantifiersEngine
* qe
, Node f
, std::vector
< Node
>& nodes
)
48 : d_quantEngine( qe
), d_f( f
) {
49 d_nodes
.insert( d_nodes
.begin(), nodes
.begin(), nodes
.end() );
50 Trace("trigger") << "Trigger for " << f
<< ": " << std::endl
;
51 for( unsigned i
=0; i
<d_nodes
.size(); i
++ ){
52 Trace("trigger") << " " << d_nodes
[i
] << std::endl
;
54 if( d_nodes
.size()==1 ){
55 if( isSimpleTrigger( d_nodes
[0] ) ){
56 d_mg
= new InstMatchGeneratorSimple( f
, d_nodes
[0], qe
);
58 d_mg
= InstMatchGenerator::mkInstMatchGenerator( f
, d_nodes
[0], qe
);
61 if( options::multiTriggerCache() ){
62 d_mg
= new InstMatchGeneratorMulti( f
, d_nodes
, qe
);
64 d_mg
= InstMatchGenerator::mkInstMatchGeneratorMulti( f
, d_nodes
, qe
);
67 if( d_nodes
.size()==1 ){
68 if( isSimpleTrigger( d_nodes
[0] ) ){
69 ++(qe
->d_statistics
.d_triggers
);
71 ++(qe
->d_statistics
.d_simple_triggers
);
74 Trace("multi-trigger") << "Trigger for " << f
<< ": " << std::endl
;
75 for( unsigned i
=0; i
<d_nodes
.size(); i
++ ){
76 Trace("multi-trigger") << " " << d_nodes
[i
] << std::endl
;
78 ++(qe
->d_statistics
.d_multi_triggers
);
81 //Notice() << "Trigger : " << (*this) << " for " << f << std::endl;
82 Trace("trigger-debug") << "Finished making trigger." << std::endl
;
89 void Trigger::resetInstantiationRound(){
90 d_mg
->resetInstantiationRound( d_quantEngine
);
93 void Trigger::reset( Node eqc
){
94 d_mg
->reset( eqc
, d_quantEngine
);
97 Node
Trigger::getInstPattern(){
98 return NodeManager::currentNM()->mkNode( INST_PATTERN
, d_nodes
);
101 int Trigger::addInstantiations(InstMatch
& baseMatch
)
104 d_mg
->addInstantiations(d_f
, baseMatch
, d_quantEngine
, this);
106 if (Debug
.isOn("inst-trigger"))
108 Debug("inst-trigger") << "Added " << addedLemmas
109 << " lemmas, trigger was ";
110 for (unsigned i
= 0; i
< d_nodes
.size(); i
++)
112 Debug("inst-trigger") << d_nodes
[i
] << " ";
114 Debug("inst-trigger") << std::endl
;
120 bool Trigger::sendInstantiation(InstMatch
& m
)
122 return d_quantEngine
->addInstantiation(d_f
, m
);
125 bool Trigger::mkTriggerTerms( Node q
, std::vector
< Node
>& nodes
, unsigned n_vars
, std::vector
< Node
>& trNodes
) {
126 //only take nodes that contribute variables to the trigger when added
127 std::vector
< Node
> temp
;
128 temp
.insert( temp
.begin(), nodes
.begin(), nodes
.end() );
129 std::map
< Node
, bool > vars
;
130 std::map
< Node
, std::vector
< Node
> > patterns
;
132 std::map
< Node
, std::vector
< Node
> > varContains
;
133 quantifiers::TermUtil::getVarContains( q
, temp
, varContains
);
134 for( unsigned i
=0; i
<temp
.size(); i
++ ){
135 bool foundVar
= false;
136 for( unsigned j
=0; j
<varContains
[ temp
[i
] ].size(); j
++ ){
137 Node v
= varContains
[ temp
[i
] ][j
];
138 Assert( quantifiers::TermUtil::getInstConstAttr(v
)==q
);
139 if( vars
.find( v
)==vars
.end() ){
146 trNodes
.push_back( temp
[i
] );
147 for( unsigned j
=0; j
<varContains
[ temp
[i
] ].size(); j
++ ){
148 Node v
= varContains
[ temp
[i
] ][j
];
149 patterns
[ v
].push_back( temp
[i
] );
152 if( varCount
==n_vars
){
156 if( varCount
<n_vars
){
157 Trace("trigger-debug") << "Don't consider trigger since it does not contain specified number of variables." << std::endl
;
158 for( unsigned i
=0; i
<nodes
.size(); i
++) {
159 Trace("trigger-debug") << nodes
[i
] << " ";
161 Trace("trigger-debug") << std::endl
;
163 //do not generate multi-trigger if it does not contain all variables
166 //now, minimize the trigger
167 for( unsigned i
=0; i
<trNodes
.size(); i
++ ){
168 bool keepPattern
= false;
170 for( unsigned j
=0; j
<varContains
[ n
].size(); j
++ ){
171 Node v
= varContains
[ n
][j
];
172 if( patterns
[v
].size()==1 ){
178 //remove from pattern vector
179 for( unsigned j
=0; j
<varContains
[ n
].size(); j
++ ){
180 Node v
= varContains
[ n
][j
];
181 for( unsigned k
=0; k
<patterns
[v
].size(); k
++ ){
182 if( patterns
[v
][k
]==n
){
183 patterns
[v
].erase( patterns
[v
].begin() + k
, patterns
[v
].begin() + k
+ 1 );
188 //remove from trigger nodes
189 trNodes
.erase( trNodes
.begin() + i
, trNodes
.begin() + i
+ 1 );
197 Trigger
* Trigger::mkTrigger( QuantifiersEngine
* qe
, Node f
, std::vector
< Node
>& nodes
, bool keepAll
, int trOption
, unsigned use_n_vars
){
198 std::vector
< Node
> trNodes
;
200 unsigned n_vars
= use_n_vars
==0 ? f
[0].getNumChildren() : use_n_vars
;
201 if( !mkTriggerTerms( f
, nodes
, n_vars
, trNodes
) ){
205 trNodes
.insert( trNodes
.begin(), nodes
.begin(), nodes
.end() );
208 //check for duplicate?
209 if( trOption
!=TR_MAKE_NEW
){
210 Trigger
* t
= qe
->getTriggerDatabase()->getTrigger( trNodes
);
212 if( trOption
==TR_GET_OLD
){
213 //just return old trigger
221 // check if higher-order
222 Trace("trigger") << "Collect higher-order variable triggers..." << std::endl
;
223 std::map
<Node
, std::vector
<Node
> > ho_apps
;
224 HigherOrderTrigger::collectHoVarApplyTerms(f
, trNodes
, ho_apps
);
226 if (!ho_apps
.empty())
228 t
= new HigherOrderTrigger(qe
, f
, trNodes
, ho_apps
);
232 t
= new Trigger(qe
, f
, trNodes
);
235 qe
->getTriggerDatabase()->addTrigger( trNodes
, t
);
239 Trigger
* Trigger::mkTrigger( QuantifiersEngine
* qe
, Node f
, Node n
, bool keepAll
, int trOption
, unsigned use_n_vars
){
240 std::vector
< Node
> nodes
;
241 nodes
.push_back( n
);
242 return mkTrigger( qe
, f
, nodes
, keepAll
, trOption
, use_n_vars
);
245 bool Trigger::isUsable( Node n
, Node q
){
246 if( quantifiers::TermUtil::getInstConstAttr(n
)==q
){
247 if( isAtomicTrigger( n
) ){
248 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
249 if( !isUsable( n
[i
], q
) ){
254 }else if( n
.getKind()==INST_CONSTANT
){
257 std::map
< Node
, Node
> coeffs
;
258 if( isBooleanTermTrigger( n
) ){
260 }else if( options::purifyTriggers() ){
261 Node x
= getInversionVariable( n
);
273 Node
Trigger::getIsUsableEq( Node q
, Node n
) {
274 Assert( isRelationalTrigger( n
) );
275 for( unsigned i
=0; i
<2; i
++) {
276 if( isUsableEqTerms( q
, n
[i
], n
[1-i
] ) ){
277 if( i
==1 && n
.getKind()==EQUAL
&& !quantifiers::TermUtil::hasInstConstAttr(n
[0]) ){
278 return NodeManager::currentNM()->mkNode( n
.getKind(), n
[1], n
[0] );
287 bool Trigger::isUsableEqTerms( Node q
, Node n1
, Node n2
) {
288 if( n1
.getKind()==INST_CONSTANT
){
289 if( options::relationalTriggers() ){
290 if( !quantifiers::TermUtil::hasInstConstAttr(n2
) ){
292 }else if( n2
.getKind()==INST_CONSTANT
){
296 }else if( isUsableAtomicTrigger( n1
, q
) ){
297 if( options::relationalTriggers() && n2
.getKind()==INST_CONSTANT
&& !quantifiers::TermUtil::containsTerm( n1
, n2
) ){
299 }else if( !quantifiers::TermUtil::hasInstConstAttr(n2
) ){
306 Node
Trigger::getIsUsableTrigger( Node n
, Node q
) {
308 Trace("trigger-debug") << "Is " << n
<< " a usable trigger?" << std::endl
;
309 if( n
.getKind()==NOT
){
313 if( n
.getKind()==INST_CONSTANT
){
314 return pol
? n
: NodeManager::currentNM()->mkNode( EQUAL
, n
, NodeManager::currentNM()->mkConst( true ) ).notNode();
315 }else if( isRelationalTrigger( n
) ){
316 Node rtr
= getIsUsableEq( q
, n
);
317 if( rtr
.isNull() && n
[0].getType().isReal() ){
318 //try to solve relation
319 std::map
< Node
, Node
> m
;
320 if( QuantArith::getMonomialSumLit(n
, m
) ){
321 for( std::map
< Node
, Node
>::iterator it
= m
.begin(); it
!=m
.end(); ++it
){
322 bool trySolve
= false;
323 if( !it
->first
.isNull() ){
324 if( it
->first
.getKind()==INST_CONSTANT
){
325 trySolve
= options::relationalTriggers();
326 }else if( isUsableTrigger( it
->first
, q
) ){
331 Trace("trigger-debug") << "Try to solve for " << it
->first
<< std::endl
;
333 if( QuantArith::isolate( it
->first
, m
, veq
, n
.getKind() )!=0 ){
334 rtr
= getIsUsableEq( q
, veq
);
336 //either all solves will succeed or all solves will fail
343 Trace("relational-trigger") << "Relational trigger : " << std::endl
;
344 Trace("relational-trigger") << " " << rtr
<< " (from " << n
<< ")" << std::endl
;
345 Trace("relational-trigger") << " in quantifier " << q
<< std::endl
;
346 Node rtr2
= pol
? rtr
: rtr
.negate();
347 Trace("relational-trigger") << " return : " << rtr2
<< std::endl
;
351 Trace("trigger-debug") << n
<< " usable : " << ( quantifiers::TermUtil::getInstConstAttr(n
)==q
) << " " << isAtomicTrigger( n
) << " " << isUsable( n
, q
) << std::endl
;
352 if( isUsableAtomicTrigger( n
, q
) ){
353 return pol
? n
: NodeManager::currentNM()->mkNode( EQUAL
, n
, NodeManager::currentNM()->mkConst( true ) ).notNode();
359 bool Trigger::isUsableAtomicTrigger( Node n
, Node q
) {
360 return quantifiers::TermUtil::getInstConstAttr( n
)==q
&& isAtomicTrigger( n
) && isUsable( n
, q
);
363 bool Trigger::isUsableTrigger( Node n
, Node q
){
364 Node nu
= getIsUsableTrigger( n
, q
);
368 bool Trigger::isAtomicTrigger( Node n
){
369 return isAtomicTriggerKind( n
.getKind() );
372 bool Trigger::isAtomicTriggerKind( Kind k
) {
373 return k
== APPLY_UF
|| k
== SELECT
|| k
== STORE
|| k
== APPLY_CONSTRUCTOR
374 || k
== APPLY_SELECTOR_TOTAL
|| k
== APPLY_TESTER
|| k
== UNION
375 || k
== INTERSECTION
|| k
== SUBSET
|| k
== SETMINUS
|| k
== MEMBER
376 || k
== SINGLETON
|| k
== SEP_PTO
|| k
== BITVECTOR_TO_NAT
377 || k
== INT_TO_BITVECTOR
|| k
== HO_APPLY
;
380 bool Trigger::isRelationalTrigger( Node n
) {
381 return isRelationalTriggerKind( n
.getKind() );
384 bool Trigger::isRelationalTriggerKind( Kind k
) {
385 return k
==EQUAL
|| k
==GEQ
;
388 bool Trigger::isCbqiKind( Kind k
) {
389 if( quantifiers::TermUtil::isBoolConnective( k
) || k
==PLUS
|| k
==GEQ
|| k
==EQUAL
|| k
==MULT
){
392 //CBQI typically works for satisfaction-complete theories
393 TheoryId t
= kindToTheoryId( k
);
394 return t
==THEORY_BV
|| t
==THEORY_DATATYPES
;
398 bool Trigger::isSimpleTrigger( Node n
){
399 Node t
= n
.getKind()==NOT
? n
[0] : n
;
400 if( t
.getKind()==EQUAL
){
401 if( !quantifiers::TermUtil::hasInstConstAttr( t
[1] ) ){
405 if( isAtomicTrigger( t
) ){
406 for( unsigned i
=0; i
<t
.getNumChildren(); i
++ ){
407 if( t
[i
].getKind()!=INST_CONSTANT
&& quantifiers::TermUtil::hasInstConstAttr(t
[i
]) ){
411 if( options::purifyDtTriggers() && t
.getKind()==APPLY_SELECTOR_TOTAL
){
414 if (t
.getKind() == HO_APPLY
&& t
[0].getKind() == INST_CONSTANT
)
424 //store triggers in reqPol, indicating their polarity (if any) they must appear to falsify the quantified formula
425 void Trigger::collectPatTerms2( Node q
, Node n
, std::map
< Node
, std::vector
< Node
> >& visited
, std::map
< Node
, TriggerTermInfo
>& tinfo
,
426 quantifiers::TriggerSelMode tstrt
, std::vector
< Node
>& exclude
, std::vector
< Node
>& added
,
427 bool pol
, bool hasPol
, bool epol
, bool hasEPol
, bool knowIsUsable
){
428 std::map
< Node
, std::vector
< Node
> >::iterator itv
= visited
.find( n
);
429 if( itv
==visited
.end() ){
430 visited
[ n
].clear();
431 Trace("auto-gen-trigger-debug2") << "Collect pat terms " << n
<< " " << pol
<< " " << hasPol
<< " " << epol
<< " " << hasEPol
<< std::endl
;
432 if( n
.getKind()!=FORALL
&& n
.getKind()!=INST_CONSTANT
){
434 bool nu_single
= false;
437 }else if( n
.getKind()!=NOT
&& std::find( exclude
.begin(), exclude
.end(), n
)==exclude
.end() ){
438 nu
= getIsUsableTrigger( n
, q
);
439 if( !nu
.isNull() && nu
!=n
){
440 collectPatTerms2( q
, nu
, visited
, tinfo
, tstrt
, exclude
, added
, pol
, hasPol
, epol
, hasEPol
, true );
442 visited
[n
].insert( visited
[n
].end(), added
.begin(), added
.end() );
448 Assert( nu
.getKind()!=NOT
);
449 Trace("auto-gen-trigger-debug2") << "...found usable trigger : " << nu
<< std::endl
;
451 if( nu
.getKind()==EQUAL
){
452 if( isAtomicTrigger( nu
[0] ) && !quantifiers::TermUtil::hasInstConstAttr(nu
[1]) ){
459 Assert( reqEq
.isNull() || !quantifiers::TermUtil::hasInstConstAttr( reqEq
) );
460 Assert( isUsableTrigger( nu
, q
) );
461 //tinfo.find( nu )==tinfo.end()
462 Trace("auto-gen-trigger-debug2") << "...add usable trigger : " << nu
<< std::endl
;
463 tinfo
[ nu
].init( q
, nu
, hasEPol
? ( epol
? 1 : -1 ) : 0, reqEq
);
464 nu_single
= tinfo
[ nu
].d_fv
.size()==q
[0].getNumChildren();
466 Node nrec
= nu
.isNull() ? n
: nu
;
467 std::vector
< Node
> added2
;
468 for( unsigned i
=0; i
<nrec
.getNumChildren(); i
++ ){
469 bool newHasPol
, newPol
;
470 bool newHasEPol
, newEPol
;
471 QuantPhaseReq::getPolarity( nrec
, i
, hasPol
, pol
, newHasPol
, newPol
);
472 QuantPhaseReq::getEntailPolarity( nrec
, i
, hasEPol
, epol
, newHasEPol
, newEPol
);
473 collectPatTerms2( q
, nrec
[i
], visited
, tinfo
, tstrt
, exclude
, added2
, newPol
, newHasPol
, newEPol
, newHasEPol
);
475 // if this is not a usable trigger, don't worry about caching the results, since triggers do not contain non-usable subterms
478 for( unsigned i
=0; i
<added2
.size(); i
++ ){
479 Trace("auto-gen-trigger-debug2") << "..." << nu
<< " added child " << i
<< " : " << added2
[i
] << std::endl
;
480 Assert( added2
[i
]!=nu
);
481 // if child was not already removed
482 if( tinfo
.find( added2
[i
] )!=tinfo
.end() ){
483 if( tstrt
==quantifiers::TRIGGER_SEL_MAX
|| ( tstrt
==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX
&& !nu_single
) ){
484 //discard all subterms
485 Trace("auto-gen-trigger-debug2") << "......remove it." << std::endl
;
486 visited
[ added2
[i
] ].clear();
487 tinfo
.erase( added2
[i
] );
489 if( tinfo
[ nu
].d_fv
.size()==tinfo
[ added2
[i
] ].d_fv
.size() ){
490 //discard if we added a subterm as a trigger with all variables that nu has
491 Trace("auto-gen-trigger-debug2") << "......subsumes parent." << std::endl
;
494 if( std::find( added
.begin(), added
.end(), added2
[i
] )==added
.end() ){
495 added
.push_back( added2
[i
] );
500 if( rm_nu
&& ( tstrt
==quantifiers::TRIGGER_SEL_MIN
|| ( tstrt
==quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL
&& nu_single
) ) ){
503 if( std::find( added
.begin(), added
.end(), nu
)==added
.end() ){
504 added
.push_back( nu
);
507 visited
[n
].insert( visited
[n
].end(), added
.begin(), added
.end() );
511 for( unsigned i
=0; i
<itv
->second
.size(); ++i
){
512 Node t
= itv
->second
[i
];
513 if( std::find( added
.begin(), added
.end(), t
)==added
.end() ){
514 added
.push_back( t
);
520 bool Trigger::isBooleanTermTrigger( Node n
) {
521 if( n
.getKind()==ITE
){
522 //check for boolean term converted to ITE
523 if( n
[0].getKind()==INST_CONSTANT
&&
524 n
[1].getKind()==CONST_BITVECTOR
&&
525 n
[2].getKind()==CONST_BITVECTOR
){
526 if( ((BitVectorType
)n
[1].getType().toType()).getSize()==1 &&
527 n
[1].getConst
<BitVector
>().toInteger()==1 &&
528 n
[2].getConst
<BitVector
>().toInteger()==0 ){
536 bool Trigger::isPureTheoryTrigger( Node n
) {
537 if( n
.getKind()==APPLY_UF
|| n
.getKind()==VARIABLE
|| n
.getKind()==SKOLEM
){ //|| !quantifiers::TermUtil::hasInstConstAttr( n ) ){
540 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
541 if( !isPureTheoryTrigger( n
[i
] ) ){
549 int Trigger::getTriggerWeight( Node n
) {
550 if( isAtomicTrigger( n
) ){
553 if( options::relationalTriggers() ){
554 if( isRelationalTrigger( n
) ){
555 for( unsigned i
=0; i
<2; i
++ ){
556 if( n
[i
].getKind()==INST_CONSTANT
&& !quantifiers::TermUtil::hasInstConstAttr( n
[1-i
] ) ){
566 bool Trigger::isLocalTheoryExt( Node n
, std::vector
< Node
>& vars
, std::vector
< Node
>& patTerms
) {
567 if( !n
.getType().isBoolean() && n
.getKind()==APPLY_UF
){
568 if( std::find( patTerms
.begin(), patTerms
.end(), n
)==patTerms
.end() ){
570 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
571 if( n
[i
].getKind()==INST_CONSTANT
){
573 if( std::find( vars
.begin(), vars
.end(), n
[i
] )==vars
.end() ){
574 vars
.push_back( n
[i
] );
576 //do not allow duplicate variables
580 //do not allow nested function applications
585 patTerms
.push_back( n
);
589 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
590 if( !isLocalTheoryExt( n
[i
], vars
, patTerms
) ){
598 void Trigger::collectPatTerms( Node q
, Node n
, std::vector
< Node
>& patTerms
, quantifiers::TriggerSelMode tstrt
, std::vector
< Node
>& exclude
,
599 std::map
< Node
, TriggerTermInfo
>& tinfo
, bool filterInst
){
600 std::map
< Node
, std::vector
< Node
> > visited
;
602 //immediately do not consider any term t for which another term is an instance of t
603 std::vector
< Node
> patTerms2
;
604 std::map
< Node
, TriggerTermInfo
> tinfo2
;
605 collectPatTerms( q
, n
, patTerms2
, quantifiers::TRIGGER_SEL_ALL
, exclude
, tinfo2
, false );
606 std::vector
< Node
> temp
;
607 temp
.insert( temp
.begin(), patTerms2
.begin(), patTerms2
.end() );
608 quantifiers::TermUtil::filterInstances( temp
);
609 if( temp
.size()!=patTerms2
.size() ){
610 Trace("trigger-filter-instance") << "Filtered an instance: " << std::endl
;
611 Trace("trigger-filter-instance") << "Old: ";
612 for( unsigned i
=0; i
<patTerms2
.size(); i
++ ){
613 Trace("trigger-filter-instance") << patTerms2
[i
] << " ";
615 Trace("trigger-filter-instance") << std::endl
<< "New: ";
616 for( unsigned i
=0; i
<temp
.size(); i
++ ){
617 Trace("trigger-filter-instance") << temp
[i
] << " ";
619 Trace("trigger-filter-instance") << std::endl
;
621 if( tstrt
==quantifiers::TRIGGER_SEL_ALL
){
622 for( unsigned i
=0; i
<temp
.size(); i
++ ){
624 tinfo
[temp
[i
]].d_fv
.insert( tinfo
[temp
[i
]].d_fv
.end(), tinfo2
[temp
[i
]].d_fv
.begin(), tinfo2
[temp
[i
]].d_fv
.end() );
625 tinfo
[temp
[i
]].d_reqPol
= tinfo2
[temp
[i
]].d_reqPol
;
626 tinfo
[temp
[i
]].d_reqPolEq
= tinfo2
[temp
[i
]].d_reqPolEq
;
627 patTerms
.push_back( temp
[i
] );
631 //do not consider terms that have instances
632 for( unsigned i
=0; i
<patTerms2
.size(); i
++ ){
633 if( std::find( temp
.begin(), temp
.end(), patTerms2
[i
] )==temp
.end() ){
634 visited
[ patTerms2
[i
] ].clear();
639 std::vector
< Node
> added
;
640 collectPatTerms2( q
, n
, visited
, tinfo
, tstrt
, exclude
, added
, true, true, false, true );
641 for( std::map
< Node
, TriggerTermInfo
>::iterator it
= tinfo
.begin(); it
!= tinfo
.end(); ++it
){
642 patTerms
.push_back( it
->first
);
646 Node
Trigger::getInversionVariable( Node n
) {
647 if( n
.getKind()==INST_CONSTANT
){
649 }else if( n
.getKind()==PLUS
|| n
.getKind()==MULT
){
651 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
652 if( quantifiers::TermUtil::hasInstConstAttr(n
[i
]) ){
654 ret
= getInversionVariable( n
[i
] );
656 Trace("var-trigger-debug") << "No : multiple variables " << n
<< std::endl
;
662 }else if( n
.getKind()==MULT
){
663 if( !n
[i
].isConst() ){
664 Trace("var-trigger-debug") << "No : non-linear coefficient " << n
<< std::endl
;
668 else if( n.getType().isInteger() ){
669 Rational r = n[i].getConst<Rational>();
670 if( r!=Rational(-1) && r!=Rational(1) ){
671 Trace("var-trigger-debug") << "No : not integer coefficient " << n << std::endl;
680 Trace("var-trigger-debug") << "No : unsupported operator " << n
<< "." << std::endl
;
685 Node
Trigger::getInversion( Node n
, Node x
) {
686 if( n
.getKind()==INST_CONSTANT
){
688 }else if( n
.getKind()==PLUS
|| n
.getKind()==MULT
){
690 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
691 if( !quantifiers::TermUtil::hasInstConstAttr(n
[i
]) ){
692 if( n
.getKind()==PLUS
){
693 x
= NodeManager::currentNM()->mkNode( MINUS
, x
, n
[i
] );
694 }else if( n
.getKind()==MULT
){
695 Assert( n
[i
].isConst() );
696 if( x
.getType().isInteger() ){
697 Node coeff
= NodeManager::currentNM()->mkConst( n
[i
].getConst
<Rational
>().abs() );
698 if( !n
[i
].getConst
<Rational
>().abs().isOne() ){
699 x
= NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL
, x
, coeff
);
701 if( n
[i
].getConst
<Rational
>().sgn()<0 ){
702 x
= NodeManager::currentNM()->mkNode( UMINUS
, x
);
705 Node coeff
= NodeManager::currentNM()->mkConst( Rational(1) / n
[i
].getConst
<Rational
>() );
706 x
= NodeManager::currentNM()->mkNode( MULT
, x
, coeff
);
709 x
= Rewriter::rewrite( x
);
711 Assert( cindex
==-1 );
715 Assert( cindex
!=-1 );
716 return getInversion( n
[cindex
], x
);
721 void Trigger::getTriggerVariables(Node n
, Node q
, std::vector
<Node
>& t_vars
)
723 std::vector
< Node
> patTerms
;
724 std::map
< Node
, TriggerTermInfo
> tinfo
;
725 // collect all patterns from n
726 std::vector
< Node
> exclude
;
727 collectPatTerms(q
, n
, patTerms
, quantifiers::TRIGGER_SEL_ALL
, exclude
, tinfo
);
728 //collect all variables from all patterns in patTerms, add to t_vars
729 for( unsigned i
=0; i
<patTerms
.size(); i
++ ){
730 quantifiers::TermUtil::getVarContainsNode( q
, patTerms
[i
], t_vars
);
734 int Trigger::getActiveScore() {
735 return d_mg
->getActiveScore( d_quantEngine
);
738 TriggerTrie::TriggerTrie()
741 TriggerTrie::~TriggerTrie() {
742 for(std::map
< TNode
, TriggerTrie
* >::iterator i
= d_children
.begin(), iend
= d_children
.end();
744 TriggerTrie
* current
= (*i
).second
;
749 for( unsigned i
=0; i
<d_tr
.size(); i
++ ){
754 inst::Trigger
* TriggerTrie::getTrigger(std::vector
<Node
>& nodes
)
756 std::vector
<Node
> temp
;
757 temp
.insert(temp
.begin(), nodes
.begin(), nodes
.end());
758 std::sort(temp
.begin(), temp
.end());
759 TriggerTrie
* tt
= this;
760 for (const Node
& n
: temp
)
762 std::map
<TNode
, TriggerTrie
*>::iterator itt
= tt
->d_children
.find(n
);
763 if (itt
== tt
->d_children
.end())
772 return tt
->d_tr
.empty() ? NULL
: tt
->d_tr
[0];
775 void TriggerTrie::addTrigger(std::vector
<Node
>& nodes
, inst::Trigger
* t
)
777 std::vector
<Node
> temp
;
778 temp
.insert(temp
.begin(), nodes
.begin(), nodes
.end());
779 std::sort(temp
.begin(), temp
.end());
780 TriggerTrie
* tt
= this;
781 for (const Node
& n
: temp
)
783 std::map
<TNode
, TriggerTrie
*>::iterator itt
= tt
->d_children
.find(n
);
784 if (itt
== tt
->d_children
.end())
786 TriggerTrie
* ttn
= new TriggerTrie
;
787 tt
->d_children
[n
] = ttn
;
795 tt
->d_tr
.push_back(t
);
798 }/* CVC4::theory::inst namespace */
799 }/* CVC4::theory namespace */
800 }/* CVC4 namespace */