summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/inst_match.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/inst_match.cpp')
-rw-r--r--src/theory/quantifiers/inst_match.cpp256
1 files changed, 65 insertions, 191 deletions
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 8d472879e..e72e19119 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -27,55 +27,33 @@ namespace CVC4 {
namespace theory {
namespace inst {
-InstMatch::InstMatch() {
-}
-
-InstMatch::InstMatch( InstMatch* m ) {
- d_map = m->d_map;
-}
-
-bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m, bool & st ){
- std::map< Node, Node >::iterator vn = d_map.find( v );
- if( !m.isNull() && !m.getType().isSubtypeOf( v.getType() ) ){
- st = false;
- return false;
- }else if( vn==d_map.end() || vn->second.isNull() ){
- st = true;
- set(v,m);
- Debug("matching-debug") << "Add partial " << v << "->" << m << std::endl;
- return true;
- }else{
- st = false;
- return q->areEqual( vn->second, m );
+InstMatch::InstMatch( Node f ) {
+ for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
+ d_vals.push_back( Node::null() );
}
}
-bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m ){
- bool set;
- return setMatch(q,v,m,set);
+InstMatch::InstMatch( InstMatch* m ) {
+ d_vals.insert( d_vals.end(), m->d_vals.begin(), m->d_vals.end() );
}
bool InstMatch::add( InstMatch& m ){
- for( std::map< Node, Node >::iterator it = m.d_map.begin(); it != m.d_map.end(); ++it ){
- if( !it->second.isNull() ){
- std::map< Node, Node >::iterator itf = d_map.find( it->first );
- if( itf==d_map.end() || itf->second.isNull() ){
- d_map[it->first] = it->second;
- }
+ for( unsigned i=0; i<d_vals.size(); i++ ){
+ if( d_vals[i].isNull() ){
+ d_vals[i] = m.d_vals[i];
}
}
return true;
}
bool InstMatch::merge( EqualityQuery* q, InstMatch& m ){
- for( std::map< Node, Node >::iterator it = m.d_map.begin(); it != m.d_map.end(); ++it ){
- if( !it->second.isNull() ){
- std::map< Node, Node >::iterator itf = d_map.find( it->first );
- if( itf==d_map.end() || itf->second.isNull() ){
- d_map[ it->first ] = it->second;
+ for( unsigned i=0; i<m.d_vals.size(); i++ ){
+ if( !m.d_vals[i].isNull() ){
+ if( d_vals[i].isNull() ){
+ d_vals[i] = m.d_vals[i];
}else{
- if( !q->areEqual( it->second, itf->second ) ){
- d_map.clear();
+ if( !q->areEqual( d_vals[i], m.d_vals[i]) ){
+ clear();
return false;
}
}
@@ -85,118 +63,83 @@ bool InstMatch::merge( EqualityQuery* q, InstMatch& m ){
}
void InstMatch::debugPrint( const char* c ){
- for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
- Debug( c ) << " " << it->first << " -> " << it->second << std::endl;
+ for( unsigned i=0; i<d_vals.size(); i++ ){
+ if( !d_vals[i].isNull() ){
+ Debug( c ) << " " << i << " -> " << d_vals[i] << std::endl;
+ }
}
}
-void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){
- for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- Node ic = qe->getTermDatabase()->getInstantiationConstant( f, i );
- if( d_map.find( ic )==d_map.end() ){
- d_map[ ic ] = qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
+bool InstMatch::isComplete() {
+ for( unsigned i=0; i<d_vals.size(); i++ ){
+ if( d_vals[i].isNull() ){
+ return false;
}
}
+ return true;
}
-void InstMatch::makeRepresentative( QuantifiersEngine* qe ){
- for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
- if( qe->getEqualityQuery()->getEngine()->hasTerm( it->second ) ){
- d_map[ it->first ] = qe->getEqualityQuery()->getEngine()->getRepresentative( it->second );
+bool InstMatch::empty() {
+ for( unsigned i=0; i<d_vals.size(); i++ ){
+ if( !d_vals[i].isNull() ){
+ return false;
}
}
+ return true;
}
-void InstMatch::applyRewrite(){
- for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
- it->second = Rewriter::rewrite(it->second);
+void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){
+ for( unsigned i=0; i<d_vals.size(); i++ ){
+ if( d_vals[i].isNull() ){
+ Node ic = qe->getTermDatabase()->getInstantiationConstant( f, i );
+ d_vals[i] = qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
+ }
}
}
-/** get value */
-Node InstMatch::getValue( Node var ) const{
- std::map< Node, Node >::const_iterator it = d_map.find( var );
- if( it!=d_map.end() ){
- return it->second;
- }else{
- return Node::null();
+void InstMatch::makeRepresentative( QuantifiersEngine* qe ){
+ for( unsigned i=0; i<d_vals.size(); i++ ){
+ if( !d_vals[i].isNull() ){
+ if( qe->getEqualityQuery()->getEngine()->hasTerm( d_vals[i] ) ){
+ d_vals[i] = qe->getEqualityQuery()->getEngine()->getRepresentative( d_vals[i] );
+ }
+ }
}
}
-Node InstMatch::get( QuantifiersEngine* qe, Node f, int i ) {
- return get( qe->getTermDatabase()->getInstantiationConstant( f, i ) );
-}
-
-void InstMatch::set(TNode var, TNode n){
- Assert( !var.isNull() );
- if (Trace.isOn("inst-match-warn")) {
- if( !n.isNull() && !n.getType().isSubtypeOf( var.getType() ) ){
- Trace("inst-match-warn") << quantifiers::TermDb::getInstConstAttr(var) << std::endl;
- Trace("inst-match-warn") << var << " " << var.getType() << " " << n << " " << n.getType() << std::endl ;
+void InstMatch::applyRewrite(){
+ for( unsigned i=0; i<d_vals.size(); i++ ){
+ if( !d_vals[i].isNull() ){
+ d_vals[i] = Rewriter::rewrite( d_vals[i] );
}
}
- Assert( n.isNull() || n.getType().isSubtypeOf( var.getType() ) );
- d_map[var] = n;
}
-void InstMatch::set( QuantifiersEngine* qe, Node f, int i, TNode n ) {
- set( qe->getTermDatabase()->getInstantiationConstant( f, i ), n );
+void InstMatch::clear() {
+ for( unsigned i=0; i<d_vals.size(); i++ ){
+ d_vals[i] = Node::null();
+ }
}
+/** get value */
+Node InstMatch::get( int i ) {
+ return d_vals[i];
+}
-bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m,
- bool modEq, bool modInst, ImtIndexOrder* imtio, bool onlyExist, int index ){
- if( index==(int)f[0].getNumChildren() || ( imtio && index==(int)imtio->d_order.size() ) ){
- return false;
- }else{
- int i_index = imtio ? imtio->d_order[index] : index;
- Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) );
- std::map< Node, InstMatchTrie >::iterator it = d_data.find( n );
- if( it!=d_data.end() ){
- bool ret = it->second.addInstMatch( qe, f, m, modEq, modInst, imtio, onlyExist, index+1 );
- if( !onlyExist || !ret ){
- return ret;
- }
- }
- /*
- //check if m is an instance of another instantiation if modInst is true
- if( modInst ){
- if( !n.isNull() ){
- Node nl;
- std::map< Node, InstMatchTrie >::iterator itm = d_data.find( nl );
- if( itm!=d_data.end() ){
- if( !itm->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){
- return false;
- }
- }
- }
- }
- */
- /*
- if( modEq ){
- //check modulo equality if any other instantiation match exists
- if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
- eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
- qe->getEqualityQuery()->getEngine() );
- while( !eqc.isFinished() ){
- Node en = (*eqc);
- if( en!=n ){
- std::map< Node, InstMatchTrie >::iterator itc = d_data.find( en );
- if( itc!=d_data.end() ){
- if( itc->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){
- return false;
- }
- }
- }
- ++eqc;
- }
- }
- }
-*/
- if( !onlyExist ){
- d_data[n].addInstMatch( qe, f, m, modEq, modInst, imtio, false, index+1 );
+void InstMatch::setValue( int i, TNode n ) {
+ d_vals[i] = n;
+}
+
+bool InstMatch::set( QuantifiersEngine* qe, int i, TNode n ) {
+ if( !d_vals[i].isNull() ){
+ if( qe->getEqualityQuery()->areEqual( d_vals[i], n ) ){
+ return true;
+ }else{
+ return false;
}
+ }else{
+ d_vals[i] = n;
return true;
}
}
@@ -229,7 +172,6 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No
}
}
*/
- /*
if( modEq ){
//check modulo equality if any other instantiation match exists
if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
@@ -249,7 +191,6 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No
}
}
}
- */
if( !onlyExist ){
d_data[n].addInstMatch( qe, f, m, modEq, modInst, imtio, false, index+1 );
}
@@ -257,73 +198,6 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No
}
}
-/** exists match */
-bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m,
- context::Context* c, bool modEq, bool modInst, int index, bool onlyExist ){
- bool reset = false;
- if( !d_valid.get() ){
- if( onlyExist ){
- return true;
- }else{
- d_valid.set( true );
- reset = true;
- }
- }
- if( index==(int)f[0].getNumChildren() ){
- return false;
- }else{
- Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, index ) );
- std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
- if( it!=d_data.end() ){
- bool ret = it->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, onlyExist );
- if( !onlyExist || !ret ){
- return reset || ret;
- }
- }
- //check if m is an instance of another instantiation if modInst is true
- /*
- if( modInst ){
- if( !n.isNull() ){
- Node nl;
- std::map< Node, CDInstMatchTrie* >::iterator itm = d_data.find( nl );
- if( itm!=d_data.end() ){
- if( !itm->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, true ) ){
- return false;
- }
- }
- }
- }
- */
- if( modEq ){
- //check modulo equality if any other instantiation match exists
- if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
- eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
- qe->getEqualityQuery()->getEngine() );
- while( !eqc.isFinished() ){
- Node en = (*eqc);
- if( en!=n ){
- std::map< Node, CDInstMatchTrie* >::iterator itc = d_data.find( en );
- if( itc!=d_data.end() ){
- if( itc->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, true ) ){
- return false;
- }
- }
- }
- ++eqc;
- }
- }
- }
-
- if( !onlyExist ){
- std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
- CDInstMatchTrie* imt = new CDInstMatchTrie( c );
- d_data[n] = imt;
- imt->addInstMatch( qe, f, m, c, modEq, modInst, index+1, false );
- }
- return true;
- }
-}
-
bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m,
context::Context* c, bool modEq, bool modInst, int index, bool onlyExist ){
bool reset = false;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback