1 /********************* */
4 ** Original author: Morgan Deters
5 ** Major contributors: Francois Bobot, Andrew Reynolds
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief inst match class
15 #include "cvc4_private.h"
17 #ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
18 #define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
20 #include "util/hash.h"
21 #include "context/cdo.h"
23 #include <ext/hash_set>
26 #include "context/cdlist.h"
27 #include "expr/node.h"
32 class QuantifiersEngine
;
37 /** basic class defining an instantiation */
39 /* map from variable to ground terms */
40 std::map
< Node
, Node
> d_map
;
43 InstMatch( InstMatch
* m
);
45 /** set the match of v to m */
46 bool setMatch( EqualityQuery
* q
, TNode v
, TNode m
);
47 /* This version tell if the variable has been set */
48 bool setMatch( EqualityQuery
* q
, TNode v
, TNode m
, bool & st
);
49 /** fill all unfilled values with m */
50 bool add( InstMatch
& m
);
51 /** if compatible, fill all unfilled values with m and return true
52 return false otherwise */
53 bool merge( EqualityQuery
* q
, InstMatch
& m
);
54 /** debug print method */
55 void debugPrint( const char* c
);
57 bool isComplete( Node f
) { return d_map
.size()==f
[0].getNumChildren(); }
59 void makeComplete( Node f
, QuantifiersEngine
* qe
);
60 /** make internal representative */
61 //void makeInternalRepresentative( QuantifiersEngine* qe );
62 /** make representative */
63 void makeRepresentative( QuantifiersEngine
* qe
);
65 Node
getValue( Node var
) const;
67 void clear(){ d_map
.clear(); }
69 bool empty(){ return d_map
.empty(); }
71 inline void toStream(std::ostream
& out
) const {
72 out
<< "INST_MATCH( ";
73 for( std::map
< Node
, Node
>::const_iterator it
= d_map
.begin(); it
!= d_map
.end(); ++it
){
74 if( it
!= d_map
.begin() ){ out
<< ", "; }
75 out
<< it
->first
<< " -> " << it
->second
;
86 template<class Iterator
>
87 void erase(Iterator begin
, Iterator end
){
88 for(Iterator i
= begin
; i
!= end
; ++i
){
92 void erase(Node node
){ d_map
.erase(node
); }
94 Node
get( TNode var
) { return d_map
[var
]; }
95 Node
get( QuantifiersEngine
* qe
, Node f
, int i
);
97 void set(TNode var
, TNode n
);
98 void set( QuantifiersEngine
* qe
, Node f
, int i
, TNode n
);
100 size_t size(){ return d_map
.size(); }
102 std::map
< Node
, Node
>::iterator
begin(){ return d_map
.begin(); };
103 std::map
< Node
, Node
>::iterator
end(){ return d_map
.end(); };
104 std::map
< Node
, Node
>::iterator
find(Node var
){ return d_map
.find(var
); };
105 /* Node used for matching the trigger only for mono-trigger (just for
106 efficiency because I need only that) */
108 };/* class InstMatch */
110 inline std::ostream
& operator<<(std::ostream
& out
, const InstMatch
& m
) {
115 /** trie for InstMatch objects */
116 class InstMatchTrie
{
118 class ImtIndexOrder
{
120 std::vector
< int > d_order
;
121 };/* class InstMatchTrie ImtIndexOrder */
124 std::map
< Node
, InstMatchTrie
> d_data
;
129 /** return true if m exists in this trie
130 modEq is if we check modulo equality
131 modInst is if we return true if m is an instance of a match that exists
133 bool existsInstMatch( QuantifiersEngine
* qe
, Node f
, InstMatch
& m
, bool modEq
= false,
134 bool modInst
= false, ImtIndexOrder
* imtio
= NULL
, int index
= 0 ) {
135 return !addInstMatch( qe
, f
, m
, modEq
, modInst
, imtio
, true, index
);
137 bool existsInstMatch( QuantifiersEngine
* qe
, Node f
, std::vector
< Node
>& m
, bool modEq
= false,
138 bool modInst
= false, ImtIndexOrder
* imtio
= NULL
, int index
= 0 ) {
139 return !addInstMatch( qe
, f
, m
, modEq
, modInst
, imtio
, true, index
);
141 /** add match m for quantifier f, take into account equalities if modEq = true,
142 if imtio is non-null, this is the order to add to trie
143 return true if successful
145 bool addInstMatch( QuantifiersEngine
* qe
, Node f
, InstMatch
& m
, bool modEq
= false,
146 bool modInst
= false, ImtIndexOrder
* imtio
= NULL
, bool onlyExist
= false, int index
= 0 );
147 bool addInstMatch( QuantifiersEngine
* qe
, Node f
, std::vector
< Node
>& m
, bool modEq
= false,
148 bool modInst
= false, ImtIndexOrder
* imtio
= NULL
, bool onlyExist
= false, int index
= 0 );
149 };/* class InstMatchTrie */
151 /** trie for InstMatch objects */
152 class CDInstMatchTrie
{
155 std::map
< Node
, CDInstMatchTrie
* > d_data
;
157 context::CDO
< bool > d_valid
;
159 CDInstMatchTrie( context::Context
* c
) : d_valid( c
, false ){}
162 /** return true if m exists in this trie
163 modEq is if we check modulo equality
164 modInst is if we return true if m is an instance of a match that exists
166 bool existsInstMatch( QuantifiersEngine
* qe
, Node f
, InstMatch
& m
, context::Context
* c
, bool modEq
= false,
167 bool modInst
= false, int index
= 0 ) {
168 return !addInstMatch( qe
, f
, m
, c
, modEq
, modInst
, index
, true );
170 bool existsInstMatch( QuantifiersEngine
* qe
, Node f
, std::vector
< Node
>& m
, context::Context
* c
, bool modEq
= false,
171 bool modInst
= false, int index
= 0 ) {
172 return !addInstMatch( qe
, f
, m
, c
, modEq
, modInst
, index
, true );
174 /** add match m for quantifier f, take into account equalities if modEq = true,
175 if imtio is non-null, this is the order to add to trie
176 return true if successful
178 bool addInstMatch( QuantifiersEngine
* qe
, Node f
, InstMatch
& m
, context::Context
* c
, bool modEq
= false,
179 bool modInst
= false, int index
= 0, bool onlyExist
= false );
180 bool addInstMatch( QuantifiersEngine
* qe
, Node f
, std::vector
< Node
>& m
, context::Context
* c
, bool modEq
= false,
181 bool modInst
= false, int index
= 0, bool onlyExist
= false );
182 };/* class CDInstMatchTrie */
185 class InstMatchTrieOrdered
{
187 InstMatchTrie::ImtIndexOrder
* d_imtio
;
190 InstMatchTrieOrdered( InstMatchTrie::ImtIndexOrder
* imtio
) : d_imtio( imtio
){}
191 ~InstMatchTrieOrdered(){}
193 InstMatchTrie::ImtIndexOrder
* getOrdering() { return d_imtio
; }
195 InstMatchTrie
* getTrie() { return &d_imt
; }
197 /** add match m, return true if successful */
198 bool addInstMatch( QuantifiersEngine
* qe
, Node f
, InstMatch
& m
, bool modEq
= false, bool modInst
= false ){
199 return d_imt
.addInstMatch( qe
, f
, m
, modEq
, modInst
, d_imtio
);
201 bool existsInstMatch( QuantifiersEngine
* qe
, Node f
, InstMatch
& m
, bool modEq
= false, bool modInst
= false ){
202 return d_imt
.existsInstMatch( qe
, f
, m
, modEq
, modInst
, d_imtio
);
204 };/* class InstMatchTrieOrdered */
206 }/* CVC4::theory::inst namespace */
208 typedef CVC4::theory::inst::InstMatch InstMatch
;
210 }/* CVC4::theory namespace */
211 }/* CVC4 namespace */
213 #endif /* __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */