}
}
bool CandidateGeneratorQE::isLegalOpCandidate( Node n ) {
- if( n.hasOperator() && n.getOperator()==d_op ){
+ if( n.hasOperator() ){
if( isLegalCandidate( n ) ){
- return true;
+ return d_qe->getTermDatabase()->getOperator( n )==d_op;
}
}
return false;
d_children_map[ i ] = count;
count++;
}
+ if( n[i].getKind()==INST_CONSTANT ){
+ d_var_num[i] = n[i].getAttribute(InstVarNumAttribute());
+ }
}
}
bool hadSuccess CVC4_UNUSED = false;
for( int t=(isSelected ? 0 : 1); t<2; t++ ){
if( t==0 || !n.getAttribute(NoMatchAttribute()) ){
- considerTermsMatch[t][n] = InstMatch();
+ considerTermsMatch[t][n] = InstMatch( f );
considerTermsSuccess[t][n] = true;
for( size_t j=0; j<d_node.getNumChildren(); j++ ){
if( d_children_map.find( j )==d_children_map.end() ){
if( t!=0 || !n[j].getAttribute(ModelBasisAttribute()) ){
if( d_node[j].getKind()==INST_CONSTANT ){
- if( !considerTermsMatch[t][n].setMatch( qe->getEqualityQuery(), d_node[j], n[j] ) ){
+ if( !considerTermsMatch[t][n].set( qe, d_var_num[j], n[j] ) ){
Trace("inst-gen-cm") << "fail match: " << n[j] << " is not equal to ";
- Trace("inst-gen-cm") << considerTermsMatch[t][n].getValue( d_node[j] ) << std::endl;
+ Trace("inst-gen-cm") << considerTermsMatch[t][n].get( d_var_num[j] ) << std::endl;
considerTermsSuccess[t][n] = false;
break;
}
//if this is an interpreted function
if( doProduct ){
//combining children matches
- InstMatch curr;
+ InstMatch curr( f );
std::vector< Node > terms;
calculateMatchesInterpreted( qe, f, curr, terms, 0 );
}else{
Assert( considerVal.size()==1 );
for( int i=0; i<(int)d_children.size(); i++ ){
for( int j=0; j<(int)d_children[ i ].getNumMatches(); j++ ){
- InstMatch m;
+ InstMatch m( f );
if( d_children[ i ].getMatch( qe->getEqualityQuery(), j, m ) ){
addMatchValue( qe, f, considerVal[0], m );
}
private:
//the node we are processing
Node d_node;
+ std::map< int, int > d_var_num;
//the sub children for this node
std::vector< InstGenProcess > d_children;
std::vector< int > d_children_index;
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;
}
}
}
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;
}
}
}
}
*/
- /*
if( modEq ){
//check modulo equality if any other instantiation match exists
if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
}
}
}
- */
if( !onlyExist ){
d_data[n].addInstMatch( qe, f, m, modEq, modInst, imtio, false, index+1 );
}
}
}
-/** 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;
/** basic class defining an instantiation */
class InstMatch {
+public:
/* map from variable to ground terms */
- std::map< Node, Node > d_map;
+ std::vector< Node > d_vals;
public:
- InstMatch();
+ InstMatch(){}
+ InstMatch( Node f );
InstMatch( InstMatch* m );
- /** 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 & st);
/** fill all unfilled values with m */
bool add( InstMatch& m );
/** if compatible, fill all unfilled values with m and return true
/** debug print method */
void debugPrint( const char* c );
/** is complete? */
- bool isComplete( Node f ) { return d_map.size()==f[0].getNumChildren(); }
+ bool isComplete();
/** make complete */
void makeComplete( Node f, QuantifiersEngine* qe );
- /** make internal representative */
- //void makeInternalRepresentative( QuantifiersEngine* qe );
/** make representative */
void makeRepresentative( QuantifiersEngine* qe );
- /** get value */
- Node getValue( Node var ) const;
+ /** empty */
+ bool empty();
/** clear */
- void clear(){ d_map.clear(); }
- /** is_empty */
- bool empty(){ return d_map.empty(); }
+ void clear();
/** to stream */
inline void toStream(std::ostream& out) const {
out << "INST_MATCH( ";
- for( std::map< Node, Node >::const_iterator it = d_map.begin(); it != d_map.end(); ++it ){
- if( it != d_map.begin() ){ out << ", "; }
- out << it->first << " -> " << it->second;
+ bool printed = false;
+ for( unsigned i=0; i<d_vals.size(); i++ ){
+ if( !d_vals[i].isNull() ){
+ if( printed ){ out << ", "; }
+ out << i << " -> " << d_vals[i];
+ printed = true;
+ }
}
out << " )";
}
-
-
- //for rewrite rules
-
/** apply rewrite */
void applyRewrite();
- /** erase */
- template<class Iterator>
- void erase(Iterator begin, Iterator end){
- for(Iterator i = begin; i != end; ++i){
- d_map.erase(*i);
- };
- }
- void erase(Node node){ d_map.erase(node); }
/** get */
- Node get( TNode var ) { return d_map[var]; }
- Node get( QuantifiersEngine* qe, Node f, int i );
+ Node get( int i );
/** set */
- void set(TNode var, TNode n);
- void set( QuantifiersEngine* qe, Node f, int i, TNode n );
- /** size */
- size_t size(){ return d_map.size(); }
- /* iterator */
- std::map< Node, Node >::iterator begin(){ return d_map.begin(); };
- std::map< Node, Node >::iterator end(){ return d_map.end(); };
- std::map< Node, Node >::iterator find(Node var){ return d_map.find(var); };
- /* Node used for matching the trigger only for mono-trigger (just for
- efficiency because I need only that) */
+ void setValue( int i, TNode n );
+ bool set( QuantifiersEngine* qe, int i, TNode n );
+ /* Node used for matching the trigger */
Node d_matched;
};/* class InstMatch */
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 modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ){
+ return addInstMatch( qe, f, m.d_vals, modEq, modInst, imtio, onlyExist, index );
+ }
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 */
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 modInst = false, int index = 0, bool onlyExist = false ) {
+ return addInstMatch( qe, f, m.d_vals, c, modEq, modInst, index, onlyExist );
+ }
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 */
}
}
Trace("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl;
+ d_match_pattern_op = qe->getTermDatabase()->getOperator( d_match_pattern );
//now, collect children of d_match_pattern
int childMatchPolicy = MATCH_GEN_DEFAULT;
}
Assert( Trigger::isAtomicTrigger( d_match_pattern ) );
//we are matching only in a particular equivalence class
- d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() );
+ d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern_op );
}else if( Trigger::isAtomicTrigger( d_match_pattern ) ){
//we will be scanning lists trying to find d_match_pattern.getOperator()
- d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() );
+ d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern_op );
}else{
d_cg = new CandidateGeneratorQueue;
Trace("inst-match-gen-warn") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
d_matchPolicy = MATCH_GEN_INTERNAL_ERROR;
}
+ for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){
+ if( d_match_pattern[i].getKind()==INST_CONSTANT || Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){
+ Node vv = d_match_pattern[i];
+ if( Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){
+ vv = d_match_pattern[i][0];
+ }
+ d_var_num[i] = vv.getAttribute(InstVarNumAttribute());
+ }
+ }
}
}
EqualityQuery* q = qe->getEqualityQuery();
bool success = true;
//save previous match
- InstMatch prev( &m );
+ //InstMatch prev( &m );
+ std::vector< int > prev;
//if t is null
Assert( !t.isNull() );
Assert( !quantifiers::TermDb::hasInstConstAttr(t) );
for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){
if( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[i]) ){
if( d_match_pattern[i].getKind()==INST_CONSTANT || Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){
- Node vv = d_match_pattern[i];
Node tt = t[i];
if( Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){
- vv = d_match_pattern[i][0];
tt = NodeManager::currentNM()->mkConst(q->areEqual( tt, d_match_pattern[i][1] ));
}
- if( !m.setMatch( q, vv, tt ) ){
+ bool addToPrev = m.get( d_var_num[i] ).isNull();
+ if( !m.set( qe, d_var_num[i], tt ) ){
//match is in conflict
- Trace("matching-debug") << "Match in conflict " << tt << " and "
- << vv << " because "
- << m.get(vv)
- << std::endl;
- Trace("matching-fail") << "Match fail: " << m.get(vv) << " and " << tt << std::endl;
+ Trace("matching-fail") << "Match fail: " << m.get(d_var_num[i]) << " and " << tt << std::endl;
success = false;
break;
+ }else if( addToPrev ){
+ prev.push_back( d_var_num[i] );
}
}
}else{
}
//for relational matching
if( !d_eq_class.isNull() && d_eq_class.getKind()==INST_CONSTANT ){
+ int v = d_eq_class.getAttribute(InstVarNumAttribute());
//also must fit match to equivalence class
bool pol = d_pattern.getKind()!=NOT;
Node pat = d_pattern.getKind()==NOT ? d_pattern[0] : d_pattern;
t_match = t;
}
}
- if( !t_match.isNull() && !m.setMatch( q, d_eq_class, t_match ) ){
- success = false;
+ if( !t_match.isNull() ){
+ bool addToPrev = m.get( v ).isNull();
+ if( !m.set( qe, v, t_match ) ){
+ success = false;
+ }else if( addToPrev ){
+ prev.push_back( v );
+ }
}
}
if( success ){
//now, fit children into match
//we will be requesting candidates for matching terms for each child
- std::vector< Node > reps;
for( int i=0; i<(int)d_children.size(); i++ ){
Node rep = q->getRepresentative( t[ d_children_index[i] ] );
- reps.push_back( rep );
d_children[i]->reset( rep, qe );
}
if( d_next!=NULL ){
}
}
if( !success ){
- m = InstMatch( &prev );
+ //m = InstMatch( &prev );
+ for( unsigned i=0; i<prev.size(); i++ ){
+ m.d_vals[prev[i]] = Node::null();
+ }
}
return success;
}
int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){
//try to add instantiation for each match produced
int addedLemmas = 0;
- InstMatch m;
+ InstMatch m( f );
while( getNextMatch( f, m, qe ) ){
if( !d_active_add ){
- //m.makeInternal( d_quantEngine->getEqualityQuery() );
m.add( baseMatch );
if( qe->addInstantiation( f, m ) ){
addedLemmas++;
int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){
Assert( options::eagerInstQuant() );
if( !d_match_pattern.isNull() ){
- InstMatch m;
+ InstMatch m( f );
if( getMatch( f, t, m, qe ) ){
if( qe->addInstantiation( f, m ) ){
return 1;
for( int i=0; i<(int)d_children.size(); i++ ){
Debug("smart-multi-trigger") << "Calculate matches " << i << std::endl;
std::vector< InstMatch > newMatches;
- InstMatch m;
+ InstMatch m( f );
while( d_children[i]->getNextMatch( f, m, qe ) ){
//m.makeRepresentative( qe );
newMatches.push_back( InstMatch( &m ) );
void InstMatchGeneratorMulti::processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas ){
//see if these produce new matches
- d_children_trie[fromChildIndex].addInstMatch( qe, d_f, m, true );
+ d_children_trie[fromChildIndex].addInstMatch( qe, d_f, m );
//possibly only do the following if we know that new matches will be produced?
//the issue is that instantiations are filtered in quantifiers engine, and so there is no guarentee that
// we can safely skip the following lines, even when we have already produced this match.
processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, 0 );
}else if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){
int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex];
- Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index );
- if( m.find( curr_ic )==m.end() ){
+ //Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index );
+ Node n = m.get( curr_index );
+ if( n.isNull() ){
//if( d_var_to_node[ curr_index ].size()==1 ){ //FIXME
// //unique variable(s), defer calculation
// unique_var_tries.push_back( IndexedTrie( std::pair< int, int >( childIndex, trieIndex ), tr ) );
//shared and non-set variable, add to InstMatch
for( std::map< Node, InstMatchTrie >::iterator it = tr->d_data.begin(); it != tr->d_data.end(); ++it ){
InstMatch mn( &m );
- mn.set( curr_ic, it->first);
+ mn.setValue( curr_index, it->first);
processNewInstantiations( qe, mn, addedLemmas, &(it->second), unique_var_tries,
trieIndex+1, childIndex, endChildIndex, modEq );
}
//}
}else{
//shared and set variable, try to merge
- Node n = m.get( curr_ic );
std::map< Node, InstMatchTrie >::iterator it = tr->d_data.find( n );
if( it!=tr->d_data.end() ){
processNewInstantiations( qe, m, addedLemmas, &(it->second), unique_var_tries,
}
if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){
int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex];
- Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index );
+ //Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index );
//unique non-set variable, add to InstMatch
for( std::map< Node, InstMatchTrie >::iterator it = tr->d_data.begin(); it != tr->d_data.end(); ++it ){
InstMatch mn( &m );
- mn.set( curr_ic, it->first);
+ mn.setValue( curr_index, it->first);
processNewInstantiations2( qe, mn, addedLemmas, unique_var_tries, uvtIndex, &(it->second), trieIndex+1 );
}
}else{
Assert( options::eagerInstQuant() );
int addedLemmas = 0;
for( int i=0; i<(int)d_children.size(); i++ ){
- if( ((InstMatchGenerator*)d_children[i])->d_match_pattern.getOperator()==t.getOperator() ){
- InstMatch m;
+ Node t_op = qe->getTermDatabase()->getOperator( t );
+ if( ((InstMatchGenerator*)d_children[i])->d_match_pattern_op==t_op ){
+ InstMatch m( f );
//if it produces a match, then process it with the rest
if( ((InstMatchGenerator*)d_children[i])->getMatch( f, t, m, qe ) ){
processNewMatch( qe, m, i, addedLemmas );
return addedLemmas;
}
+InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node f, Node pat ) : d_f( f ), d_match_pattern( pat ) {
+ for( unsigned i=0; i<d_match_pattern.getNumChildren(); i++ ){
+ if( d_match_pattern[i].getKind()==INST_CONSTANT ){
+ d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute());
+ }
+ }
+}
+
+void InstMatchGeneratorSimple::resetInstantiationRound( QuantifiersEngine* qe ) {
+ d_op = qe->getTermDatabase()->getOperator( d_match_pattern );
+}
+
int InstMatchGeneratorSimple::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){
- InstMatch m;
+ InstMatch m( f );
m.add( baseMatch );
int addedLemmas = 0;
+
if( d_match_pattern.getType()==NodeManager::currentNM()->booleanType() ){
for( int i=0; i<2; i++ ){
- addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_pred_map_trie[i][ d_match_pattern.getOperator() ]) );
+ addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_pred_map_trie[i][ d_op ]) );
}
}else{
- addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_func_map_trie[ d_match_pattern.getOperator() ]) );
+ addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_func_map_trie[ d_op ]) );
}
return addedLemmas;
}
//m is an instantiation
if( qe->addInstantiation( d_f, m ) ){
addedLemmas++;
- Debug("simple-multi-trigger") << "-> Produced instantiation " << m << std::endl;
+ Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl;
}
}else{
if( d_match_pattern[argIndex].getKind()==INST_CONSTANT ){
- Node ic = d_match_pattern[argIndex];
+ int v = d_var_num[argIndex];
for( std::map< Node, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
Node t = it->first;
- if( ( m.get( ic ).isNull() || m.get( ic )==t ) && ic.getType()==t.getType() ){
- Node prev = m.get( ic );
- m.set( ic, t);
+ Node prev = m.get( v );
+ if( ( prev.isNull() || prev==t ) && d_match_pattern[argIndex].getType()==t.getType() ){
+ m.setValue( v, t);
addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
- m.set( ic, prev);
+ m.setValue( v, prev);
}
}
}else{
int InstMatchGeneratorSimple::addTerm( Node f, Node t, QuantifiersEngine* qe ){
Assert( options::eagerInstQuant() );
- InstMatch m;
+ InstMatch m( f );
for( int i=0; i<(int)t.getNumChildren(); i++ ){
if( d_match_pattern[i].getKind()==INST_CONSTANT ){
- m.set(d_match_pattern[i], t[i]);
+ m.setValue(d_var_num[i], t[i]);
}else if( !qe->getEqualityQuery()->areEqual( d_match_pattern[i], t[i] ) ){
return 0;
}
Node d_eq_class;
/** for arithmetic matching */
std::map< Node, Node > d_arith_coeffs;
+ /** variable numbers */
+ std::map< int, int > d_var_num;
/** initialize pattern */
void initialize( QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens );
public:
Node d_pattern;
/** match pattern */
Node d_match_pattern;
+ /** match pattern op */
+ Node d_match_pattern_op;
public:
/** reset instantiation round (call this whenever equivalence classes have changed) */
void resetInstantiationRound( QuantifiersEngine* qe );
Node d_f;
/** match term */
Node d_match_pattern;
+ /** operator */
+ Node d_op;
+ /** to indicies */
+ std::map< int, int > d_var_num;
/** add instantiations */
void addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat );
public:
/** constructors */
- InstMatchGeneratorSimple( Node f, Node pat ) : d_f( f ), d_match_pattern( pat ){}
+ InstMatchGeneratorSimple( Node f, Node pat );
/** destructor */
~InstMatchGeneratorSimple(){}
/** reset instantiation round (call this whenever equivalence classes have changed) */
- void resetInstantiationRound( QuantifiersEngine* qe ) {}
+ void resetInstantiationRound( QuantifiersEngine* qe );
/** reset, eqc is the equivalence class to search in (any if eqc=null) */
void reset( Node eqc, QuantifiersEngine* qe ) {}
/** get the next match. must call reset( eqc ) before this function. (not implemented) */
// where e is a vector of terms , and t is vector of ground terms.
// Say one term in A*e is coeff*e_i, where e_i is an instantiation constant
// We will construct the term ( beta - B*t)/coeff to use for e_i.
- InstMatch m;
+ InstMatch m( f );
//By default, choose the first instantiation constant to be e_i.
Node var = d_ceTableaux[ic][x].begin()->first;
if( var.getType().isInteger() ){
}
instVal = Rewriter::rewrite( instVal );
//use as instantiation value for var
- m.set(var, instVal);
+ int vn = var.getAttribute(InstVarNumAttribute());
+ m.setValue( vn, instVal );
Debug("quant-arith") << "Add instantiation " << m << std::endl;
return d_quantEngine->addInstantiation( f, m );
}
if( e<2 ){
return InstStrategy::STATUS_UNFINISHED;
}else if( e==2 ){
- InstMatch m;
+ InstMatch m( f );
for( int j = 0; j<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){
Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
if( i.getType().isDatatype() ){
Node n = getValueFor( i );
Debug("quant-datatypes-debug") << "Value for " << i << " is " << n << std::endl;
- m.set(i,n);
+ m.setValue( j, n);
}
}
//d_quantEngine->addInstantiation( f, m );
if( processTrigger ){
//if( d_user_gen[f][i]->isMultiTrigger() )
Trace("process-trigger") << " Process (user) " << (*d_user_gen[f][i]) << "..." << std::endl;
- InstMatch baseMatch;
+ InstMatch baseMatch( f );
int numInst = d_user_gen[f][i]->addInstantiations( baseMatch );
//if( d_user_gen[f][i]->isMultiTrigger() )
Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl;
d_processed_trigger[f][tr] = true;
//if( tr->isMultiTrigger() )
Trace("process-trigger") << " Process " << (*tr) << "..." << std::endl;
- InstMatch baseMatch;
+ InstMatch baseMatch( f );
int numInst = tr->addInstantiations( baseMatch );
//if( tr->isMultiTrigger() )
Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl;
if( d_guessed.find( f )==d_guessed.end() ){
Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl;
d_guessed[f] = true;
- InstMatch m;
+ InstMatch m( f );
if( d_quantEngine->addInstantiation( f, m ) ){
++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
}
// Notice() << "Unhandled phase req: " << n << std::endl;
// }
//}
+ d_quant_basis_match[f] = InstMatch( f );
for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
- Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, j );
- Node t = d_qe->getTermDatabase()->getModelBasisTerm( ic.getType() );
+ Node t = d_qe->getTermDatabase()->getModelBasisTerm( f[0][j].getType() );
//calculate the basis match for f
- d_quant_basis_match[f].set( ic, t);
+ d_quant_basis_match[f].setValue( j, t );
}
++(d_statistics.d_num_quants_init);
}
riter.increment2( depIndex );
}else{
//instantiation was not shown to be true, construct the match
- InstMatch m;
+ InstMatch m( f );
for( int i=0; i<riter.getNumTerms(); i++ ){
- m.set( d_qe, f, riter.d_index_order[i], riter.getTerm( i ) );
+ m.set( d_qe, riter.d_index_order[i], riter.getTerm( i ) );
}
Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
//add as instantiation
for( int i=0; i<igp.getNumMatches(); i++ ){
//if the match is not already true in the model
if( igp.getMatchValue( i )!=fm->d_true ){
- InstMatch m;
+ InstMatch m( f );
igp.getMatch( d_qe->getEqualityQuery(), i, m );
//Trace("inst-gen-debug") << "Inst Gen : " << m << std::endl;
//we only consider matches that are non-empty
if( !m.empty() ){
Trace("inst-gen-debug") << "Get in terms of parent..." << std::endl;
//translate to be in terms match in terms of fp
- InstMatch mp;
+ InstMatch mp(f);
getParentQuantifierMatch( mp, fp, m, f );
//if this is a partial instantion
- if( !m.isComplete( f ) ){
+ if( !m.isComplete() ){
//need to make it internal here
//Trace("mkInternal") << "Make internal representative " << mp << std::endl;
//mp.makeInternalRepresentative( d_qe );
//std::cout << " " << fp[0].getNumChildren() << " " << f[0].getNumChildren() << std::endl;
int counter = 0;
for( size_t i=0; i<fp[0].getNumChildren(); i++ ){
- Node icp = d_qe->getTermDatabase()->getInstantiationConstant( fp, i );
if( (int)counter< (int)f[0].getNumChildren() ){
if( fp[0][i]==f[0][counter] ){
- Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, counter );
- Node n = m.getValue( ic );
+ Node n = m.get( counter );
if( !n.isNull() ){
- mp.setMatch( d_qe->getEqualityQuery(), icp, n );
+ mp.set( d_qe, i, n );
}
counter++;
}
int addedLemmas = 0;
while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
//instantiation was not shown to be true, construct the match
- InstMatch m;
+ InstMatch m( f );
for( int i=0; i<riter.getNumTerms(); i++ ){
- m.set( d_quantEngine, f, riter.d_index_order[i], riter.getTerm( i ) );
+ m.set( d_quantEngine, riter.d_index_order[i], riter.getTerm( i ) );
}
Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
triedLemmas++;
void RelevantDomain::computeRelevantDomain( Node n, bool hasPol, bool pol ) {
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( n.getKind()==APPLY_UF ){
- RDomain * rf = getRDomain( n.getOperator(), i );
+ Node op = d_qe->getTermDatabase()->getOperator( n );
+ if( !op.isNull() ){
+ RDomain * rf = getRDomain( op, i );
if( n[i].getKind()==INST_CONSTANT ){
Node q = d_qe->getTermDatabase()->getInstConstAttr( n[i] );
//merge the RDomains
bool success;
do
{
- InstMatch m;
+ InstMatch m( f );
success = d_rr_triggers[f][i]->getNextMatch( f, m );
if( success ){
//see if instantiation is true in the model
}
+Node TermDb::getOperator( Node n ) {
+ //return n.getOperator();
+
+ if( n.getKind()==SELECT || n.getKind()==STORE ){
+ //since it is parametric, use a particular one as op
+ TypeNode tn1 = n[0].getType();
+ TypeNode tn2 = n[1].getType();
+ Node op = n.getOperator();
+ std::map< Node, std::map< TypeNode, std::map< TypeNode, Node > > >::iterator ito = d_par_op_map.find( op );
+ if( ito!=d_par_op_map.end() ){
+ std::map< TypeNode, std::map< TypeNode, Node > >::iterator it = ito->second.find( tn1 );
+ if( it!=ito->second.end() ){
+ std::map< TypeNode, Node >::iterator it2 = it->second.find( tn2 );
+ if( it2!=it->second.end() ){
+ return it2->second;
+ }
+ }
+ }
+ d_par_op_map[op][tn1][tn2] = n;
+ return n;
+ }else if( n.getKind()==APPLY_UF ){
+ return n.getOperator();
+ }else{
+ return Node::null();
+ }
+}
+
void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
//don't add terms in quantifier bodies
if( withinQuant && !options::registerQuantBodyTerms() ){
if( !TermDb::hasInstConstAttr(n) ){
Trace("term-db") << "register term in db " << n << std::endl;
//std::cout << "register trigger term " << n << std::endl;
- Node op = n.getOperator();
+ Node op = getOperator( n );
d_op_map[op].push_back( n );
added.insert( n );
computeModelBasisArgAttribute( en );
if( en.getKind()==APPLY_UF && !TermDb::hasInstConstAttr(en) ){
if( !en.getAttribute(NoMatchAttribute()) ){
- Node op = en.getOperator();
+ Node op = getOperator( en );
if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){
NoMatchAttribute nma;
en.setAttribute(nma,true);
QuantifiersEngine* d_quantEngine;
/** terms processed */
std::hash_set< Node, NodeHashFunction > d_processed;
+private:
+ /** select op map */
+ std::map< Node, std::map< TypeNode, std::map< TypeNode, Node > > > d_par_op_map;
public:
TermDb( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
~TermDb(){}
void addTerm( Node n, std::set< Node >& added, bool withinQuant = false );
/** reset (calculate which terms are active) */
void reset( Theory::Effort effort );
+ /** get operation */
+ Node getOperator( Node n );
private:
/** for efficient e-matching */
void addTermEfficient( Node n, std::set< Node >& added);
//Notice() << "Trigger : " << (*this) << " for " << f << std::endl;
if( options::eagerInstQuant() ){
for( int i=0; i<(int)d_nodes.size(); i++ ){
- qe->getTermDatabase()->registerTrigger( this, d_nodes[i].getOperator() );
+ Node op = qe->getTermDatabase()->getOperator( d_nodes[i] );
+ qe->getTermDatabase()->registerTrigger( this, op );
}
}
Trace("trigger-debug") << "Finished making trigger." << std::endl;
static bool isBooleanTermTrigger( Node n );
inline void toStream(std::ostream& out) const {
+ /*
out << "TRIGGER( ";
for( int i=0; i<(int)d_nodes.size(); i++ ){
if( i>0 ){ out << ", "; }
out << d_nodes[i];
}
out << " )";
+ */
}
};
}
void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, 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] );
+ for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+ Node n = m.get( i );
if( !n.isNull() ){
vars.push_back( f[0][i] );
terms.push_back( n );
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 );
- Node val = m.getValue( ic );
+ Node val = m.get( i );
if( val.isNull() ){
+ Node ic = d_term_db->getInstantiationConstant( f, i );
val = d_term_db->getFreeVariableForInstConstant( ic );
Trace("inst-add-debug") << "mkComplete " << val << std::endl;
}
Trace("inst-add-debug") << std::endl;
//check for duplication
- bool alreadyExists = false;
///*
+ bool alreadyExists = false;
if( options::incrementalSolving() ){
Trace("inst-add-debug") << "Adding into context-dependent inst trie" << std::endl;
inst::CDInstMatchTrie* imt;
++(d_statistics.d_inst_duplicate_eq);
return false;
}
+ //*/
//add the instantiation
bool addedInst = addInstantiation( f, d_term_db->d_vars[f], terms );
if( c.getType() == ty ) ele.insert(c);
}
if( !ele.empty() ){
- // for(std::vector<Node>::iterator i = db->d_op_map[op].begin(), end = db->d_op_map[op].end(); i != end; ++i){
- // if(CandidateGenerator::isLegalCandidate(*i)) ele.insert(*i);
- // }
if(Debug.isOn("efficient-e-match-stats")){
Debug("efficient-e-match-stats") << "pattern " << pats << " initialized with " << ele.size() << " terms"<< std::endl;
}
}
} else {
- Node op = pats[0].getOperator();
TermDb* db = d_quantEngine->getTermDatabase();
+ Node op = db->getOperator( pats[0] );
if(db->d_op_map[op].begin() != db->d_op_map[op].end()){
SetNode ele;
- // for(std::vector<Node>::iterator i = db->d_op_map[op].begin(), end = db->d_op_map[op].end(); i != end; ++i){
- // if(CandidateGenerator::isLegalCandidate(*i)) ele.insert(*i);
- // }
ele.insert(db->d_op_map[op].begin(), db->d_op_map[op].end());
if(Debug.isOn("efficient-e-match-stats")){
Debug("efficient-e-match-stats") << "pattern " << pats << " initialized with " << ele.size() << " terms"<< std::endl;
namespace theory{
namespace rrinst{
-typedef CVC4::theory::inst::InstMatch InstMatch;
+
+
+
+InstMatch::InstMatch() {
+}
+
+InstMatch::InstMatch( InstMatch* m ) {
+ d_map = m->d_map;
+}
+
+bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m, bool & set ){
+ std::map< Node, Node >::iterator vn = d_map.find( v );
+ if( !m.isNull() && !m.getType().isSubtypeOf( v.getType() ) ){
+ set = false;
+ return false;
+ }else if( vn==d_map.end() || vn->second.isNull() ){
+ set = true;
+ this->set(v,m);
+ Debug("matching-debug") << "Add partial " << v << "->" << m << std::endl;
+ return true;
+ }else{
+ set = false;
+ return q->areEqual( vn->second, m );
+ }
+}
+
+bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m ){
+ bool set;
+ return setMatch(q,v,m,set);
+}
+
+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;
+ }
+ }
+ }
+ 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;
+ }else{
+ if( !q->areEqual( it->second, itf->second ) ){
+ d_map.clear();
+ return false;
+ }
+ }
+ }
+ }
+ return true;
+}
+
+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;
+ }
+ //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 ){
+ 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 );
+ }
+ }
+}
+
+//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 ) ){
+ d_map[ it->first ] = qe->getEqualityQuery()->getEngine()->getRepresentative( it->second );
+ }
+ }
+}
+
+void InstMatch::applyRewrite(){
+ for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
+ it->second = Rewriter::rewrite(it->second);
+ }
+}
+
+/** 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();
+ }
+}
+
+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")) {
+ // 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 ;
+ }
+ }
+ 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 );
+}
+
+
+
+
+
+
+typedef CVC4::theory::rrinst::InstMatch InstMatch;
typedef CVC4::theory::inst::CandidateGeneratorQueue CandidateGeneratorQueue;
template<bool modEq>
AuxMatcher2 am2(am3,LegalTest());
/** Iter on the equivalence class of the given term */
TermDb* tdb = qe->getTermDatabase();
- CandidateGeneratorTheoryUfOp cdtUfEq(pat.getOperator(),tdb);
+ Node op = tdb->getOperator( pat );
+ CandidateGeneratorTheoryUfOp cdtUfEq(op,tdb);
/* Create a matcher from the candidate generator */
AuxMatcher1 am1(cdtUfEq,am2);
return am1;
d_im.add( baseMatch );
while( getNextMatch( qe ) ){
InstMatch im_copy = getInstMatch();
+ std::vector< Node > terms;
+ for( unsigned i=0; i<quant[0].getNumChildren(); i++ ){
+ terms.push_back( im_copy.get( qe, quant, i ) );
+ }
+
//m.makeInternal( d_quantEngine->getEqualityQuery() );
- if( qe->addInstantiation( quant, im_copy ) ){
+ if( qe->addInstantiation( quant, terms ) ){
addedLemmas++;
}
}
resetInstantiationRound( qe );
while( getNextMatch( qe ) ){
InstMatch im_copy = getInstMatch();
+ std::vector< Node > terms;
+ for( unsigned i=0; i<quant[0].getNumChildren(); i++ ){
+ terms.push_back( im_copy.get( qe, quant, i ) );
+ }
+
//m.makeInternal( d_quantEngine->getEqualityQuery() );
- if( qe->addInstantiation( quant, im_copy ) ){
+ if( qe->addInstantiation( quant, terms ) ){
addedLemmas++;
}
}
#include "theory/uf/theory_uf.h"
#include "context/cdlist.h"
-#include "theory/quantifiers/inst_match.h"
#include "theory/quantifiers/term_database.h"
#include "expr/node_manager.h"
#include "expr/node_builder.h"
namespace CVC4 {
namespace theory {
+class EqualityQuery;
+
namespace rrinst{
+/** basic class defining an instantiation */
+class InstMatch {
+ /* map from variable to ground terms */
+ std::map< Node, Node > d_map;
+public:
+ InstMatch();
+ InstMatch( InstMatch* m );
+
+ /** 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);
+ /** fill all unfilled values with m */
+ bool add( InstMatch& m );
+ /** if compatible, fill all unfilled values with m and return true
+ return false otherwise */
+ bool merge( EqualityQuery* q, InstMatch& m );
+ /** debug print method */
+ void debugPrint( const char* c );
+ /** is complete? */
+ bool isComplete( Node f ) { return d_map.size()==f[0].getNumChildren(); }
+ /** make complete */
+ void makeComplete( Node f, QuantifiersEngine* qe );
+ /** make internal representative */
+ //void makeInternalRepresentative( QuantifiersEngine* qe );
+ /** make representative */
+ void makeRepresentative( QuantifiersEngine* qe );
+ /** get value */
+ Node getValue( Node var ) const;
+ /** clear */
+ void clear(){ d_map.clear(); }
+ /** is_empty */
+ bool empty(){ return d_map.empty(); }
+ /** to stream */
+ inline void toStream(std::ostream& out) const {
+ out << "INST_MATCH( ";
+ for( std::map< Node, Node >::const_iterator it = d_map.begin(); it != d_map.end(); ++it ){
+ if( it != d_map.begin() ){ out << ", "; }
+ out << it->first << " -> " << it->second;
+ }
+ out << " )";
+ }
+
+
+ //for rewrite rules
+
+ /** apply rewrite */
+ void applyRewrite();
+ /** erase */
+ template<class Iterator>
+ void erase(Iterator begin, Iterator end){
+ for(Iterator i = begin; i != end; ++i){
+ d_map.erase(*i);
+ };
+ }
+ void erase(Node node){ d_map.erase(node); }
+ /** get */
+ Node get( TNode var ) { return d_map[var]; }
+ Node get( QuantifiersEngine* qe, Node f, int i );
+ /** set */
+ void set(TNode var, TNode n);
+ void set( QuantifiersEngine* qe, Node f, int i, TNode n );
+ /** size */
+ size_t size(){ return d_map.size(); }
+ /* iterator */
+ std::map< Node, Node >::iterator begin(){ return d_map.begin(); };
+ std::map< Node, Node >::iterator end(){ return d_map.end(); };
+ std::map< Node, Node >::iterator find(Node var){ return d_map.find(var); };
+ /* Node used for matching the trigger only for mono-trigger (just for
+ efficiency because I need only that) */
+ Node d_matched;
+};/* class InstMatch */
+
+
+
class CandidateGenerator
{
public:
}
void TheoryRewriteRules::addMatchRuleTrigger(const RewriteRule * r,
- InstMatch & im,
+ rrinst::InstMatch & im,
bool delay){
++r->nb_matched;
++d_statistics.d_match_found;
/** Test the possible matching one by one */
while(tr.getNextMatch()){
- InstMatch im = tr.getInstMatch();
+ rrinst::InstMatch im = tr.getInstMatch();
addMatchRuleTrigger(r, im, true);
}
}
ApplyMatcher * tr = r->trigger_for_body_match;
Assert(tr != NULL);
tr->resetInstantiationRound(getQuantifiersEngine());
- InstMatch im;
+ rrinst::InstMatch im;
TNode m = inst->substNode(*this,(*p).first, cache);
Assert( m.getKind() == kind::APPLY_UF );
ee->addTerm(m);
~RewriteRule();
bool noGuard()const throw () { return guards.size() == 0; };
- bool inCache(TheoryRewriteRules & re, InstMatch & im)const;
+ bool inCache(TheoryRewriteRules & re, rrinst::InstMatch & im)const;
void toStream(std::ostream& out) const;
void addRewriteRule(const Node r);
void computeMatchBody ( const RewriteRule * r, size_t start = 0);
void addMatchRuleTrigger(const RewriteRule* r,
- InstMatch & im, bool delay = true);
+ rrinst::InstMatch & im, bool delay = true);
Node normalizeConjunction(NodeBuilder<> & conjunction);
};
-bool RewriteRule::inCache(TheoryRewriteRules & re, InstMatch & im)const{
+bool RewriteRule::inCache(TheoryRewriteRules & re, rrinst::InstMatch & im)const{
bool res = !d_cache.addInstMatch(im);
Debug("rewriterules::matching") << "rewriterules::cache " << im
<< (res ? " HIT" : " MISS") << std::endl;
projects / cvc5.git / commitdiff