1 /********************* */
2 /*! \file rr_inst_match_impl.h
4 ** Original author: bobot
5 ** Major contributors: none
6 ** Minor contributors (to current version): ajreynol, 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 inst match class
17 #include "cvc4_private.h"
19 #ifndef __CVC4__RR_INST_MATCH_IMPL_H
20 #define __CVC4__RR_INST_MATCH_IMPL_H
22 #include "theory/rr_inst_match.h"
23 #include "theory/theory_engine.h"
24 #include "theory/quantifiers_engine.h"
25 #include "theory/rr_candidate_generator.h"
26 #include "theory/uf/equality_engine.h"
33 InstMatchTrie2Gen
<modEq
>::InstMatchTrie2Gen(context::Context
* c
, QuantifiersEngine
* qe
):
34 d_context(c
), d_mods(c
) {
35 d_eQ
= qe
->getEqualityQuery();
36 d_cG
= qe
->getRRCanGenClass();
39 /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
41 void InstMatchTrie2Gen
<modEq
>::addSubTree( Tree
* root
, mapIter current
, mapIter end
, size_t currLevel
) {
42 if( current
== end
) return;
44 Assert(root
->e
.find(current
->second
) == root
->e
.end());
45 Tree
* root2
= new Tree(currLevel
);
46 root
->e
.insert(std::make_pair(current
->second
, root2
));
47 addSubTree(root2
, ++current
, end
, currLevel
);
52 bool InstMatchTrie2Gen
<modEq
>::existsInstMatch(InstMatchTrie2Gen
<modEq
>::Tree
* root
,
53 mapIter
& current
, mapIter
& end
,
54 Tree
* & e
, mapIter
& diverge
) const{
55 if( current
== end
) {
56 Debug("Trie2") << "Trie2 Bottom " << std::endl
;
61 if (current
->first
> diverge
->first
){
62 // this point is the deepest point currently seen map are ordered
67 TNode n
= current
->second
;
68 typename InstMatchTrie2Gen
<modEq
>::Tree::MLevel::iterator it
=
70 if( it
!=root
->e
.end() &&
71 existsInstMatch( (*it
).second
, ++current
, end
, e
, diverge
) ){
72 Debug("Trie2") << "Trie2 Directly here " << n
<< std::endl
;
76 Assert( it
==root
->e
.end() || e
!= root
);
78 // Even if n is in the trie others of the equivalence class
79 // can also be in it since the equality can have appeared
80 // after they have been added
81 if( modEq
&& d_eQ
->hasTerm( n
) ){
82 //check modulo equality if any other instantiation match exists
83 d_cG
->reset( d_eQ
->getRepresentative( n
) );
84 for(TNode en
= d_cG
->getNextCandidate() ; !en
.isNull() ;
85 en
= d_cG
->getNextCandidate() ){
86 if( en
== n
) continue; // already tested
87 typename InstMatchTrie2Gen
<modEq
>::Tree::MLevel::iterator itc
=
89 if( itc
!=root
->e
.end() &&
90 existsInstMatch( (*itc
).second
, ++current
, end
, e
, diverge
) ){
91 Debug("Trie2") << "Trie2 Indirectly here by equality " << n
<< " = " << en
<< std::endl
;
95 Assert( itc
==root
->e
.end() || e
!= root
);
103 bool InstMatchTrie2Gen
<modEq
>::
104 addInstMatch( InstMatch
& m
, InstMatchTrie2Gen
<modEq
>::Tree
* e
) {
105 d_cG
->resetInstantiationRound();
106 mapIter begin
= m
.begin();
107 mapIter end
= m
.end();
108 mapIter diverge
= begin
;
109 if( !existsInstMatch(e
, begin
, end
, e
, diverge
) ){
110 Assert(!diverge
->second
.isNull());
111 size_t currLevel
= d_context
->getLevel();
112 addSubTree( e
, diverge
, end
, currLevel
);
113 if(e
->level
!= currLevel
)
114 //If same level that e, will be removed at the same time than e
115 d_mods
.push_back(std::make_pair(e
,diverge
->second
));
122 }/* CVC4::theory::rrinst namespace */
124 }/* CVC4::theory namespace */
126 }/* CVC4 namespace */
128 #endif /* __CVC4__RR_INST_MATCH_IMPL_H */