1 /********************* */
2 /*! \file inst_match.cpp
4 ** Original author: Morgan Deters
5 ** Major contributors: Andrew Reynolds
6 ** Minor contributors (to current version): Clark Barrett, Francois Bobot
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 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( Node 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::setValue( int i
, TNode n
) {
134 bool InstMatch::set( QuantifiersEngine
* qe
, int i
, TNode n
) {
135 if( !d_vals
[i
].isNull() ){
136 if( qe
->getEqualityQuery()->areEqual( d_vals
[i
], n
) ){
147 bool InstMatchTrie::addInstMatch( QuantifiersEngine
* qe
, Node f
, std::vector
< Node
>& m
, bool modEq
,
148 bool modInst
, ImtIndexOrder
* imtio
, bool onlyExist
, int index
) {
149 if( index
==(int)f
[0].getNumChildren() || ( imtio
&& index
==(int)imtio
->d_order
.size() ) ){
152 int i_index
= imtio
? imtio
->d_order
[index
] : index
;
154 std::map
< Node
, InstMatchTrie
>::iterator it
= d_data
.find( n
);
155 if( it
!=d_data
.end() ){
156 bool ret
= it
->second
.addInstMatch( qe
, f
, m
, modEq
, modInst
, imtio
, onlyExist
, index
+1 );
157 if( !onlyExist
|| !ret
){
162 //check if m is an instance of another instantiation if modInst is true
166 std::map< Node, InstMatchTrie >::iterator itm = d_data.find( nl );
167 if( itm!=d_data.end() ){
168 if( !itm->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){
176 //check modulo equality if any other instantiation match exists
177 if( !n
.isNull() && qe
->getEqualityQuery()->getEngine()->hasTerm( n
) ){
178 eq::EqClassIterator
eqc( qe
->getEqualityQuery()->getEngine()->getRepresentative( n
),
179 qe
->getEqualityQuery()->getEngine() );
180 while( !eqc
.isFinished() ){
183 std::map
< Node
, InstMatchTrie
>::iterator itc
= d_data
.find( en
);
184 if( itc
!=d_data
.end() ){
185 if( itc
->second
.addInstMatch( qe
, f
, m
, modEq
, modInst
, imtio
, true, index
+1 ) ){
195 d_data
[n
].addInstMatch( qe
, f
, m
, modEq
, modInst
, imtio
, false, index
+1 );
201 void InstMatchTrie::print( const char * c
, Node q
, std::vector
< Node
>& terms
) const {
202 if( terms
.size()==q
[0].getNumChildren() ){
204 for( unsigned i
=0; i
<terms
.size(); i
++ ){
205 if( i
>0 ) Trace(c
) << ", ";
206 Trace(c
) << terms
[i
];
208 Trace(c
) << " )" << std::endl
;
210 for( std::map
< Node
, InstMatchTrie
>::const_iterator it
= d_data
.begin(); it
!= d_data
.end(); ++it
){
211 terms
.push_back( it
->first
);
212 it
->second
.print( c
, q
, terms
);
219 bool CDInstMatchTrie::addInstMatch( QuantifiersEngine
* qe
, Node f
, std::vector
< Node
>& m
,
220 context::Context
* c
, bool modEq
, bool modInst
, int index
, bool onlyExist
){
222 if( !d_valid
.get() ){
230 if( index
==(int)f
[0].getNumChildren() ){
234 std::map
< Node
, CDInstMatchTrie
* >::iterator it
= d_data
.find( n
);
235 if( it
!=d_data
.end() ){
236 bool ret
= it
->second
->addInstMatch( qe
, f
, m
, c
, modEq
, modInst
, index
+1, onlyExist
);
237 if( !onlyExist
|| !ret
){
241 //check if m is an instance of another instantiation if modInst is true
246 std::map< Node, CDInstMatchTrie* >::iterator itm = d_data.find( nl );
247 if( itm!=d_data.end() ){
248 if( !itm->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, true ) ){
256 //check modulo equality if any other instantiation match exists
257 if( !n
.isNull() && qe
->getEqualityQuery()->getEngine()->hasTerm( n
) ){
258 eq::EqClassIterator
eqc( qe
->getEqualityQuery()->getEngine()->getRepresentative( n
),
259 qe
->getEqualityQuery()->getEngine() );
260 while( !eqc
.isFinished() ){
263 std::map
< Node
, CDInstMatchTrie
* >::iterator itc
= d_data
.find( en
);
264 if( itc
!=d_data
.end() ){
265 if( itc
->second
->addInstMatch( qe
, f
, m
, c
, modEq
, modInst
, index
+1, true ) ){
276 // std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
277 CDInstMatchTrie
* imt
= new CDInstMatchTrie( c
);
279 imt
->addInstMatch( qe
, f
, m
, c
, modEq
, modInst
, index
+1, false );
285 void CDInstMatchTrie::print( const char * c
, Node q
, std::vector
< Node
>& terms
) const{
287 if( terms
.size()==q
[0].getNumChildren() ){
289 for( unsigned i
=0; i
<terms
.size(); i
++ ){
290 if( i
>0 ) Trace(c
) << ", ";
291 Trace(c
) << terms
[i
];
293 Trace(c
) << " )" << std::endl
;
295 for( std::map
< Node
, CDInstMatchTrie
* >::const_iterator it
= d_data
.begin(); it
!= d_data
.end(); ++it
){
296 terms
.push_back( it
->first
);
297 it
->second
->print( c
, q
, terms
);
304 }/* CVC4::theory::inst namespace */
305 }/* CVC4::theory namespace */
306 }/* CVC4 namespace */