1 /********************* */
2 /*! \file rr_inst_match.cpp
4 ** Original author: ajreynol
5 ** Major contributors: bobot
6 ** Minor contributors (to current version): mdeters
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief Implementation of inst match class
17 #include "theory/inst_match.h"
18 #include "theory/theory_engine.h"
19 #include "theory/quantifiers_engine.h"
20 #include "theory/uf/theory_uf_instantiator.h"
21 #include "theory/uf/equality_engine.h"
22 #include "theory/arrays/theory_arrays.h"
23 #include "theory/datatypes/theory_datatypes.h"
24 #include "theory/rr_inst_match.h"
25 #include "theory/rr_trigger.h"
26 #include "theory/rr_inst_match_impl.h"
27 #include "theory/rr_candidate_generator.h"
30 using namespace CVC4::kind
;
31 using namespace CVC4::context
;
32 using namespace CVC4::theory
;
33 using namespace CVC4::theory::rrinst
;
34 using namespace CVC4::theory::uf::rrinst
;
35 using namespace CVC4::theory::eq::rrinst
;
41 typedef CVC4::theory::inst::InstMatch InstMatch
;
42 typedef CVC4::theory::inst::CandidateGeneratorQueue CandidateGeneratorQueue
;
45 class InstMatchTrie2Pairs
47 typename
std::vector
< std::vector
< typename InstMatchTrie2Gen
<modEq
>::Tree
> > d_data
;
48 InstMatchTrie2Gen
<modEq
> d_backtrack
;
50 InstMatchTrie2Pairs(context::Context
* c
, QuantifiersEngine
* q
, size_t n
):
52 // resize to a triangle
59 for(size_t i
=0; i
< n
; ++i
){
60 d_data
[i
].resize(i
+1,typename InstMatchTrie2Gen
<modEq
>::Tree(0));
63 InstMatchTrie2Pairs(const InstMatchTrie2Pairs
&) CVC4_UNDEFINED
;
64 const InstMatchTrie2Pairs
& operator =(const InstMatchTrie2Pairs
& e
) CVC4_UNDEFINED
;
65 /** add match m in the trie,
66 return true if it was never seen */
67 inline bool addInstMatch( size_t i
, size_t j
, InstMatch
& m
){
68 size_t k
= std::min(i
,j
);
69 size_t l
= std::max(i
,j
);
70 return d_backtrack
.addInstMatch(m
,&(d_data
[l
][k
]));
72 inline bool addInstMatch( size_t i
, InstMatch
& m
){
73 return d_backtrack
.addInstMatch(m
,&(d_data
[i
][i
]));
79 // Currently the implementation doesn't take into account that
80 // variable should have the same value given.
81 // TODO use the d_children way perhaps
82 // TODO replace by a real dictionnary
83 // We should create a real substitution? slower more precise
84 // We don't do that often
85 bool nonunifiable( TNode t0
, TNode pat
, const std::vector
<Node
> & vars
){
86 if(pat
.isNull()) return true;
88 typedef std::vector
<std::pair
<TNode
,TNode
> > tstack
;
89 tstack
stack(1,std::make_pair(t0
,pat
)); // t * pat
91 while(!stack
.empty()){
92 const std::pair
<TNode
,TNode
> p
= stack
.back(); stack
.pop_back();
93 const TNode
& t
= p
.first
;
94 const TNode
& pat
= p
.second
;
96 // t or pat is a variable currently we consider that can match anything
97 if( find(vars
.begin(),vars
.end(),t
) != vars
.end() ) continue;
98 if( pat
.getKind() == INST_CONSTANT
) continue;
100 // t and pat are nonunifiable
101 if( !Trigger::isAtomicTrigger( t
) || !Trigger::isAtomicTrigger( pat
) ) {
102 if(t
== pat
) continue;
105 if( t
.getOperator() != pat
.getOperator() ) return true;
107 //put the children on the stack
108 for( size_t i
=0; i
< pat
.getNumChildren(); i
++ ){
109 stack
.push_back(std::make_pair(t
[i
],pat
[i
]));
112 // The heuristic can't find non-unifiability
117 class DumbMatcher
: public Matcher
{
118 void resetInstantiationRound( QuantifiersEngine
* qe
){};
119 bool reset( TNode n
, InstMatch
& m
, QuantifiersEngine
* qe
){
122 bool getNextMatch( InstMatch
& m
, QuantifiersEngine
* qe
){
127 class DumbPatMatcher
: public PatMatcher
{
128 void resetInstantiationRound( QuantifiersEngine
* qe
){};
129 bool reset( InstMatch
& m
, QuantifiersEngine
* qe
){
132 bool getNextMatch( InstMatch
& m
, QuantifiersEngine
* qe
){
138 /* The order of the matching is:
139 reset arg1, nextMatch arg1, reset arg2, nextMatch arg2, ... */
140 ApplyMatcher::ApplyMatcher( Node pat
, QuantifiersEngine
* qe
): d_pattern(pat
){
141 // Assert( pat.hasAttribute(InstConstantAttribute()) );
143 //set-up d_variables, d_constants, d_childrens
144 for( size_t i
=0; i
< d_pattern
.getNumChildren(); ++i
){
145 EqualityQuery
* q
= qe
->getEqualityQuery(d_pattern
[i
].getType());
147 if( d_pattern
[i
].hasAttribute(InstConstantAttribute()) ){
148 if( d_pattern
[i
].getKind()==INST_CONSTANT
){
150 d_variables
.push_back(make_triple((TNode
)d_pattern
[i
],i
,q
));
152 //It's neither a constant argument neither a variable
153 //we create the matcher for the subpattern
154 d_childrens
.push_back(make_triple(mkMatcher((TNode
)d_pattern
[i
], qe
),i
,q
));
158 d_constants
.push_back(make_triple((TNode
)d_pattern
[i
],i
,q
));
163 void ApplyMatcher::resetInstantiationRound( QuantifiersEngine
* qe
){
164 for( size_t i
=0; i
< d_childrens
.size(); i
++ ){
165 d_childrens
[i
].first
->resetInstantiationRound( qe
);
169 bool ApplyMatcher::reset(TNode t
, InstMatch
& m
, QuantifiersEngine
* qe
){
170 Debug("matching") << "Matching " << t
<< " against pattern " << d_pattern
<< " ("
171 << m
.size() << ")" << std::endl
;
174 Assert( !t
.isNull() );
175 Assert( !t
.hasAttribute(InstConstantAttribute()) );
176 Assert( t
.getKind()==d_pattern
.getKind() );
177 Assert( (t
.getKind()!=APPLY_UF
&& t
.getKind()!=APPLY_CONSTRUCTOR
)
178 || t
.getOperator()==d_pattern
.getOperator() );
180 typedef std::vector
< triple
<TNode
,size_t,EqualityQuery
*> >::iterator iterator
;
181 for(iterator i
= d_constants
.begin(), end
= d_constants
.end();
183 if( !i
->third
->areEqual( i
->first
, t
[i
->second
] ) ){
184 Debug("matching-fail") << "Match fail arg: " << i
->first
<< " and " << t
[i
->second
] << std::endl
;
185 //setMatchFail( qe, d_pattern[i], t[i] );
186 //ground arguments are not equal
193 for(iterator i
= d_variables
.begin(), end
= d_variables
.end();
195 if( !m
.setMatch( i
->third
, i
->first
, t
[i
->second
], set
) ){
196 //match is in conflict
197 Debug("matching-debug") << "Match in conflict " << t
[i
->second
] << " and "
198 << i
->first
<< " because "
201 Debug("matching-fail") << "Match fail: " << m
.get(i
->first
) << " and " << t
[i
->second
] << std::endl
;
202 //setMatchFail( qe, partial[0].d_map[d_pattern[i]], t[i] );
203 m
.erase(d_binded
.begin(), d_binded
.end());
206 if(set
){ //The variable has just been set
207 d_binded
.push_back(i
->first
);
212 //now, fit children into match
213 //we will be requesting candidates for matching terms for each child
215 for( size_t i
=0; i
< d_childrens
.size(); i
++ ){
216 Debug("matching-debug") << "Take the representative of " << t
[ d_childrens
[i
].second
] << std::endl
;
217 Assert( d_childrens
[i
].third
->hasTerm(t
[ d_childrens
[i
].second
]) );
218 Node rep
= d_childrens
[i
].third
->getRepresentative( t
[ d_childrens
[i
].second
] );
219 d_reps
.push_back( rep
);
222 if(d_childrens
.size() == 0) return true;
223 else return getNextMatch(m
, qe
, true);
226 bool ApplyMatcher::getNextMatch(InstMatch
& m
, QuantifiersEngine
* qe
, bool reset
){
227 Assert(d_childrens
.size() > 0);
228 const size_t max
= d_childrens
.size() - 1;
229 size_t index
= reset
? 0 : max
;
230 Assert(d_childrens
.size() == d_reps
.size());
233 d_childrens
[index
].first
->reset( d_reps
[index
], m
, qe
) :
234 d_childrens
[index
].first
->getNextMatch( m
, qe
)){
235 if(index
==max
) return true;
240 m
.erase(d_binded
.begin(), d_binded
.end());
249 bool ApplyMatcher::getNextMatch(InstMatch
& m
, QuantifiersEngine
* qe
){
250 if(d_childrens
.size() == 0){
251 m
.erase(d_binded
.begin(), d_binded
.end());
253 } else return getNextMatch(m
, qe
, false);
256 /** Proxy that call the sub-matcher on the result return by the given candidate generator */
257 template <class CG
, class M
>
258 class CandidateGeneratorMatcher
: public Matcher
{
259 /** candidate generator */
261 /** the sub-matcher */
264 CandidateGeneratorMatcher(CG cg
, M m
): d_cg(cg
), d_m(m
)
265 {/* last is Null */};
266 void resetInstantiationRound( QuantifiersEngine
* qe
){
267 d_cg
.resetInstantiationRound();
268 d_m
.resetInstantiationRound(qe
);
270 bool reset( TNode n
, InstMatch
& m
, QuantifiersEngine
* qe
){
272 return findMatch(m
,qe
);
274 bool getNextMatch( InstMatch
& m
, QuantifiersEngine
* qe
){
275 // The sub-matcher has another match
276 return d_m
.getNextMatch(m
, qe
) || findMatch(m
,qe
);
279 bool findMatch( InstMatch
& m
, QuantifiersEngine
* qe
){
280 // Otherwise try to find a new candidate that has at least one match
282 TNode n
= d_cg
.getNextCandidate();//kept somewhere Term-db
283 Debug("matching") << "GenCand " << n
<< " (" << this << ")" << std::endl
;
284 if(n
.isNull()) return false;
285 if(d_m
.reset(n
,m
,qe
)) return true;
290 /** Proxy that call the sub-matcher on the result return by the given candidate generator */
292 class PatOfMatcher
: public PatMatcher
{
295 inline PatOfMatcher(M m
): d_m(m
){}
296 void resetInstantiationRound(QuantifiersEngine
* qe
){
297 d_m
.resetInstantiationRound(qe
);
299 bool reset(InstMatch
& m
, QuantifiersEngine
* qe
){
300 return d_m
.reset(Node::null(),m
,qe
);
302 bool getNextMatch(InstMatch
& m
, QuantifiersEngine
* qe
){
303 return d_m
.getNextMatch(m
,qe
);
307 class ArithMatcher
: public Matcher
{
309 /** for arithmetic matching */
310 std::map
< Node
, Node
> d_arith_coeffs
;
311 /** get the match against ground term or formula t.
312 d_match_mattern and t should have the same shape.
313 only valid for use where !d_match_pattern.isNull().
315 /** the variable that are set by this matcher */
316 std::vector
< TNode
> d_binded
; /* TNode because the variables are already in d_arith_coeffs */
317 Node d_pattern
; //for debugging
319 ArithMatcher(Node pat
, QuantifiersEngine
* qe
);
320 void resetInstantiationRound( QuantifiersEngine
* qe
){};
321 bool reset( TNode n
, InstMatch
& m
, QuantifiersEngine
* qe
);
322 bool getNextMatch( InstMatch
& m
, QuantifiersEngine
* qe
);
325 /** Match just a variable */
326 class VarMatcher
: public Matcher
{
328 bool d_binded
; /* True if the reset bind the variable to some value */
331 VarMatcher(Node var
, QuantifiersEngine
* qe
): d_var(var
), d_binded(false){
332 d_q
= qe
->getEqualityQuery(var
.getType());
334 void resetInstantiationRound( QuantifiersEngine
* qe
){};
335 bool reset( TNode n
, InstMatch
& m
, QuantifiersEngine
* qe
){
336 if(!m
.setMatch( d_q
, d_var
, n
, d_binded
)){
337 //match is in conflict
338 Debug("matching-fail") << "Match fail: " << m
.get(d_var
)
339 << " and " << n
<< std::endl
;
343 bool getNextMatch( InstMatch
& m
, QuantifiersEngine
* qe
){
344 //match is in conflict
345 if (d_binded
) m
.erase(d_var
);
350 template <class M
, class Test
>
351 class TestMatcher
: public Matcher
{
355 inline TestMatcher(M m
, Test test
): d_m(m
), d_test(test
){}
356 inline void resetInstantiationRound(QuantifiersEngine
* qe
){
357 d_m
.resetInstantiationRound(qe
);
359 inline bool reset(TNode n
, InstMatch
& m
, QuantifiersEngine
* qe
){
360 return d_test(n
) && d_m
.reset(n
, m
, qe
);
362 inline bool getNextMatch( InstMatch
& m
, QuantifiersEngine
* qe
){
363 return d_m
.getNextMatch(m
, qe
);
367 class LegalOpTest
/*: public unary_function<TNode,bool>*/ {
370 inline LegalOpTest(Node op
): d_op(op
){}
371 inline bool operator() (TNode n
) {
373 CandidateGenerator::isLegalCandidate(n
) &&
374 // ( // n.getKind()==SELECT || n.getKind()==STORE ||
375 // n.getKind()==APPLY_UF || n.getKind()==APPLY_CONSTRUCTOR) &&
377 n
.getOperator()==d_op
;
381 class LegalKindTest
/* : public unary_function<TNode,bool>*/ {
384 inline LegalKindTest(Kind kind
): d_kind(kind
){}
385 inline bool operator() (TNode n
) {
387 CandidateGenerator::isLegalCandidate(n
) &&
392 class LegalTypeTest
/* : public unary_function<TNode,bool>*/ {
395 inline LegalTypeTest(TypeNode type
): d_type(type
){}
396 inline bool operator() (TNode n
) {
398 CandidateGenerator::isLegalCandidate(n
) &&
403 class LegalTest
/* : public unary_function<TNode,bool>*/ {
405 inline bool operator() (TNode n
) {
406 return CandidateGenerator::isLegalCandidate(n
);
410 size_t numFreeVar(TNode t
){
412 for( size_t i
=0, size
=t
.getNumChildren(); i
< size
; ++i
){
413 if( t
[i
].hasAttribute(InstConstantAttribute()) ){
414 if( t
[i
].getKind()==INST_CONSTANT
){
418 //neither variable nor constant
419 n
+= numFreeVar(t
[i
]);
426 class OpMatcher
: public Matcher
{
428 typedef ApplyMatcher AuxMatcher3
;
429 typedef TestMatcher
< AuxMatcher3
, LegalOpTest
> AuxMatcher2
;
430 typedef CandidateGeneratorMatcher
< CandidateGeneratorTheoryEeClass
, AuxMatcher2
> AuxMatcher1
;
432 static inline AuxMatcher1
createCgm(Node pat
, QuantifiersEngine
* qe
){
433 Assert( pat
.getKind() == kind::APPLY_UF
);
434 /** In reverse order of matcher sequence */
435 AuxMatcher3
am3(pat
,qe
);
436 /** Keep only the one that have the good operator */
437 AuxMatcher2
am2(am3
,LegalOpTest(pat
.getOperator()));
438 /** Iter on the equivalence class of the given term */
439 uf::TheoryUF
* uf
= static_cast<uf::TheoryUF
*>(qe
->getTheoryEngine()->getTheory( theory::THEORY_UF
));
440 eq::EqualityEngine
* ee
= static_cast<eq::EqualityEngine
*>(uf
->getEqualityEngine());
441 CandidateGeneratorTheoryEeClass
cdtUfEq(ee
);
442 /* Create a matcher from the candidate generator */
443 AuxMatcher1
am1(cdtUfEq
,am2
);
449 OpMatcher( Node pat
, QuantifiersEngine
* qe
):
450 d_cgm(createCgm(pat
, qe
)),d_num_var(numFreeVar(pat
)),
453 void resetInstantiationRound( QuantifiersEngine
* qe
){
454 d_cgm
.resetInstantiationRound(qe
);
456 bool reset( TNode t
, InstMatch
& m
, QuantifiersEngine
* qe
){
457 // size_t m_size = m.d_map.size();
458 // if(m_size == d_num_var){
459 // uf::EqualityEngine<uf::TheoryUF::NotifyClass>* ee = (static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->getTheory( theory::THEORY_UF )))->getEqualityEngine();
461 // return ee->areEqual(m.subst(d_pat),t);
463 // std::cout << m.d_map.size() << std::endl;
464 return d_cgm
.reset(t
, m
, qe
);
467 bool getNextMatch( InstMatch
& m
, QuantifiersEngine
* qe
){
468 return d_cgm
.getNextMatch(m
, qe
);
472 class DatatypesMatcher
: public Matcher
{
474 typedef ApplyMatcher AuxMatcher3
;
475 typedef TestMatcher
< AuxMatcher3
, LegalOpTest
> AuxMatcher2
;
476 typedef CandidateGeneratorMatcher
< CandidateGeneratorTheoryEeClass
, AuxMatcher2
> AuxMatcher1
;
478 static inline AuxMatcher1
createCgm(Node pat
, QuantifiersEngine
* qe
){
479 Assert( pat
.getKind() == kind::APPLY_CONSTRUCTOR
,
480 "For datatypes only constructor are accepted in pattern" );
481 /** In reverse order of matcher sequence */
482 AuxMatcher3
am3(pat
,qe
);
483 /** Keep only the one that have the good operator */
484 AuxMatcher2
am2(am3
,LegalOpTest(pat
.getOperator()));
485 /** Iter on the equivalence class of the given term */
486 datatypes::TheoryDatatypes
* dt
= static_cast<datatypes::TheoryDatatypes
*>(qe
->getTheoryEngine()->getTheory( theory::THEORY_DATATYPES
));
487 eq::EqualityEngine
* ee
= static_cast<eq::EqualityEngine
*>(dt
->getEqualityEngine());
488 CandidateGeneratorTheoryEeClass
cdtDtEq(ee
);
489 /* Create a matcher from the candidate generator */
490 AuxMatcher1
am1(cdtDtEq
,am2
);
495 DatatypesMatcher( Node pat
, QuantifiersEngine
* qe
):
496 d_cgm(createCgm(pat
, qe
)),
499 void resetInstantiationRound( QuantifiersEngine
* qe
){
500 d_cgm
.resetInstantiationRound(qe
);
502 bool reset( TNode t
, InstMatch
& m
, QuantifiersEngine
* qe
){
503 Debug("matching") << "datatypes: " << t
<< " matches " << d_pat
<< std::endl
;
504 return d_cgm
.reset(t
, m
, qe
);
506 bool getNextMatch( InstMatch
& m
, QuantifiersEngine
* qe
){
507 return d_cgm
.getNextMatch(m
, qe
);
511 class ArrayMatcher
: public Matcher
{
513 typedef ApplyMatcher AuxMatcher3
;
514 typedef TestMatcher
< AuxMatcher3
, LegalKindTest
> AuxMatcher2
;
515 typedef CandidateGeneratorMatcher
< CandidateGeneratorTheoryEeClass
, AuxMatcher2
> AuxMatcher1
;
517 static inline AuxMatcher1
createCgm(Node pat
, QuantifiersEngine
* qe
){
518 Assert( pat
.getKind() == kind::SELECT
|| pat
.getKind() == kind::STORE
);
519 /** In reverse order of matcher sequence */
520 AuxMatcher3
am3(pat
,qe
);
521 /** Keep only the one that have the good operator */
522 AuxMatcher2
am2(am3
, LegalKindTest(pat
.getKind()));
523 /** Iter on the equivalence class of the given term */
524 arrays::TheoryArrays
* ar
= static_cast<arrays::TheoryArrays
*>(qe
->getTheoryEngine()->getTheory( theory::THEORY_ARRAY
));
525 eq::EqualityEngine
* ee
=
526 static_cast<eq::EqualityEngine
*>(ar
->getEqualityEngine());
527 CandidateGeneratorTheoryEeClass
cdtUfEq(ee
);
528 /* Create a matcher from the candidate generator */
529 AuxMatcher1
am1(cdtUfEq
,am2
);
535 ArrayMatcher( Node pat
, QuantifiersEngine
* qe
):
536 d_cgm(createCgm(pat
, qe
)),d_num_var(numFreeVar(pat
)),
539 void resetInstantiationRound( QuantifiersEngine
* qe
){
540 d_cgm
.resetInstantiationRound(qe
);
542 bool reset( TNode t
, InstMatch
& m
, QuantifiersEngine
* qe
){
543 // size_t m_size = m.d_map.size();
544 // if(m_size == d_num_var){
545 // uf::EqualityEngine<uf::TheoryUF::NotifyClass>* ee = (static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->getTheory( theory::THEORY_UF )))->getEqualityEngine();
547 // return ee->areEqual(m.subst(d_pat),t);
549 // std::cout << m.d_map.size() << std::endl;
550 return d_cgm
.reset(t
, m
, qe
);
553 bool getNextMatch( InstMatch
& m
, QuantifiersEngine
* qe
){
554 return d_cgm
.getNextMatch(m
, qe
);
558 class AllOpMatcher
: public PatMatcher
{
560 typedef ApplyMatcher AuxMatcher3
;
561 typedef TestMatcher
< AuxMatcher3
, LegalTest
> AuxMatcher2
;
562 typedef CandidateGeneratorMatcher
< CandidateGeneratorTheoryUfOp
, AuxMatcher2
> AuxMatcher1
;
564 static inline AuxMatcher1
createCgm(Node pat
, QuantifiersEngine
* qe
){
565 Assert( pat
.hasOperator() );
566 /** In reverse order of matcher sequence */
567 AuxMatcher3
am3(pat
,qe
);
568 /** Keep only the one that have the good operator */
569 AuxMatcher2
am2(am3
,LegalTest());
570 /** Iter on the equivalence class of the given term */
571 TermDb
* tdb
= qe
->getTermDatabase();
572 CandidateGeneratorTheoryUfOp
cdtUfEq(pat
.getOperator(),tdb
);
573 /* Create a matcher from the candidate generator */
574 AuxMatcher1
am1(cdtUfEq
,am2
);
580 AllOpMatcher( TNode pat
, QuantifiersEngine
* qe
):
581 d_cgm(createCgm(pat
, qe
)), d_num_var(numFreeVar(pat
)),
584 void resetInstantiationRound( QuantifiersEngine
* qe
){
585 d_cgm
.resetInstantiationRound(qe
);
587 bool reset( InstMatch
& m
, QuantifiersEngine
* qe
){
588 // std::cout << m.d_map.size() << "/" << d_num_var << std::endl;
589 return d_cgm
.reset(Node::null(), m
, qe
);
591 bool getNextMatch( InstMatch
& m
, QuantifiersEngine
* qe
){
592 return d_cgm
.getNextMatch(m
, qe
);
596 template <bool classes
> /** true classes | false class */
597 class GenericCandidateGeneratorClasses
: public CandidateGenerator
{
599 CandidateGenerator
* d_cg
;
600 QuantifiersEngine
* d_qe
;
603 void mkCandidateGenerator(){
605 d_cg
= d_qe
->getRRCanGenClasses();
607 d_cg
= d_qe
->getRRCanGenClass();
610 GenericCandidateGeneratorClasses(QuantifiersEngine
* qe
):
612 mkCandidateGenerator();
614 ~GenericCandidateGeneratorClasses(){
617 const GenericCandidateGeneratorClasses
& operator =(const GenericCandidateGeneratorClasses
& m
){
618 mkCandidateGenerator();
621 GenericCandidateGeneratorClasses(const GenericCandidateGeneratorClasses
& m
):
623 mkCandidateGenerator();
625 void resetInstantiationRound(){
626 d_cg
->resetInstantiationRound();
628 void reset( TNode eqc
){
629 Assert( !classes
|| eqc
.isNull() );
631 }; //* the argument is not used
632 TNode
getNextCandidate(){
633 return d_cg
->getNextCandidate();
635 }; /* MetaCandidateGeneratorClasses */
638 class GenericMatcher
: public Matcher
{
640 typedef ApplyMatcher AuxMatcher3
;
641 typedef TestMatcher
< AuxMatcher3
, LegalOpTest
> AuxMatcher2
;
642 typedef CandidateGeneratorMatcher
< GenericCandidateGeneratorClasses
<false>, AuxMatcher2
> AuxMatcher1
;
644 static inline AuxMatcher1
createCgm(Node pat
, QuantifiersEngine
* qe
){
645 /** In reverse order of matcher sequence */
646 AuxMatcher3
am3(pat
,qe
);
647 /** Keep only the one that have the good operator */
648 AuxMatcher2
am2(am3
,LegalOpTest(pat
.getOperator()));
649 /** Iter on the equivalence class of the given term */
650 GenericCandidateGeneratorClasses
<false> cdtG(qe
);
651 /* Create a matcher from the candidate generator */
652 AuxMatcher1
am1(cdtG
,am2
);
657 GenericMatcher( Node pat
, QuantifiersEngine
* qe
):
658 d_cgm(createCgm(pat
, qe
)),
661 void resetInstantiationRound( QuantifiersEngine
* qe
){
662 d_cgm
.resetInstantiationRound(qe
);
664 bool reset( TNode t
, InstMatch
& m
, QuantifiersEngine
* qe
){
665 return d_cgm
.reset(t
, m
, qe
);
667 bool getNextMatch( InstMatch
& m
, QuantifiersEngine
* qe
){
668 return d_cgm
.getNextMatch(m
, qe
);
673 class GenericPatMatcher
: public PatMatcher
{
675 typedef ApplyMatcher AuxMatcher3
;
676 typedef TestMatcher
< AuxMatcher3
, LegalOpTest
> AuxMatcher2
;
677 typedef CandidateGeneratorMatcher
< GenericCandidateGeneratorClasses
<true>, AuxMatcher2
> AuxMatcher1
;
679 static inline AuxMatcher1
createCgm(Node pat
, QuantifiersEngine
* qe
){
680 /** In reverse order of matcher sequence */
681 AuxMatcher3
am3(pat
,qe
);
682 /** Keep only the one that have the good operator */
683 AuxMatcher2
am2(am3
,LegalOpTest(pat
.getOperator()));
684 /** Iter on the equivalence class of the given term */
685 GenericCandidateGeneratorClasses
<true> cdtG(qe
);
686 /* Create a matcher from the candidate generator */
687 AuxMatcher1
am1(cdtG
,am2
);
692 GenericPatMatcher( Node pat
, QuantifiersEngine
* qe
):
693 d_cgm(createCgm(pat
, qe
)),
696 void resetInstantiationRound( QuantifiersEngine
* qe
){
697 d_cgm
.resetInstantiationRound(qe
);
699 bool reset( InstMatch
& m
, QuantifiersEngine
* qe
){
700 return d_cgm
.reset(Node::null(), m
, qe
);
702 bool getNextMatch( InstMatch
& m
, QuantifiersEngine
* qe
){
703 return d_cgm
.getNextMatch(m
, qe
);
707 class MetaCandidateGeneratorClasses
: public CandidateGenerator
{
709 CandidateGenerator
* d_cg
;
714 CandidateGenerator
* mkCandidateGenerator(TypeNode ty
, TheoryEngine
* te
){
715 Debug("inst-match-gen") << "MetaCandidateGenerator for type: " << ty
716 << " Theory : " << Theory::theoryOf(ty
) << std::endl
;
717 if( Theory::theoryOf(ty
) == theory::THEORY_DATATYPES
){
718 // datatypes::TheoryDatatypes* dt = static_cast<datatypes::TheoryDatatypes *>(te->getTheory( theory::THEORY_DATATYPES ));
719 // return new datatypes::rrinst::CandidateGeneratorTheoryClasses(dt);
720 Unimplemented("MetaCandidateGeneratorClasses for THEORY_DATATYPES");
721 }else if ( Theory::theoryOf(ty
) == theory::THEORY_ARRAY
){
722 arrays::TheoryArrays
* ar
= static_cast<arrays::TheoryArrays
*>(te
->getTheory( theory::THEORY_ARRAY
));
723 eq::EqualityEngine
* ee
=
724 static_cast<eq::EqualityEngine
*>(ar
->getEqualityEngine());
725 return new CandidateGeneratorTheoryEeClasses(ee
);
727 uf::TheoryUF
* uf
= static_cast<uf::TheoryUF
*>(te
->getTheory( theory::THEORY_UF
));
728 eq::EqualityEngine
* ee
=
729 static_cast<eq::EqualityEngine
*>(uf
->getEqualityEngine());
730 return new CandidateGeneratorTheoryEeClasses(ee
);
733 MetaCandidateGeneratorClasses(TypeNode ty
, TheoryEngine
* te
):
735 d_cg
= mkCandidateGenerator(ty
,te
);
737 ~MetaCandidateGeneratorClasses(){
740 const MetaCandidateGeneratorClasses
& operator =(const MetaCandidateGeneratorClasses
& m
){
741 d_cg
= mkCandidateGenerator(m
.d_ty
, m
.d_te
);
744 MetaCandidateGeneratorClasses(const MetaCandidateGeneratorClasses
& m
):
745 d_ty(m
.d_ty
), d_te(m
.d_te
){
746 d_cg
= mkCandidateGenerator(m
.d_ty
, m
.d_te
);
748 void resetInstantiationRound(){
749 d_cg
->resetInstantiationRound();
751 void reset( TNode eqc
){
753 }; //* the argument is not used
754 TNode
getNextCandidate(){
755 return d_cg
->getNextCandidate();
757 }; /* MetaCandidateGeneratorClasses */
759 /** Match just a variable */
760 class AllVarMatcher
: public PatMatcher
{
763 typedef VarMatcher AuxMatcher3
;
764 typedef TestMatcher
< AuxMatcher3
, LegalTypeTest
> AuxMatcher2
;
765 typedef CandidateGeneratorMatcher
< MetaCandidateGeneratorClasses
, AuxMatcher2
> AuxMatcher1
;
767 static inline AuxMatcher1
createCgm(TNode pat
, QuantifiersEngine
* qe
){
768 Assert( pat
.getKind()==INST_CONSTANT
);
769 TypeNode ty
= pat
.getType();
770 Debug("inst-match-gen") << "create AllVarMatcher for type: " << ty
<< std::endl
;
771 /** In reverse order of matcher sequence */
772 /** Distribute it to all the pattern */
773 AuxMatcher3
am3(pat
,qe
);
774 /** Keep only the one that have the good type */
775 AuxMatcher2
am2(am3
,LegalTypeTest(ty
));
776 /** Generate one term by eq classes */
777 MetaCandidateGeneratorClasses
mcdt(ty
,qe
->getTheoryEngine());
778 /* Create a matcher from the candidate generator */
779 AuxMatcher1
am1(mcdt
,am2
);
783 AllVarMatcher( TNode pat
, QuantifiersEngine
* qe
):
784 d_cgm(createCgm(pat
, qe
)){}
786 void resetInstantiationRound( QuantifiersEngine
* qe
){
787 d_cgm
.resetInstantiationRound(qe
);
789 bool reset( InstMatch
& m
, QuantifiersEngine
* qe
){
790 return d_cgm
.reset(Node::null(), m
, qe
); //cdtUfEq doesn't use it's argument for reset
792 bool getNextMatch( InstMatch
& m
, QuantifiersEngine
* qe
){
793 return d_cgm
.getNextMatch(m
, qe
);
797 /** Match all the pattern with the same term */
798 class SplitMatcher
: public Matcher
{
801 ApplyMatcher d_m
; /** Use ApplyMatcher by creating a fake application */
803 SplitMatcher(std::vector
< Node
> pats
, QuantifiersEngine
* qe
):
805 d_m(NodeManager::currentNM()->mkNode(kind::INST_PATTERN
,pats
), qe
) {}
806 void resetInstantiationRound( QuantifiersEngine
* qe
){
807 d_m
.resetInstantiationRound(qe
);
809 bool reset( TNode ex
, InstMatch
& m
, QuantifiersEngine
* qe
){
810 NodeBuilder
<> n(kind::INST_PATTERN
);
811 for(size_t i
= 0; i
< size
; ++i
) n
<< ex
;
813 return d_m
.reset(nn
,m
,qe
);
815 bool getNextMatch( InstMatch
& m
, QuantifiersEngine
* qe
){
816 return getNextMatch(m
, qe
);
821 /** Match uf term in a fixed equivalence class */
822 class UfCstEqMatcher
: public PatMatcher
{
824 /* equivalence class to match */
829 UfCstEqMatcher( Node pat
, Node cst
, QuantifiersEngine
* qe
):
831 d_cgm(OpMatcher(pat
,qe
)) {};
832 void resetInstantiationRound( QuantifiersEngine
* qe
){
833 d_cgm
.resetInstantiationRound(qe
);
835 bool reset( InstMatch
& m
, QuantifiersEngine
* qe
){
836 return d_cgm
.reset(d_cst
, m
, qe
);
838 bool getNextMatch( InstMatch
& m
, QuantifiersEngine
* qe
){
839 return d_cgm
.getNextMatch(m
, qe
);
843 /** Match equalities */
844 class UfEqMatcher
: public PatMatcher
{
847 typedef SplitMatcher AuxMatcher3
;
848 typedef TestMatcher
< AuxMatcher3
, LegalTypeTest
> AuxMatcher2
;
849 typedef CandidateGeneratorMatcher
< CandidateGeneratorTheoryEeClasses
, AuxMatcher2
> AuxMatcher1
;
851 static inline AuxMatcher1
createCgm(std::vector
<Node
> & pat
, QuantifiersEngine
* qe
){
852 Assert( pat
.size() > 0);
853 TypeNode ty
= pat
[0].getType();
854 for(size_t i
= 1; i
< pat
.size(); ++i
){
855 Assert(pat
[i
].getType() == ty
);
857 /** In reverse order of matcher sequence */
858 /** Distribute it to all the pattern */
859 AuxMatcher3
am3(pat
,qe
);
860 /** Keep only the one that have the good type */
861 AuxMatcher2
am2(am3
,LegalTypeTest(ty
));
862 /** Generate one term by eq classes */
863 uf::TheoryUF
* uf
= static_cast<uf::TheoryUF
*>(qe
->getTheoryEngine()->getTheory( theory::THEORY_UF
));
864 eq::EqualityEngine
* ee
=
865 static_cast<eq::EqualityEngine
*>(uf
->getEqualityEngine());
866 CandidateGeneratorTheoryEeClasses
cdtUfEq(ee
);
867 /* Create a matcher from the candidate generator */
868 AuxMatcher1
am1(cdtUfEq
,am2
);
872 UfEqMatcher( std::vector
<Node
> & pat
, QuantifiersEngine
* qe
):
873 d_cgm(createCgm(pat
, qe
)){}
875 void resetInstantiationRound( QuantifiersEngine
* qe
){
876 d_cgm
.resetInstantiationRound(qe
);
878 bool reset( InstMatch
& m
, QuantifiersEngine
* qe
){
879 return d_cgm
.reset(Node::null(), m
, qe
); //cdtUfEq doesn't use it's argument for reset
881 bool getNextMatch( InstMatch
& m
, QuantifiersEngine
* qe
){
882 return d_cgm
.getNextMatch(m
, qe
);
887 /** Match dis-equalities */
888 class UfDeqMatcher
: public PatMatcher
{
891 typedef ApplyMatcher AuxMatcher3
;
893 class EqTest
/* : public unary_function<Node,bool>*/ {
896 inline EqTest(TypeNode type
): d_type(type
){};
897 inline bool operator() (Node n
) {
899 CandidateGenerator::isLegalCandidate(n
) &&
900 n
.getKind() == kind::EQUAL
&&
901 n
[0].getType()==d_type
;
904 typedef TestMatcher
< AuxMatcher3
, EqTest
> AuxMatcher2
;
905 typedef CandidateGeneratorMatcher
< CandidateGeneratorTheoryEeClass
, AuxMatcher2
> AuxMatcher1
;
908 static inline AuxMatcher1
createCgm(Node pat
, QuantifiersEngine
* qe
){
909 Assert( pat
.getKind() == kind::NOT
);
911 Assert( eq
.getKind() == kind::EQUAL
);
912 TypeNode ty
= eq
[0].getType();
913 /** In reverse order of matcher sequence */
914 /** Distribute it to all the pattern */
915 AuxMatcher3
am3(eq
,qe
);
916 /** Keep only the one that have the good type */
917 AuxMatcher2
am2(am3
,EqTest(ty
));
918 /** Will generate all the terms of the eq class of false */
919 uf::TheoryUF
* uf
= static_cast<uf::TheoryUF
*>(qe
->getTheoryEngine()->getTheory( theory::THEORY_UF
));
920 eq::EqualityEngine
* ee
=
921 static_cast<eq::EqualityEngine
*>(uf
->getEqualityEngine());
922 CandidateGeneratorTheoryEeClass
cdtUfEq(ee
);
923 /* Create a matcher from the candidate generator */
924 AuxMatcher1
am1(cdtUfEq
,am2
);
928 UfDeqMatcher( Node pat
, QuantifiersEngine
* qe
):
929 d_cgm(createCgm(pat
, qe
)),
930 false_term((static_cast<uf::TheoryUF
*>(qe
->getTheoryEngine()->getTheory( theory::THEORY_UF
)))->getEqualityEngine()->
931 getRepresentative(NodeManager::currentNM()->mkConst
<bool>(false) )){};
932 void resetInstantiationRound( QuantifiersEngine
* qe
){
933 d_cgm
.resetInstantiationRound(qe
);
935 bool reset( InstMatch
& m
, QuantifiersEngine
* qe
){
936 return d_cgm
.reset(false_term
, m
, qe
);
938 bool getNextMatch( InstMatch
& m
, QuantifiersEngine
* qe
){
939 return d_cgm
.getNextMatch(m
, qe
);
943 Matcher
* mkMatcher( Node pat
, QuantifiersEngine
* qe
){
944 Debug("inst-match-gen") << "mkMatcher: Pattern term is " << pat
<< std::endl
;
946 // if( pat.getKind() == kind::APPLY_UF){
947 // return new OpMatcher(pat, qe);
948 // } else if( pat.getKind() == kind::APPLY_CONSTRUCTOR ){
949 // return new DatatypesMatcher(pat, qe);
950 // } else if( pat.getKind() == kind::SELECT || pat.getKind() == kind::STORE ){
951 // return new ArrayMatcher(pat, qe);
952 if( pat
.getKind() == kind::APPLY_UF
||
953 pat
.getKind() == kind::APPLY_CONSTRUCTOR
||
954 pat
.getKind() == kind::SELECT
|| pat
.getKind() == kind::STORE
){
955 return new GenericMatcher(pat
, qe
);
956 } else { /* Arithmetic? */
957 /** TODO: something simpler to see if the pattern is a good
958 arithmetic pattern */
959 std::map
< Node
, Node
> d_arith_coeffs
;
960 if( !Trigger::getPatternArithmetic( pat
.getAttribute(InstConstantAttribute()), pat
, d_arith_coeffs
) ){
961 Message() << "(?) Unknown matching pattern is " << pat
<< std::endl
;
962 Unimplemented("pattern not implemented");
963 return new DumbMatcher();
965 Debug("matching-arith") << "Generated arithmetic pattern for " << pat
<< ": " << std::endl
;
966 for( std::map
< Node
, Node
>::iterator it
= d_arith_coeffs
.begin(); it
!= d_arith_coeffs
.end(); ++it
){
967 Debug("matching-arith") << " " << it
->first
<< " -> " << it
->second
<< std::endl
;
969 ArithMatcher
am3 (pat
, qe
);
970 TestMatcher
<ArithMatcher
, LegalTypeTest
>
971 am2(am3
,LegalTypeTest(pat
.getType()));
973 uf::TheoryUF
* uf
= static_cast<uf::TheoryUF
*>(qe
->getTheoryEngine()->getTheory( theory::THEORY_UF
));
974 eq::EqualityEngine
* ee
=
975 static_cast<eq::EqualityEngine
*> (uf
->getEqualityEngine());
976 CandidateGeneratorTheoryEeClass
cdtUfEq(ee
);
977 return new CandidateGeneratorMatcher
< CandidateGeneratorTheoryEeClass
,
978 TestMatcher
<ArithMatcher
, LegalTypeTest
> > (cdtUfEq
,am2
);
983 PatMatcher
* mkPattern( Node pat
, QuantifiersEngine
* qe
){
984 Debug("inst-match-gen") << "Pattern term is " << pat
<< std::endl
;
985 Assert( pat
.hasAttribute(InstConstantAttribute()) );
987 if( pat
.getKind()==kind::NOT
&& pat
[0].getKind() == kind::EQUAL
){
989 return new UfDeqMatcher(pat
, qe
);
990 } else if (pat
.getKind() == kind::EQUAL
){
991 if( !pat
[0].hasAttribute(InstConstantAttribute() )){
992 Assert(pat
[1].hasAttribute(InstConstantAttribute()));
993 return new UfCstEqMatcher(pat
[1], pat
[0], qe
);
994 }else if( !pat
[1].hasAttribute(InstConstantAttribute() )){
995 Assert(pat
[0].hasAttribute(InstConstantAttribute()));
996 return new UfCstEqMatcher(pat
[0], pat
[1], qe
);
998 std::vector
< Node
> pats(pat
.begin(),pat
.end());
999 return new UfEqMatcher(pats
,qe
);
1001 } else if( Trigger::isAtomicTrigger( pat
) ){
1002 return new AllOpMatcher(pat
, qe
);
1003 // return new GenericPatMatcher(pat, qe);
1004 } else if( pat
.getKind()==INST_CONSTANT
){
1006 return new AllVarMatcher(pat
, qe
);
1007 } else { /* Arithmetic? */
1008 /** TODO: something simpler to see if the pattern is a good
1009 arithmetic pattern */
1010 std::map
< Node
, Node
> d_arith_coeffs
;
1011 if( !Trigger::getPatternArithmetic( pat
.getAttribute(InstConstantAttribute()), pat
, d_arith_coeffs
) ){
1012 Debug("inst-match-gen") << "(?) Unknown matching pattern is " << pat
<< std::endl
;
1013 Message() << "(?) Unknown matching pattern is " << pat
<< std::endl
;
1014 return new DumbPatMatcher();
1016 Debug("matching-arith") << "Generated arithmetic pattern for " << pat
<< ": " << std::endl
;
1017 for( std::map
< Node
, Node
>::iterator it
= d_arith_coeffs
.begin(); it
!= d_arith_coeffs
.end(); ++it
){
1018 Debug("matching-arith") << " " << it
->first
<< " -> " << it
->second
<< std::endl
;
1020 ArithMatcher
am3 (pat
, qe
);
1021 TestMatcher
<ArithMatcher
, LegalTest
>
1022 am2(am3
,LegalTest());
1024 TermDb
* tdb
= qe
->getTermDatabase();
1025 CandidateGeneratorTheoryUfType
cdtUfEq(pat
.getType(),tdb
);
1026 typedef CandidateGeneratorMatcher
< CandidateGeneratorTheoryUfType
,
1027 TestMatcher
<ArithMatcher
, LegalTest
> > AuxMatcher1
;
1028 return new PatOfMatcher
<AuxMatcher1
>(AuxMatcher1(cdtUfEq
,am2
));
1033 ArithMatcher::ArithMatcher(Node pat
, QuantifiersEngine
* qe
): d_pattern(pat
){
1035 if(Trigger::getPatternArithmetic(pat
.getAttribute(InstConstantAttribute()), pat
, d_arith_coeffs
) )
1037 Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_pattern
<< std::endl
;
1040 Debug("matching-arith") << "Generated arithmetic pattern for " << d_pattern
<< ": " << std::endl
;
1041 for( std::map
< Node
, Node
>::iterator it
= d_arith_coeffs
.begin(); it
!= d_arith_coeffs
.end(); ++it
){
1042 Debug("matching-arith") << " " << it
->first
<< " -> " << it
->second
<< std::endl
;
1048 bool ArithMatcher::reset( TNode t
, InstMatch
& m
, QuantifiersEngine
* qe
){
1049 Debug("matching-arith") << "Matching " << t
<< " " << d_pattern
<< std::endl
;
1051 if( !d_arith_coeffs
.empty() ){
1052 NodeBuilder
<> tb(kind::PLUS
);
1053 Node ic
= Node::null();
1054 for( std::map
< Node
, Node
>::iterator it
= d_arith_coeffs
.begin(); it
!= d_arith_coeffs
.end(); ++it
){
1055 Debug("matching-arith") << it
->first
<< " -> " << it
->second
<< std::endl
;
1056 if( !it
->first
.isNull() ){
1057 if( m
.find( it
->first
)==m
.end() ){
1058 //see if we can choose this to set
1059 if( ic
.isNull() && ( it
->second
.isNull() || !it
->first
.getType().isInteger() ) ){
1063 Debug("matching-arith") << "already set " << m
.get( it
->first
) << std::endl
;
1064 Node tm
= m
.get( it
->first
);
1065 if( !it
->second
.isNull() ){
1066 tm
= NodeManager::currentNM()->mkNode( MULT
, it
->second
, tm
);
1076 if( tb
.getNumChildren()==0 ){
1079 tm
= tb
.getNumChildren()==1 ? tb
.getChild( 0 ) : tb
;
1080 tm
= NodeManager::currentNM()->mkNode( MINUS
, t
, tm
);
1082 if( !d_arith_coeffs
[ ic
].isNull() ){
1083 Assert( !ic
.getType().isInteger() );
1084 Node coeff
= NodeManager::currentNM()->mkConst( Rational(1) / d_arith_coeffs
[ ic
].getConst
<Rational
>() );
1085 tm
= NodeManager::currentNM()->mkNode( MULT
, coeff
, tm
);
1087 m
.set( ic
, Rewriter::rewrite( tm
));
1088 d_binded
.push_back(ic
);
1089 //set the rest to zeros
1090 for( std::map
< Node
, Node
>::iterator it
= d_arith_coeffs
.begin(); it
!= d_arith_coeffs
.end(); ++it
){
1091 if( !it
->first
.isNull() ){
1092 if( m
.find( it
->first
)==m
.end() ){
1093 m
.set( it
->first
, NodeManager::currentNM()->mkConst( Rational(0) ));
1094 d_binded
.push_back(ic
);
1098 Debug("matching-arith") << "Setting " << ic
<< " to " << tm
<< std::endl
;
1101 m
.erase(d_binded
.begin(), d_binded
.end());
1105 m
.erase(d_binded
.begin(), d_binded
.end());
1110 bool ArithMatcher::getNextMatch( InstMatch
& m
, QuantifiersEngine
* qe
){
1111 m
.erase(d_binded
.begin(), d_binded
.end());
1116 class MultiPatsMatcher
: public PatsMatcher
{
1119 std::vector
< PatMatcher
* > d_patterns
;
1121 bool reset( QuantifiersEngine
* qe
){
1123 d_reset_done
= true;
1125 return getNextMatch(qe
,true);
1128 bool getNextMatch(QuantifiersEngine
* qe
, bool reset
){
1129 const size_t max
= d_patterns
.size() - 1;
1130 size_t index
= reset
? 0 : max
;
1132 Debug("matching") << "MultiPatsMatcher::index " << index
<< "/"
1133 << max
<< (reset
? " reset_phase" : "") << std::endl
;
1135 d_patterns
[index
]->reset( d_im
, qe
) :
1136 d_patterns
[index
]->getNextMatch( d_im
, qe
)){
1137 if(index
==max
) return true;
1141 if(index
==0) return false;
1149 MultiPatsMatcher(std::vector
< Node
> & pats
, QuantifiersEngine
* qe
):
1150 d_reset_done(false){
1151 Assert(pats
.size() > 0);
1152 for( size_t i
=0; i
< pats
.size(); i
++ ){
1153 d_patterns
.push_back(mkPattern(pats
[i
],qe
));
1156 void resetInstantiationRound( QuantifiersEngine
* qe
){
1157 for( size_t i
=0; i
< d_patterns
.size(); i
++ ){
1158 d_patterns
[i
]->resetInstantiationRound( qe
);
1160 d_reset_done
= false;
1163 bool getNextMatch( QuantifiersEngine
* qe
){
1164 Assert(d_patterns
.size()>0);
1165 if(d_reset_done
) return getNextMatch(qe
,false);
1166 else return reset(qe
);
1168 const InstMatch
& getInstMatch(){return d_im
;};
1170 int addInstantiations( InstMatch
& baseMatch
, Node quant
, QuantifiersEngine
* qe
);
1175 ES_GET_MONO_CANDIDATE
,
1176 ES_GET_MULTI_CANDIDATE
,
1184 static inline std::ostream
& operator<<(std::ostream
& out
, const EffiStep
& step
) {
1186 case ES_STOP
: out
<< "STOP"; break;
1187 case ES_GET_MONO_CANDIDATE
: out
<< "GET_MONO_CANDIDATE"; break;
1188 case ES_GET_MULTI_CANDIDATE
: out
<< "GET_MULTI_CANDIDATE"; break;
1189 case ES_RESET1
: out
<< "RESET1"; break;
1190 case ES_RESET2
: out
<< "RESET2"; break;
1191 case ES_NEXT1
: out
<< "NEXT1"; break;
1192 case ES_NEXT2
: out
<< "NEXT2"; break;
1193 case ES_RESET_OTHER
: out
<< "RESET_OTHER"; break;
1194 case ES_NEXT_OTHER
: out
<< "NEXT_OTHER"; break;
1200 int MultiPatsMatcher::addInstantiations( InstMatch
& baseMatch
, Node quant
, QuantifiersEngine
* qe
){
1201 //now, try to add instantiation for each match produced
1202 int addedLemmas
= 0;
1203 resetInstantiationRound( qe
);
1204 d_im
.add( baseMatch
);
1205 while( getNextMatch( qe
) ){
1206 InstMatch im_copy
= getInstMatch();
1207 //m.makeInternal( d_quantEngine->getEqualityQuery() );
1208 if( qe
->addInstantiation( quant
, im_copy
) ){
1212 //return number of lemmas added
1216 PatsMatcher
* mkPatterns( std::vector
< Node
> pat
, QuantifiersEngine
* qe
){
1217 return new MultiPatsMatcher( pat
, qe
);
1220 class MultiEfficientPatsMatcher
: public PatsMatcher
{
1223 bool d_phase_new_term
;
1224 std::vector
< PatMatcher
* > d_patterns
;
1225 std::vector
< Matcher
* > d_direct_patterns
;
1227 uf::EfficientHandler d_eh
;
1228 uf::EfficientHandler::MultiCandidate d_mc
;
1229 InstMatchTrie2Pairs
<true> d_cache
;
1230 std::vector
<Node
> d_pats
;
1231 // bool indexDone( size_t i){
1232 // return i == d_c.first.second ||
1233 // ( i == d_c.second.second && d_c.second.first.empty());
1238 static const EffiStep ES_START
= ES_GET_MONO_CANDIDATE
;
1241 //return true if it becomes bigger than d_patterns.size() - 1
1242 bool incrIndex(size_t & index
){
1243 if(index
== d_patterns
.size() - 1) return true;
1245 if(index
== d_mc
.first
.second
1246 || (!d_phase_mono
&& index
== d_mc
.second
.second
))
1247 return incrIndex(index
);
1251 //return true if it becomes smaller than 0
1252 bool decrIndex(size_t & index
){
1253 if(index
== 0) return true;
1255 if(index
== d_mc
.first
.second
1256 || (!d_phase_mono
&& index
== d_mc
.second
.second
))
1257 return decrIndex(index
);
1261 bool resetOther( QuantifiersEngine
* qe
){
1262 return getNextMatchOther(qe
,true);
1266 bool getNextMatchOther(QuantifiersEngine
* qe
, bool reset
){
1267 size_t index
= reset
? 0 : d_patterns
.size();
1268 if(!reset
&& decrIndex(index
)) return false;
1270 (index
== d_mc
.first
.second
1271 || (!d_phase_mono
&& index
== d_mc
.second
.second
))
1272 && incrIndex(index
)) return true;
1274 Debug("matching") << "MultiEfficientPatsMatcher::index " << index
<< "/"
1275 << d_patterns
.size() - 1 << std::endl
;
1277 d_patterns
[index
]->reset( d_im
, qe
) :
1278 d_patterns
[index
]->getNextMatch( d_im
, qe
)){
1279 if(incrIndex(index
)) return true;
1282 if(decrIndex(index
)) return false;
1288 inline EffiStep
TestMonoCache(QuantifiersEngine
* qe
){
1289 if( //!d_phase_new_term ||
1290 d_pats
.size() == 1) return ES_RESET_OTHER
;
1291 if(d_cache
.addInstMatch(d_mc
.first
.second
,d_im
)){
1292 Debug("inst-match::cache") << "Cache miss" << d_im
<< std::endl
;
1293 ++qe
->d_statistics
.d_mono_candidates_cache_miss
;
1294 return ES_RESET_OTHER
;
1296 Debug("inst-match::cache") << "Cache hit" << d_im
<< std::endl
;
1297 ++qe
->d_statistics
.d_mono_candidates_cache_hit
;
1300 // ++qe->d_statistics.d_mono_candidates_cache_miss;
1301 // return ES_RESET_OTHER;
1304 inline EffiStep
TestMultiCache(QuantifiersEngine
* qe
){
1305 if(d_cache
.addInstMatch(d_mc
.first
.second
,d_mc
.second
.second
,d_im
)){
1306 ++qe
->d_statistics
.d_multi_candidates_cache_miss
;
1307 return ES_RESET_OTHER
;
1309 ++qe
->d_statistics
.d_multi_candidates_cache_hit
;
1317 bool getNextMatch( QuantifiersEngine
* qe
){
1318 Assert( d_step
== ES_START
|| d_step
== ES_NEXT_OTHER
|| d_step
== ES_STOP
);
1320 Debug("matching") << "d_step=" << d_step
<< " "
1321 << "d_im=" << d_im
<< std::endl
;
1323 case ES_GET_MONO_CANDIDATE
:
1324 Assert(d_im
.empty());
1325 if(d_phase_new_term
? d_eh
.getNextMonoCandidate(d_mc
.first
) : d_eh
.getNextMonoCandidateNewTerm(d_mc
.first
)){
1326 if(d_phase_new_term
) ++qe
->d_statistics
.d_num_mono_candidates_new_term
;
1327 else ++qe
->d_statistics
.d_num_mono_candidates
;
1328 d_phase_mono
= true;
1330 } else if (!d_phase_new_term
){
1331 d_phase_new_term
= true;
1332 d_step
= ES_GET_MONO_CANDIDATE
;
1334 d_phase_new_term
= false;
1335 d_step
= ES_GET_MULTI_CANDIDATE
;
1338 case ES_GET_MULTI_CANDIDATE
:
1339 Assert(d_im
.empty());
1340 if(d_eh
.getNextMultiCandidate(d_mc
)){
1341 ++qe
->d_statistics
.d_num_multi_candidates
;
1342 d_phase_mono
= false;
1344 } else d_step
= ES_STOP
;
1347 if(d_direct_patterns
[d_mc
.first
.second
]->reset(d_mc
.first
.first
,d_im
,qe
))
1348 d_step
= d_phase_mono
? TestMonoCache(qe
) : ES_RESET2
;
1349 else d_step
= d_phase_mono
? ES_GET_MONO_CANDIDATE
: ES_GET_MULTI_CANDIDATE
;
1352 Assert(!d_phase_mono
);
1353 if(d_direct_patterns
[d_mc
.second
.second
]->reset(d_mc
.second
.first
,d_im
,qe
))
1354 d_step
= TestMultiCache(qe
);
1355 else d_step
= ES_NEXT1
;
1358 if(d_direct_patterns
[d_mc
.first
.second
]->getNextMatch(d_im
,qe
))
1359 d_step
= d_phase_mono
? TestMonoCache(qe
) : ES_RESET2
;
1360 else d_step
= d_phase_mono
? ES_GET_MONO_CANDIDATE
: ES_GET_MULTI_CANDIDATE
;
1363 if(d_direct_patterns
[d_mc
.second
.second
]->getNextMatch(d_im
,qe
))
1364 d_step
= TestMultiCache(qe
);
1365 else d_step
= ES_NEXT1
;
1367 case ES_RESET_OTHER
:
1369 d_step
= ES_NEXT_OTHER
;
1371 } else d_step
= d_phase_mono
? ES_NEXT1
: ES_NEXT2
;
1375 if(!getNextMatchOther(qe
,false)){
1376 d_step
= d_phase_mono
? ES_NEXT1
: ES_NEXT2
;
1378 d_step
= ES_NEXT_OTHER
;
1384 Assert(d_im
.empty());
1390 MultiEfficientPatsMatcher(std::vector
< Node
> & pats
, QuantifiersEngine
* qe
):
1391 d_eh(qe
->getTheoryEngine()->getSatContext()),
1392 d_cache(qe
->getTheoryEngine()->getSatContext(),qe
,pats
.size()),
1393 d_pats(pats
), d_step(ES_START
) {
1394 Assert(pats
.size() > 0);
1395 for( size_t i
=0; i
< pats
.size(); i
++ ){
1396 d_patterns
.push_back(mkPattern(pats
[i
],qe
));
1397 if(pats
[i
].getKind()==kind::INST_CONSTANT
){
1398 d_direct_patterns
.push_back(new VarMatcher(pats
[i
],qe
));
1399 } else if( pats
[i
].getKind() == kind::NOT
&& pats
[i
][0].getKind() == kind::EQUAL
){
1400 d_direct_patterns
.push_back(new ApplyMatcher(pats
[i
][0],qe
));
1402 d_direct_patterns
.push_back(new ApplyMatcher(pats
[i
],qe
));
1405 Theory
* th_uf
= qe
->getTheoryEngine()->getTheory( theory::THEORY_UF
);
1406 uf::InstantiatorTheoryUf
* ith
= (uf::InstantiatorTheoryUf
*)th_uf
->getInstantiator();
1407 ith
->registerEfficientHandler(d_eh
, pats
);
1409 void resetInstantiationRound( QuantifiersEngine
* qe
){
1410 Assert(d_step
== ES_START
|| d_step
== ES_STOP
);
1411 for( size_t i
=0; i
< d_patterns
.size(); i
++ ){
1412 d_patterns
[i
]->resetInstantiationRound( qe
);
1413 d_direct_patterns
[i
]->resetInstantiationRound( qe
);
1416 d_phase_new_term
= false;
1417 Assert(d_im
.empty());
1420 const InstMatch
& getInstMatch(){return d_im
;};
1422 int addInstantiations( InstMatch
& baseMatch
, Node quant
, QuantifiersEngine
* qe
);
1425 int MultiEfficientPatsMatcher::addInstantiations( InstMatch
& baseMatch
, Node quant
, QuantifiersEngine
* qe
){
1426 //now, try to add instantiation for each match produced
1427 int addedLemmas
= 0;
1428 Assert(baseMatch
.empty());
1429 resetInstantiationRound( qe
);
1430 while( getNextMatch( qe
) ){
1431 InstMatch im_copy
= getInstMatch();
1432 //m.makeInternal( d_quantEngine->getEqualityQuery() );
1433 if( qe
->addInstantiation( quant
, im_copy
) ){
1437 //return number of lemmas added
1441 PatsMatcher
* mkPatternsEfficient( std::vector
< Node
> pat
, QuantifiersEngine
* qe
){
1442 return new MultiEfficientPatsMatcher( pat
, qe
);
1445 } /* CVC4::theory::rrinst */
1446 } /* CVC4::theory */