1 /********************* */
2 /*! \file inst_match.cpp
4 ** Original author: Morgan Deters
5 ** Major contributors: Andrew Reynolds
6 ** Minor contributors (to current version): Kshitij Bansal, Francois Bobot, Clark Barrett
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 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 Implementation of inst match class
15 #include "theory/quantifiers/inst_match.h"
16 #include "theory/quantifiers/term_database.h"
17 #include "theory/quantifiers/quant_util.h"
18 #include "theory/quantifiers_engine.h"
22 using namespace CVC4::kind
;
23 using namespace CVC4::context
;
24 using namespace CVC4::theory
;
30 InstMatch::InstMatch( TNode f
) {
31 for( unsigned i
=0; i
<f
[0].getNumChildren(); i
++ ){
32 d_vals
.push_back( Node::null() );
36 InstMatch::InstMatch( InstMatch
* m
) {
37 d_vals
.insert( d_vals
.end(), m
->d_vals
.begin(), m
->d_vals
.end() );
40 bool InstMatch::add( InstMatch
& m
){
41 for( unsigned i
=0; i
<d_vals
.size(); i
++ ){
42 if( d_vals
[i
].isNull() ){
43 d_vals
[i
] = m
.d_vals
[i
];
49 bool InstMatch::merge( EqualityQuery
* q
, InstMatch
& m
){
50 for( unsigned i
=0; i
<m
.d_vals
.size(); i
++ ){
51 if( !m
.d_vals
[i
].isNull() ){
52 if( d_vals
[i
].isNull() ){
53 d_vals
[i
] = m
.d_vals
[i
];
55 if( !q
->areEqual( d_vals
[i
], m
.d_vals
[i
]) ){
65 void InstMatch::debugPrint( const char* c
){
66 for( unsigned i
=0; i
<d_vals
.size(); i
++ ){
67 if( !d_vals
[i
].isNull() ){
68 Debug( c
) << " " << i
<< " -> " << d_vals
[i
] << std::endl
;
73 bool InstMatch::isComplete() {
74 for( unsigned i
=0; i
<d_vals
.size(); i
++ ){
75 if( d_vals
[i
].isNull() ){
82 bool InstMatch::empty() {
83 for( unsigned i
=0; i
<d_vals
.size(); i
++ ){
84 if( !d_vals
[i
].isNull() ){
91 void InstMatch::makeComplete( Node f
, QuantifiersEngine
* qe
){
92 for( unsigned i
=0; i
<d_vals
.size(); i
++ ){
93 if( d_vals
[i
].isNull() ){
94 Node ic
= qe
->getTermDatabase()->getInstantiationConstant( f
, i
);
95 d_vals
[i
] = qe
->getTermDatabase()->getFreeVariableForInstConstant( ic
);
100 void InstMatch::makeRepresentative( QuantifiersEngine
* qe
){
101 for( unsigned i
=0; i
<d_vals
.size(); i
++ ){
102 if( !d_vals
[i
].isNull() ){
103 if( qe
->getEqualityQuery()->getEngine()->hasTerm( d_vals
[i
] ) ){
104 d_vals
[i
] = qe
->getEqualityQuery()->getEngine()->getRepresentative( d_vals
[i
] );
110 void InstMatch::applyRewrite(){
111 for( unsigned i
=0; i
<d_vals
.size(); i
++ ){
112 if( !d_vals
[i
].isNull() ){
113 d_vals
[i
] = Rewriter::rewrite( d_vals
[i
] );
118 void InstMatch::clear() {
119 for( unsigned i
=0; i
<d_vals
.size(); i
++ ){
120 d_vals
[i
] = Node::null();
126 Node
InstMatch::get( int i
) {
130 void InstMatch::getTerms( QuantifiersEngine
* qe
, Node f
, std::vector
< Node
>& inst
){
131 for( size_t i
=0; i
<f
[0].getNumChildren(); i
++ ){
134 Node ic
= qe
->getTermDatabase()->getInstantiationConstant( f
, i
);
135 val
= qe
->getTermDatabase()->getFreeVariableForInstConstant( ic
);
137 inst
.push_back( val
);
141 void InstMatch::setValue( int i
, TNode n
) {
145 bool InstMatch::set( QuantifiersEngine
* qe
, int i
, TNode n
) {
146 if( !d_vals
[i
].isNull() ){
147 if( qe
->getEqualityQuery()->areEqual( d_vals
[i
], n
) ){
158 bool InstMatchTrie::addInstMatch( QuantifiersEngine
* qe
, Node f
, std::vector
< Node
>& m
, bool modEq
,
159 bool modInst
, ImtIndexOrder
* imtio
, bool onlyExist
, int index
) {
160 if( index
==(int)f
[0].getNumChildren() || ( imtio
&& index
==(int)imtio
->d_order
.size() ) ){
163 int i_index
= imtio
? imtio
->d_order
[index
] : index
;
165 std::map
< Node
, InstMatchTrie
>::iterator it
= d_data
.find( n
);
166 if( it
!=d_data
.end() ){
167 bool ret
= it
->second
.addInstMatch( qe
, f
, m
, modEq
, modInst
, imtio
, onlyExist
, index
+1 );
168 if( !onlyExist
|| !ret
){
173 //check if m is an instance of another instantiation if modInst is true
177 std::map< Node, InstMatchTrie >::iterator itm = d_data.find( nl );
178 if( itm!=d_data.end() ){
179 if( !itm->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){
187 //check modulo equality if any other instantiation match exists
188 if( !n
.isNull() && qe
->getEqualityQuery()->getEngine()->hasTerm( n
) ){
189 eq::EqClassIterator
eqc( qe
->getEqualityQuery()->getEngine()->getRepresentative( n
),
190 qe
->getEqualityQuery()->getEngine() );
191 while( !eqc
.isFinished() ){
194 std::map
< Node
, InstMatchTrie
>::iterator itc
= d_data
.find( en
);
195 if( itc
!=d_data
.end() ){
196 if( itc
->second
.addInstMatch( qe
, f
, m
, modEq
, modInst
, imtio
, true, index
+1 ) ){
206 d_data
[n
].addInstMatch( qe
, f
, m
, modEq
, modInst
, imtio
, false, index
+1 );
212 void InstMatchTrie::print( std::ostream
& out
, Node q
, std::vector
< TNode
>& terms
) const {
213 if( terms
.size()==q
[0].getNumChildren() ){
215 for( unsigned i
=0; i
<terms
.size(); i
++ ){
216 if( i
>0 ){ out
<< ", ";}
219 out
<< " )" << std::endl
;
221 for( std::map
< Node
, InstMatchTrie
>::const_iterator it
= d_data
.begin(); it
!= d_data
.end(); ++it
){
222 terms
.push_back( it
->first
);
223 it
->second
.print( out
, q
, terms
);
230 bool CDInstMatchTrie::addInstMatch( QuantifiersEngine
* qe
, Node f
, std::vector
< Node
>& m
,
231 context::Context
* c
, bool modEq
, bool modInst
, int index
, bool onlyExist
){
233 if( !d_valid
.get() ){
241 if( index
==(int)f
[0].getNumChildren() ){
245 std::map
< Node
, CDInstMatchTrie
* >::iterator it
= d_data
.find( n
);
246 if( it
!=d_data
.end() ){
247 bool ret
= it
->second
->addInstMatch( qe
, f
, m
, c
, modEq
, modInst
, index
+1, onlyExist
);
248 if( !onlyExist
|| !ret
){
252 //check if m is an instance of another instantiation if modInst is true
257 std::map< Node, CDInstMatchTrie* >::iterator itm = d_data.find( nl );
258 if( itm!=d_data.end() ){
259 if( !itm->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, true ) ){
267 //check modulo equality if any other instantiation match exists
268 if( !n
.isNull() && qe
->getEqualityQuery()->getEngine()->hasTerm( n
) ){
269 eq::EqClassIterator
eqc( qe
->getEqualityQuery()->getEngine()->getRepresentative( n
),
270 qe
->getEqualityQuery()->getEngine() );
271 while( !eqc
.isFinished() ){
274 std::map
< Node
, CDInstMatchTrie
* >::iterator itc
= d_data
.find( en
);
275 if( itc
!=d_data
.end() ){
276 if( itc
->second
->addInstMatch( qe
, f
, m
, c
, modEq
, modInst
, index
+1, true ) ){
287 // std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
288 CDInstMatchTrie
* imt
= new CDInstMatchTrie( c
);
290 imt
->addInstMatch( qe
, f
, m
, c
, modEq
, modInst
, index
+1, false );
296 void CDInstMatchTrie::print( std::ostream
& out
, Node q
, std::vector
< TNode
>& terms
) const{
298 if( terms
.size()==q
[0].getNumChildren() ){
300 for( unsigned i
=0; i
<terms
.size(); i
++ ){
301 if( i
>0 ) out
<< ", ";
304 out
<< " )" << std::endl
;
306 for( std::map
< Node
, CDInstMatchTrie
* >::const_iterator it
= d_data
.begin(); it
!= d_data
.end(); ++it
){
307 terms
.push_back( it
->first
);
308 it
->second
->print( out
, q
, terms
);
315 }/* CVC4::theory::inst namespace */
316 }/* CVC4::theory namespace */
317 }/* CVC4 namespace */