}
}else{
//just add the instance
- InstMatch m;
- for( unsigned j=0; j<inst.size(); j++) {
- m.set( d_qe, f, j, inst[j] );
- }
d_triedLemmas++;
- if( d_qe->addInstantiation( f, m ) ){
+ if( d_qe->addInstantiation( f, inst ) ){
Trace("fmc-debug-inst") << "** Added instantiation." << std::endl;
d_addedLemmas++;
}else{
Trace("fmc-exh-debug") << ", index = " << ev_index << " / " << d_quant_models[f].d_value.size();
Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index];
if (ev!=d_true) {
- InstMatch m;
- for( unsigned i=0; i<inst.size(); i++ ){
- m.set( d_qe, f, i, inst[i] );
- }
Trace("fmc-exh-debug") << ", add!";
//add as instantiation
- if( d_qe->addInstantiation( f, m ) ){
+ if( d_qe->addInstantiation( f, inst ) ){
Trace("fmc-exh-debug") << " ...success.";
addedLemmas++;
}else{
d_map = m->d_map;
}
-bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m, bool & set ){
+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() ) ){
- set = false;
+ st = false;
return false;
}else if( vn==d_map.end() || vn->second.isNull() ){
- set = true;
- this->set(v,m);
+ st = true;
+ set(v,m);
Debug("matching-debug") << "Add partial " << v << "->" << m << std::endl;
return true;
}else{
- set = false;
+ st = false;
return q->areEqual( vn->second, m );
}
}
for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
Debug( c ) << " " << it->first << " -> " << it->second << std::endl;
}
- //if( !d_splits.empty() ){
- // Debug( c ) << " Conditions: ";
- // for( std::map< Node, Node >::iterator it = d_splits.begin(); it !=d_splits.end(); ++it ){
- // Debug( c ) << it->first << " = " << it->second << " ";
- // }
- // Debug( c ) << std::endl;
- //}
}
void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){
}
}
-//void InstMatch::makeInternalRepresentative( QuantifiersEngine* qe ){
-// EqualityQueryQuantifiersEngine* eqqe = (EqualityQueryQuantifiersEngine*)qe->getEqualityQuery();
-// for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
-// d_map[ it->first ] = eqqe->getInternalRepresentative( it->second );
-// }
-//}
-
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 ) ){
void InstMatch::set(TNode var, TNode n){
Assert( !var.isNull() );
if (Trace.isOn("inst-match-warn")) {
- // For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations
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 InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio ){
- if( long(index)<long(f[0].getNumChildren()) && ( !imtio || long(index)<long(imtio->d_order.size()) ) ){
- int i_index = imtio ? imtio->d_order[index] : index;
- Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) );
- d_data[n].addInstMatch2( qe, f, m, index+1, imtio );
- }
-}
-
-bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio ){
- if( long(index)==long(f[0].getNumChildren()) || ( imtio && long(index)==long(imtio->d_order.size()) ) ){
- return true;
+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() ){
- if( it->second.existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
- return true;
+ 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;
- it = d_data.find( nl );
- if( it!=d_data.end() ){
- if( it->second.existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
- return true;
+ 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 ) ){
if( en!=n ){
std::map< Node, InstMatchTrie >::iterator itc = d_data.find( en );
if( itc!=d_data.end() ){
- if( itc->second.existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
- return true;
+ if( itc->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){
+ return false;
}
}
}
}
}
}
- return false;
- }
-}
-
-bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, ImtIndexOrder* imtio ){
- return existsInstMatch2( qe, f, m, modEq, modInst, 0, imtio );
-}
-
-bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, ImtIndexOrder* imtio ){
- if( !existsInstMatch( qe, f, m, modEq, modInst, imtio ) ){
- addInstMatch2( qe, f, m, 0, imtio );
+*/
+ if( !onlyExist ){
+ d_data[n].addInstMatch( qe, f, m, modEq, modInst, imtio, false, index+1 );
+ }
return true;
- }else{
- return false;
}
}
-*/
-
-
-
-bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, ImtIndexOrder* imtio, bool onlyExist, int index ){
+bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& 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 ) );
+ Node n = m[i_index];
std::map< Node, InstMatchTrie >::iterator it = d_data.find( n );
if( it!=d_data.end() ){
- return it->second.addInstMatch( qe, f, m, modEq, modInst, imtio, onlyExist, index+1 );
- }else{
-
- /*
- //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;
- }
+ 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;
- }
+ }
+ */
+ /*
+ 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;
}
+ ++eqc;
}
}
- */
- if( !onlyExist ){
- d_data[n].addInstMatch( qe, f, m, modEq, modInst, imtio, false, index+1 );
- }
- return true;
}
+ */
+ if( !onlyExist ){
+ d_data[n].addInstMatch( qe, f, m, modEq, modInst, imtio, false, index+1 );
+ }
+ return true;
}
}
-
-
/** exists match */
-bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq, bool modInst, int index, bool onlyExist ){
+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 false;
+ return true;
}else{
d_valid.set( true );
+ reset = true;
}
}
if( index==(int)f[0].getNumChildren() ){
- return true;
+ return false;
}else{
Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, index ) );
- if( onlyExist ){
- std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
- if( it!=d_data.end() ){
- if( !it->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, true ) ){
- return false;
- }
+ 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;
}
}
}
+ */
if( modEq ){
//check modulo equality if any other instantiation match exists
if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
}
}
}
+
if( !onlyExist ){
std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
- CDInstMatchTrie* imt;
- if( it!=d_data.end() ){
- imt = it->second;
- it->second->d_valid.set( true );
- }else{
- imt = new CDInstMatchTrie( c );
- d_data[n] = imt;
- }
- return imt->addInstMatch( qe, f, m, c, modEq, modInst, index+1, false );
+ 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;
+ 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[ 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;
}
}
/** set the match of v to m */
bool setMatch( EqualityQuery* q, TNode v, TNode m );
/* This version tell if the variable has been set */
- bool setMatch( EqualityQuery* q, TNode v, TNode m, bool & set);
+ bool setMatch( EqualityQuery* q, TNode v, TNode m, bool & st);
/** fill all unfilled values with m */
bool add( InstMatch& m );
/** if compatible, fill all unfilled values with m and return true
bool modInst = false, ImtIndexOrder* imtio = NULL, int index = 0 ) {
return !addInstMatch( qe, f, m, modEq, modInst, imtio, true, index );
}
+ bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
+ bool modInst = false, ImtIndexOrder* imtio = NULL, int index = 0 ) {
+ return !addInstMatch( qe, f, m, modEq, modInst, imtio, true, index );
+ }
/** add match m for quantifier f, take into account equalities if modEq = true,
if imtio is non-null, this is the order to add to trie
return true if successful
*/
bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
+ bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
+ bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
};/* class InstMatchTrie */
-
-#if 0
-
-/** trie for InstMatch objects */
-class CDInstMatchTrie {
-public:
- class ImtIndexOrder {
- public:
- std::vector< int > d_order;
- };/* class InstMatchTrie ImtIndexOrder */
-private:
- /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
- void addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, int index, ImtIndexOrder* imtio );
- /** exists match */
- bool existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio );
-public:
- /** the data */
- std::map< Node, CDInstMatchTrie* > d_data;
- /** is valid */
- context::CDO< bool > d_valid;
-public:
- CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){}
- ~CDInstMatchTrie(){}
-public:
- /** return true if m exists in this trie
- modEq is if we check modulo equality
- modInst is if we return true if m is an instance of a match that exists
- */
- bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false,
- bool modInst = false, ImtIndexOrder* imtio = NULL );
- /** add match m for quantifier f, take into account equalities if modEq = true,
- if imtio is non-null, this is the order to add to trie
- return true if successful
- */
- bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false,
- bool modInst = false, ImtIndexOrder* imtio = NULL );
-};/* class CDInstMatchTrie */
-
-#else
-
-
/** trie for InstMatch objects */
class CDInstMatchTrie {
public:
bool modInst = false, int index = 0 ) {
return !addInstMatch( qe, f, m, c, modEq, modInst, index, true );
}
+ bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false,
+ bool modInst = false, int index = 0 ) {
+ return !addInstMatch( qe, f, m, c, modEq, modInst, index, true );
+ }
/** add match m for quantifier f, take into account equalities if modEq = true,
if imtio is non-null, this is the order to add to trie
return true if successful
*/
bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false,
bool modInst = false, int index = 0, bool onlyExist = false );
+ bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false,
+ bool modInst = false, int index = 0, bool onlyExist = false );
};/* class CDInstMatchTrie */
}
};/* class InstMatchTrieOrdered */
-#endif
-
-
}/* CVC4::theory::inst namespace */
typedef CVC4::theory::inst::InstMatch InstMatch;
if( success ){
index--;
//try instantiation
- InstMatch m;
+ std::vector< Node > terms;
for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
- m.set( d_quantEngine, f, i, rd->getRDomain( f, i )->d_terms[childIndex[i]] );
+ terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] );
}
- if( d_quantEngine->addInstantiation( f, m, true, false, false ) ){
+ if( d_quantEngine->addInstantiation( f, terms, false ) ){
++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
return STATUS_UNKNOWN;
}
//try to add it
Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl;
//add model basis instantiation
- if( d_qe->addInstantiation( fp, d_quant_basis_match[f], false, false, false ) ){
+ if( d_qe->addInstantiation( fp, d_quant_basis_match[f], false ) ){
d_quant_basis_match_added[f] = true;
return 1;
}else{
if( fmqint->d_var_order[q]->getInstantiation( fmqint, l, u, inst ) ){\r
Trace("qint-inst") << "** Instantiate with ";\r
//just add the instance\r
- InstMatch m;\r
for( unsigned j=0; j<inst.size(); j++) {\r
- m.set( d_qe, q, j, inst[j] );\r
Trace("qint-inst") << inst[j] << " ";\r
}\r
Trace("qint-inst") << std::endl;\r
d_triedLemmas++;\r
- if( d_qe->addInstantiation( q, m ) ){\r
+ if( d_qe->addInstantiation( q, inst ) ){\r
Trace("qint-inst") << " ...added instantiation." << std::endl;\r
d_addedLemmas++;\r
}else{\r
}\r
\r
\r
+void QuantInfo::initialize( Node q ) {\r
+ d_q = q;\r
+ for( unsigned i=0; i<q[0].getNumChildren(); i++ ){\r
+ d_match.push_back( TNode::null() );\r
+ d_match_term.push_back( TNode::null() );\r
+ }\r
+}\r
+\r
void QuantInfo::reset_round( QuantConflictFind * p ) {\r
- d_match.clear();\r
- d_match_term.clear();\r
+ for( unsigned i=0; i<d_match.size(); i++ ){\r
+ d_match[i] = TNode::null();\r
+ d_match_term[i] = TNode::null();\r
+ }\r
d_curr_var_deq.clear();\r
//add built-in variable constraints\r
for( unsigned r=0; r<2; r++ ){\r
}\r
\r
int QuantInfo::getCurrentRepVar( int v ) {\r
- std::map< int, TNode >::iterator it = d_match.find( v );\r
- if( it!=d_match.end() ){\r
- int vn = getVarNum( it->second );\r
+ if( v!=-1 && !d_match[v].isNull() ){\r
+ int vn = getVarNum( d_match[v] );\r
if( vn!=-1 ){\r
//int vr = getCurrentRepVar( vn );\r
//d_match[v] = d_vars[vr];\r
if( v==-1 ){\r
return n;\r
}else{\r
- std::map< int, TNode >::iterator it = d_match.find( v );\r
- if( it==d_match.end() ){\r
+ if( d_match[v].isNull() ){\r
return n;\r
}else{\r
- Assert( getVarNum( it->second )!=v );\r
- return getCurrentValue( it->second );\r
+ Assert( getVarNum( d_match[v] )!=v );\r
+ return getCurrentValue( d_match[v] );\r
}\r
}\r
}\r
if( doRemove ){\r
if( vn!=-1 ){\r
//if set to this in the opposite direction, clean up opposite instead\r
- std::map< int, TNode >::iterator itmn = d_match.find( vn );\r
- if( itmn!=d_match.end() && itmn->second==d_vars[v] ){\r
+ // std::map< int, TNode >::iterator itmn = d_match.find( vn );\r
+ if( d_match[vn]==d_vars[v] ){\r
return addConstraint( p, vn, d_vars[v], v, true, true );\r
}else{\r
//unsetting variables equal\r
}\r
}\r
}\r
- d_match.erase( v );\r
+ d_match[v] = TNode::null();\r
return 1;\r
}else{\r
- std::map< int, TNode >::iterator itm = d_match.find( v );\r
+ //std::map< int, TNode >::iterator itm = d_match.find( v );\r
\r
if( vn!=-1 ){\r
Debug("qcf-match-debug") << " ...Variable bound to variable" << std::endl;\r
- std::map< int, TNode >::iterator itmn = d_match.find( vn );\r
- if( itm==d_match.end() ){\r
+ //std::map< int, TNode >::iterator itmn = d_match.find( vn );\r
+ if( d_match[v].isNull() ){\r
//setting variables equal\r
bool alreadySet = false;\r
- if( itmn!=d_match.end() ){\r
+ if( !d_match[vn].isNull() ){\r
alreadySet = true;\r
- Assert( !itmn->second.isNull() && !isVar( itmn->second ) );\r
+ Assert( !isVar( d_match[vn] ) );\r
}\r
\r
//copy or check disequalities\r
d_curr_var_deq[vn][dv] = v;\r
}\r
}else{\r
- if( !p->areMatchDisequal( itmn->second, dv ) ){\r
+ if( !p->areMatchDisequal( d_match[vn], dv ) ){\r
Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl;\r
return -1;\r
}\r
n = getCurrentValue( n );\r
}\r
}else{\r
- if( itmn==d_match.end() ){\r
+ if( d_match[vn].isNull() ){\r
Debug("qcf-match-debug") << " ...Reverse direction" << std::endl;\r
//set the opposite direction\r
return addConstraint( p, vn, d_vars[v], v, true, false );\r
}else{\r
Debug("qcf-match-debug") << " -> Both variables bound, compare" << std::endl;\r
//are they currently equal\r
- return p->areMatchEqual( itm->second, itmn->second ) ? 0 : -1;\r
+ return p->areMatchEqual( d_match[v], d_match[vn] ) ? 0 : -1;\r
}\r
}\r
}else{\r
Debug("qcf-match-debug") << " ...Variable bound to ground" << std::endl;\r
- if( itm==d_match.end() ){\r
-\r
+ if( d_match[v].isNull() ){\r
}else{\r
//compare ground values\r
- Debug("qcf-match-debug") << " -> Ground value, compare " << itm->second << " "<< n << std::endl;\r
- return p->areMatchEqual( itm->second, n ) ? 0 : -1;\r
+ Debug("qcf-match-debug") << " -> Ground value, compare " << d_match[v] << " "<< n << std::endl;\r
+ return p->areMatchEqual( d_match[v], n ) ? 0 : -1;\r
}\r
}\r
if( setMatch( p, v, n ) ){\r
}else{\r
if( d_curr_var_deq[v].find( n )==d_curr_var_deq[v].end() ){\r
//check if it respects equality\r
- std::map< int, TNode >::iterator itm = d_match.find( v );\r
- if( itm!=d_match.end() ){\r
+ //std::map< int, TNode >::iterator itm = d_match.find( v );\r
+ if( !d_match[v].isNull() ){\r
TNode nv = getCurrentValue( n );\r
- if( !p->areMatchDisequal( nv, itm->second ) ){\r
+ if( !p->areMatchDisequal( nv, d_match[v] ) ){\r
Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl;\r
return -1;\r
}\r
return true;\r
}else{\r
Node vv = getVar( v );\r
- for( std::map< int, TNode >::iterator it = d_match.begin(); it != d_match.end(); ++it ){\r
- if( it->second==vv ){\r
+ //for( std::map< int, TNode >::iterator it = d_match.begin(); it != d_match.end(); ++it ){\r
+ for( unsigned i=0; i<d_match.size(); i++ ){\r
+ if( d_match[i]==vv ){\r
return true;\r
}\r
}\r
\r
bool QuantInfo::isMatchSpurious( QuantConflictFind * p ) {\r
for( int i=0; i<getNumVars(); i++ ){\r
- std::map< int, TNode >::iterator it = d_match.find( i );\r
- if( it!=d_match.end() ){\r
- if( !getCurrentCanBeEqual( p, i, it->second, p->d_effort==QuantConflictFind::effort_conflict ) ){\r
+ //std::map< int, TNode >::iterator it = d_match.find( i );\r
+ if( !d_match[i].isNull() ){\r
+ if( !getCurrentCanBeEqual( p, i, d_match[i], p->d_effort==QuantConflictFind::effort_conflict ) ){\r
return true;\r
}\r
}\r
std::vector< int > unassigned[2];\r
std::vector< TypeNode > unassigned_tn[2];\r
for( int i=0; i<getNumVars(); i++ ){\r
- if( d_match.find( i )==d_match.end() ){\r
+ if( d_match[i].isNull() ){\r
//Assert( i<(int)q[0].getNumChildren() );\r
int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;\r
unassigned[rindex].push_back( i );\r
Trace("qcf-check-unassign") << " Try: " << std::endl;\r
for( unsigned i=0; i<unassigned[r].size(); i++ ){\r
int ui = unassigned[r][i];\r
- if( d_match.find( ui )!=d_match.end() ){\r
+ if( !d_match[ui].isNull() ){\r
Trace("qcf-check-unassign") << " Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;\r
}\r
}\r
return true;\r
}else{\r
for( unsigned i=0; i<assigned.size(); i++ ){\r
- d_match.erase( assigned[i] );\r
+ d_match[ assigned[i] ] = TNode::null();\r
}\r
assigned.clear();\r
return false;\r
void QuantInfo::debugPrintMatch( const char * c ) {\r
for( int i=0; i<getNumVars(); i++ ){\r
Trace(c) << " " << d_vars[i] << " -> ";\r
- if( d_match.find( i )!=d_match.end() ){\r
+ if( !d_match[i].isNull() ){\r
Trace(c) << d_match[i];\r
}else{\r
Trace(c) << "(unassigned) ";\r
for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){\r
Debug("qcf-match") << " Clean up bound var " << it->second << std::endl;\r
Assert( it->second<qi->getNumVars() );\r
- qi->d_match.erase( it->second );\r
- qi->d_match_term.erase( it->second );\r
+ qi->d_match[ it->second ] = TNode::null();\r
+ qi->d_match_term[ it->second ] = TNode::null();\r
}\r
d_qni_bound.clear();\r
}\r
int repVar = qi->getCurrentRepVar( itv->second );\r
Debug("qcf-match-debug") << " Match " << index << " is a variable " << itv->second << ", which is repVar " << repVar << std::endl;\r
//get the value the rep variable\r
- std::map< int, TNode >::iterator itm = qi->d_match.find( repVar );\r
- if( itm!=qi->d_match.end() ){\r
- val = itm->second;\r
- Assert( !val.isNull() );\r
+ //std::map< int, TNode >::iterator itm = qi->d_match.find( repVar );\r
+ if( !qi->d_match[repVar].isNull() ){\r
+ val = qi->d_match[repVar];\r
Debug("qcf-match-debug") << " Variable is already bound to " << val << std::endl;\r
}else{\r
//binding a variable\r
for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){\r
Debug("qcf-match-debug") << " position " << it->first << " bounded " << it->second << " / " << qi->d_q[0].getNumChildren() << std::endl;\r
if( it->second<(int)qi->d_q[0].getNumChildren() && it->first>0 ){ //if it is an actual variable, we are interested in knowing the actual term\r
- Assert( qi->d_match.find( it->second )!=qi->d_match.end() );\r
+ Assert( !qi->d_match[ it->second ].isNull() );\r
Assert( p->areEqual( t[it->first-1], qi->d_match[ it->second ] ) );\r
qi->d_match_term[it->second] = t[it->first-1];\r
}\r
//Trace("qcf-qregister") << " Flatten term " << n[i] << std::endl;\r
d_qinfo[q].d_var_num[n] = d_qinfo[q].d_vars.size();\r
d_qinfo[q].d_vars.push_back( n );\r
+ d_qinfo[q].d_match.push_back( TNode::null() );\r
+ d_qinfo[q].d_match_term.push_back( TNode::null() );\r
}\r
for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
flatten( q, n[i] );\r
void QuantConflictFind::registerQuantifier( Node q ) {\r
d_quants.push_back( q );\r
d_quant_id[q] = d_quants.size();\r
- d_qinfo[q].d_q = q;\r
+ d_qinfo[q].initialize( q );\r
Trace("qcf-qregister") << "Register ";\r
debugPrintQuant( "qcf-qregister", q );\r
Trace("qcf-qregister") << " : " << q << std::endl;\r
if( !qi->isMatchSpurious( this ) ){\r
std::vector< int > assigned;\r
if( qi->completeMatch( this, assigned ) ){\r
- InstMatch m;\r
+ std::vector< Node > terms;\r
for( unsigned i=0; i<q[0].getNumChildren(); i++ ){\r
//Node cv = qi->getCurrentValue( qi->d_match[i] );\r
int repVar = qi->getCurrentRepVar( i );\r
Node cv;\r
- std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar );\r
- if( itmt!=qi->d_match_term.end() ){\r
- cv = itmt->second;\r
+ //std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar );\r
+ if( !qi->d_match_term[repVar].isNull() ){\r
+ cv = qi->d_match_term[repVar];\r
}else{\r
cv = qi->d_match[repVar];\r
}\r
-\r
-\r
Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << qi->d_match[i] << std::endl;\r
- m.set( d_quantEngine, q, i, cv );\r
+ terms.push_back( cv );\r
}\r
if( Debug.isOn("qcf-check-inst") ){\r
//if( e==effort_conflict ){\r
- Node inst = d_quantEngine->getInstantiation( q, m );\r
+ Node inst = d_quantEngine->getInstantiation( q, terms );\r
Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;\r
Assert( evaluate( inst )!=1 );\r
Assert( evaluate( inst )==-1 || e>effort_conflict );\r
//}\r
}\r
- if( d_quantEngine->addInstantiation( q, m ) ){\r
+ if( d_quantEngine->addInstantiation( q, terms ) ){\r
Trace("qcf-check") << " ... Added instantiation" << std::endl;\r
++addedLemmas;\r
if( e==effort_conflict ){\r
}\r
//clean up assigned\r
for( unsigned i=0; i<assigned.size(); i++ ){\r
- qi->d_match.erase( assigned[i] );\r
+ qi->d_match[ assigned[i] ] = TNode::null();\r
}\r
}else{\r
Trace("qcf-check") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;\r
std::map< int, MatchGen * > d_var_mg;\r
void reset_round( QuantConflictFind * p );\r
public:\r
+ //initialize\r
+ void initialize( Node q );\r
//current constraints\r
- std::map< int, TNode > d_match;\r
- std::map< int, TNode > d_match_term;\r
+ std::vector< TNode > d_match;\r
+ std::vector< TNode > d_match_term;\r
std::map< int, std::map< TNode, int > > d_curr_var_deq;\r
int getCurrentRepVar( int v );\r
TNode getCurrentValue( TNode n );\r
}
}
-bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool modInst, bool mkRep ){
- Trace("inst-add-debug") << "Add instantiation: " << m << std::endl;
+bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool mkRep, bool modEq, bool modInst ){
+ std::vector< Node > terms;
//make sure there are values for each variable we are instantiating
for( size_t i=0; i<f[0].getNumChildren(); i++ ){
Node ic = d_term_db->getInstantiationConstant( f, i );
if( val.isNull() ){
val = d_term_db->getFreeVariableForInstConstant( ic );
Trace("inst-add-debug") << "mkComplete " << val << std::endl;
- m.set( ic, val );
}
+ terms.push_back( val );
+ }
+ return addInstantiation( f, terms, mkRep, modEq, modInst );
+}
+
+bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst ) {
+ Assert( terms.size()==f[0].getNumChildren() );
+ Trace("inst-add-debug") << "Add instantiation: ";
+ for( unsigned i=0; i<terms.size(); i++ ){
+ if( i>0 ) Trace("inst-add-debug") << ", ";
+ Trace("inst-add-debug") << f[0][i] << " -> " << terms[i];
//make it representative, this is helpful for recognizing duplication
if( mkRep ){
//pick the best possible representative for instantiation, based on past use and simplicity of term
- Node r = d_eq_query->getInternalRepresentative( val, f, i );
- Trace("inst-add-debug") << "mkRep " << r << " " << val << std::endl;
- m.set( ic, r );
+ terms[i] = d_eq_query->getInternalRepresentative( terms[i], f, i );
+ //Trace("inst-add-debug") << " (" << terms[i] << ")";
}
}
- //check for duplication modulo equality
+ Trace("inst-add-debug") << std::endl;
+
+ //check for duplication
bool alreadyExists = false;
///*
- Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
if( options::incrementalSolving() ){
+ Trace("inst-add-debug") << "Adding into context-dependent inst trie" << std::endl;
inst::CDInstMatchTrie* imt;
std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( f );
if( it!=d_c_inst_match_trie.end() ){
imt = new CDInstMatchTrie( getUserContext() );
d_c_inst_match_trie[f] = imt;
}
- alreadyExists = !imt->addInstMatch( this, f, m, getUserContext(), modEq, modInst );
+ alreadyExists = !imt->addInstMatch( this, f, terms, getUserContext(), modEq, modInst );
}else{
- alreadyExists = !d_inst_match_trie[f].addInstMatch( this, f, m, modEq, modInst );
+ Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
+ alreadyExists = !d_inst_match_trie[f].addInstMatch( this, f, terms, modEq, modInst );
}
- //*/
if( alreadyExists ){
- Trace("inst-add-debug") << " -> Already exists." << std::endl;
- ++(d_statistics.d_inst_duplicate_eq);
- return false;
- }
- Trace("inst-add-debug") << "compute terms" << std::endl;
- //compute the vector of terms for the instantiation
- std::vector< Node > terms;
- for( size_t i=0; i<d_term_db->d_inst_constants[f].size(); i++ ){
- Node n = m.getValue( d_term_db->d_inst_constants[f][i] );
- Assert( !n.isNull() );
- terms.push_back( n );
+ Trace("inst-add-debug") << " -> Already exists." << std::endl;
+ ++(d_statistics.d_inst_duplicate_eq);
+ return false;
}
+
//add the instantiation
bool addedInst = addInstantiation( f, d_term_db->d_vars[f], terms );
//report the result
if( addedInst ){
- Trace("inst-add") << "Added instantiation for " << f << ": " << std::endl;
- Trace("inst-add") << " " << m << std::endl;
Trace("inst-add-debug") << " -> Success." << std::endl;
return true;
}else{
}
}
+
bool QuantifiersEngine::addSplit( Node n, bool reqPhase, bool reqPhasePol ){
n = Rewriter::rewrite( n );
Node lem = NodeManager::currentNM()->mkNode( OR, n, n.notNode() );
/** add lemma lem */
bool addLemma( Node lem );
/** do instantiation specified by m */
- bool addInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false, bool mkRep = true );
+ bool addInstantiation( Node f, InstMatch& m, bool mkRep = true, bool modEq = false, bool modInst = false );
+ /** add instantiation */
+ bool addInstantiation( Node f, std::vector< Node >& terms, bool mkRep = true, bool modEq = false, bool modInst = false );
/** split on node n */
bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true );
/** add split equality */
projects / cvc5.git / commitdiff