1 /********************* */
2 /*! \file inst_match.cpp
4 ** Original author: ajreynol
5 ** Major contributors: bobot
6 ** Minor contributors (to current version): barrett, mdeters
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009-2012 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() {
33 InstMatch::InstMatch( InstMatch
* m
) {
37 bool InstMatch::setMatch( EqualityQuery
* q
, TNode v
, TNode m
, bool & set
){
38 std::map
< Node
, Node
>::iterator vn
= d_map
.find( v
);
39 if( vn
==d_map
.end() || vn
->second
.isNull() ){
42 Debug("matching-debug") << "Add partial " << v
<< "->" << m
<< std::endl
;
46 return q
->areEqual( vn
->second
, m
);
50 bool InstMatch::setMatch( EqualityQuery
* q
, TNode v
, TNode m
){
52 return setMatch(q
,v
,m
,set
);
55 bool InstMatch::add( InstMatch
& m
){
56 for( std::map
< Node
, Node
>::iterator it
= m
.d_map
.begin(); it
!= m
.d_map
.end(); ++it
){
57 if( !it
->second
.isNull() ){
58 std::map
< Node
, Node
>::iterator itf
= d_map
.find( it
->first
);
59 if( itf
==d_map
.end() || itf
->second
.isNull() ){
60 d_map
[it
->first
] = it
->second
;
67 bool InstMatch::merge( EqualityQuery
* q
, InstMatch
& m
){
68 for( std::map
< Node
, Node
>::iterator it
= m
.d_map
.begin(); it
!= m
.d_map
.end(); ++it
){
69 if( !it
->second
.isNull() ){
70 std::map
< Node
, Node
>::iterator itf
= d_map
.find( it
->first
);
71 if( itf
==d_map
.end() || itf
->second
.isNull() ){
72 d_map
[ it
->first
] = it
->second
;
74 if( !q
->areEqual( it
->second
, itf
->second
) ){
84 void InstMatch::debugPrint( const char* c
){
85 for( std::map
< Node
, Node
>::iterator it
= d_map
.begin(); it
!= d_map
.end(); ++it
){
86 Debug( c
) << " " << it
->first
<< " -> " << it
->second
<< std::endl
;
88 //if( !d_splits.empty() ){
89 // Debug( c ) << " Conditions: ";
90 // for( std::map< Node, Node >::iterator it = d_splits.begin(); it !=d_splits.end(); ++it ){
91 // Debug( c ) << it->first << " = " << it->second << " ";
93 // Debug( c ) << std::endl;
97 void InstMatch::makeComplete( Node f
, QuantifiersEngine
* qe
){
98 for( size_t i
=0; i
<f
[0].getNumChildren(); i
++ ){
99 Node ic
= qe
->getTermDatabase()->getInstantiationConstant( f
, i
);
100 if( d_map
.find( ic
)==d_map
.end() ){
101 d_map
[ ic
] = qe
->getTermDatabase()->getFreeVariableForInstConstant( ic
);
106 void InstMatch::makeInternalRepresentative( QuantifiersEngine
* qe
){
107 EqualityQueryQuantifiersEngine
* eqqe
= (EqualityQueryQuantifiersEngine
*)qe
->getEqualityQuery();
108 for( std::map
< Node
, Node
>::iterator it
= d_map
.begin(); it
!= d_map
.end(); ++it
){
109 d_map
[ it
->first
] = eqqe
->getInternalRepresentative( it
->second
);
113 void InstMatch::makeRepresentative( QuantifiersEngine
* qe
){
114 for( std::map
< Node
, Node
>::iterator it
= d_map
.begin(); it
!= d_map
.end(); ++it
){
115 if( qe
->getEqualityQuery()->getEngine()->hasTerm( it
->second
) ){
116 d_map
[ it
->first
] = qe
->getEqualityQuery()->getEngine()->getRepresentative( it
->second
);
121 void InstMatch::applyRewrite(){
122 for( std::map
< Node
, Node
>::iterator it
= d_map
.begin(); it
!= d_map
.end(); ++it
){
123 it
->second
= Rewriter::rewrite(it
->second
);
128 Node
InstMatch::getValue( Node var
) const{
129 std::map
< Node
, Node
>::const_iterator it
= d_map
.find( var
);
130 if( it
!=d_map
.end() ){
137 /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
138 void InstMatchTrie::addInstMatch2( QuantifiersEngine
* qe
, Node f
, InstMatch
& m
, int index
, ImtIndexOrder
* imtio
){
139 if( long(index
)<long(f
[0].getNumChildren()) && ( !imtio
|| long(index
)<long(imtio
->d_order
.size()) ) ){
140 int i_index
= imtio
? imtio
->d_order
[index
] : index
;
141 Node n
= m
.getValue( qe
->getTermDatabase()->getInstantiationConstant( f
, i_index
) );
142 d_data
[n
].addInstMatch2( qe
, f
, m
, index
+1, imtio
);
147 bool InstMatchTrie::existsInstMatch2( QuantifiersEngine
* qe
, Node f
, InstMatch
& m
, bool modEq
, bool modInst
, int index
, ImtIndexOrder
* imtio
){
148 if( long(index
)==long(f
[0].getNumChildren()) || ( imtio
&& long(index
)==long(imtio
->d_order
.size()) ) ){
151 int i_index
= imtio
? imtio
->d_order
[index
] : index
;
152 Node n
= m
.getValue( qe
->getTermDatabase()->getInstantiationConstant( f
, i_index
) );
153 std::map
< Node
, InstMatchTrie
>::iterator it
= d_data
.find( n
);
154 if( it
!=d_data
.end() ){
155 if( it
->second
.existsInstMatch2( qe
, f
, m
, modEq
, modInst
, index
+1, imtio
) ){
159 //check if m is an instance of another instantiation if modInst is true
163 it
= d_data
.find( nl
);
164 if( it
!=d_data
.end() ){
165 if( it
->second
.existsInstMatch2( qe
, f
, m
, modEq
, modInst
, index
+1, imtio
) ){
172 //check modulo equality if any other instantiation match exists
173 if( !n
.isNull() && qe
->getEqualityQuery()->getEngine()->hasTerm( n
) ){
174 eq::EqClassIterator
eqc( qe
->getEqualityQuery()->getEngine()->getRepresentative( n
),
175 qe
->getEqualityQuery()->getEngine() );
176 while( !eqc
.isFinished() ){
179 std::map
< Node
, InstMatchTrie
>::iterator itc
= d_data
.find( en
);
180 if( itc
!=d_data
.end() ){
181 if( itc
->second
.existsInstMatch2( qe
, f
, m
, modEq
, modInst
, index
+1, imtio
) ){
194 bool InstMatchTrie::existsInstMatch( QuantifiersEngine
* qe
, Node f
, InstMatch
& m
, bool modEq
, bool modInst
, ImtIndexOrder
* imtio
){
195 return existsInstMatch2( qe
, f
, m
, modEq
, modInst
, 0, imtio
);
198 bool InstMatchTrie::addInstMatch( QuantifiersEngine
* qe
, Node f
, InstMatch
& m
, bool modEq
, bool modInst
, ImtIndexOrder
* imtio
){
199 if( !existsInstMatch( qe
, f
, m
, modEq
, modInst
, imtio
) ){
200 addInstMatch2( qe
, f
, m
, 0, imtio
);
208 }/* CVC4::theory::inst namespace */
209 }/* CVC4::theory namespace */
210 }/* CVC4 namespace */