diff options
| author | François Bobot <francois@bobot.eu> | 2012-07-27 13:36:32 +0000 |
|---|---|---|
| committer | François Bobot <francois@bobot.eu> | 2012-07-27 13:36:32 +0000 |
| commit | 4bfa927dac67bbcadf219f70e61f1d123e33944b (patch) | |
| tree | f295343430799748de8b9a823f1a3c641c096905 /src/theory | |
| parent | 988c97d92fa617c5dccaeb1ef33121bfa6459afc (diff) | |
Merge quantifiers2-trunk:
- new syntax for rewrite rules
- better rewrite rules theory
- remove the rewriting with rewrite rules during ppRewrite temporarily
- theory can define their own candidate generator
- define a general candidate generator (inefficient ask to every theory)
- split inst_match between the pattern matching used for quantifiers (inst_match.*) and
the one used for rewrite rules (rr_inst_match.*):
- the pattern matching is less exhaustive for quantifiers,
- the one for rewrite rules can use efficient-e-matching.
Diffstat (limited to 'src/theory')
42 files changed, 4790 insertions, 793 deletions
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 1aae03aa5..2bd85f712 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -40,8 +40,12 @@ libtheory_la_SOURCES = \ quantifiers_engine.cpp \ instantiator_default.h \ instantiator_default.cpp \ + rr_inst_match.h \ + rr_inst_match_impl.h \ + rr_inst_match.cpp \ + rr_trigger.h \ + rr_trigger.cpp \ inst_match.h \ - inst_match_impl.h \ inst_match.cpp \ trigger.h \ trigger.cpp \ diff --git a/src/theory/arith/theory_arith_instantiator.cpp b/src/theory/arith/theory_arith_instantiator.cpp index c4cb2f493..ab3a1548e 100644 --- a/src/theory/arith/theory_arith_instantiator.cpp +++ b/src/theory/arith/theory_arith_instantiator.cpp @@ -376,7 +376,7 @@ bool InstantiatorTheoryArith::doInstantiation2( Node f, Node term, ArithVar x, I } instVal = Rewriter::rewrite( instVal ); //use as instantiation value for var - m.d_map[ var ] = instVal; + m.set(var, instVal); Debug("quant-arith") << "Add instantiation " << m << std::endl; return d_quantEngine->addInstantiation( f, m ); } diff --git a/src/theory/arrays/theory_arrays_instantiator.cpp b/src/theory/arrays/theory_arrays_instantiator.cpp index 2e446c57f..ca9001fe5 100644 --- a/src/theory/arrays/theory_arrays_instantiator.cpp +++ b/src/theory/arrays/theory_arrays_instantiator.cpp @@ -17,6 +17,7 @@ #include "theory/theory_engine.h" #include "theory/arrays/theory_arrays_instantiator.h" #include "theory/arrays/theory_arrays.h" +#include "theory/uf/theory_uf_candidate_generator.h" using namespace std; using namespace CVC4; @@ -83,3 +84,16 @@ Node InstantiatorTheoryArrays::getRepresentative( Node a ){ } } +rrinst::CandidateGenerator* InstantiatorTheoryArrays::getRRCanGenClasses(){ + arrays::TheoryArrays* ar = static_cast<arrays::TheoryArrays *>(getTheory()); + eq::EqualityEngine* ee = + static_cast<eq::EqualityEngine*>(ar->getEqualityEngine()); + return new eq::rrinst::CandidateGeneratorTheoryEeClasses(ee); +} + +rrinst::CandidateGenerator* InstantiatorTheoryArrays::getRRCanGenClass(){ + arrays::TheoryArrays* ar = static_cast<arrays::TheoryArrays *>(getTheory()); + eq::EqualityEngine* ee = + static_cast<eq::EqualityEngine*>(ar->getEqualityEngine()); + return new eq::rrinst::CandidateGeneratorTheoryEeClass(ee); +} diff --git a/src/theory/arrays/theory_arrays_instantiator.h b/src/theory/arrays/theory_arrays_instantiator.h index ade43fdb0..f711229b2 100644 --- a/src/theory/arrays/theory_arrays_instantiator.h +++ b/src/theory/arrays/theory_arrays_instantiator.h @@ -21,6 +21,7 @@ #define __CVC4__INSTANTIATOR_THEORY_ARRAYS_H #include "theory/quantifiers_engine.h" +#include "theory/uf/equality_engine.h" namespace CVC4 { namespace theory { @@ -48,10 +49,13 @@ public: bool areEqual( Node a, Node b ); bool areDisequal( Node a, Node b ); Node getRepresentative( Node a ); + /** general creators of candidate generators */ + rrinst::CandidateGenerator* getRRCanGenClasses(); + rrinst::CandidateGenerator* getRRCanGenClass(); };/* class Instantiatior */ } } } -#endif
\ No newline at end of file +#endif diff --git a/src/theory/datatypes/Makefile.am b/src/theory/datatypes/Makefile.am index 14bbf64d4..f282ce74d 100644 --- a/src/theory/datatypes/Makefile.am +++ b/src/theory/datatypes/Makefile.am @@ -16,6 +16,7 @@ libdatatypes_la_SOURCES = \ explanation_manager.h \ explanation_manager.cpp \ theory_datatypes_instantiator.h \ - theory_datatypes_instantiator.cpp + theory_datatypes_instantiator.cpp \ + theory_datatypes_candidate_generator.h EXTRA_DIST = kinds diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 783c0ebc7..80c20a7d9 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -38,9 +38,17 @@ namespace theory { namespace datatypes { class InstantiatorTheoryDatatypes; +class EqualityQueryTheory; + +namespace rrinst{ + class CandidateGeneratorTheoryClass; +} class TheoryDatatypes : public Theory { friend class InstantiatorTheoryDatatypes; + friend class EqualityQueryTheory; + friend class rrinst::CandidateGeneratorTheoryClass; + private: typedef context::CDChunkList<TNode> EqList; typedef context::CDHashMap<Node, EqList*, NodeHashFunction> EqLists; diff --git a/src/theory/datatypes/theory_datatypes_candidate_generator.h b/src/theory/datatypes/theory_datatypes_candidate_generator.h new file mode 100644 index 000000000..46c7ce7fb --- /dev/null +++ b/src/theory/datatypes/theory_datatypes_candidate_generator.h @@ -0,0 +1,67 @@ +/********************* */ +/*! \file theory_uf_candidate generator.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Theory datatypes candidate generator + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY_DATATYPES_CANDIDATE_GENERATOR_H +#define __CVC4__THEORY_DATATYPES_CANDIDATE_GENERATOR_H + +#include "theory/quantifiers_engine.h" +#include "theory/datatypes/theory_datatypes.h" +#include "theory/rr_inst_match.h" + +namespace CVC4 { +namespace theory { +namespace datatypes { + +namespace rrinst { +typedef CVC4::theory::rrinst::CandidateGenerator CandidateGenerator; + +// Just iterate amoung the equivalence class of the given node +// node::Null() *can't* be given to reset +class CandidateGeneratorTheoryClass : public CandidateGenerator{ +private: + //instantiator pointer + TheoryDatatypes* d_th; + //the equality class iterator + TheoryDatatypes::EqListN::const_iterator d_eqc_i; + TheoryDatatypes::EqListN* d_eqc; +public: + CandidateGeneratorTheoryClass( TheoryDatatypes* th): d_th( th ), d_eqc(NULL){} + ~CandidateGeneratorTheoryClass(){} + void resetInstantiationRound(){}; + void reset( TNode n ){ + TheoryDatatypes::EqListsN::const_iterator i = d_th->d_equivalence_class.find(n); + if(i == d_th->d_equivalence_class.end()){ + d_eqc = NULL; + } else { + d_eqc = (*i).second; + d_eqc_i = d_eqc->begin(); + } + }; //* the argument is not used + TNode getNextCandidate(){ + if( d_eqc == NULL || d_eqc_i == d_eqc->end() ) return Node::null(); + return *(d_eqc_i++); + }; +}; + + +} +} +} +} + +#endif /* __CVC4__THEORY_DATATYPES_CANDIDATE_GENERATOR_H */ diff --git a/src/theory/datatypes/theory_datatypes_instantiator.cpp b/src/theory/datatypes/theory_datatypes_instantiator.cpp index 9495e4d48..57e9324df 100644 --- a/src/theory/datatypes/theory_datatypes_instantiator.cpp +++ b/src/theory/datatypes/theory_datatypes_instantiator.cpp @@ -15,6 +15,7 @@ **/ #include "theory/datatypes/theory_datatypes_instantiator.h" +#include "theory/datatypes/theory_datatypes_candidate_generator.h" #include "theory/datatypes/theory_datatypes.h" #include "theory/theory_engine.h" #include "theory/quantifiers/term_database.h" @@ -26,9 +27,9 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::datatypes; -InstantiatorTheoryDatatypes::InstantiatorTheoryDatatypes(context::Context* c, QuantifiersEngine* ie, Theory* th) : -Instantiator( c, ie, th ){ +InstantiatorTheoryDatatypes::InstantiatorTheoryDatatypes(context::Context* c, QuantifiersEngine* ie, TheoryDatatypes* th) : +Instantiator( c, ie, th ){ } void InstantiatorTheoryDatatypes::assertNode( Node assertion ){ @@ -60,7 +61,7 @@ int InstantiatorTheoryDatatypes::process( Node f, Theory::Effort effort, int e ) if( i.getType().isDatatype() ){ Node n = getValueFor( i ); Debug("quant-datatypes-debug") << "Value for " << i << " is " << n << std::endl; - m.d_map[ i ] = n; + m.set(i,n); } } d_quantEngine->addInstantiation( f, m ); @@ -168,3 +169,8 @@ bool InstantiatorTheoryDatatypes::areDisequal( Node a, Node b ){ Node InstantiatorTheoryDatatypes::getRepresentative( Node a ){ return ((TheoryDatatypes*)d_th)->getRepresentative( a ); } + +CVC4::theory::rrinst::CandidateGenerator* InstantiatorTheoryDatatypes::getRRCanGenClass(){ + TheoryDatatypes* th = static_cast<TheoryDatatypes *>(getTheory()); + return new datatypes::rrinst::CandidateGeneratorTheoryClass(th); +} diff --git a/src/theory/datatypes/theory_datatypes_instantiator.h b/src/theory/datatypes/theory_datatypes_instantiator.h index a080465af..fd7190a22 100644 --- a/src/theory/datatypes/theory_datatypes_instantiator.h +++ b/src/theory/datatypes/theory_datatypes_instantiator.h @@ -28,10 +28,12 @@ namespace CVC4 { namespace theory { namespace datatypes { +class TheoryDatatypes; + class InstantiatorTheoryDatatypes : public Instantiator{ friend class QuantifiersEngine; public: - InstantiatorTheoryDatatypes(context::Context* c, QuantifiersEngine* ie, Theory* th); + InstantiatorTheoryDatatypes(context::Context* c, QuantifiersEngine* ie, TheoryDatatypes* th); ~InstantiatorTheoryDatatypes() {} /** assertNode function, assertion is asserted to theory */ @@ -59,10 +61,13 @@ public: bool areEqual( Node a, Node b ); bool areDisequal( Node a, Node b ); Node getRepresentative( Node a ); + /** general creators of candidate generators */ + CVC4::theory::rrinst::CandidateGenerator* getRRCanGenClass(); };/* class InstantiatiorTheoryDatatypes */ + } } } -#endif
\ No newline at end of file +#endif diff --git a/src/theory/inst_match.cpp b/src/theory/inst_match.cpp index abcf5aa7f..4f1bfe67e 100644 --- a/src/theory/inst_match.cpp +++ b/src/theory/inst_match.cpp @@ -30,6 +30,7 @@ using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::theory; +using namespace CVC4::theory::inst; bool CandidateGenerator::isLegalCandidate( Node n ){ @@ -71,16 +72,24 @@ InstMatch::InstMatch( InstMatch* m ) { d_map = m->d_map; } -bool InstMatch::setMatch( EqualityQuery* q, Node v, Node m ){ - if( d_map.find( v )==d_map.end() ){ - d_map[v] = m; +bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m, bool & set ){ + std::map< Node, Node >::iterator vn = d_map.find( v ); + if( vn==d_map.end() ){ + set = true; + this->set(v,m); Debug("matching-debug") << "Add partial " << v << "->" << m << std::endl; return true; }else{ - return q->areEqual( d_map[v], m ); + 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( d_map.find( it->first )==d_map.end() ){ @@ -174,7 +183,7 @@ void InstMatch::computeTermVec( const std::vector< Node >& vars, std::vector< No 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.d_map[ qe->getTermDatabase()->getInstantiationConstant( f, i_index ) ]; + Node n = m.get( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) ); d_data[n].addInstMatch2( qe, f, m, index+1, imtio ); } } @@ -185,7 +194,7 @@ bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m return true; }else{ int i_index = imtio ? imtio->d_order[index] : index; - Node n = m.d_map[ qe->getTermDatabase()->getInstantiationConstant( f, i_index ) ]; + Node n = m.get( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) ); std::map< Node, InstMatchTrie >::iterator it = d_data.find( n ); if( it!=d_data.end() ){ if( it->second.existsInstMatch( qe, f, m, modEq, index+1, imtio ) ){ @@ -301,10 +310,10 @@ void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){ //we will be producing candidates via literal matching heuristics if( d_pattern.getKind()!=NOT ){ //candidates will be all equalities - d_cg = new uf::CandidateGeneratorTheoryUfLitEq( ith, d_match_pattern ); + d_cg = new uf::inst::CandidateGeneratorTheoryUfLitEq( ith, d_match_pattern ); }else{ //candidates will be all disequalities - d_cg = new uf::CandidateGeneratorTheoryUfLitDeq( ith, d_match_pattern ); + d_cg = new uf::inst::CandidateGeneratorTheoryUfLitDeq( ith, d_match_pattern ); } }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF || d_pattern.getKind()==NOT ){ Assert( d_matchPolicy==MATCH_GEN_DEFAULT ); @@ -313,20 +322,16 @@ void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){ }else{ Assert( Trigger::isAtomicTrigger( d_match_pattern ) ); //we are matching only in a particular equivalence class - d_cg = new uf::CandidateGeneratorTheoryUf( ith, d_match_pattern.getOperator() ); + d_cg = new uf::inst::CandidateGeneratorTheoryUf( ith, d_match_pattern.getOperator() ); //store the equivalence class that we will call d_cg->reset( ... ) on d_eq_class = d_pattern[1]; } }else if( Trigger::isAtomicTrigger( d_match_pattern ) ){ - if( d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ){ - //we will manually add candidates to queue - d_cg = new CandidateGeneratorQueue; - //register this candidate generator - ith->registerCandidateGenerator( d_cg, d_match_pattern ); - }else{ - //we will be scanning lists trying to find d_match_pattern.getOperator() - d_cg = new uf::CandidateGeneratorTheoryUf( ith, d_match_pattern.getOperator() ); - } + //if( d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ){ + //Warning() << "Currently efficient e matching is not taken into account for quantifiers: " << d_pattern << std::endl; + //} + //we will be scanning lists trying to find d_match_pattern.getOperator() + d_cg = new uf::inst::CandidateGeneratorTheoryUf( ith, d_match_pattern.getOperator() ); }else{ d_cg = new CandidateGeneratorQueue; if( !Trigger::getPatternArithmetic( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){ @@ -347,7 +352,7 @@ void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){ /** get match (not modulo equality) */ bool InstMatchGenerator::getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ){ Debug("matching") << "Matching " << t << " against pattern " << d_match_pattern << " (" - << m.d_map.size() << ")" << ", " << d_children.size() << std::endl; + << m.size() << ")" << ", " << d_children.size() << std::endl; Assert( !d_match_pattern.isNull() ); if( qe->d_optMatchIgnoreModelBasis && t.getAttribute(ModelBasisAttribute()) ){ return true; @@ -373,9 +378,9 @@ bool InstMatchGenerator::getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ) //match is in conflict Debug("matching-debug") << "Match in conflict " << t[i] << " and " << d_match_pattern[i] << " because " - << partial[0].d_map[d_match_pattern[i]] + << partial[0].get(d_match_pattern[i]) << std::endl; - Debug("matching-fail") << "Match fail: " << partial[0].d_map[d_match_pattern[i]] << " and " << t[i] << std::endl; + Debug("matching-fail") << "Match fail: " << partial[0].get(d_match_pattern[i]) << " and " << t[i] << std::endl; return false; } } @@ -443,14 +448,14 @@ bool InstMatchGenerator::getMatchArithmetic( Node t, InstMatch& m, QuantifiersEn for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){ Debug("matching-arith") << it->first << " -> " << it->second << std::endl; if( !it->first.isNull() ){ - if( m.d_map.find( it->first )==m.d_map.end() ){ + if( m.find( it->first )==m.end() ){ //see if we can choose this to set if( ic.isNull() && ( it->second.isNull() || !it->first.getType().isInteger() ) ){ ic = it->first; } }else{ - Debug("matching-arith") << "already set " << m.d_map[ it->first ] << std::endl; - Node tm = m.d_map[ it->first ]; + Debug("matching-arith") << "already set " << m.get( it->first ) << std::endl; + Node tm = m.get( it->first ); if( !it->second.isNull() ){ tm = NodeManager::currentNM()->mkNode( MULT, it->second, tm ); } @@ -473,12 +478,12 @@ bool InstMatchGenerator::getMatchArithmetic( Node t, InstMatch& m, QuantifiersEn Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_arith_coeffs[ ic ].getConst<Rational>() ); tm = NodeManager::currentNM()->mkNode( MULT, coeff, tm ); } - m.d_map[ ic ] = Rewriter::rewrite( tm ); + m.set( ic, Rewriter::rewrite( tm )); //set the rest to zeros for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){ if( !it->first.isNull() ){ - if( m.d_map.find( it->first )==m.d_map.end() ){ - m.d_map[ it->first ] = NodeManager::currentNM()->mkConst( Rational(0) ); + if( m.find( it->first )==m.end() ){ + m.set( it->first, NodeManager::currentNM()->mkConst( Rational(0) ) ); } } } @@ -754,7 +759,7 @@ void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, I }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.d_map.find( curr_ic )==m.d_map.end() ){ + if( m.find( curr_ic )==m.end() ){ //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 ) ); @@ -765,14 +770,14 @@ void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, I //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.d_map[ curr_ic ] = it->first; + mn.set( curr_ic, 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.d_map[ curr_ic ]; + 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, @@ -819,7 +824,7 @@ void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe, //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.d_map[ curr_ic ] = it->first; + mn.set( curr_ic, it->first); processNewInstantiations2( qe, mn, addedLemmas, unique_var_tries, uvtIndex, &(it->second), trieIndex+1 ); } }else{ @@ -875,11 +880,11 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin Node ic = d_match_pattern[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.d_map[ ic ].isNull() || m.d_map[ ic ]==t ){ - Node prev = m.d_map[ ic ]; - m.d_map[ ic ] = t; + if( m.get( ic ).isNull() || m.get( ic )==t ){ + Node prev = m.get( ic ); + m.set( ic, t); addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); - m.d_map[ ic ] = prev; + m.set( ic, prev); } } }else{ @@ -897,7 +902,7 @@ int InstMatchGeneratorSimple::addTerm( Node f, Node t, QuantifiersEngine* qe ){ InstMatch m; for( int i=0; i<(int)t.getNumChildren(); i++ ){ if( d_match_pattern[i].getKind()==INST_CONSTANT ){ - m.d_map[d_match_pattern[i]] = t[i]; + m.set(d_match_pattern[i], t[i]); }else if( !qe->getEqualityQuery()->areEqual( d_match_pattern[i], t[i] ) ){ return 0; } diff --git a/src/theory/inst_match.h b/src/theory/inst_match.h index 7cc5b2249..31a59b261 100644 --- a/src/theory/inst_match.h +++ b/src/theory/inst_match.h @@ -44,14 +44,40 @@ typedef expr::Attribute< NoMatchAttributeId, true // context dependent > NoMatchAttribute; +// attribute for "contains instantiation constants from" +struct InstConstantAttributeId {}; +typedef expr::Attribute<InstConstantAttributeId, Node> InstConstantAttribute; + +struct InstLevelAttributeId {}; +typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute; + +struct InstVarNumAttributeId {}; +typedef expr::Attribute<InstVarNumAttributeId, uint64_t> InstVarNumAttribute; + +// Attribute that tell if a node have been asserted in this branch +struct AvailableInTermDbId {}; +/** use the special for boolean flag */ +typedef expr::Attribute<AvailableInTermDbId, + bool, + expr::attr::NullCleanupStrategy, + true // context dependent + > AvailableInTermDb; + + class QuantifiersEngine; +namespace quantifiers{ + class TermArgTrie; +} -namespace uf { +namespace uf{ class InstantiatorTheoryUf; class TheoryUF; }/* CVC4::theory::uf namespace */ -class CandidateGenerator { +namespace inst { + +class CandidateGenerator +{ public: CandidateGenerator(){} ~CandidateGenerator(){} @@ -95,7 +121,7 @@ public: class EqualityQuery { public: EqualityQuery(){} - ~EqualityQuery(){} + virtual ~EqualityQuery(){}; /** contains term */ virtual bool hasTerm( Node a ) = 0; /** get the representative of the equivalence class of a */ @@ -113,12 +139,16 @@ public: /** 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, Node v, Node 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 @@ -140,10 +170,30 @@ public: void computeTermVec( const std::vector< Node >& vars, std::vector< Node >& match ); /** clear */ void clear(){ d_map.clear(); } + /** 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); } /** is_empty */ bool empty(){ return d_map.empty(); } - /* map from variable to ground terms */ - std::map< Node, Node > d_map; + /** set */ + void set(TNode var, TNode n){ + //std::cout << "var.getType() " << var.getType() << "n.getType() " << n.getType() << std::endl ; + Assert( !var.isNull() ); + Assert( n.isNull() ||// For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations + var.getType() == n.getType() ); + d_map[var] = n; + } + Node get(TNode var){ return d_map[var]; } + 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; @@ -207,67 +257,6 @@ public: } };/* class InstMatchTrieOrdered */ -template<bool modEq = false> -class InstMatchTrie2 { -private: - - class Tree { - public: - typedef std::hash_map< Node, Tree *, NodeHashFunction > MLevel; - MLevel e; - const size_t level; //context level of creation - Tree() CVC4_UNDEFINED; - const Tree & operator =(const Tree & t) CVC4_UNDEFINED; - Tree(size_t l): level(l) {}; - ~Tree(){ - for(typename MLevel::iterator i = e.begin(); i!=e.end(); ++i) - delete(i->second); - }; - };/* class InstMatchTrie2::Tree */ - - - typedef std::pair<Tree *, TNode> Mod; - - class CleanUp { - public: - inline void operator()(Mod * m){ - typename Tree::MLevel::iterator i = m->first->e.find(m->second); - Assert (i != m->first->e.end()); //should not have been already removed - m->first->e.erase(i); - } - };/* class InstMatchTrie2::CleanUp */ - - EqualityQuery* d_eQ; - eq::EqualityEngine* d_eE; - - /* before for the order of destruction */ - Tree d_data; - - context::Context* d_context; - context::CDList<Mod, CleanUp, std::allocator<Mod> > d_mods; - - typedef std::map<Node, Node>::const_iterator mapIter; - - /** add the substitution given by the iterator*/ - void addSubTree( Tree* root, mapIter current, mapIter end, size_t currLevel); - /** test if it exists match, modulo uf-equations if modEq is true if - * return false the deepest point of divergence is put in [e] and - * [diverge]. - */ - bool existsInstMatch( Tree* root, - mapIter & current, mapIter& end, - Tree*& e, mapIter& diverge) const; - -public: - InstMatchTrie2(context::Context* c, QuantifiersEngine* q); - InstMatchTrie2(const InstMatchTrie2&) CVC4_UNDEFINED; - const InstMatchTrie2& operator=(const InstMatchTrie2 & e) CVC4_UNDEFINED; - /** add match m in the trie, - modEq specify to take into account equalities, - return true if it was never seen */ - bool addInstMatch( InstMatch& m); -};/* class InstMatchTrie2 */ - /** base class for producing InstMatch objects */ class IMGenerator { public: @@ -405,10 +394,6 @@ public: int addTerm( Node f, Node t, QuantifiersEngine* qe ); };/* class InstMatchGeneratorMulti */ -namespace quantifiers{ - class TermArgTrie; -} - /** smart (single)-trigger implementation */ class InstMatchGeneratorSimple : public IMGenerator { private: @@ -438,6 +423,11 @@ public: int addTerm( Node f, Node t, QuantifiersEngine* qe ); };/* class InstMatchGeneratorSimple */ +}/* CVC4::theory::inst namespace */ + +typedef CVC4::theory::inst::InstMatch InstMatch; +typedef CVC4::theory::inst::EqualityQuery EqualityQuery; + }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/instantiator_default.cpp b/src/theory/instantiator_default.cpp index a1766ce3c..cff16962a 100644 --- a/src/theory/instantiator_default.cpp +++ b/src/theory/instantiator_default.cpp @@ -46,7 +46,7 @@ int InstantiatorDefault::process( Node f, Theory::Effort effort, int e ){ if( d_quantEngine->getTheoryEngine()->theoryOf( i )==getTheory() ){ //if it belongs to this theory Node val = d_th->getValue( i ); Debug("quant-default") << "Default Instantiate for " << d_th->getId() << ", setting " << i << " = " << val << std::endl; - m.d_map[ i ] = val; + m.set( i, val); } } d_quantEngine->addInstantiation( f, m ); diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index fae54c151..2b79cd8b9 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -104,7 +104,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ int e_use = e; if( e_use>=0 ){ //use each theory instantiator to instantiate f - for( int i=0; i<theory::THEORY_LAST; i++ ){ + for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){ if( d_quantEngine->getInstantiator( i ) ){ Debug("inst-engine-debug") << "Do " << d_quantEngine->getInstantiator( i )->identify() << " " << e_use << std::endl; int quantStatus = d_quantEngine->getInstantiator( i )->doInstantiation( f, effort, e_use ); @@ -126,7 +126,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ //Notice() << "All instantiators finished, # added lemmas = " << (int)d_lemmas_waiting.size() << std::endl; if( !d_quantEngine->hasAddedLemma() ){ Debug("inst-engine-stuck") << "No instantiations produced at this state: " << std::endl; - for( int i=0; i<theory::THEORY_LAST; i++ ){ + for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){ if( d_quantEngine->getInstantiator( i ) ){ d_quantEngine->getInstantiator( i )->debugPrint("inst-engine-stuck"); Debug("inst-engine-stuck") << std::endl; diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index ad259f864..663f270eb 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -39,6 +39,7 @@ using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; +using namespace CVC4::theory::inst; ModelEngineBuilder::ModelEngineBuilder( QuantifiersEngine* qe ) : TheoryEngineModelBuilder( qe->getTheoryEngine() ), @@ -503,7 +504,7 @@ int ModelEngine::initializeQuantifier( Node f ){ ics.push_back( ic ); terms.push_back( t ); //calculate the basis match for f - d_builder.d_quant_basis_match[f].d_map[ ic ] = t; + d_builder.d_quant_basis_match[f].set( ic, t); } ++(d_statistics.d_num_quants_init); //register model basis body diff --git a/src/theory/quantifiers/rep_set_iterator.cpp b/src/theory/quantifiers/rep_set_iterator.cpp index 02041480f..a29f815db 100644 --- a/src/theory/quantifiers/rep_set_iterator.cpp +++ b/src/theory/quantifiers/rep_set_iterator.cpp @@ -97,7 +97,7 @@ bool RepSetIterator::isFinished(){ void RepSetIterator::getMatch( QuantifiersEngine* qe, InstMatch& m ){
for( int i=0; i<(int)d_index.size(); i++ ){
- m.d_map[ qe->getTermDatabase()->getInstantiationConstant( d_f, d_index_order[i] ) ] = getTerm( i );
+ m.set( qe->getTermDatabase()->getInstantiationConstant( d_f, d_index_order[i] ), getTerm( i ));
}
}
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 55ea693ef..55715353d 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1,324 +1,365 @@ -/********************* */
-/*! \file term_database.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of term databse class
- **/
-
- #include "theory/quantifiers/term_database.h"
- #include "theory/quantifiers_engine.h"
- #include "theory/uf/theory_uf_instantiator.h"
- #include "theory/theory_engine.h"
- #include "theory/quantifiers/first_order_model.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-
- bool TermArgTrie::addTerm2( QuantifiersEngine* qe, Node n, int argIndex ){
- if( argIndex<(int)n.getNumChildren() ){
- Node r = qe->getEqualityQuery()->getRepresentative( n[ argIndex ] );
- std::map< Node, TermArgTrie >::iterator it = d_data.find( r );
- if( it==d_data.end() ){
- d_data[r].addTerm2( qe, n, argIndex+1 );
- return true;
- }else{
- return it->second.addTerm2( qe, n, argIndex+1 );
- }
- }else{
- //store n in d_data (this should be interpretted as the "data" and not as a reference to a child)
- d_data[n].d_data.clear();
- return false;
- }
- }
-
- void TermDb::addTerm( Node n, std::vector< Node >& added, bool withinQuant ){
- //don't add terms in quantifier bodies
- if( !withinQuant || Options::current()->registerQuantBodyTerms ){
- if( d_processed.find( n )==d_processed.end() ){
- d_processed[n] = true;
- //if this is an atomic trigger, consider adding it
- if( Trigger::isAtomicTrigger( n ) ){
- if( !n.hasAttribute(InstConstantAttribute()) ){
- Debug("term-db") << "register trigger term " << n << std::endl;
- //Notice() << "register trigger term " << n << std::endl;
- Node op = n.getOperator();
- d_op_map[op].push_back( n );
- d_type_map[ n.getType() ].push_back( n );
- added.push_back( n );
-
- uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF );
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- addTerm( n[i], added, withinQuant );
- if( Options::current()->efficientEMatching ){
- if( d_parents[n[i]][op].empty() ){
- //must add parent to equivalence class info
- Node nir = d_ith->getRepresentative( n[i] );
- uf::EqClassInfo* eci_nir = d_ith->getEquivalenceClassInfo( nir );
- if( eci_nir ){
- eci_nir->d_pfuns[ op ] = true;
- }
- }
- //add to parent structure
- if( std::find( d_parents[n[i]][op][i].begin(), d_parents[n[i]][op][i].end(), n )==d_parents[n[i]][op][i].end() ){
- d_parents[n[i]][op][i].push_back( n );
- }
- }
- }
- if( Options::current()->efficientEMatching ){
- //new term, add n to candidate generators
- for( int i=0; i<(int)d_ith->d_cand_gens[op].size(); i++ ){
- d_ith->d_cand_gens[op][i]->addCandidate( n );
- }
- }
- if( Options::current()->eagerInstQuant ){
- if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
- int addedLemmas = 0;
- for( int i=0; i<(int)d_ith->d_op_triggers[op].size(); i++ ){
- addedLemmas += d_ith->d_op_triggers[op][i]->addTerm( n );
- }
- //Message() << "Terms, added lemmas: " << addedLemmas << std::endl;
- d_quantEngine->flushLemmas( &d_quantEngine->getTheoryEngine()->getTheory( THEORY_QUANTIFIERS )->getOutputChannel() );
- }
- }
- }
- }
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- addTerm( n[i], added, withinQuant );
- }
- }
- }
- }
-
- void TermDb::reset( Theory::Effort effort ){
- int nonCongruentCount = 0;
- int congruentCount = 0;
- int alreadyCongruentCount = 0;
- //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms
- for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
- if( !it->second.empty() ){
- if( it->second[0].getType()==NodeManager::currentNM()->booleanType() ){
- d_pred_map_trie[ 0 ][ it->first ].d_data.clear();
- d_pred_map_trie[ 1 ][ it->first ].d_data.clear();
- }else{
- d_func_map_trie[ it->first ].d_data.clear();
- for( int i=0; i<(int)it->second.size(); i++ ){
- Node n = it->second[i];
- if( !n.getAttribute(NoMatchAttribute()) ){
- if( !d_func_map_trie[ it->first ].addTerm( d_quantEngine, n ) ){
- NoMatchAttribute nma;
- n.setAttribute(nma,true);
- congruentCount++;
- }else{
- nonCongruentCount++;
- }
- }else{
- congruentCount++;
- alreadyCongruentCount++;
- }
- }
- }
- }
- }
- for( int i=0; i<2; i++ ){
- Node n = NodeManager::currentNM()->mkConst( i==1 );
- eq::EqClassIterator eqc( d_quantEngine->getEqualityQuery()->getRepresentative( n ),
- ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine() );
- while( !eqc.isFinished() ){
- Node en = (*eqc);
- if( en.getKind()==APPLY_UF && !en.hasAttribute(InstConstantAttribute()) ){
- if( !en.getAttribute(NoMatchAttribute()) ){
- Node op = en.getOperator();
- if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){
- NoMatchAttribute nma;
- en.setAttribute(nma,true);
- congruentCount++;
- }else{
- nonCongruentCount++;
- }
- }else{
- alreadyCongruentCount++;
- }
- }
- ++eqc;
- }
- }
- Debug("term-db-cong") << "TermDb: Reset" << std::endl;
- Debug("term-db-cong") << "Congruent/Non-Congruent = ";
- Debug("term-db-cong") << congruentCount << "(" << alreadyCongruentCount << ") / " << nonCongruentCount << std::endl;
-}
-
-void TermDb::registerModelBasis( Node n, Node gn ){
- if( d_model_basis.find( n )==d_model_basis.end() ){
- d_model_basis[n] = gn;
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- registerModelBasis( n[i], gn[i] );
- }
- }
-}
-
-Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
- if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){
- std::stringstream ss;
- ss << Expr::setlanguage(Options::current()->outputLanguage);
- ss << "e_" << tn;
- d_model_basis_term[tn] = NodeManager::currentNM()->mkVar( ss.str(), tn );
- ModelBasisAttribute mba;
- d_model_basis_term[tn].setAttribute(mba,true);
- }
- return d_model_basis_term[tn];
-}
-
-Node TermDb::getModelBasisOpTerm( Node op ){
- if( d_model_basis_op_term.find( op )==d_model_basis_op_term.end() ){
- TypeNode t = op.getType();
- std::vector< Node > children;
- children.push_back( op );
- for( size_t i=0; i<t.getNumChildren()-1; i++ ){
- children.push_back( getModelBasisTerm( t[i] ) );
- }
- d_model_basis_op_term[op] = NodeManager::currentNM()->mkNode( APPLY_UF, children );
- }
- return d_model_basis_op_term[op];
-}
-
-void TermDb::computeModelBasisArgAttribute( Node n ){
- if( !n.hasAttribute(ModelBasisArgAttribute()) ){
- uint64_t val = 0;
- //determine if it has model basis attribute
- for( int j=0; j<(int)n.getNumChildren(); j++ ){
- if( n[j].getAttribute(ModelBasisAttribute()) ){
- val = 1;
- break;
- }
- }
- ModelBasisArgAttribute mbaa;
- n.setAttribute( mbaa, val );
- }
-}
-
-void TermDb::makeInstantiationConstantsFor( Node f ){
- if( d_inst_constants.find( f )==d_inst_constants.end() ){
- Debug("quantifiers-engine") << "Instantiation constants for " << f << " : " << std::endl;
- for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
- d_vars[f].push_back( f[0][i] );
- //make instantiation constants
- Node ic = NodeManager::currentNM()->mkInstConstant( f[0][i].getType() );
- d_inst_constants_map[ic] = f;
- d_inst_constants[ f ].push_back( ic );
- Debug("quantifiers-engine") << " " << ic << std::endl;
- //set the var number attribute
- InstVarNumAttribute ivna;
- ic.setAttribute(ivna,i);
- }
- }
-}
-
-void TermDb::setInstantiationLevelAttr( Node n, uint64_t level ){
- if( !n.hasAttribute(InstLevelAttribute()) ){
- InstLevelAttribute ila;
- n.setAttribute(ila,level);
- }
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- setInstantiationLevelAttr( n[i], level );
- }
-}
-
-
-void TermDb::setInstantiationConstantAttr( Node n, Node f ){
- if( !n.hasAttribute(InstConstantAttribute()) ){
- bool setAttr = false;
- if( n.getKind()==INST_CONSTANT ){
- setAttr = true;
- }else{
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- setInstantiationConstantAttr( n[i], f );
- if( n[i].hasAttribute(InstConstantAttribute()) ){
- setAttr = true;
- }
- }
- }
- if( setAttr ){
- InstConstantAttribute ica;
- n.setAttribute(ica,f);
- //also set the no-match attribute
- NoMatchAttribute nma;
- n.setAttribute(nma,true);
- }
- }
-}
-
-
-Node TermDb::getCounterexampleBody( Node f ){
- std::map< Node, Node >::iterator it = d_counterexample_body.find( f );
- if( it==d_counterexample_body.end() ){
- makeInstantiationConstantsFor( f );
- Node n = getSubstitutedNode( f[1], f );
- d_counterexample_body[ f ] = n;
- return n;
- }else{
- return it->second;
- }
-}
-
-Node TermDb::getSkolemizedBody( Node f ){
- Assert( f.getKind()==FORALL );
- if( d_skolem_body.find( f )==d_skolem_body.end() ){
- std::vector< Node > vars;
- for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
- Node skv = NodeManager::currentNM()->mkSkolem( f[0][i].getType() );
- d_skolem_constants[ f ].push_back( skv );
- vars.push_back( f[0][i] );
- }
- d_skolem_body[ f ] = f[ 1 ].substitute( vars.begin(), vars.end(),
- d_skolem_constants[ f ].begin(), d_skolem_constants[ f ].end() );
- if( f.hasAttribute(InstLevelAttribute()) ){
- setInstantiationLevelAttr( d_skolem_body[ f ], f.getAttribute(InstLevelAttribute()) );
- }
- }
- return d_skolem_body[ f ];
-}
-
-
-Node TermDb::getSubstitutedNode( Node n, Node f ){
- return convertNodeToPattern(n,f,d_vars[f],d_inst_constants[ f ]);
-}
-
-Node TermDb::convertNodeToPattern( Node n, Node f, const std::vector<Node> & vars,
- const std::vector<Node> & inst_constants){
- Node n2 = n.substitute( vars.begin(), vars.end(),
- inst_constants.begin(),
- inst_constants.end() );
- setInstantiationConstantAttr( n2, f );
- return n2;
-}
-
-Node TermDb::getFreeVariableForInstConstant( Node n ){
- TypeNode tn = n.getType();
- if( d_free_vars.find( tn )==d_free_vars.end() ){
- //if integer or real, make zero
- if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){
- Rational z(0);
- d_free_vars[tn] = NodeManager::currentNM()->mkConst( z );
- }else{
- if( d_type_map[ tn ].empty() ){
- d_free_vars[tn] = NodeManager::currentNM()->mkVar( tn );
- }else{
- d_free_vars[tn] = d_type_map[ tn ][ 0 ];
- }
- }
- }
- return d_free_vars[tn];
-}
\ No newline at end of file +/********************* */ +/*! \file term_database.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): bobot + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of term databse class + **/ + + #include "theory/quantifiers/term_database.h" + #include "theory/quantifiers_engine.h" + #include "theory/uf/theory_uf_instantiator.h" + #include "theory/theory_engine.h" + #include "theory/quantifiers/first_order_model.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; + +using namespace CVC4::theory::inst; + bool TermArgTrie::addTerm2( QuantifiersEngine* qe, Node n, int argIndex ){ + if( argIndex<(int)n.getNumChildren() ){ + Node r = qe->getEqualityQuery()->getRepresentative( n[ argIndex ] ); + std::map< Node, TermArgTrie >::iterator it = d_data.find( r ); + if( it==d_data.end() ){ + d_data[r].addTerm2( qe, n, argIndex+1 ); + return true; + }else{ + return it->second.addTerm2( qe, n, argIndex+1 ); + } + }else{ + //store n in d_data (this should be interpretted as the "data" and not as a reference to a child) + d_data[n].d_data.clear(); + return false; + } + } + +void addTermEfficient( Node n, std::set< Node >& added){ + static AvailableInTermDb aitdi; + if (Trigger::isAtomicTrigger( n ) && !n.getAttribute(aitdi)){ + //Already processed but new in this branch + n.setAttribute(aitdi,true); + added.insert( n ); + for( size_t i=0; i< n.getNumChildren(); i++ ){ + addTermEfficient(n[i],added); + } + } + +} + + +void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ + //don't add terms in quantifier bodies + if( withinQuant && !Options::current()->registerQuantBodyTerms ){ + return; + } + if( d_processed.find( n )==d_processed.end() ){ + ++(d_quantEngine->d_statistics.d_term_in_termdb); + d_processed.insert(n); + n.setAttribute(AvailableInTermDb(),true); + //if this is an atomic trigger, consider adding it + //Call the children? + if( Trigger::isAtomicTrigger( n ) || n.getKind() == kind::APPLY_CONSTRUCTOR ){ + if( !n.hasAttribute(InstConstantAttribute()) ){ + Debug("term-db") << "register trigger term " << n << std::endl; + //std::cout << "register trigger term " << n << std::endl; + Node op = n.getOperator(); + d_op_map[op].push_back( n ); + d_type_map[ n.getType() ].push_back( n ); + added.insert( n ); + + uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF ); + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + addTerm( n[i], added, withinQuant ); + if( Options::current()->efficientEMatching ){ + if( d_parents[n[i]][op].empty() ){ + //must add parent to equivalence class info + Node nir = d_ith->getRepresentative( n[i] ); + uf::EqClassInfo* eci_nir = d_ith->getEquivalenceClassInfo( nir ); + if( eci_nir ){ + eci_nir->d_pfuns[ op ] = true; + } + } + //add to parent structure + if( std::find( d_parents[n[i]][op][i].begin(), d_parents[n[i]][op][i].end(), n )==d_parents[n[i]][op][i].end() ){ + d_parents[n[i]][op][i].push_back( n ); + Assert(!getParents(n[i],op,i).empty()); + } + } + if( Options::current()->eagerInstQuant ){ + if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){ + int addedLemmas = 0; + for( int i=0; i<(int)d_ith->d_op_triggers[op].size(); i++ ){ + addedLemmas += d_ith->d_op_triggers[op][i]->addTerm( n ); + } + //Message() << "Terms, added lemmas: " << addedLemmas << std::endl; + d_quantEngine->flushLemmas( &d_quantEngine->getTheoryEngine()->getTheory( THEORY_QUANTIFIERS )->getOutputChannel() ); + } + } + } + } + }else{ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + addTerm( n[i], added, withinQuant ); + } + } + }else{ + if( Options::current()->efficientEMatching && + !n.hasAttribute(InstConstantAttribute())){ + //Efficient e-matching must be notified + //The term in triggers are not important here + Debug("term-db") << "New in this branch term " << n << std::endl; + addTermEfficient(n,added); + } + } +}; + + void TermDb::reset( Theory::Effort effort ){ + int nonCongruentCount = 0; + int congruentCount = 0; + int alreadyCongruentCount = 0; + //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms + for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){ + if( !it->second.empty() ){ + if( it->second[0].getType()==NodeManager::currentNM()->booleanType() ){ + d_pred_map_trie[ 0 ][ it->first ].d_data.clear(); + d_pred_map_trie[ 1 ][ it->first ].d_data.clear(); + }else{ + d_func_map_trie[ it->first ].d_data.clear(); + for( int i=0; i<(int)it->second.size(); i++ ){ + Node n = it->second[i]; + if( !n.getAttribute(NoMatchAttribute()) ){ + if( !d_func_map_trie[ it->first ].addTerm( d_quantEngine, n ) ){ + NoMatchAttribute nma; + n.setAttribute(nma,true); + congruentCount++; + }else{ + nonCongruentCount++; + } + }else{ + congruentCount++; + alreadyCongruentCount++; + } + } + } + } + } + for( int i=0; i<2; i++ ){ + Node n = NodeManager::currentNM()->mkConst( i==1 ); + eq::EqClassIterator eqc( d_quantEngine->getEqualityQuery()->getRepresentative( n ), + ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine() ); + while( !eqc.isFinished() ){ + Node en = (*eqc); + if( en.getKind()==APPLY_UF && !en.hasAttribute(InstConstantAttribute()) ){ + if( !en.getAttribute(NoMatchAttribute()) ){ + Node op = en.getOperator(); + if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){ + NoMatchAttribute nma; + en.setAttribute(nma,true); + congruentCount++; + }else{ + nonCongruentCount++; + } + }else{ + alreadyCongruentCount++; + } + } + ++eqc; + } + } + Debug("term-db-cong") << "TermDb: Reset" << std::endl; + Debug("term-db-cong") << "Congruent/Non-Congruent = "; + Debug("term-db-cong") << congruentCount << "(" << alreadyCongruentCount << ") / " << nonCongruentCount << std::endl; +} + +void TermDb::registerModelBasis( Node n, Node gn ){ + if( d_model_basis.find( n )==d_model_basis.end() ){ + d_model_basis[n] = gn; + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + registerModelBasis( n[i], gn[i] ); + } + } +} + +Node TermDb::getModelBasisTerm( TypeNode tn, int i ){ + if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){ + std::stringstream ss; + ss << Expr::setlanguage(Options::current()->outputLanguage); + ss << "e_" << tn; + d_model_basis_term[tn] = NodeManager::currentNM()->mkVar( ss.str(), tn ); + ModelBasisAttribute mba; + d_model_basis_term[tn].setAttribute(mba,true); + } + return d_model_basis_term[tn]; +} + +Node TermDb::getModelBasisOpTerm( Node op ){ + if( d_model_basis_op_term.find( op )==d_model_basis_op_term.end() ){ + TypeNode t = op.getType(); + std::vector< Node > children; + children.push_back( op ); + for( size_t i=0; i<t.getNumChildren()-1; i++ ){ + children.push_back( getModelBasisTerm( t[i] ) ); + } + d_model_basis_op_term[op] = NodeManager::currentNM()->mkNode( APPLY_UF, children ); + } + return d_model_basis_op_term[op]; +} + +void TermDb::computeModelBasisArgAttribute( Node n ){ + if( !n.hasAttribute(ModelBasisArgAttribute()) ){ + uint64_t val = 0; + //determine if it has model basis attribute + for( int j=0; j<(int)n.getNumChildren(); j++ ){ + if( n[j].getAttribute(ModelBasisAttribute()) ){ + val = 1; + break; + } + } + ModelBasisArgAttribute mbaa; + n.setAttribute( mbaa, val ); + } +} + +void TermDb::makeInstantiationConstantsFor( Node f ){ + if( d_inst_constants.find( f )==d_inst_constants.end() ){ + Debug("quantifiers-engine") << "Instantiation constants for " << f << " : " << std::endl; + for( int i=0; i<(int)f[0].getNumChildren(); i++ ){ + d_vars[f].push_back( f[0][i] ); + //make instantiation constants + Node ic = NodeManager::currentNM()->mkInstConstant( f[0][i].getType() ); + d_inst_constants_map[ic] = f; + d_inst_constants[ f ].push_back( ic ); + Debug("quantifiers-engine") << " " << ic << std::endl; + //set the var number attribute + InstVarNumAttribute ivna; + ic.setAttribute(ivna,i); + } + } +} + +void TermDb::setInstantiationLevelAttr( Node n, uint64_t level ){ + if( !n.hasAttribute(InstLevelAttribute()) ){ + InstLevelAttribute ila; + n.setAttribute(ila,level); + } + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + setInstantiationLevelAttr( n[i], level ); + } +} + + +void TermDb::setInstantiationConstantAttr( Node n, Node f ){ + if( !n.hasAttribute(InstConstantAttribute()) ){ + bool setAttr = false; + if( n.getKind()==INST_CONSTANT ){ + setAttr = true; + }else{ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + setInstantiationConstantAttr( n[i], f ); + if( n[i].hasAttribute(InstConstantAttribute()) ){ + setAttr = true; + } + } + } + if( setAttr ){ + InstConstantAttribute ica; + n.setAttribute(ica,f); + //also set the no-match attribute + NoMatchAttribute nma; + n.setAttribute(nma,true); + } + } +} + + +Node TermDb::getCounterexampleBody( Node f ){ + std::map< Node, Node >::iterator it = d_counterexample_body.find( f ); + if( it==d_counterexample_body.end() ){ + makeInstantiationConstantsFor( f ); + Node n = getSubstitutedNode( f[1], f ); + d_counterexample_body[ f ] = n; + return n; + }else{ + return it->second; + } +} + +Node TermDb::getSkolemizedBody( Node f ){ + Assert( f.getKind()==FORALL ); + if( d_skolem_body.find( f )==d_skolem_body.end() ){ + std::vector< Node > vars; + for( int i=0; i<(int)f[0].getNumChildren(); i++ ){ + Node skv = NodeManager::currentNM()->mkSkolem( f[0][i].getType() ); + d_skolem_constants[ f ].push_back( skv ); + vars.push_back( f[0][i] ); + } + d_skolem_body[ f ] = f[ 1 ].substitute( vars.begin(), vars.end(), + d_skolem_constants[ f ].begin(), d_skolem_constants[ f ].end() ); + if( f.hasAttribute(InstLevelAttribute()) ){ + setInstantiationLevelAttr( d_skolem_body[ f ], f.getAttribute(InstLevelAttribute()) ); + } + } + return d_skolem_body[ f ]; +} + + +Node TermDb::getSubstitutedNode( Node n, Node f ){ + return convertNodeToPattern(n,f,d_vars[f],d_inst_constants[ f ]); +} + +Node TermDb::convertNodeToPattern( Node n, Node f, const std::vector<Node> & vars, + const std::vector<Node> & inst_constants){ + Node n2 = n.substitute( vars.begin(), vars.end(), + inst_constants.begin(), + inst_constants.end() ); + setInstantiationConstantAttr( n2, f ); + return n2; +} + +Node TermDb::getFreeVariableForInstConstant( Node n ){ + TypeNode tn = n.getType(); + if( d_free_vars.find( tn )==d_free_vars.end() ){ + //if integer or real, make zero + if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){ + Rational z(0); + d_free_vars[tn] = NodeManager::currentNM()->mkConst( z ); + }else{ + if( d_type_map[ tn ].empty() ){ + d_free_vars[tn] = NodeManager::currentNM()->mkVar( tn ); + }else{ + d_free_vars[tn] = d_type_map[ tn ][ 0 ]; + } + } + } + return d_free_vars[tn]; +} + +const std::vector<Node> & TermDb::getParents(TNode n, TNode f, int arg){ + std::hash_map< Node, std::hash_map< Node, std::hash_map< int, std::vector< Node > >,NodeHashFunction >,NodeHashFunction >::const_iterator + rn = d_parents.find( n ); + if( rn !=d_parents.end() ){ + std::hash_map< Node, std::hash_map< int, std::vector< Node > > , NodeHashFunction > ::const_iterator + rf = rn->second.find(f); + if( rf != rn->second.end() ){ + std::hash_map< int, std::vector< Node > > ::const_iterator + ra = rf->second.find(arg); + if( ra != rf->second.end() ){ + return ra->second; + } + } + } + static std::vector<Node> empty; + return empty; +} diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 5bf3d7900..5004a82dc 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -48,7 +48,7 @@ private: /** calculated no match terms */
bool d_matching_active;
/** terms processed */
- std::map< Node, bool > d_processed;
+ std::hash_set< Node, NodeHashFunction > d_processed;
public:
TermDb( QuantifiersEngine* qe ) : d_quantEngine( qe ), d_matching_active( true ){}
~TermDb(){}
@@ -61,7 +61,7 @@ public: /** map from type nodes to terms of that type */
std::map< TypeNode, std::vector< Node > > d_type_map;
/** add a term to the database */
- void addTerm( Node n, std::vector< Node >& added, bool withinQuant = false );
+ void addTerm( Node n, std::set< Node >& added, bool withinQuant = false );
/** reset (calculate which terms are active) */
void reset( Theory::Effort effort );
/** set active */
@@ -75,7 +75,9 @@ public: has operator "op", and n'["index"] = n.
for example, d_parents[n][f][1] = { f( t1, n ), f( t2, n ), ... }
*/
- std::map< Node, std::map< Node, std::map< int, std::vector< Node > > > > d_parents;
+ /* Todo replace int by size_t */
+ std::hash_map< Node, std::hash_map< Node, std::hash_map< int, std::vector< Node > >, NodeHashFunction > , NodeHashFunction > d_parents;
+ const std::vector<Node> & getParents(TNode n, TNode f, int arg);
private:
//map from types to model basis terms
std::map< TypeNode, Node > d_model_basis_term;
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 517786400..1e42abd22 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -30,10 +30,11 @@ #include <map> namespace CVC4 { +class TheoryEngine; + namespace theory { namespace quantifiers { -class TheoryEngine; class ModelEngine; class InstantiationEngine; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index e4e3df9be..448224b81 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -32,6 +32,7 @@ using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::theory; +using namespace CVC4::theory::inst; //#define COMPUTE_RELEVANCE //#define REWRITE_ASSERTED_QUANTIFIERS @@ -93,7 +94,11 @@ d_active( c ){ d_optInstLimit = 0; } -Instantiator* QuantifiersEngine::getInstantiator( int id ){ +QuantifiersEngine::~QuantifiersEngine(){ + delete(d_term_db); +} + +Instantiator* QuantifiersEngine::getInstantiator( theory::TheoryId id ){ return d_te->getTheory( id )->getInstantiator(); } @@ -212,7 +217,7 @@ void QuantifiersEngine::registerQuantifier( Node f ){ void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) { for(std::vector<Node>::iterator p = pattern.begin(); p != pattern.end(); ++p){ - std::vector< Node > added; + std::set< Node > added; getTermDatabase()->addTerm(*p,added); } } @@ -236,7 +241,7 @@ void QuantifiersEngine::propagate( Theory::Effort level ){ } void QuantifiersEngine::resetInstantiationRound( Theory::Effort level ){ - for( int i=0; i<theory::THEORY_LAST; i++ ){ + for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){ if( getInstantiator( i ) ){ getInstantiator( i )->resetInstantiationRound( level ); } @@ -245,13 +250,19 @@ void QuantifiersEngine::resetInstantiationRound( Theory::Effort level ){ } void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){ - std::vector< Node > added; - getTermDatabase()->addTerm( n, added, withinQuant ); -#ifdef COMPUTE_RELEVANCE - for( int i=0; i<(int)added.size(); i++ ){ - if( !withinQuant ){ - setRelevance( added[i].getOperator(), 0 ); + std::set< Node > added; + getTermDatabase()->addTerm( n, added, withinQuant ); + if( Options::current()->efficientEMatching ){ + uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)getInstantiator( THEORY_UF ); + d_ith->newTerms(added); } +#ifdef COMPUTE_RELEVANCE + //added contains also the Node that just have been asserted in this branch + for( std::set< Node >::iterator i=added.begin(), end=added.end(); + i!=end; i++ ){ + if( !withinQuant ){ + setRelevance( i->getOperator(), 0 ); + } } #endif @@ -530,7 +541,15 @@ QuantifiersEngine::Statistics::Statistics(): d_triggers("QuantifiersEngine::Triggers", 0), d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0), d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0), - d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0) + d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0), + d_term_in_termdb("QuantifiersEngine::Term_in_TermDb", 0), + d_num_mono_candidates("QuantifiersEngine::NumMonoCandidates", 0), + d_num_mono_candidates_new_term("QuantifiersEngine::NumMonoCandidatesNewTerm", 0), + d_num_multi_candidates("QuantifiersEngine::NumMultiCandidates", 0), + d_mono_candidates_cache_hit("QuantifiersEngine::MonoCandidatesCacheHit", 0), + d_mono_candidates_cache_miss("QuantifiersEngine::MonoCandidatesCacheMiss", 0), + d_multi_candidates_cache_hit("QuantifiersEngine::MultiCandidatesCacheHit", 0), + d_multi_candidates_cache_miss("QuantifiersEngine::MultiCandidatesCacheMiss", 0) { StatisticsRegistry::registerStat(&d_num_quant); StatisticsRegistry::registerStat(&d_instantiation_rounds); @@ -548,6 +567,14 @@ QuantifiersEngine::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_simple_triggers); StatisticsRegistry::registerStat(&d_multi_triggers); StatisticsRegistry::registerStat(&d_multi_trigger_instantiations); + StatisticsRegistry::registerStat(&d_term_in_termdb); + StatisticsRegistry::registerStat(&d_num_mono_candidates); + StatisticsRegistry::registerStat(&d_num_mono_candidates_new_term); + StatisticsRegistry::registerStat(&d_num_multi_candidates); + StatisticsRegistry::registerStat(&d_mono_candidates_cache_hit); + StatisticsRegistry::registerStat(&d_mono_candidates_cache_miss); + StatisticsRegistry::registerStat(&d_multi_candidates_cache_hit); + StatisticsRegistry::registerStat(&d_multi_candidates_cache_miss); } QuantifiersEngine::Statistics::~Statistics(){ @@ -567,6 +594,14 @@ QuantifiersEngine::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_simple_triggers); StatisticsRegistry::unregisterStat(&d_multi_triggers); StatisticsRegistry::unregisterStat(&d_multi_trigger_instantiations); + StatisticsRegistry::unregisterStat(&d_term_in_termdb); + StatisticsRegistry::unregisterStat(&d_num_mono_candidates); + StatisticsRegistry::unregisterStat(&d_num_mono_candidates_new_term); + StatisticsRegistry::unregisterStat(&d_num_multi_candidates); + StatisticsRegistry::unregisterStat(&d_mono_candidates_cache_hit); + StatisticsRegistry::unregisterStat(&d_mono_candidates_cache_miss); + StatisticsRegistry::unregisterStat(&d_multi_candidates_cache_hit); + StatisticsRegistry::unregisterStat(&d_multi_candidates_cache_miss); } /** compute symbols */ @@ -608,7 +643,7 @@ bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){ if( ee->hasTerm( a ) ){ return true; } - for( int i=0; i<theory::THEORY_LAST; i++ ){ + for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){ if( d_qe->getInstantiator( i ) ){ if( d_qe->getInstantiator( i )->hasTerm( a ) ){ return true; @@ -623,7 +658,7 @@ Node EqualityQueryQuantifiersEngine::getRepresentative( Node a ){ if( ee->hasTerm( a ) ){ return ee->getRepresentative( a ); } - for( int i=0; i<theory::THEORY_LAST; i++ ){ + for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){ if( d_qe->getInstantiator( i ) ){ if( d_qe->getInstantiator( i )->hasTerm( a ) ){ return d_qe->getInstantiator( i )->getRepresentative( a ); @@ -643,7 +678,7 @@ bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){ return true; } } - for( int i=0; i<theory::THEORY_LAST; i++ ){ + for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){ if( d_qe->getInstantiator( i ) ){ if( d_qe->getInstantiator( i )->areEqual( a, b ) ){ return true; @@ -662,7 +697,7 @@ bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){ return true; } } - for( int i=0; i<theory::THEORY_LAST; i++ ){ + for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){ if( d_qe->getInstantiator( i ) ){ if( d_qe->getInstantiator( i )->areDisequal( a, b ) ){ return true; @@ -674,7 +709,7 @@ bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){ } Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a ){ - //for( int i=0; i<theory::THEORY_LAST; i++ ){ + //for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){ // if( d_qe->getInstantiator( i ) ){ // if( d_qe->getInstantiator( i )->hasTerm( a ) ){ // return d_qe->getInstantiator( i )->getInternalRepresentative( a ); @@ -684,3 +719,217 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a ){ //return a; return d_qe->getInstantiator( THEORY_UF )->getInternalRepresentative( a ); } + +inst::EqualityQuery* QuantifiersEngine::getEqualityQuery(TypeNode t) { + /** Should use skeleton (in order to have the type and the kind + or any needed other information) instead of only the type */ + + // TheoryId id = Theory::theoryOf(t); + // inst::EqualityQuery* eq = d_eq_query_arr[id]; + // if(eq == NULL) return d_eq_query_arr[theory::THEORY_UF]; + // else return eq; + + /** hack because the generic one is too slow */ + // TheoryId id = Theory::theoryOf(t); + // if( true || id == theory::THEORY_UF){ + // uf::InstantiatorTheoryUf* ith = static_cast<uf::InstantiatorTheoryUf*>( getInstantiator( theory::THEORY_UF )); + // return new uf::EqualityQueryInstantiatorTheoryUf(ith); + // } + // inst::EqualityQuery* eq = d_eq_query_arr[id]; + // if(eq == NULL) return d_eq_query_arr[theory::THEORY_UF]; + // else return eq; + + + //Currently we use the generic EqualityQuery + return getEqualityQuery(); +} + + +// // Just iterate amoung the equivalence class of the given node +// // node::Null() *can't* be given to reset +// class CandidateGeneratorClassGeneric : public CandidateGenerator{ +// private: +// //instantiator pointer +// EqualityEngine* d_ee; +// //the equality class iterator +// eq::EqClassIterator d_eqc; +// /* For the case where the given term doesn't exists in uf */ +// Node d_retNode; +// public: +// CandidateGeneratorTheoryEeClass( EqualityEngine* ee): d_ee( ee ){} +// ~CandidateGeneratorTheoryEeClass(){} +// void resetInstantiationRound(){}; +// void reset( TNode eqc ){ +// Assert(!eqc.isNull()); +// if( d_ee->hasTerm( eqc ) ){ +// /* eqc is in uf */ +// eqc = d_ee->getRepresentative( eqc ); +// d_eqc = eq::EqClassIterator( eqc, d_ee ); +// d_retNode = Node::null(); +// }else{ +// /* If eqc if not a term known by uf, it is the only one in its +// equivalence class. So we will return only it */ +// d_retNode = eqc; +// d_eqc = eq::EqClassIterator(); +// } +// }; //* the argument is not used +// TNode getNextCandidate(){ +// if(d_retNode.isNull()){ +// if( !d_eqc.isFinished() ) return (*(d_eqc++)); +// else return Node::null(); +// }else{ +// /* the case where eqc not in uf */ +// Node ret = d_retNode; +// d_retNode = Node::null(); /* d_eqc.isFinished() must be true */ +// return ret; +// } +// }; +// }; + + +class GenericCandidateGeneratorClasses: public rrinst::CandidateGenerator{ + + /** The candidate generators */ + rrinst::CandidateGenerator* d_can_gen[theory::THEORY_LAST]; + /** The current theory which candidategenerator is used */ + TheoryId d_can_gen_id; + +public: + GenericCandidateGeneratorClasses(QuantifiersEngine * qe){ + for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ + if(qe->getInstantiator(i) != NULL) + d_can_gen[i] = qe->getInstantiator(i)->getRRCanGenClasses(); + else d_can_gen[i] = NULL; + }; + } + + ~GenericCandidateGeneratorClasses(){ + for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ + delete(d_can_gen[i]); + }; + } + + void resetInstantiationRound(){ + for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ + if(d_can_gen[i] != NULL) d_can_gen[i]->resetInstantiationRound(); + }; + d_can_gen_id=THEORY_FIRST; + } + + void reset(TNode eqc){ + Assert(eqc.isNull()); + for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ + if(d_can_gen[i] != NULL) d_can_gen[i]->reset(eqc); + }; + d_can_gen_id=THEORY_FIRST; + lookForNextTheory(); + } + + TNode getNextCandidate(){ + Assert(THEORY_FIRST <= d_can_gen_id && d_can_gen_id <= THEORY_LAST); + /** No more */ + if(d_can_gen_id == THEORY_LAST) return TNode::null(); + /** Try with this theory */ + TNode cand = d_can_gen[d_can_gen_id]->getNextCandidate(); + if( !cand.isNull() ) return cand; + lookForNextTheory(); + return getNextCandidate(); + } + + void lookForNextTheory(){ + do{ /* look for the next available generator */ + ++d_can_gen_id; + } while( d_can_gen_id < THEORY_LAST && d_can_gen[d_can_gen_id] == NULL); + } + +}; + +class GenericCandidateGeneratorClass: public rrinst::CandidateGenerator{ + + /** The candidate generators */ + rrinst::CandidateGenerator* d_can_gen[theory::THEORY_LAST]; + /** The current theory which candidategenerator is used */ + TheoryId d_can_gen_id; + /** current node to look for equivalence class */ + Node d_node; + /** QuantifierEngine */ + QuantifiersEngine* d_qe; + +public: + GenericCandidateGeneratorClass(QuantifiersEngine * qe): d_qe(qe) { + for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ + if(d_qe->getInstantiator(i) != NULL) + d_can_gen[i] = d_qe->getInstantiator(i)->getRRCanGenClass(); + else d_can_gen[i] = NULL; + }; + } + + ~GenericCandidateGeneratorClass(){ + for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ + delete(d_can_gen[i]); + }; + } + + void resetInstantiationRound(){ + for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ + if(d_can_gen[i] != NULL) d_can_gen[i]->resetInstantiationRound(); + }; + d_can_gen_id=THEORY_FIRST; + } + + void reset(TNode eqc){ + for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ + if(d_can_gen[i] != NULL) d_can_gen[i]->reset(eqc); + }; + d_can_gen_id=THEORY_FIRST; + d_node = eqc; + lookForNextTheory(); + } + + TNode getNextCandidate(){ + Assert(THEORY_FIRST <= d_can_gen_id && d_can_gen_id <= THEORY_LAST); + /** No more */ + if(d_can_gen_id == THEORY_LAST) return TNode::null(); + /** Try with this theory */ + TNode cand = d_can_gen[d_can_gen_id]->getNextCandidate(); + if( !cand.isNull() ) return cand; + lookForNextTheory(); + return getNextCandidate(); + } + + void lookForNextTheory(){ + do{ /* look for the next available generator, where the element is */ + ++d_can_gen_id; + } while( + d_can_gen_id < THEORY_LAST && + (d_can_gen[d_can_gen_id] == NULL || + !d_qe->getInstantiator( d_can_gen_id )->hasTerm( d_node )) + ); + } + +}; + + +rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClasses() { + return new GenericCandidateGeneratorClasses(this); +} + +rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClass() { + return new GenericCandidateGeneratorClass(this); +} + +rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClasses(TypeNode t) { + // TheoryId id = Theory::theoryOf(t); + // rrinst::CandidateGenerator* eq = getInstantiator(id)->getRRCanGenClasses(); + // if(eq == NULL) return getInstantiator(id)->getRRCanGenClasses(); + // else return eq; + return getRRCanGenClasses(); +} + +rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClass(TypeNode t) { + // TheoryId id = Theory::theoryOf(t); + // rrinst::CandidateGenerator* eq = getInstantiator(id)->getRRCanGenClass(); + // if(eq == NULL) return getInstantiator(id)->getRRCanGenClass(); + // else return eq; + return getRRCanGenClass(); +} diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 5477214b0..157c0ac53 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -21,7 +21,8 @@ #include "theory/theory.h" #include "util/hash.h" -#include "theory/trigger.h" +#include "theory/inst_match.h" +#include "theory/rr_inst_match.h" #include "util/stats.h" @@ -33,16 +34,6 @@ namespace CVC4 { class TheoryEngine; -// attribute for "contains instantiation constants from" -struct InstConstantAttributeId {}; -typedef expr::Attribute<InstConstantAttributeId, Node> InstConstantAttribute; - -struct InstLevelAttributeId {}; -typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute; - -struct InstVarNumAttributeId {}; -typedef expr::Attribute<InstVarNumAttributeId, uint64_t> InstVarNumAttribute; - namespace theory { class QuantifiersEngine; @@ -126,7 +117,7 @@ namespace quantifiers { class QuantifiersEngine { friend class quantifiers::InstantiationEngine; friend class quantifiers::ModelEngine; - friend class InstMatch; + friend class inst::InstMatch; private: typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; /** reference to theory engine object */ @@ -139,7 +130,7 @@ private: quantifiers::ModelEngine* d_model_engine; /** equality query class */ EqualityQuery* d_eq_query; - +public: /** list of all quantifiers (pre-rewrite) */ std::vector< Node > d_quants; /** list of all quantifiers (post-rewrite) */ @@ -153,7 +144,7 @@ private: /** has added lemma this round */ bool d_hasAddedLemma; /** inst matches produced for each quantifier */ - std::map< Node, InstMatchTrie > d_inst_match_trie; + std::map< Node, inst::InstMatchTrie > d_inst_match_trie; /** owner of quantifiers */ std::map< Node, Theory* > d_owner; /** term database */ @@ -184,13 +175,24 @@ private: public: QuantifiersEngine(context::Context* c, TheoryEngine* te); - ~QuantifiersEngine(){} + ~QuantifiersEngine(); /** get instantiator for id */ - Instantiator* getInstantiator( int id ); + Instantiator* getInstantiator( theory::TheoryId id ); /** get theory engine */ TheoryEngine* getTheoryEngine() { return d_te; } - /** get equality query object */ - EqualityQuery* getEqualityQuery() { return d_eq_query; } + /** get equality query object for the given type. The default is the + generic one */ + inst::EqualityQuery* getEqualityQuery(TypeNode t); + inst::EqualityQuery* getEqualityQuery() { + return d_eq_query; + } + /** get equality query object for the given type. The default is the + one of UF */ + rrinst::CandidateGenerator* getRRCanGenClasses(TypeNode t); + rrinst::CandidateGenerator* getRRCanGenClass(TypeNode t); + /* generic candidate generator */ + rrinst::CandidateGenerator* getRRCanGenClasses(); + rrinst::CandidateGenerator* getRRCanGenClass(); /** get instantiation engine */ quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; } /** get model engine */ @@ -301,6 +303,14 @@ public: IntStat d_simple_triggers; IntStat d_multi_triggers; IntStat d_multi_trigger_instantiations; + IntStat d_term_in_termdb; + IntStat d_num_mono_candidates; + IntStat d_num_mono_candidates_new_term; + IntStat d_num_multi_candidates; + IntStat d_mono_candidates_cache_hit; + IntStat d_mono_candidates_cache_miss; + IntStat d_multi_candidates_cache_hit; + IntStat d_multi_candidates_cache_miss; Statistics(); ~Statistics(); };/* class QuantifiersEngine::Statistics */ diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp index 265026b39..57bc6d9cf 100644 --- a/src/theory/rewriterules/theory_rewriterules.cpp +++ b/src/theory/rewriterules/theory_rewriterules.cpp @@ -23,6 +23,8 @@ #include "theory/rewriterules/theory_rewriterules_preprocess.h" #include "theory/rewriter.h" +#include "util/options.h" + using namespace std; using namespace CVC4; @@ -30,6 +32,7 @@ using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::rewriterules; +using namespace CVC4::theory::rrinst; namespace CVC4 { @@ -69,14 +72,14 @@ size_t RuleInst::findGuard(TheoryRewriteRules & re, size_t start)const{ Node g = substNode(re,rule->guards[start],cache); switch(re.addWatchIfDontKnow(g,this,start)){ case ATRUE: - Debug("rewriterules") << g << "is true" << std::endl; + Debug("rewriterules::guards") << g << "is true" << std::endl; ++start; continue; case AFALSE: - Debug("rewriterules") << g << "is false" << std::endl; + Debug("rewriterules::guards") << g << "is false" << std::endl; return -1; case ADONTKNOW: - Debug("rewriterules") << g << "is unknown" << std::endl; + Debug("rewriterules::guards") << g << "is unknown" << std::endl; return start; } } @@ -132,31 +135,31 @@ TheoryRewriteRules::TheoryRewriteRules(context::Context* c, QuantifiersEngine* qe) : Theory(THEORY_REWRITERULES, c, u, out, valuation, logicInfo, qe), d_rules(c), d_ruleinsts(c), d_guardeds(c), d_checkLevel(c,0), - d_explanations(c), d_ruleinsts_to_add() + d_explanations(c), d_ruleinsts_to_add(), d_ppAssert_on(false) { d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); - Debug("rewriterules") << Node::setdepth(-1); - Debug("rewriterules-rewrite") << Node::setdepth(-1); } void TheoryRewriteRules::addMatchRuleTrigger(const RewriteRule * r, InstMatch & im, bool delay){ ++r->nb_matched; + ++d_statistics.d_match_found; if(rewrite_instantiation) im.applyRewrite(); if(representative_instantiation) im.makeRepresentative( getQuantifiersEngine() ); if(!cache_match || !r->inCache(*this,im)){ ++r->nb_applied; + ++d_statistics.d_cache_miss; std::vector<Node> subst; im.computeTermVec(getQuantifiersEngine(), r->inst_vars , subst); RuleInst * ri = new RuleInst(*this,r,subst, r->directrr ? im.d_matched : Node::null()); - Debug("rewriterules") << "One matching found" - << (delay? "(delayed)":"") - << ":" << *ri << std::endl; + Debug("rewriterules::matching") << "One matching found" + << (delay? "(delayed)":"") + << ":" << *ri << std::endl; // Find the first non verified guard, don't save the rule if the // rule can already be fired In fact I save it otherwise strange // things append. @@ -168,6 +171,8 @@ void TheoryRewriteRules::addMatchRuleTrigger(const RewriteRule * r, d_ruleinsts.push_back(ri); else delete(ri); }; + }else{ + ++d_statistics.d_cache_hit; }; } @@ -179,7 +184,11 @@ void TheoryRewriteRules::check(Effort level) { while(!done()) { // Get all the assertions // TODO: Test that it have already been ppAsserted - get(); + + //if we are here and ppAssert has not been done + // that means that ppAssert is off so we need to assert now + if(!d_ppAssert_on) addRewriteRule(get()); + else get(); // Assertion assertion = get(); // TNode fact = assertion.assertion; @@ -190,30 +199,30 @@ void TheoryRewriteRules::check(Effort level) { }; - Debug("rewriterules") << "Check:" << d_checkLevel << (level==EFFORT_FULL? " EFFORT_FULL":"") << std::endl; + Debug("rewriterules::check") << "RewriteRules::Check start " << d_checkLevel << (level==EFFORT_FULL? " EFFORT_FULL":"") << std::endl; /** Test each rewrite rule */ for(size_t rid = 0, end = d_rules.size(); rid < end; ++rid) { RewriteRule * r = d_rules[rid]; if (level!=EFFORT_FULL && r->d_split) continue; - Debug("rewriterules") << " rule: " << r << std::endl; + Debug("rewriterules::check") << "RewriteRules::Check rule: " << *r << std::endl; Trigger & tr = r->trigger; //reset instantiation round for trigger (set up match production) tr.resetInstantiationRound(); - //begin iterating from the first match produced by the trigger - tr.reset( Node::null() ); /** Test the possible matching one by one */ - InstMatch im; - while(tr.getNextMatch( im )){ + while(tr.getNextMatch()){ + InstMatch im = tr.getInstMatch(); addMatchRuleTrigger(r, im, true); - im.clear(); } } const bool do_notification = d_checkLevel == 0 || level==EFFORT_FULL; bool polldone = false; + if(level==EFFORT_FULL) ++d_statistics.d_full_check; + else ++d_statistics.d_check; + GuardedMap::const_iterator p = d_guardeds.begin(); do{ @@ -221,7 +230,7 @@ void TheoryRewriteRules::check(Effort level) { //dequeue instantiated rules for(; !d_ruleinsts_to_add.empty();){ RuleInst * ri = d_ruleinsts_to_add.back(); d_ruleinsts_to_add.pop_back(); - if(simulateRewritting && ri->alreadyRewritten(*this)) break; + if(simulateRewritting && ri->alreadyRewritten(*this)) continue; if(ri->findGuard(*this, 0) != ri->rule->guards.size()) d_ruleinsts.push_back(ri); else delete(ri); @@ -239,7 +248,7 @@ void TheoryRewriteRules::check(Effort level) { bool value; if(getValuation().hasSatValue(g,value)){ if(value) polldone = true; //One guard is true so pass n check - Debug("rewriterules") << "Poll value:" << g + Debug("rewriterules::guards") << "Poll value:" << g << " is " << (value ? "true" : "false") << std::endl; notification(g,value); //const Guarded & glast2 = (*l)[l->size()-1]; @@ -266,14 +275,14 @@ void TheoryRewriteRules::check(Effort level) { // If it has a value it should already has been notified bool value; value = value; // avoiding the warning in non debug mode Assert(!getValuation().hasSatValue(g,value)); - Debug("rewriterules") << "Narrowing on:" << g << std::endl; + Debug("rewriterules::check") << "RewriteRules::Check Narrowing on:" << g << std::endl; /** Can split on already rewritten instrule... but... */ getOutputChannel().split(g); } } Assert(d_ruleinsts_to_add.empty()); - Debug("rewriterules") << "Check done:" << d_checkLevel << std::endl; + Debug("rewriterules::check") << "RewriteRules::Check done " << d_checkLevel << std::endl; }; @@ -283,7 +292,13 @@ Trigger TheoryRewriteRules::createTrigger( TNode n, std::vector<Node> & pattern // Debug("rewriterules") << "createTrigger:"; getQuantifiersEngine()->registerPattern(pattern); return *Trigger::mkTrigger(getQuantifiersEngine(),n,pattern, - match_gen_kind, true); + Options::current()->efficientEMatching? + Trigger::MATCH_GEN_EFFICIENT_E_MATCH : + Trigger::MATCH_GEN_DEFAULT, + true, + Trigger::TR_MAKE_NEW, + false); + // Options::current()->smartMultiTriggers); }; bool TheoryRewriteRules::notifyIfKnown(const GList * const ltested, @@ -299,9 +314,9 @@ bool TheoryRewriteRules::notifyIfKnown(const GList * const ltested, void TheoryRewriteRules::notification(GList * const lpropa, bool b){ if (b){ - for(GList::const_iterator g = lpropa->begin(); - g != lpropa->end(); ++g) { - (*g).nextGuard(*this); + for(size_t ig = 0; + ig != lpropa->size(); ++ig) { + (*lpropa)[ig].nextGuard(*this); }; lpropa->push_back(Guarded(RULEINST_TRUE,0)); }else{ @@ -315,16 +330,6 @@ void TheoryRewriteRules::notification(GList * const lpropa, bool b){ Answer TheoryRewriteRules::addWatchIfDontKnow(Node g0, const RuleInst* ri, const size_t gid){ - /** TODO: Should use the representative of g, but should I keep the - mapping for myself? */ - //AJR: removed this code after talking with Francois - ///* If it false in one model (current valuation) it's false for all */ - //if (useCurrentModel){ - // Node val = getValuation().getValue(g0); - // Debug("rewriterules") << "getValue:" << g0 << " = " - // << val << " is " << (val == d_false) << std::endl; - // if (val == d_false) return AFALSE; - //}; /** Currently create a node with a literal */ Node g = getValuation().ensureLiteral(g0); GuardedMap::iterator l_i = d_guardeds.find(g); @@ -384,68 +389,119 @@ void TheoryRewriteRules::notifyEq(TNode lhs, TNode rhs) { }; +Node TheoryRewriteRules::normalizeConjunction(NodeBuilder<> & conjunction){ + Assert(conjunction.getKind() == kind::AND); + switch(conjunction.getNumChildren()){ + case 0: + return d_true; + case 1: + return conjunction[0]; + default: + return conjunction; + } + +} + +void explainInstantiation(const RuleInst *inst, TNode substHead, NodeBuilder<> & conjunction ){ + TypeNode booleanType = NodeManager::currentNM()->booleanType(); + // if the rule is directly applied by the rewriter, + // we should take care to use the representative that can't be directly rewritable: + // If "car(a)" is somewhere and we know that "a = cons(x,l)" we shouldn't + // add the constraint car(cons(x,l) = x because it is rewritten to x = x. + // But we should say cons(a) = x + Assert(!inst->d_matched.isNull()); + Assert( inst->d_matched.getKind() == kind::APPLY_UF); + Assert( substHead.getKind() == kind::APPLY_UF ); + Assert( inst->d_matched.getOperator() == substHead.getOperator() ); + Assert(conjunction.getKind() == kind::AND); + // replace the left hand side by the term really matched + NodeBuilder<2> nb; + for(size_t i = 0, + iend = inst->d_matched.getNumChildren(); i < iend; ++i){ + nb.clear( inst->d_matched[i].getType(false) == booleanType ? + kind::IFF : kind::EQUAL ); + nb << inst->d_matched[i] << substHead[i]; + conjunction << static_cast<Node>(nb); + } +} + +Node skolemizeBody( Node f ){ + /*TODO skolemize the subformula of s with constant or skolemize + directly in the body of the rewrite rule with an uninterpreted + function. + */ + if ( f.getKind()!=EXISTS ) return f; + std::vector< Node > vars; + std::vector< Node > csts; + for( int i=0; i<(int)f[0].getNumChildren(); i++ ){ + csts.push_back( NodeManager::currentNM()->mkSkolem( f[0][i].getType()) ); + vars.push_back( f[0][i] ); + } + return f[ 1 ].substitute( vars.begin(), vars.end(), + csts.begin(), csts.end() ); +} + + void TheoryRewriteRules::propagateRule(const RuleInst * inst, TCache cache){ // Debug("rewriterules") << "A rewrite rules is verified. Add lemma:"; - Debug("rewriterules") << "propagateRule" << *inst << std::endl; + Debug("rewriterules::propagate") << "propagateRule" << *inst << std::endl; const RewriteRule * rule = inst->rule; ++rule->nb_applied; // Can be more something else than an equality in fact (eg. propagation rule) - Node equality = inst->substNode(*this,rule->body,cache); + Node equality = skolemizeBody(inst->substNode(*this,rule->body,cache)); if(propagate_as_lemma){ Node lemma = equality; - if(rule->guards.size() > 0){ - // TODO: problem with reduction rule => instead of <=> - lemma = substGuards(inst, cache).impNode(equality); - }; if(rule->directrr){ - TypeNode booleanType = NodeManager::currentNM()->booleanType(); - // if the rule is directly applied by the rewriter, - // we should take care to use the representative that can't be directly rewritable: - // If "car(a)" is somewhere and we know that "a = cons(x,l)" we shouldn't - // add the constraint car(cons(x,l) = x because it is rewritten to x = x. - // But we should say cons(a) = x - Assert(lemma.getKind() == kind::EQUAL || - lemma.getKind() == kind::IMPLIES); - Assert(!inst->d_matched.isNull()); - Assert( inst->d_matched.getOperator() == lemma[0].getOperator() ); - // replace the left hand side by the term really matched + NodeBuilder<> conjunction(kind::AND); + explainInstantiation(inst, + rule->guards.size() > 0? + inst->substNode(*this,rule->guards[0],cache) : equality[0], + conjunction); Debug("rewriterules-directrr") << "lemma:" << lemma << " :: " << inst->d_matched; - Node hyp; - NodeBuilder<2> nb; - if(inst->d_matched.getNumChildren() == 1){ - nb.clear( inst->d_matched[0].getType(false) == booleanType ? - kind::IFF : kind::EQUAL ); - nb << inst->d_matched[0] << lemma[0][0]; - hyp = nb; - }else{ - NodeBuilder<> andb(kind::AND); - for(size_t i = 0, - iend = inst->d_matched.getNumChildren(); i < iend; ++i){ - nb.clear( inst->d_matched[i].getType(false) == booleanType ? - kind::IFF : kind::EQUAL ); - nb << inst->d_matched[i] << lemma[0][i]; - andb << static_cast<Node>(nb); - } - hyp = andb; - }; - nb.clear(lemma.getKind()); - nb << inst->d_matched << lemma[1]; - lemma = hyp.impNode(static_cast<Node>(nb)); + //rewrite rule + TypeNode booleanType = NodeManager::currentNM()->booleanType(); + if(equality[1].getType(false) == booleanType) + equality = inst->d_matched.iffNode(equality[1]); + else equality = inst->d_matched.eqNode(equality[1]); + lemma = normalizeConjunction(conjunction).impNode(equality); Debug("rewriterules-directrr") << " -> " << lemma << std::endl; - }; - // Debug("rewriterules") << "lemma:" << lemma << std::endl; + } + else if(rule->guards.size() > 0){ + // We can use implication for reduction rules since the head is known + // to be true + NodeBuilder<> conjunction(kind::AND); + substGuards(inst,cache,conjunction); + lemma = normalizeConjunction(conjunction).impNode(equality); + } + Debug("rewriterules::propagate") << "propagated " << lemma << std::endl; getOutputChannel().lemma(lemma); }else{ - Assert(!direct_rewrite); - Node lemma_lit = getValuation().ensureLiteral(equality); + Node lemma_lit = equality; + if(rule->directrr && rule->guards.size() == 0) + lemma_lit = inst->d_matched.eqNode(equality[1]); // rewrite rules + lemma_lit = getValuation().ensureLiteral(lemma_lit); ExplanationMap::const_iterator p = d_explanations.find(lemma_lit); if(p!=d_explanations.end()) return; //Already propagated bool value; if(getValuation().hasSatValue(lemma_lit,value)){ /* Already assigned */ if (!value){ - Node conflict = substGuards(inst,cache,lemma_lit); - getOutputChannel().conflict(conflict); + NodeBuilder<> conflict(kind::AND); + + if(rule->directrr){ + explainInstantiation(inst, + rule->guards.size() > 0? + inst->substNode(*this,rule->guards[0],cache) : equality[0], + conflict); + if(rule->guards.size() > 0){ + //reduction rule + Assert(rule->guards.size() == 1); + conflict << inst->d_matched; //this one will be two times + } + } + substGuards(inst,cache,conflict); + conflict << lemma_lit; + getOutputChannel().conflict(normalizeConjunction(conflict)); }; }else{ getOutputChannel().propagate(lemma_lit); @@ -456,57 +512,79 @@ void TheoryRewriteRules::propagateRule(const RuleInst * inst, TCache cache){ if(simulateRewritting){ static NoMatchAttribute rewrittenNodeAttribute; // Tag the rewritted terms - for(std::vector<Node>::iterator i = rule->to_remove.begin(); - i == rule->to_remove.end(); ++i){ - (*i).setAttribute(rewrittenNodeAttribute,true); + // for(std::vector<Node>::iterator i = rule->to_remove.begin(); + // i == rule->to_remove.end(); ++i){ + // (*i).setAttribute(rewrittenNodeAttribute,true); + // }; + for(size_t i = 0; i < rule->to_remove.size(); ++i){ + Node rewritten = inst->substNode(*this,rule->to_remove[i],cache); + Debug("rewriterules::simulateRewriting") << "tag " << rewritten << " as rewritten" << std::endl; + rewritten.setAttribute(rewrittenNodeAttribute,true); }; + }; - //Verify that this instantiation can't immediately fire another rule - for(RewriteRule::BodyMatch::const_iterator p = rule->body_match.begin(); - p != rule->body_match.end(); ++p){ - RewriteRule * r = (*p).second; - // Debug("rewriterules") << " rule: " << r << std::endl; - // Use trigger2 since we can be in check - Trigger & tr = r->trigger_for_body_match; - InstMatch im; - TNode m = inst->substNode(*this,(*p).first, cache); - tr.getMatch(m,im); - if(!im.empty()){ - im.d_matched = m; - addMatchRuleTrigger(r, im); + if ( compute_opt && !rule->body_match.empty() ){ + + uf::TheoryUF* uf = static_cast<uf::TheoryUF *>(getQuantifiersEngine()->getTheoryEngine()->getTheory( theory::THEORY_UF )); + eq::EqualityEngine* ee = + static_cast<eq::EqualityEngine*>(uf->getEqualityEngine()); + + //Verify that this instantiation can't immediately fire another rule + for(RewriteRule::BodyMatch::const_iterator p = rule->body_match.begin(); + p != rule->body_match.end(); ++p){ + RewriteRule * r = (*p).second; + // Use trigger2 since we can be in check + ApplyMatcher * tr = r->trigger_for_body_match; + Assert(tr != NULL); + tr->resetInstantiationRound(getQuantifiersEngine()); + InstMatch im; + TNode m = inst->substNode(*this,(*p).first, cache); + Assert( m.getKind() == kind::APPLY_UF ); + ee->addTerm(m); + if( tr->reset(m,im,getQuantifiersEngine()) ){ + im.d_matched = m; + Debug("rewriterules::matching") << "SimulatedRewrite: " << std::endl; + addMatchRuleTrigger(r, im); + } } + } }; - -Node TheoryRewriteRules::substGuards(const RuleInst *inst, +void TheoryRewriteRules::substGuards(const RuleInst *inst, TCache cache, - /* Already substituted */ - Node last){ + NodeBuilder<> & conjunction){ const RewriteRule * r = inst->rule; - /** No guards */ - const size_t size = r->guards.size(); - if(size == 0) return (last.isNull()?d_true:last); - /** One guard */ - if(size == 1 && last.isNull()) return inst->substNode(*this,r->guards[0],cache); /** Guards */ /* TODO remove the duplicate with a set like in uf? */ - NodeBuilder<> conjunction(kind::AND); for(std::vector<Node>::const_iterator p = r->guards.begin(); p != r->guards.end(); ++p) { Assert(!p->isNull()); conjunction << inst->substNode(*this,*p,cache); }; - if (!last.isNull()) conjunction << last; - return conjunction; } Node TheoryRewriteRules::explain(TNode n){ ExplanationMap::const_iterator p = d_explanations.find(n); Assert(p!=d_explanations.end(),"I forget the explanation..."); - RuleInst i = (*p).second; - //Notice() << n << "<-" << *(i.rule) << std::endl; - return substGuards(&i, TCache ()); + RuleInst inst = (*p).second; + const RewriteRule * rule = inst.rule; + TCache cache; + NodeBuilder<> explanation(kind::AND); + if(rule->directrr){ + explainInstantiation(&inst, + rule->guards.size() > 0? + inst.substNode(*this,rule->guards[0],cache): + inst.substNode(*this,rule->body[0] ,cache), + explanation); + if(rule->guards.size() > 0){ + //reduction rule + Assert(rule->guards.size() == 1); + explanation << inst.d_matched; //this one will be two times + } + }; + substGuards(&inst, cache ,explanation); + return normalizeConjunction(explanation); } void TheoryRewriteRules::collectModelInfo( TheoryModel* m ){ @@ -515,9 +593,39 @@ void TheoryRewriteRules::collectModelInfo( TheoryModel* m ){ Theory::PPAssertStatus TheoryRewriteRules::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { addRewriteRule(in); + d_ppAssert_on = true; return PP_ASSERT_STATUS_UNSOLVED; } +TheoryRewriteRules::Statistics::Statistics(): + d_num_rewriterules("TheoryRewriteRules::Num_RewriteRules", 0), + d_check("TheoryRewriteRules::Check", 0), + d_full_check("TheoryRewriteRules::FullCheck", 0), + d_poll("TheoryRewriteRules::Poll", 0), + d_match_found("TheoryRewriteRules::MatchFound", 0), + d_cache_hit("TheoryRewriteRules::CacheHit", 0), + d_cache_miss("TheoryRewriteRules::CacheMiss", 0) +{ + StatisticsRegistry::registerStat(&d_num_rewriterules); + StatisticsRegistry::registerStat(&d_check); + StatisticsRegistry::registerStat(&d_full_check); + StatisticsRegistry::registerStat(&d_poll); + StatisticsRegistry::registerStat(&d_match_found); + StatisticsRegistry::registerStat(&d_cache_hit); + StatisticsRegistry::registerStat(&d_cache_miss); +} + +TheoryRewriteRules::Statistics::~Statistics(){ + StatisticsRegistry::unregisterStat(&d_num_rewriterules); + StatisticsRegistry::unregisterStat(&d_check); + StatisticsRegistry::unregisterStat(&d_full_check); + StatisticsRegistry::unregisterStat(&d_poll); + StatisticsRegistry::unregisterStat(&d_match_found); + StatisticsRegistry::unregisterStat(&d_cache_hit); + StatisticsRegistry::unregisterStat(&d_cache_miss); +} + + }/* CVC4::theory::rewriterules namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h index d1c3eecf3..fcbdfe8b9 100644 --- a/src/theory/rewriterules/theory_rewriterules.h +++ b/src/theory/rewriterules/theory_rewriterules.h @@ -27,7 +27,9 @@ #include "theory/theory_engine.h" #include "theory/quantifiers_engine.h" #include "context/context_mm.h" -#include "theory/inst_match_impl.h" +#include "theory/rr_inst_match_impl.h" +#include "theory/rr_trigger.h" +#include "theory/rr_inst_match.h" #include "util/stats.h" #include "theory/rewriterules/theory_rewriterules_preprocess.h" #include "theory/model.h" @@ -35,6 +37,8 @@ namespace CVC4 { namespace theory { namespace rewriterules { +using namespace CVC4::theory::rrinst; +typedef CVC4::theory::rrinst::Trigger Trigger; typedef std::hash_map<TNode, TNode, TNodeHashFunction> TCache; @@ -45,6 +49,7 @@ typedef std::hash_map<TNode, TNode, TNodeHashFunction> TCache; class RewriteRule{ public: // constant + const size_t id; //for debugging const bool d_split; mutable Trigger trigger; std::vector<Node> guards; @@ -58,7 +63,7 @@ typedef std::hash_map<TNode, TNode, TNodeHashFunction> TCache; rule) */ typedef context::CDList< std::pair<TNode,RewriteRule* > > BodyMatch; mutable BodyMatch body_match; - mutable Trigger trigger_for_body_match; // used because we can be matching + mutable ApplyMatcher * trigger_for_body_match; // used because we can be matching // trigger when we need new match. // So currently we use another // trigger for that. @@ -70,7 +75,7 @@ typedef std::hash_map<TNode, TNode, TNodeHashFunction> TCache; const bool directrr; RewriteRule(TheoryRewriteRules & re, - Trigger & tr, Trigger & tr2, + Trigger & tr, ApplyMatcher * tr2, std::vector<Node> & g, Node b, TNode nt, std::vector<Node> & fv,std::vector<Node> & iv, std::vector<Node> & to_r, bool drr); @@ -183,6 +188,7 @@ private: inside check */ typedef std::vector< RuleInst* > QRuleInsts; QRuleInsts d_ruleinsts_to_add; + bool d_ppAssert_on; //Indicate if a ppAssert have been done public: /** true and false for predicate */ @@ -240,15 +246,17 @@ private: already true */ bool notifyIfKnown(const GList * const ltested, GList * const lpropa); - Node substGuards(const RuleInst * inst, + void substGuards(const RuleInst * inst, TCache cache, - Node last = Node::null()); + NodeBuilder<> & conjunction); void addRewriteRule(const Node r); void computeMatchBody ( const RewriteRule * r, size_t start = 0); void addMatchRuleTrigger(const RewriteRule* r, InstMatch & im, bool delay = true); + Node normalizeConjunction(NodeBuilder<> & conjunction); + /* rewrite pattern */ typedef std::hash_map< Node, rewriter::RRPpRewrite*, NodeHashFunction > RegisterRRPpRewrite; RegisterRRPpRewrite d_registeredRRPpRewrite; @@ -257,6 +265,21 @@ private: rewriter::Subst & pvars, rewriter::Subst & vars); + /** statistics class */ + class Statistics { + public: + IntStat d_num_rewriterules; + IntStat d_check; + IntStat d_full_check; + IntStat d_poll; + IntStat d_match_found; + IntStat d_cache_hit; + IntStat d_cache_miss; + Statistics(); + ~Statistics(); + }; + Statistics d_statistics; + };/* class TheoryRewriteRules */ }/* CVC4::theory::rewriterules namespace */ diff --git a/src/theory/rewriterules/theory_rewriterules_params.h b/src/theory/rewriterules/theory_rewriterules_params.h index 9ab2ae3e7..de51215d1 100644 --- a/src/theory/rewriterules/theory_rewriterules_params.h +++ b/src/theory/rewriterules/theory_rewriterules_params.h @@ -17,7 +17,6 @@ ** \todo document this file **/ - #ifndef __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PARAMS_H #define __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PARAMS_H @@ -58,7 +57,7 @@ static const bool representative_instantiation = false; Allow to break loop with other theories. */ -static const size_t checkSlowdown = 10; +static const size_t checkSlowdown = 0; /** Use the current model to eliminate guard before asking for notification @@ -68,14 +67,7 @@ static const bool useCurrentModel = false; /** Simulate rewriting by tagging rewritten terms. */ -static const bool simulateRewritting = false; - -/** - Choose the kind of matching to use: - - InstMatchGenerator::MATCH_GEN_DEFAULT 0 - - InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH 1 -*/ -static const int match_gen_kind = 0; +static const bool simulateRewritting = true; /** Do narrowing at full effort @@ -85,7 +77,7 @@ static const bool narrowing_full_effort = false; /** Direct rewrite: Add rewrite rules directly in the rewriter. */ -static const bool direct_rewrite = true; +static const bool direct_rewrite = false; }/* CVC4::theory::rewriterules namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/rewriterules/theory_rewriterules_rules.cpp b/src/theory/rewriterules/theory_rewriterules_rules.cpp index c3116aba0..1ad8fdaa7 100644 --- a/src/theory/rewriterules/theory_rewriterules_rules.cpp +++ b/src/theory/rewriterules/theory_rewriterules_rules.cpp @@ -21,6 +21,7 @@ #include "theory/rewriterules/theory_rewriterules_params.h" #include "theory/rewriterules/theory_rewriterules_preprocess.h" #include "theory/rewriterules/theory_rewriterules.h" +#include "util/options.h" #include "theory/quantifiers/term_database.h" @@ -30,12 +31,46 @@ using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::rewriterules; +using namespace CVC4::theory::rrinst; namespace CVC4 { namespace theory { namespace rewriterules { +// TODO replace by a real dictionnary +// We should create a real substitution? slower more precise +// We don't do that often +bool nonunifiable( TNode t0, TNode pattern, const std::vector<Node> & vars){ + typedef std::vector<std::pair<TNode,TNode> > tstack; + tstack stack(1,std::make_pair(t0,pattern)); // t * pat + + while(!stack.empty()){ + const std::pair<TNode,TNode> p = stack.back(); stack.pop_back(); + const TNode & t = p.first; + const TNode & pat = p.second; + + // t or pat is a variable currently we consider that can match anything + if( find(vars.begin(),vars.end(),t) != vars.end() ) continue; + if( pat.getKind() == INST_CONSTANT ) continue; + + // t and pat are nonunifiable + if( !Trigger::isAtomicTrigger( t ) || !Trigger::isAtomicTrigger( pat ) ) { + if(t == pat) continue; + else return true; + }; + if( t.getOperator() != pat.getOperator() ) return true; + + //put the children on the stack + for( size_t i=0; i < pat.getNumChildren(); i++ ){ + stack.push_back(std::make_pair(t[i],pat[i])); + }; + } + // The heuristic can't find non-unifiability + return false; +} + + void TheoryRewriteRules::computeMatchBody ( const RewriteRule * rule, size_t start){ std::vector<TNode> stack(1,rule->new_terms); @@ -50,9 +85,9 @@ void TheoryRewriteRules::computeMatchBody ( const RewriteRule * rule, if( t.getKind() == APPLY_UF ){ for(size_t rid = start, end = d_rules.size(); rid < end; ++rid) { RewriteRule * r = d_rules[rid]; - if(r->d_split) continue; - Trigger & tr = const_cast<Trigger &> (r->trigger_for_body_match); - if(!tr.nonunifiable(t, rule->free_vars)){ + if(r->d_split || r->trigger_for_body_match == NULL) continue; + //the split rules are not computed and the one with multi-pattern + if( !nonunifiable(t, r->trigger_for_body_match->d_pattern, rule->free_vars)){ rule->body_match.push_back(std::make_pair(t,r)); } } @@ -74,7 +109,10 @@ inline void addPattern(TheoryRewriteRules & re, TNode r){ if (tri.getKind() == kind::NOT && tri[0].getKind() == kind::APPLY_UF) tri = tri[0]; - pattern.push_back(re.getQuantifiersEngine()->getTermDatabase()-> + pattern.push_back( + Options::current()->rewriteRulesAsAxioms? + static_cast<Node>(tri): + re.getQuantifiersEngine()->getTermDatabase()-> convertNodeToPattern(tri,r,vars,inst_constants)); } @@ -106,6 +144,7 @@ bool checkPatternVars(const std::vector<Node> & pattern, void TheoryRewriteRules::addRewriteRule(const Node r) { Assert(r.getKind() == kind::REWRITE_RULE); + Kind rrkind = r[2].getKind(); /* Replace variables by Inst_* variable and tag the terms that contain them */ std::vector<Node> vars; @@ -125,16 +164,20 @@ void TheoryRewriteRules::addRewriteRule(const Node r) when fired */ /* shortcut */ TNode head = r[2][0]; - switch(r[2].getKind()){ + TypeNode booleanType = NodeManager::currentNM()->booleanType(); + switch(rrkind){ case kind::RR_REWRITE: /* Equality */ to_remove.push_back(head); addPattern(*this,head,pattern,vars,inst_constants,r); - body = head.eqNode(body); + if(head.getType(false) == booleanType) body = head.iffNode(body); + else body = head.eqNode(body); break; case kind::RR_REDUCTION: /** Add head to remove */ - to_remove.push_back(head); + for(Node::iterator i = head.begin(); i != head.end(); ++i) { + to_remove.push_back(*i); + }; case kind::RR_DEDUCTION: /** Add head to guards and pattern */ switch(head.getKind()){ @@ -171,32 +214,65 @@ void TheoryRewriteRules::addRewriteRule(const Node r) }; /* Add the other triggers */ if( r[2].getNumChildren() >= 3 ) - for(Node::iterator i = r[2][2].begin(); i != r[2][2].end(); ++i) { + for(Node::iterator i = r[2][2][0].begin(); i != r[2][2][0].end(); ++i) { // todo test during typing that its a good term (no not, atom, or term...) - addPattern(*this,(*i)[0],pattern,vars,inst_constants,r); + addPattern(*this,*i,pattern,vars,inst_constants,r); }; // Assert(pattern.size() == 1, "currently only single pattern are supported"); + + + + + //If we convert to usual axioms + if(Options::current()->rewriteRulesAsAxioms){ + NodeBuilder<> forallB(kind::FORALL); + forallB << r[0]; + NodeBuilder<> guardsB(kind::AND); + guardsB.append(guards); + forallB << normalizeConjunction(guardsB).impNode(body); + NodeBuilder<> patternB(kind::INST_PATTERN); + patternB.append(pattern); + NodeBuilder<> patternListB(kind::INST_PATTERN_LIST); + patternListB << static_cast<Node>(patternB); + forallB << static_cast<Node>(patternListB); + getOutputChannel().lemma((Node) forallB); + return; + } + + //turn all to propagate + // if(true){ + // NodeBuilder<> guardsB(kind::AND); + // guardsB.append(guards); + // body = normalizeConjunction(guardsB).impNode(body); + // guards.clear(); + // rrkind = kind::RR_DEDUCTION; + // } + + //Every variable must be seen in the pattern if (!checkPatternVars(pattern,inst_constants)){ - Warning() << "The rule" << r << + Warning() << Node::setdepth(-1) << "The rule" << r << " has been removed since it doesn't contain every variables." << std::endl; return; } + //Add to direct rewrite rule bool directrr = false; if(direct_rewrite && - ((guards.size() == 0 && r[2].getKind() == kind::RR_REWRITE) || - (guards.size() == 1 && r[2].getKind() == kind::RR_REDUCTION)) + guards.size() == 0 && rrkind == kind::RR_REWRITE && pattern.size() == 1){ directrr = addRewritePattern(pattern[0],new_terms, inst_constants, vars); } + // final construction Trigger trigger = createTrigger(r,pattern); - Trigger trigger2 = createTrigger(r,pattern); //Hack - RewriteRule * rr = new RewriteRule(*this, trigger, trigger2, + ApplyMatcher * applymatcher = + pattern.size() == 1 && pattern[0].getKind() == kind::APPLY_UF? + new ApplyMatcher(pattern[0],getQuantifiersEngine()) : NULL; + RewriteRule * rr = new RewriteRule(*this, trigger, applymatcher, guards, body, new_terms, vars, inst_constants, to_remove, directrr); @@ -209,7 +285,7 @@ void TheoryRewriteRules::addRewriteRule(const Node r) computeMatchBody(d_rules[rid], d_rules.size() - 1); - Debug("rewriterules") << "created rewriterule"<< (rr->d_split?"(split)":"") << ":(" << d_rules.size() - 1 << ")" + Debug("rewriterules::new") << "created rewriterule"<< (rr->d_split?"(split)":"") << ":(" << d_rules.size() - 1 << ")" << *rr << std::endl; } @@ -227,7 +303,7 @@ bool willDecide(TNode node, bool positive = true){ case XOR: return true; case IMPLIES: - return false; + return true; case ITE: return true; case NOT: @@ -237,45 +313,50 @@ bool willDecide(TNode node, bool positive = true){ } } - +static size_t id_next = 0; RewriteRule::RewriteRule(TheoryRewriteRules & re, - Trigger & tr, Trigger & tr2, + Trigger & tr, ApplyMatcher * applymatcher, std::vector<Node> & g, Node b, TNode nt, std::vector<Node> & fv,std::vector<Node> & iv, std::vector<Node> & to_r, bool drr) : - d_split(willDecide(b)), + id(++id_next), d_split(willDecide(b)), trigger(tr), body(b), new_terms(nt), free_vars(), inst_vars(), - body_match(re.getSatContext()),trigger_for_body_match(tr2), + body_match(re.getSatContext()),trigger_for_body_match(applymatcher), d_cache(re.getSatContext(),re.getQuantifiersEngine()), directrr(drr){ free_vars.swap(fv); inst_vars.swap(iv); guards.swap(g); to_remove.swap(to_r); }; bool RewriteRule::inCache(TheoryRewriteRules & re, InstMatch & im)const{ - return !d_cache.addInstMatch(im); + bool res = !d_cache.addInstMatch(im); + Debug("rewriterules::matching") << "rewriterules::cache " << im + << (res ? " HIT" : " MISS") << std::endl; + return res; }; /** A rewrite rule */ void RewriteRule::toStream(std::ostream& out) const{ + out << "[" << id << "] "; for(std::vector<Node>::const_iterator iter = guards.begin(); iter != guards.end(); ++iter){ out << *iter; }; out << "=>" << body << std::endl; - out << "["; + out << "{"; for(BodyMatch::const_iterator iter = body_match.begin(); iter != body_match.end(); ++iter){ - out << (*iter).first << "(" << (*iter).second << ")" << ","; + out << (*iter).first << "[" << (*iter).second->id << "]" << ","; }; - out << "]" << (directrr?"*":"") << std::endl; + out << "}" << (directrr?"*":"") << std::endl; } RewriteRule::~RewriteRule(){ - Debug("rewriterule-stats") << *this + Debug("rewriterule::stats") << *this << " (" << nb_matched << "," << nb_applied << "," << nb_propagated << ")" << std::endl; + delete(trigger_for_body_match); } bool TheoryRewriteRules::addRewritePattern(TNode pattern, TNode body, diff --git a/src/theory/rewriterules/theory_rewriterules_type_rules.h b/src/theory/rewriterules/theory_rewriterules_type_rules.h index 8bc4522a1..605324b20 100644 --- a/src/theory/rewriterules/theory_rewriterules_type_rules.h +++ b/src/theory/rewriterules/theory_rewriterules_type_rules.h @@ -45,16 +45,16 @@ public: Assert(n.getKind() == kind::REWRITE_RULE && n.getNumChildren()==3 ); if( check ){ if( n[ 0 ].getType(check)!=nodeManager->boundVarListType() ){ - throw TypeCheckingExceptionPrivate(n, + throw TypeCheckingExceptionPrivate(n[0], "first argument of rewrite rule is not bound var list"); } if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){ - throw TypeCheckingExceptionPrivate(n, + throw TypeCheckingExceptionPrivate(n[1], "guard of rewrite rule is not an actual guard"); } if( n[2].getType(check) != TypeNode(nodeManager->mkTypeConst<TypeConstant>(RRHB_TYPE))){ - throw TypeCheckingExceptionPrivate(n, + throw TypeCheckingExceptionPrivate(n[2], "not a correct rewrite rule"); } } diff --git a/src/theory/rr_inst_match.cpp b/src/theory/rr_inst_match.cpp new file mode 100644 index 000000000..3ba0c8d32 --- /dev/null +++ b/src/theory/rr_inst_match.cpp @@ -0,0 +1,1447 @@ +/********************* */ +/*! \file inst_match.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of inst match class + **/ + +#include "theory/inst_match.h" +#include "theory/rr_inst_match.h" +#include "theory/rr_trigger.h" +#include "theory/rr_inst_match_impl.h" +#include "theory/theory_engine.h" +#include "theory/quantifiers_engine.h" +#include "theory/uf/theory_uf_instantiator.h" +#include "theory/uf/theory_uf_candidate_generator.h" +#include "theory/datatypes/theory_datatypes_candidate_generator.h" +#include "theory/uf/equality_engine.h" +#include "theory/arrays/theory_arrays.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::rrinst; +using namespace CVC4::theory::uf::rrinst; +using namespace CVC4::theory::eq::rrinst; + +namespace CVC4{ +namespace theory{ +namespace rrinst{ + +typedef CVC4::theory::inst::InstMatch InstMatch; +typedef CVC4::theory::inst::CandidateGeneratorQueue CandidateGeneratorQueue; + +template<bool modEq> +class InstMatchTrie2Pairs +{ + typename std::vector< std::vector < typename InstMatchTrie2Gen<modEq>::Tree > > d_data; + InstMatchTrie2Gen<modEq> d_backtrack; +public: + InstMatchTrie2Pairs(context::Context* c, QuantifiersEngine* q, size_t n): + d_backtrack(c,q) { + // resize to a triangle + // + // | * + // | * * + // | * * * + // | -----> i + d_data.resize(n); + for(size_t i=0; i < n; ++i){ + d_data[i].resize(i+1,typename InstMatchTrie2Gen<modEq>::Tree(0)); + } + }; + InstMatchTrie2Pairs(const InstMatchTrie2Pairs &) CVC4_UNDEFINED; + const InstMatchTrie2Pairs & operator =(const InstMatchTrie2Pairs & e) CVC4_UNDEFINED; + /** add match m in the trie, + return true if it was never seen */ + inline bool addInstMatch( size_t i, size_t j, InstMatch& m){ + size_t k = std::min(i,j); + size_t l = std::max(i,j); + return d_backtrack.addInstMatch(m,&(d_data[l][k])); + }; + inline bool addInstMatch( size_t i, InstMatch& m){ + return d_backtrack.addInstMatch(m,&(d_data[i][i])); + }; + +}; + + +// Currently the implementation doesn't take into account that +// variable should have the same value given. +// TODO use the d_children way perhaps +// TODO replace by a real dictionnary +// We should create a real substitution? slower more precise +// We don't do that often +bool nonunifiable( TNode t0, TNode pat, const std::vector<Node> & vars){ + if(pat.isNull()) return true; + + typedef std::vector<std::pair<TNode,TNode> > tstack; + tstack stack(1,std::make_pair(t0,pat)); // t * pat + + while(!stack.empty()){ + const std::pair<TNode,TNode> p = stack.back(); stack.pop_back(); + const TNode & t = p.first; + const TNode & pat = p.second; + + // t or pat is a variable currently we consider that can match anything + if( find(vars.begin(),vars.end(),t) != vars.end() ) continue; + if( pat.getKind() == INST_CONSTANT ) continue; + + // t and pat are nonunifiable + if( !Trigger::isAtomicTrigger( t ) || !Trigger::isAtomicTrigger( pat ) ) { + if(t == pat) continue; + else return true; + }; + if( t.getOperator() != pat.getOperator() ) return true; + + //put the children on the stack + for( size_t i=0; i < pat.getNumChildren(); i++ ){ + stack.push_back(std::make_pair(t[i],pat[i])); + }; + } + // The heuristic can't find non-unifiability + return false; +}; + +/** New things */ +class DumbMatcher: public Matcher{ + void resetInstantiationRound( QuantifiersEngine* qe ){}; + bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe ){ + return false; + } + bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ + return false; + } +}; + +class DumbPatMatcher: public PatMatcher{ + void resetInstantiationRound( QuantifiersEngine* qe ){}; + bool reset( InstMatch& m, QuantifiersEngine* qe ){ + return false; + } + bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ + return false; + } +}; + + +/* The order of the matching is: + reset arg1, nextMatch arg1, reset arg2, nextMatch arg2, ... */ +ApplyMatcher::ApplyMatcher( Node pat, QuantifiersEngine* qe): d_pattern(pat){ + // Assert( pat.hasAttribute(InstConstantAttribute()) ); + + //set-up d_variables, d_constants, d_childrens + for( size_t i=0; i< d_pattern.getNumChildren(); ++i ){ + EqualityQuery* q = qe->getEqualityQuery(d_pattern[i].getType()); + Assert( q != NULL ); + if( d_pattern[i].hasAttribute(InstConstantAttribute()) ){ + if( d_pattern[i].getKind()==INST_CONSTANT ){ + //It's a variable + d_variables.push_back(make_triple((TNode)d_pattern[i],i,q)); + }else{ + //It's neither a constant argument neither a variable + //we create the matcher for the subpattern + d_childrens.push_back(make_triple(mkMatcher((TNode)d_pattern[i], qe),i,q)); + }; + }else{ + // It's a constant + d_constants.push_back(make_triple((TNode)d_pattern[i],i,q)); + } + } +} + +void ApplyMatcher::resetInstantiationRound( QuantifiersEngine* qe ){ + for( size_t i=0; i< d_childrens.size(); i++ ){ + d_childrens[i].first->resetInstantiationRound( qe ); + } +} + +bool ApplyMatcher::reset(TNode t, InstMatch & m, QuantifiersEngine* qe){ + Debug("matching") << "Matching " << t << " against pattern " << d_pattern << " (" + << m.size() << ")" << std::endl; + + //if t is null + Assert( !t.isNull() ); + Assert( !t.hasAttribute(InstConstantAttribute()) ); + Assert( t.getKind()==d_pattern.getKind() ); + Assert( (t.getKind()!=APPLY_UF && t.getKind()!=APPLY_CONSTRUCTOR) + || t.getOperator()==d_pattern.getOperator() ); + + typedef std::vector< triple<TNode,size_t,EqualityQuery*> >::iterator iterator; + for(iterator i = d_constants.begin(), end = d_constants.end(); + i != end; ++i){ + if( !i->third->areEqual( i->first, t[i->second] ) ){ + Debug("matching-fail") << "Match fail arg: " << i->first << " and " << t[i->second] << std::endl; + //setMatchFail( qe, d_pattern[i], t[i] ); + //ground arguments are not equal + return false; + } + } + + d_binded.clear(); + bool set; + for(iterator i = d_variables.begin(), end = d_variables.end(); + i != end; ++i){ + if( !m.setMatch( i->third, i->first, t[i->second], set) ){ + //match is in conflict + Debug("matching-debug") << "Match in conflict " << t[i->second] << " and " + << i->first << " because " + << m.get(i->first) + << std::endl; + Debug("matching-fail") << "Match fail: " << m.get(i->first) << " and " << t[i->second] << std::endl; + //setMatchFail( qe, partial[0].d_map[d_pattern[i]], t[i] ); + m.erase(d_binded.begin(), d_binded.end()); + return false; + }else{ + if(set){ //The variable has just been set + d_binded.push_back(i->first); + } + } + } + + //now, fit children into match + //we will be requesting candidates for matching terms for each child + d_reps.clear(); + for( size_t i=0; i< d_childrens.size(); i++ ){ + Debug("matching-debug") << "Take the representative of " << t[ d_childrens[i].second ] << std::endl; + Assert( d_childrens[i].third->hasTerm(t[ d_childrens[i].second ]) ); + Node rep = d_childrens[i].third->getRepresentative( t[ d_childrens[i].second ] ); + d_reps.push_back( rep ); + } + + if(d_childrens.size() == 0) return true; + else return getNextMatch(m, qe, true); +} + +bool ApplyMatcher::getNextMatch(InstMatch& m, QuantifiersEngine* qe, bool reset){ + Assert(d_childrens.size() > 0); + const size_t max = d_childrens.size() - 1; + size_t index = reset ? 0 : max; + Assert(d_childrens.size() == d_reps.size()); + while(true){ + if(reset ? + d_childrens[index].first->reset( d_reps[index], m, qe ) : + d_childrens[index].first->getNextMatch( m, qe )){ + if(index==max) return true; + ++index; + reset=true; + }else{ + if(index==0){ + m.erase(d_binded.begin(), d_binded.end()); + return false; + } + --index; + reset=false; + }; + } +} + +bool ApplyMatcher::getNextMatch(InstMatch& m, QuantifiersEngine* qe){ + if(d_childrens.size() == 0){ + m.erase(d_binded.begin(), d_binded.end()); + return false; + } else return getNextMatch(m, qe, false); +} + +/** Proxy that call the sub-matcher on the result return by the given candidate generator */ +template <class CG, class M> +class CandidateGeneratorMatcher: public Matcher{ + /** candidate generator */ + CG d_cg; + /** the sub-matcher */ + M d_m; +public: + CandidateGeneratorMatcher(CG cg, M m): d_cg(cg), d_m(m) + {/* last is Null */}; + void resetInstantiationRound( QuantifiersEngine* qe ){ + d_cg.resetInstantiationRound(); + d_m.resetInstantiationRound(qe); + }; + bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe ){ + d_cg.reset(n); + return findMatch(m,qe); + } + bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ + // The sub-matcher has another match + return d_m.getNextMatch(m, qe) || findMatch(m,qe); + } +private: + bool findMatch( InstMatch& m, QuantifiersEngine* qe ){ + // Otherwise try to find a new candidate that has at least one match + while(true){ + TNode n = d_cg.getNextCandidate();//kept somewhere Term-db + Debug("matching") << "GenCand " << n << " (" << this << ")" << std::endl; + if(n.isNull()) return false; + if(d_m.reset(n,m,qe)) return true; + }; + } +}; + +/** Proxy that call the sub-matcher on the result return by the given candidate generator */ +template<class M> +class PatOfMatcher: public PatMatcher{ + M d_m; +public: + inline PatOfMatcher(M m): d_m(m){} + void resetInstantiationRound(QuantifiersEngine* qe){ + d_m.resetInstantiationRound(qe); + } + bool reset(InstMatch& m, QuantifiersEngine* qe){ + return d_m.reset(Node::null(),m,qe); + }; + bool getNextMatch(InstMatch& m, QuantifiersEngine* qe){ + return d_m.getNextMatch(m,qe); + }; +}; + +class ArithMatcher: public Matcher{ +private: + /** for arithmetic matching */ + std::map< Node, Node > d_arith_coeffs; + /** get the match against ground term or formula t. + d_match_mattern and t should have the same shape. + only valid for use where !d_match_pattern.isNull(). + */ + /** the variable that are set by this matcher */ + std::vector< TNode > d_binded; /* TNode because the variables are already in d_arith_coeffs */ + Node d_pattern; //for debugging +public: + ArithMatcher(Node pat, QuantifiersEngine* qe); + void resetInstantiationRound( QuantifiersEngine* qe ){}; + bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe ); + bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ); +}; + +/** Match just a variable */ +class VarMatcher: public Matcher{ + Node d_var; + bool d_binded; /* True if the reset bind the variable to some value */ + EqualityQuery* d_q; +public: + VarMatcher(Node var, QuantifiersEngine* qe): d_var(var), d_binded(false){ + d_q = qe->getEqualityQuery(var.getType()); + } + void resetInstantiationRound( QuantifiersEngine* qe ){}; + bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe ){ + if(!m.setMatch( d_q, d_var, n, d_binded )){ + //match is in conflict + Debug("matching-fail") << "Match fail: " << m.get(d_var) + << " and " << n << std::endl; + return false; + } else return true; + }; + bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ + //match is in conflict + if (d_binded) m.erase(d_var); + return false; + } +}; + +template <class M, class Test > +class TestMatcher: public Matcher{ + M d_m; + Test d_test; +public: + inline TestMatcher(M m, Test test): d_m(m), d_test(test){} + inline void resetInstantiationRound(QuantifiersEngine* qe){ + d_m.resetInstantiationRound(qe); + } + inline bool reset(TNode n, InstMatch& m, QuantifiersEngine* qe){ + return d_test(n) && d_m.reset(n, m, qe); + } + inline bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ + return d_m.getNextMatch(m, qe); + } +}; + +class LegalOpTest/*: public unary_function<TNode,bool>*/ { + Node d_op; +public: + inline LegalOpTest(Node op): d_op(op){} + inline bool operator() (TNode n) { + return + CandidateGenerator::isLegalCandidate(n) && + // ( // n.getKind()==SELECT || n.getKind()==STORE || + // n.getKind()==APPLY_UF || n.getKind()==APPLY_CONSTRUCTOR) && + n.hasOperator() && + n.getOperator()==d_op; + }; +}; + +class LegalKindTest/* : public unary_function<TNode,bool>*/ { + Kind d_kind; +public: + inline LegalKindTest(Kind kind): d_kind(kind){} + inline bool operator() (TNode n) { + return + CandidateGenerator::isLegalCandidate(n) && + n.getKind()==d_kind; + }; +}; + +class LegalTypeTest/* : public unary_function<TNode,bool>*/ { + TypeNode d_type; +public: + inline LegalTypeTest(TypeNode type): d_type(type){} + inline bool operator() (TNode n) { + return + CandidateGenerator::isLegalCandidate(n) && + n.getType()==d_type; + }; +}; + +class LegalTest/* : public unary_function<TNode,bool>*/ { +public: + inline bool operator() (TNode n) { + return CandidateGenerator::isLegalCandidate(n); + }; +}; + +size_t numFreeVar(TNode t){ + size_t n = 0; + for( size_t i=0, size =t.getNumChildren(); i < size; ++i ){ + if( t[i].hasAttribute(InstConstantAttribute()) ){ + if( t[i].getKind()==INST_CONSTANT ){ + //variable + ++n; + }else{ + //neither variable nor constant + n += numFreeVar(t[i]); + } + } + } + return n; +} + +class OpMatcher: public Matcher{ + /* The matcher */ + typedef ApplyMatcher AuxMatcher3; + typedef TestMatcher< AuxMatcher3, LegalOpTest > AuxMatcher2; + typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryEeClass, AuxMatcher2> AuxMatcher1; + AuxMatcher1 d_cgm; + static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){ + Assert( pat.getKind() == kind::APPLY_UF ); + /** In reverse order of matcher sequence */ + AuxMatcher3 am3(pat,qe); + /** Keep only the one that have the good operator */ + AuxMatcher2 am2(am3,LegalOpTest(pat.getOperator())); + /** Iter on the equivalence class of the given term */ + uf::TheoryUF* uf = static_cast<uf::TheoryUF *>(qe->getTheoryEngine()->getTheory( theory::THEORY_UF )); + eq::EqualityEngine* ee = + static_cast<eq::EqualityEngine*>(uf->getEqualityEngine()); + CandidateGeneratorTheoryEeClass cdtUfEq(ee); + /* Create a matcher from the candidate generator */ + AuxMatcher1 am1(cdtUfEq,am2); + return am1; + } + size_t d_num_var; + Node d_pat; +public: + OpMatcher( Node pat, QuantifiersEngine* qe ): + d_cgm(createCgm(pat, qe)),d_num_var(numFreeVar(pat)), + d_pat(pat) {} + + void resetInstantiationRound( QuantifiersEngine* qe ){ + d_cgm.resetInstantiationRound(qe); + }; + bool reset( TNode t, InstMatch& m, QuantifiersEngine* qe ){ + // size_t m_size = m.d_map.size(); + // if(m_size == d_num_var){ + // uf::EqualityEngine<uf::TheoryUF::NotifyClass>* ee = (static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->getTheory( theory::THEORY_UF )))->getEqualityEngine(); + // std::cout << "!"; + // return ee->areEqual(m.subst(d_pat),t); + // }else{ + // std::cout << m.d_map.size() << std::endl; + return d_cgm.reset(t, m, qe); + // } + } + bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ + return d_cgm.getNextMatch(m, qe); + } +}; + +class DatatypesMatcher: public Matcher{ + /* The matcher */ + typedef ApplyMatcher AuxMatcher3; + typedef TestMatcher< AuxMatcher3, LegalOpTest > AuxMatcher2; + typedef CandidateGeneratorMatcher< datatypes::rrinst::CandidateGeneratorTheoryClass, AuxMatcher2> AuxMatcher1; + AuxMatcher1 d_cgm; + static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){ + Assert( pat.getKind() == kind::APPLY_CONSTRUCTOR, + "For datatypes only constructor are accepted in pattern" ); + /** In reverse order of matcher sequence */ + AuxMatcher3 am3(pat,qe); + /** Keep only the one that have the good operator */ + AuxMatcher2 am2(am3,LegalOpTest(pat.getOperator())); + /** Iter on the equivalence class of the given term */ + datatypes::TheoryDatatypes* dt = static_cast<datatypes::TheoryDatatypes *>(qe->getTheoryEngine()->getTheory( theory::THEORY_DATATYPES )); + datatypes::rrinst::CandidateGeneratorTheoryClass cdtDtEq(dt); + /* Create a matcher from the candidate generator */ + AuxMatcher1 am1(cdtDtEq,am2); + return am1; + } + Node d_pat; +public: + DatatypesMatcher( Node pat, QuantifiersEngine* qe ): + d_cgm(createCgm(pat, qe)), + d_pat(pat) {} + + void resetInstantiationRound( QuantifiersEngine* qe ){ + d_cgm.resetInstantiationRound(qe); + }; + bool reset( TNode t, InstMatch& m, QuantifiersEngine* qe ){ + Debug("matching") << "datatypes: " << t << " matches " << d_pat << std::endl; + return d_cgm.reset(t, m, qe); + } + bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ + return d_cgm.getNextMatch(m, qe); + } +}; + +class ArrayMatcher: public Matcher{ + /* The matcher */ + typedef ApplyMatcher AuxMatcher3; + typedef TestMatcher< AuxMatcher3, LegalKindTest > AuxMatcher2; + typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryEeClass, AuxMatcher2> AuxMatcher1; + AuxMatcher1 d_cgm; + static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){ + Assert( pat.getKind() == kind::SELECT || pat.getKind() == kind::STORE ); + /** In reverse order of matcher sequence */ + AuxMatcher3 am3(pat,qe); + /** Keep only the one that have the good operator */ + AuxMatcher2 am2(am3, LegalKindTest(pat.getKind())); + /** Iter on the equivalence class of the given term */ + arrays::TheoryArrays* ar = static_cast<arrays::TheoryArrays *>(qe->getTheoryEngine()->getTheory( theory::THEORY_ARRAY )); + eq::EqualityEngine* ee = + static_cast<eq::EqualityEngine*>(ar->getEqualityEngine()); + CandidateGeneratorTheoryEeClass cdtUfEq(ee); + /* Create a matcher from the candidate generator */ + AuxMatcher1 am1(cdtUfEq,am2); + return am1; + } + size_t d_num_var; + Node d_pat; +public: + ArrayMatcher( Node pat, QuantifiersEngine* qe ): + d_cgm(createCgm(pat, qe)),d_num_var(numFreeVar(pat)), + d_pat(pat) {} + + void resetInstantiationRound( QuantifiersEngine* qe ){ + d_cgm.resetInstantiationRound(qe); + }; + bool reset( TNode t, InstMatch& m, QuantifiersEngine* qe ){ + // size_t m_size = m.d_map.size(); + // if(m_size == d_num_var){ + // uf::EqualityEngine<uf::TheoryUF::NotifyClass>* ee = (static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->getTheory( theory::THEORY_UF )))->getEqualityEngine(); + // std::cout << "!"; + // return ee->areEqual(m.subst(d_pat),t); + // }else{ + // std::cout << m.d_map.size() << std::endl; + return d_cgm.reset(t, m, qe); + // } + } + bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ + return d_cgm.getNextMatch(m, qe); + } +}; + +class AllOpMatcher: public PatMatcher{ + /* The matcher */ + typedef ApplyMatcher AuxMatcher3; + typedef TestMatcher< AuxMatcher3, LegalTest > AuxMatcher2; + typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryUfOp, AuxMatcher2> AuxMatcher1; + AuxMatcher1 d_cgm; + static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){ + Assert( pat.hasOperator() ); + /** In reverse order of matcher sequence */ + AuxMatcher3 am3(pat,qe); + /** Keep only the one that have the good operator */ + AuxMatcher2 am2(am3,LegalTest()); + /** Iter on the equivalence class of the given term */ + TermDb* tdb = qe->getTermDatabase(); + CandidateGeneratorTheoryUfOp cdtUfEq(pat.getOperator(),tdb); + /* Create a matcher from the candidate generator */ + AuxMatcher1 am1(cdtUfEq,am2); + return am1; + } + size_t d_num_var; + Node d_pat; +public: + AllOpMatcher( TNode pat, QuantifiersEngine* qe ): + d_cgm(createCgm(pat, qe)), d_num_var(numFreeVar(pat)), + d_pat(pat) {} + + void resetInstantiationRound( QuantifiersEngine* qe ){ + d_cgm.resetInstantiationRound(qe); + }; + bool reset( InstMatch& m, QuantifiersEngine* qe ){ + // std::cout << m.d_map.size() << "/" << d_num_var << std::endl; + return d_cgm.reset(Node::null(), m, qe); + } + bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ + return d_cgm.getNextMatch(m, qe); + } +}; + +template <bool classes> /** true classes | false class */ +class GenericCandidateGeneratorClasses: public CandidateGenerator{ +private: + CandidateGenerator* d_cg; + QuantifiersEngine* d_qe; + +public: + void mkCandidateGenerator(){ + if(classes) + d_cg = d_qe->getRRCanGenClasses(); + else + d_cg = d_qe->getRRCanGenClass(); + } + + GenericCandidateGeneratorClasses(QuantifiersEngine* qe): + d_qe(qe) { + mkCandidateGenerator(); + } + ~GenericCandidateGeneratorClasses(){ + delete(d_cg); + } + const GenericCandidateGeneratorClasses & operator =(const GenericCandidateGeneratorClasses & m){ + mkCandidateGenerator(); + return m; + }; + GenericCandidateGeneratorClasses(const GenericCandidateGeneratorClasses & m): + d_qe(m.d_qe){ + mkCandidateGenerator(); + } + void resetInstantiationRound(){ + d_cg->resetInstantiationRound(); + }; + void reset( TNode eqc ){ + Assert( !classes || eqc.isNull() ); + d_cg->reset(eqc); + }; //* the argument is not used + TNode getNextCandidate(){ + return d_cg->getNextCandidate(); + }; +}; /* MetaCandidateGeneratorClasses */ + + +class GenericMatcher: public Matcher{ + /* The matcher */ + typedef ApplyMatcher AuxMatcher3; + typedef TestMatcher< AuxMatcher3, LegalOpTest > AuxMatcher2; + typedef CandidateGeneratorMatcher< GenericCandidateGeneratorClasses<false>, AuxMatcher2> AuxMatcher1; + AuxMatcher1 d_cgm; + static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){ + /** In reverse order of matcher sequence */ + AuxMatcher3 am3(pat,qe); + /** Keep only the one that have the good operator */ + AuxMatcher2 am2(am3,LegalOpTest(pat.getOperator())); + /** Iter on the equivalence class of the given term */ + GenericCandidateGeneratorClasses<false> cdtG(qe); + /* Create a matcher from the candidate generator */ + AuxMatcher1 am1(cdtG,am2); + return am1; + } + Node d_pat; +public: + GenericMatcher( Node pat, QuantifiersEngine* qe ): + d_cgm(createCgm(pat, qe)), + d_pat(pat) {} + + void resetInstantiationRound( QuantifiersEngine* qe ){ + d_cgm.resetInstantiationRound(qe); + }; + bool reset( TNode t, InstMatch& m, QuantifiersEngine* qe ){ + return d_cgm.reset(t, m, qe); + } + bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ + return d_cgm.getNextMatch(m, qe); + } +}; + + +class GenericPatMatcher: public PatMatcher{ + /* The matcher */ + typedef ApplyMatcher AuxMatcher3; + typedef TestMatcher< AuxMatcher3, LegalOpTest > AuxMatcher2; + typedef CandidateGeneratorMatcher< GenericCandidateGeneratorClasses<true>, AuxMatcher2> AuxMatcher1; + AuxMatcher1 d_cgm; + static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){ + /** In reverse order of matcher sequence */ + AuxMatcher3 am3(pat,qe); + /** Keep only the one that have the good operator */ + AuxMatcher2 am2(am3,LegalOpTest(pat.getOperator())); + /** Iter on the equivalence class of the given term */ + GenericCandidateGeneratorClasses<true> cdtG(qe); + /* Create a matcher from the candidate generator */ + AuxMatcher1 am1(cdtG,am2); + return am1; + } + Node d_pat; +public: + GenericPatMatcher( Node pat, QuantifiersEngine* qe ): + d_cgm(createCgm(pat, qe)), + d_pat(pat) {} + + void resetInstantiationRound( QuantifiersEngine* qe ){ + d_cgm.resetInstantiationRound(qe); + }; + bool reset( InstMatch& m, QuantifiersEngine* qe ){ + return d_cgm.reset(Node::null(), m, qe); + } + bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ + return d_cgm.getNextMatch(m, qe); + } +}; + +class MetaCandidateGeneratorClasses: public CandidateGenerator{ +private: + CandidateGenerator* d_cg; + TypeNode d_ty; + TheoryEngine* d_te; + +public: + CandidateGenerator* mkCandidateGenerator(TypeNode ty, TheoryEngine* te){ + Debug("inst-match-gen") << "MetaCandidateGenerator for type: " << ty + << " Theory : " << Theory::theoryOf(ty) << std::endl; + if( Theory::theoryOf(ty) == theory::THEORY_DATATYPES ){ + // datatypes::TheoryDatatypes* dt = static_cast<datatypes::TheoryDatatypes *>(te->getTheory( theory::THEORY_DATATYPES )); + // return new datatypes::rrinst::CandidateGeneratorTheoryClasses(dt); + Unimplemented("MetaCandidateGeneratorClasses for THEORY_DATATYPES"); + }else if ( Theory::theoryOf(ty) == theory::THEORY_ARRAY ){ + arrays::TheoryArrays* ar = static_cast<arrays::TheoryArrays *>(te->getTheory( theory::THEORY_ARRAY )); + eq::EqualityEngine* ee = + static_cast<eq::EqualityEngine*>(ar->getEqualityEngine()); + return new CandidateGeneratorTheoryEeClasses(ee); + } else { + uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(te->getTheory( theory::THEORY_UF )); + eq::EqualityEngine* ee = + static_cast<eq::EqualityEngine*>(uf->getEqualityEngine()); + return new CandidateGeneratorTheoryEeClasses(ee); + } + } + MetaCandidateGeneratorClasses(TypeNode ty, TheoryEngine* te): + d_ty(ty), d_te(te) { + d_cg = mkCandidateGenerator(ty,te); + } + ~MetaCandidateGeneratorClasses(){ + delete(d_cg); + } + const MetaCandidateGeneratorClasses & operator =(const MetaCandidateGeneratorClasses & m){ + d_cg = mkCandidateGenerator(m.d_ty, m.d_te); + return m; + }; + MetaCandidateGeneratorClasses(const MetaCandidateGeneratorClasses & m): + d_ty(m.d_ty), d_te(m.d_te){ + d_cg = mkCandidateGenerator(m.d_ty, m.d_te); + } + void resetInstantiationRound(){ + d_cg->resetInstantiationRound(); + }; + void reset( TNode eqc ){ + d_cg->reset(eqc); + }; //* the argument is not used + TNode getNextCandidate(){ + return d_cg->getNextCandidate(); + }; +}; /* MetaCandidateGeneratorClasses */ + +/** Match just a variable */ +class AllVarMatcher: public PatMatcher{ +private: + /* generator */ + typedef VarMatcher AuxMatcher3; + typedef TestMatcher< AuxMatcher3, LegalTypeTest > AuxMatcher2; + typedef CandidateGeneratorMatcher< MetaCandidateGeneratorClasses, AuxMatcher2 > AuxMatcher1; + AuxMatcher1 d_cgm; + static inline AuxMatcher1 createCgm(TNode pat, QuantifiersEngine* qe){ + Assert( pat.getKind()==INST_CONSTANT ); + TypeNode ty = pat.getType(); + Debug("inst-match-gen") << "create AllVarMatcher for type: " << ty << std::endl; + /** In reverse order of matcher sequence */ + /** Distribute it to all the pattern */ + AuxMatcher3 am3(pat,qe); + /** Keep only the one that have the good type */ + AuxMatcher2 am2(am3,LegalTypeTest(ty)); + /** Generate one term by eq classes */ + MetaCandidateGeneratorClasses mcdt(ty,qe->getTheoryEngine()); + /* Create a matcher from the candidate generator */ + AuxMatcher1 am1(mcdt,am2); + return am1; + } +public: + AllVarMatcher( TNode pat, QuantifiersEngine* qe ): + d_cgm(createCgm(pat, qe)){} + + void resetInstantiationRound( QuantifiersEngine* qe ){ + d_cgm.resetInstantiationRound(qe); + }; + bool reset( InstMatch& m, QuantifiersEngine* qe ){ + return d_cgm.reset(Node::null(), m, qe); //cdtUfEq doesn't use it's argument for reset + } + bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ + return d_cgm.getNextMatch(m, qe); + } +}; + +/** Match all the pattern with the same term */ +class SplitMatcher: public Matcher{ +private: + const size_t size; + ApplyMatcher d_m; /** Use ApplyMatcher by creating a fake application */ +public: + SplitMatcher(std::vector< Node > pats, QuantifiersEngine* qe): + size(pats.size()), + d_m(NodeManager::currentNM()->mkNode(kind::INST_PATTERN,pats), qe) {} + void resetInstantiationRound( QuantifiersEngine* qe ){ + d_m.resetInstantiationRound(qe); + }; + bool reset( TNode ex, InstMatch& m, QuantifiersEngine* qe ){ + NodeBuilder<> n(kind::INST_PATTERN); + for(size_t i = 0; i < size; ++i) n << ex; + Node nn = n; + return d_m.reset(nn,m,qe); + }; + bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ + return getNextMatch(m, qe); + } +}; + + +/** Match uf term in a fixed equivalence class */ +class UfCstEqMatcher: public PatMatcher{ +private: + /* equivalence class to match */ + Node d_cst; + /* generator */ + OpMatcher d_cgm; +public: + UfCstEqMatcher( Node pat, Node cst, QuantifiersEngine* qe ): + d_cst(cst), + d_cgm(OpMatcher(pat,qe)) {}; + void resetInstantiationRound( QuantifiersEngine* qe ){ + d_cgm.resetInstantiationRound(qe); + }; + bool reset( InstMatch& m, QuantifiersEngine* qe ){ + return d_cgm.reset(d_cst, m, qe); + } + bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ + return d_cgm.getNextMatch(m, qe); + } +}; + +/** Match equalities */ +class UfEqMatcher: public PatMatcher{ +private: + /* generator */ + typedef SplitMatcher AuxMatcher3; + typedef TestMatcher< AuxMatcher3, LegalTypeTest > AuxMatcher2; + typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryEeClasses, AuxMatcher2 > AuxMatcher1; + AuxMatcher1 d_cgm; + static inline AuxMatcher1 createCgm(std::vector<Node> & pat, QuantifiersEngine* qe){ + Assert( pat.size() > 0); + TypeNode ty = pat[0].getType(); + for(size_t i = 1; i < pat.size(); ++i){ + Assert(pat[i].getType() == ty); + } + /** In reverse order of matcher sequence */ + /** Distribute it to all the pattern */ + AuxMatcher3 am3(pat,qe); + /** Keep only the one that have the good type */ + AuxMatcher2 am2(am3,LegalTypeTest(ty)); + /** Generate one term by eq classes */ + uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->getTheory( theory::THEORY_UF )); + eq::EqualityEngine* ee = + static_cast<eq::EqualityEngine*>(uf->getEqualityEngine()); + CandidateGeneratorTheoryEeClasses cdtUfEq(ee); + /* Create a matcher from the candidate generator */ + AuxMatcher1 am1(cdtUfEq,am2); + return am1; + } +public: + UfEqMatcher( std::vector<Node> & pat, QuantifiersEngine* qe ): + d_cgm(createCgm(pat, qe)){} + + void resetInstantiationRound( QuantifiersEngine* qe ){ + d_cgm.resetInstantiationRound(qe); + }; + bool reset( InstMatch& m, QuantifiersEngine* qe ){ + return d_cgm.reset(Node::null(), m, qe); //cdtUfEq doesn't use it's argument for reset + } + bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ + return d_cgm.getNextMatch(m, qe); + } +}; + + +/** Match dis-equalities */ +class UfDeqMatcher: public PatMatcher{ +private: + /* generator */ + typedef ApplyMatcher AuxMatcher3; + + class EqTest/* : public unary_function<Node,bool>*/ { + TypeNode d_type; + public: + inline EqTest(TypeNode type): d_type(type){}; + inline bool operator() (Node n) { + return + CandidateGenerator::isLegalCandidate(n) && + n.getKind() == kind::EQUAL && + n[0].getType()==d_type; + }; + }; + typedef TestMatcher< AuxMatcher3, EqTest > AuxMatcher2; + typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryEeClass, AuxMatcher2 > AuxMatcher1; + AuxMatcher1 d_cgm; + Node false_term; + static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){ + Assert( pat.getKind() == kind::NOT); + TNode eq = pat[0]; + Assert( eq.getKind() == kind::EQUAL); + TypeNode ty = eq[0].getType(); + /** In reverse order of matcher sequence */ + /** Distribute it to all the pattern */ + AuxMatcher3 am3(eq,qe); + /** Keep only the one that have the good type */ + AuxMatcher2 am2(am3,EqTest(ty)); + /** Will generate all the terms of the eq class of false */ + uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->getTheory( theory::THEORY_UF )); + eq::EqualityEngine* ee = + static_cast<eq::EqualityEngine*>(uf->getEqualityEngine()); + CandidateGeneratorTheoryEeClass cdtUfEq(ee); + /* Create a matcher from the candidate generator */ + AuxMatcher1 am1(cdtUfEq,am2); + return am1; + } +public: + UfDeqMatcher( Node pat, QuantifiersEngine* qe ): + d_cgm(createCgm(pat, qe)), + false_term((static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->getTheory( theory::THEORY_UF )))->getEqualityEngine()-> + getRepresentative(NodeManager::currentNM()->mkConst<bool>(false) )){}; + void resetInstantiationRound( QuantifiersEngine* qe ){ + d_cgm.resetInstantiationRound(qe); + }; + bool reset( InstMatch& m, QuantifiersEngine* qe ){ + return d_cgm.reset(false_term, m, qe); + } + bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ + return d_cgm.getNextMatch(m, qe); + } +}; + +Matcher* mkMatcher( Node pat, QuantifiersEngine* qe ){ + Debug("inst-match-gen") << "mkMatcher: Pattern term is " << pat << std::endl; + + // if( pat.getKind() == kind::APPLY_UF){ + // return new OpMatcher(pat, qe); + // } else if( pat.getKind() == kind::APPLY_CONSTRUCTOR ){ + // return new DatatypesMatcher(pat, qe); + // } else if( pat.getKind() == kind::SELECT || pat.getKind() == kind::STORE ){ + // return new ArrayMatcher(pat, qe); + if( pat.getKind() == kind::APPLY_UF || + pat.getKind() == kind::APPLY_CONSTRUCTOR || + pat.getKind() == kind::SELECT || pat.getKind() == kind::STORE ){ + return new GenericMatcher(pat, qe); + } else { /* Arithmetic? */ + /** TODO: something simpler to see if the pattern is a good + arithmetic pattern */ + std::map< Node, Node > d_arith_coeffs; + if( !Trigger::getPatternArithmetic( pat.getAttribute(InstConstantAttribute()), pat, d_arith_coeffs ) ){ + std::cout << "(?) Unknown matching pattern is " << pat << std::endl; + Unimplemented("pattern not implemented"); + return new DumbMatcher(); + }else{ + Debug("matching-arith") << "Generated arithmetic pattern for " << pat << ": " << std::endl; + for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){ + Debug("matching-arith") << " " << it->first << " -> " << it->second << std::endl; + } + ArithMatcher am3 (pat, qe); + TestMatcher<ArithMatcher, LegalTypeTest> + am2(am3,LegalTypeTest(pat.getType())); + /* generator */ + uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(qe->getTheoryEngine()->getTheory( theory::THEORY_UF )); + eq::EqualityEngine* ee = + static_cast<eq::EqualityEngine*> (uf->getEqualityEngine()); + CandidateGeneratorTheoryEeClass cdtUfEq(ee); + return new CandidateGeneratorMatcher< CandidateGeneratorTheoryEeClass, + TestMatcher<ArithMatcher, LegalTypeTest> > (cdtUfEq,am2); + } + } +}; + +PatMatcher* mkPattern( Node pat, QuantifiersEngine* qe ){ + Debug("inst-match-gen") << "Pattern term is " << pat << std::endl; + Assert( pat.hasAttribute(InstConstantAttribute()) ); + + if( pat.getKind()==kind::NOT && pat[0].getKind() == kind::EQUAL){ + /* Difference */ + return new UfDeqMatcher(pat, qe); + } else if (pat.getKind() == kind::EQUAL){ + if( !pat[0].hasAttribute(InstConstantAttribute() )){ + Assert(pat[1].hasAttribute(InstConstantAttribute())); + return new UfCstEqMatcher(pat[1], pat[0], qe); + }else if( !pat[1].hasAttribute(InstConstantAttribute() )){ + Assert(pat[0].hasAttribute(InstConstantAttribute())); + return new UfCstEqMatcher(pat[0], pat[1], qe); + }else{ + std::vector< Node > pats(pat.begin(),pat.end()); + return new UfEqMatcher(pats,qe); + } + } else if( Trigger::isAtomicTrigger( pat ) ){ + return new AllOpMatcher(pat, qe); + // return new GenericPatMatcher(pat, qe); + } else if( pat.getKind()==INST_CONSTANT ){ + // just a variable + return new AllVarMatcher(pat, qe); + } else { /* Arithmetic? */ + /** TODO: something simpler to see if the pattern is a good + arithmetic pattern */ + std::map< Node, Node > d_arith_coeffs; + if( !Trigger::getPatternArithmetic( pat.getAttribute(InstConstantAttribute()), pat, d_arith_coeffs ) ){ + Debug("inst-match-gen") << "(?) Unknown matching pattern is " << pat << std::endl; + std::cout << "(?) Unknown matching pattern is " << pat << std::endl; + return new DumbPatMatcher(); + }else{ + Debug("matching-arith") << "Generated arithmetic pattern for " << pat << ": " << std::endl; + for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){ + Debug("matching-arith") << " " << it->first << " -> " << it->second << std::endl; + } + ArithMatcher am3 (pat, qe); + TestMatcher<ArithMatcher, LegalTest> + am2(am3,LegalTest()); + /* generator */ + TermDb* tdb = qe->getTermDatabase(); + CandidateGeneratorTheoryUfType cdtUfEq(pat.getType(),tdb); + typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryUfType, + TestMatcher<ArithMatcher, LegalTest> > AuxMatcher1; + return new PatOfMatcher<AuxMatcher1>(AuxMatcher1(cdtUfEq,am2)); + } + } +}; + +ArithMatcher::ArithMatcher(Node pat, QuantifiersEngine* qe): d_pattern(pat){ + + if(Trigger::getPatternArithmetic(pat.getAttribute(InstConstantAttribute()), pat, d_arith_coeffs ) ) + { + Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_pattern << std::endl; + Assert(false); + }else{ + Debug("matching-arith") << "Generated arithmetic pattern for " << d_pattern << ": " << std::endl; + for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){ + Debug("matching-arith") << " " << it->first << " -> " << it->second << std::endl; + } + } + +}; + +bool ArithMatcher::reset( TNode t, InstMatch& m, QuantifiersEngine* qe ){ + Debug("matching-arith") << "Matching " << t << " " << d_pattern << std::endl; + d_binded.clear(); + if( !d_arith_coeffs.empty() ){ + NodeBuilder<> tb(kind::PLUS); + Node ic = Node::null(); + for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){ + Debug("matching-arith") << it->first << " -> " << it->second << std::endl; + if( !it->first.isNull() ){ + if( m.find( it->first )==m.end() ){ + //see if we can choose this to set + if( ic.isNull() && ( it->second.isNull() || !it->first.getType().isInteger() ) ){ + ic = it->first; + } + }else{ + Debug("matching-arith") << "already set " << m.get( it->first ) << std::endl; + Node tm = m.get( it->first ); + if( !it->second.isNull() ){ + tm = NodeManager::currentNM()->mkNode( MULT, it->second, tm ); + } + tb << tm; + } + }else{ + tb << it->second; + } + } + if( !ic.isNull() ){ + Node tm; + if( tb.getNumChildren()==0 ){ + tm = t; + }else{ + tm = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb; + tm = NodeManager::currentNM()->mkNode( MINUS, t, tm ); + } + if( !d_arith_coeffs[ ic ].isNull() ){ + Assert( !ic.getType().isInteger() ); + Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_arith_coeffs[ ic ].getConst<Rational>() ); + tm = NodeManager::currentNM()->mkNode( MULT, coeff, tm ); + } + m.set( ic, Rewriter::rewrite( tm )); + d_binded.push_back(ic); + //set the rest to zeros + for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){ + if( !it->first.isNull() ){ + if( m.find( it->first )==m.end() ){ + m.set( it->first, NodeManager::currentNM()->mkConst( Rational(0) )); + d_binded.push_back(ic); + } + } + } + Debug("matching-arith") << "Setting " << ic << " to " << tm << std::endl; + return true; + }else{ + m.erase(d_binded.begin(), d_binded.end()); + return false; + } + }else{ + m.erase(d_binded.begin(), d_binded.end()); + return false; + } +}; + +bool ArithMatcher::getNextMatch( InstMatch& m, QuantifiersEngine* qe ){ + m.erase(d_binded.begin(), d_binded.end()); + return false; +}; + + +class MultiPatsMatcher: public PatsMatcher{ +private: + bool d_reset_done; + std::vector< PatMatcher* > d_patterns; + InstMatch d_im; + bool reset( QuantifiersEngine* qe ){ + d_im.clear(); + d_reset_done = true; + + return getNextMatch(qe,true); + }; + + bool getNextMatch(QuantifiersEngine* qe, bool reset){ + const size_t max = d_patterns.size() - 1; + size_t index = reset ? 0 : max; + while(true){ + Debug("matching") << "MultiPatsMatcher::index " << index << "/" + << max << (reset ? " reset_phase" : "") << std::endl; + if(reset ? + d_patterns[index]->reset( d_im, qe ) : + d_patterns[index]->getNextMatch( d_im, qe )){ + if(index==max) return true; + ++index; + reset=true; + }else{ + if(index==0) return false; + --index; + reset=false; + }; + } + } + +public: + MultiPatsMatcher(std::vector< Node > & pats, QuantifiersEngine* qe): + d_reset_done(false){ + Assert(pats.size() > 0); + for( size_t i=0; i< pats.size(); i++ ){ + d_patterns.push_back(mkPattern(pats[i],qe)); + }; + }; + void resetInstantiationRound( QuantifiersEngine* qe ){ + for( size_t i=0; i< d_patterns.size(); i++ ){ + d_patterns[i]->resetInstantiationRound( qe ); + }; + d_reset_done = false; + d_im.clear(); + }; + bool getNextMatch( QuantifiersEngine* qe ){ + Assert(d_patterns.size()>0); + if(d_reset_done) return getNextMatch(qe,false); + else return reset(qe); + } + const InstMatch& getInstMatch(){return d_im;}; + + int addInstantiations( InstMatch& baseMatch, Node quant, QuantifiersEngine* qe); +}; + +enum EffiStep{ + ES_STOP, + ES_GET_MONO_CANDIDATE, + ES_GET_MULTI_CANDIDATE, + ES_RESET1, + ES_RESET2, + ES_NEXT1, + ES_NEXT2, + ES_RESET_OTHER, + ES_NEXT_OTHER, +}; +static inline std::ostream& operator<<(std::ostream& out, const EffiStep& step) { + switch(step){ + case ES_STOP: out << "STOP"; break; + case ES_GET_MONO_CANDIDATE: out << "GET_MONO_CANDIDATE"; break; + case ES_GET_MULTI_CANDIDATE: out << "GET_MULTI_CANDIDATE"; break; + case ES_RESET1: out << "RESET1"; break; + case ES_RESET2: out << "RESET2"; break; + case ES_NEXT1: out << "NEXT1"; break; + case ES_NEXT2: out << "NEXT2"; break; + case ES_RESET_OTHER: out << "RESET_OTHER"; break; + case ES_NEXT_OTHER: out << "NEXT_OTHER"; break; + } + return out; +} + + +int MultiPatsMatcher::addInstantiations( InstMatch& baseMatch, Node quant, QuantifiersEngine* qe){ + //now, try to add instantiation for each match produced + int addedLemmas = 0; + resetInstantiationRound( qe ); + d_im.add( baseMatch ); + while( getNextMatch( qe ) ){ + InstMatch im_copy = getInstMatch(); + //m.makeInternal( d_quantEngine->getEqualityQuery() ); + if( qe->addInstantiation( quant, im_copy ) ){ + addedLemmas++; + } + } + //return number of lemmas added + return addedLemmas; +} + +PatsMatcher* mkPatterns( std::vector< Node > pat, QuantifiersEngine* qe ){ + return new MultiPatsMatcher( pat, qe); +} + +class MultiEfficientPatsMatcher: public PatsMatcher{ +private: + bool d_phase_mono; + bool d_phase_new_term; + std::vector< PatMatcher* > d_patterns; + std::vector< Matcher* > d_direct_patterns; + InstMatch d_im; + uf::EfficientHandler d_eh; + uf::EfficientHandler::MultiCandidate d_mc; + InstMatchTrie2Pairs<true> d_cache; + std::vector<Node> d_pats; + // bool indexDone( size_t i){ + // return i == d_c.first.second || + // ( i == d_c.second.second && d_c.second.first.empty()); + // } + + + + static const EffiStep ES_START = ES_GET_MONO_CANDIDATE; + EffiStep d_step; + + //return true if it becomes bigger than d_patterns.size() - 1 + bool incrIndex(size_t & index){ + if(index == d_patterns.size() - 1) return true; + ++index; + if(index == d_mc.first.second + || (!d_phase_mono && index == d_mc.second.second)) + return incrIndex(index); + else return false; + } + + //return true if it becomes smaller than 0 + bool decrIndex(size_t & index){ + if(index == 0) return true; + --index; + if(index == d_mc.first.second + || (!d_phase_mono && index == d_mc.second.second)) + return decrIndex(index); + else return false; + } + + bool resetOther( QuantifiersEngine* qe ){ + return getNextMatchOther(qe,true); + }; + + + bool getNextMatchOther(QuantifiersEngine* qe, bool reset){ + size_t index = reset ? 0 : d_patterns.size(); + if(!reset && decrIndex(index)) return false; + if( reset && + (index == d_mc.first.second + || (!d_phase_mono && index == d_mc.second.second)) + && incrIndex(index)) return true; + while(true){ + Debug("matching") << "MultiEfficientPatsMatcher::index " << index << "/" + << d_patterns.size() - 1 << std::endl; + if(reset ? + d_patterns[index]->reset( d_im, qe ) : + d_patterns[index]->getNextMatch( d_im, qe )){ + if(incrIndex(index)) return true; + reset=true; + }else{ + if(decrIndex(index)) return false; + reset=false; + }; + } + } + + inline EffiStep TestMonoCache(QuantifiersEngine* qe){ + if( //!d_phase_new_term || + d_pats.size() == 1) return ES_RESET_OTHER; + if(d_cache.addInstMatch(d_mc.first.second,d_im)){ + Debug("inst-match::cache") << "Cache miss" << d_im << std::endl; + ++qe->d_statistics.d_mono_candidates_cache_miss; + return ES_RESET_OTHER; + } else { + Debug("inst-match::cache") << "Cache hit" << d_im << std::endl; + ++qe->d_statistics.d_mono_candidates_cache_hit; + return ES_NEXT1; + } + // ++qe->d_statistics.d_mono_candidates_cache_miss; + // return ES_RESET_OTHER; + } + + inline EffiStep TestMultiCache(QuantifiersEngine* qe){ + if(d_cache.addInstMatch(d_mc.first.second,d_mc.second.second,d_im)){ + ++qe->d_statistics.d_multi_candidates_cache_miss; + return ES_RESET_OTHER; + } else { + ++qe->d_statistics.d_multi_candidates_cache_hit; + return ES_NEXT2; + } + } + + +public: + + bool getNextMatch( QuantifiersEngine* qe ){ + Assert( d_step == ES_START || d_step == ES_NEXT_OTHER || d_step == ES_STOP ); + while(true){ + Debug("matching") << "d_step=" << d_step << " " + << "d_im=" << d_im << std::endl; + switch(d_step){ + case ES_GET_MONO_CANDIDATE: + Assert(d_im.empty()); + if(d_phase_new_term ? d_eh.getNextMonoCandidate(d_mc.first) : d_eh.getNextMonoCandidateNewTerm(d_mc.first)){ + if(d_phase_new_term) ++qe->d_statistics.d_num_mono_candidates_new_term; + else ++qe->d_statistics.d_num_mono_candidates; + d_phase_mono = true; + d_step = ES_RESET1; + } else if (!d_phase_new_term){ + d_phase_new_term = true; + d_step = ES_GET_MONO_CANDIDATE; + } else { + d_phase_new_term = false; + d_step = ES_GET_MULTI_CANDIDATE; + } + break; + case ES_GET_MULTI_CANDIDATE: + Assert(d_im.empty()); + if(d_eh.getNextMultiCandidate(d_mc)){ + ++qe->d_statistics.d_num_multi_candidates; + d_phase_mono = false; + d_step = ES_RESET1; + } else d_step = ES_STOP; + break; + case ES_RESET1: + if(d_direct_patterns[d_mc.first.second]->reset(d_mc.first.first,d_im,qe)) + d_step = d_phase_mono ? TestMonoCache(qe) : ES_RESET2; + else d_step = d_phase_mono ? ES_GET_MONO_CANDIDATE : ES_GET_MULTI_CANDIDATE; + break; + case ES_RESET2: + Assert(!d_phase_mono); + if(d_direct_patterns[d_mc.second.second]->reset(d_mc.second.first,d_im,qe)) + d_step = TestMultiCache(qe); + else d_step = ES_NEXT1; + break; + case ES_NEXT1: + if(d_direct_patterns[d_mc.first.second]->getNextMatch(d_im,qe)) + d_step = d_phase_mono ? TestMonoCache(qe) : ES_RESET2; + else d_step = d_phase_mono ? ES_GET_MONO_CANDIDATE : ES_GET_MULTI_CANDIDATE; + break; + case ES_NEXT2: + if(d_direct_patterns[d_mc.second.second]->getNextMatch(d_im,qe)) + d_step = TestMultiCache(qe); + else d_step = ES_NEXT1; + break; + case ES_RESET_OTHER: + if(resetOther(qe)){ + d_step = ES_NEXT_OTHER; + return true; + } else d_step = d_phase_mono ? ES_NEXT1 : ES_NEXT2; + break; + case ES_NEXT_OTHER: + { + if(!getNextMatchOther(qe,false)){ + d_step = d_phase_mono ? ES_NEXT1 : ES_NEXT2; + }else{ + d_step = ES_NEXT_OTHER; + return true; + } + } + break; + case ES_STOP: + Assert(d_im.empty()); + return false; + } + } + } + + MultiEfficientPatsMatcher(std::vector< Node > & pats, QuantifiersEngine* qe): + d_eh(qe->getTheoryEngine()->getSatContext()), + d_cache(qe->getTheoryEngine()->getSatContext(),qe,pats.size()), + d_pats(pats), d_step(ES_START) { + Assert(pats.size() > 0); + for( size_t i=0; i< pats.size(); i++ ){ + d_patterns.push_back(mkPattern(pats[i],qe)); + if(pats[i].getKind()==kind::INST_CONSTANT){ + d_direct_patterns.push_back(new VarMatcher(pats[i],qe)); + } else if( pats[i].getKind() == kind::NOT && pats[i][0].getKind() == kind::EQUAL){ + d_direct_patterns.push_back(new ApplyMatcher(pats[i][0],qe)); + } else { + d_direct_patterns.push_back(new ApplyMatcher(pats[i],qe)); + } + }; + Theory* th_uf = qe->getTheoryEngine()->getTheory( theory::THEORY_UF ); + uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)th_uf->getInstantiator(); + ith->registerEfficientHandler(d_eh, pats); + }; + void resetInstantiationRound( QuantifiersEngine* qe ){ + Assert(d_step == ES_START || d_step == ES_STOP); + for( size_t i=0; i< d_patterns.size(); i++ ){ + d_patterns[i]->resetInstantiationRound( qe ); + d_direct_patterns[i]->resetInstantiationRound( qe ); + }; + d_step = ES_START; + d_phase_new_term = false; + Assert(d_im.empty()); + }; + + const InstMatch& getInstMatch(){return d_im;}; + + int addInstantiations( InstMatch& baseMatch, Node quant, QuantifiersEngine* qe); +}; + +int MultiEfficientPatsMatcher::addInstantiations( InstMatch& baseMatch, Node quant, QuantifiersEngine* qe){ + //now, try to add instantiation for each match produced + int addedLemmas = 0; + Assert(baseMatch.empty()); + resetInstantiationRound( qe ); + while( getNextMatch( qe ) ){ + InstMatch im_copy = getInstMatch(); + //m.makeInternal( d_quantEngine->getEqualityQuery() ); + if( qe->addInstantiation( quant, im_copy ) ){ + addedLemmas++; + } + } + //return number of lemmas added + return addedLemmas; +}; + +PatsMatcher* mkPatternsEfficient( std::vector< Node > pat, QuantifiersEngine* qe ){ + return new MultiEfficientPatsMatcher( pat, qe); +} + +} /* CVC4::theory::rrinst */ +} /* CVC4::theory */ +} /* CVC4 */ diff --git a/src/theory/rr_inst_match.h b/src/theory/rr_inst_match.h new file mode 100644 index 000000000..d89b221bb --- /dev/null +++ b/src/theory/rr_inst_match.h @@ -0,0 +1,263 @@ +/********************* */ +/*! \file inst_match.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief inst match class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__RR_INST_MATCH_H +#define __CVC4__RR_INST_MATCH_H + +#include "theory/theory.h" +#include "util/hash.h" +#include "util/ntuple.h" + +#include <ext/hash_set> +#include <iostream> +#include <map> + +#include "theory/uf/equality_engine.h" +#include "theory/uf/theory_uf.h" +#include "context/cdlist.h" + +#include "theory/inst_match.h" +#include "expr/node_manager.h" +#include "expr/node_builder.h" + +//#define USE_EFFICIENT_E_MATCHING + +namespace CVC4 { +namespace theory { + +namespace rrinst{ + +class CandidateGenerator +{ +public: + CandidateGenerator(){} + virtual ~CandidateGenerator(){}; + + /** Get candidates functions. These set up a context to get all match candidates. + cg->reset( eqc ); + do{ + Node cand = cg->getNextCandidate(); + //....... + }while( !cand.isNull() ); + + eqc is the equivalence class you are searching in + */ + virtual void reset( TNode eqc ) = 0; + virtual TNode getNextCandidate() = 0; + /** call this at the beginning of each instantiation round */ + virtual void resetInstantiationRound() = 0; +public: + /** legal candidate */ + static inline bool isLegalCandidate( TNode n ){ + return !n.getAttribute(NoMatchAttribute()) && + ( !Options::current()->cbqi || !n.hasAttribute(InstConstantAttribute())) && + ( !Options::current()->efficientEMatching || n.hasAttribute(AvailableInTermDb()) ); +} + +}; + + +inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) { + m.toStream(out); + return out; +} + +template<bool modEq = false> class InstMatchTrie2; +template<bool modEq = false> class InstMatchTrie2Pairs; + +template<bool modEq = false> +class InstMatchTrie2Gen +{ + friend class InstMatchTrie2<modEq>; + friend class InstMatchTrie2Pairs<modEq>; + +private: + + class Tree { + public: + typedef std::hash_map< Node, Tree *, NodeHashFunction > MLevel; + MLevel e; + const size_t level; //context level of creation + Tree() CVC4_UNDEFINED; + const Tree & operator =(const Tree & t){ + Assert(t.e.empty()); Assert(e.empty()); + Assert(t.level == level); + return t; + } + Tree(size_t l): level(l) {}; + ~Tree(){ + for(typename MLevel::iterator i = e.begin(); i!=e.end(); ++i) + delete(i->second); + }; + }; + + + typedef std::pair<Tree *, TNode> Mod; + + class CleanUp{ + public: + inline void operator()(Mod * m){ + typename Tree::MLevel::iterator i = m->first->e.find(m->second); + Assert (i != m->first->e.end()); //should not have been already removed + m->first->e.erase(i); + }; + }; + + EqualityQuery* d_eQ; + CandidateGenerator * d_cG; + + context::Context* d_context; + context::CDList<Mod, CleanUp, std::allocator<Mod> > d_mods; + + + typedef std::map<Node, Node>::const_iterator mapIter; + + /** add the substitution given by the iterator*/ + void addSubTree( Tree * root, mapIter current, mapIter end, size_t currLevel); + /** test if it exists match, modulo uf-equations if modEq is true if + * return false the deepest point of divergence is put in [e] and + * [diverge]. + */ + bool existsInstMatch( Tree * root, + mapIter & current, mapIter & end, + Tree * & e, mapIter & diverge) const; + + /** add match m in the trie root + return true if it was never seen */ + bool addInstMatch( InstMatch& m, Tree * root); + +public: + InstMatchTrie2Gen(context::Context* c, QuantifiersEngine* q); + InstMatchTrie2Gen(const InstMatchTrie2Gen &) CVC4_UNDEFINED; + const InstMatchTrie2Gen & operator =(const InstMatchTrie2Gen & e) CVC4_UNDEFINED; +}; + +template<bool modEq> +class InstMatchTrie2 +{ + typename InstMatchTrie2Gen<modEq>::Tree d_data; + InstMatchTrie2Gen<modEq> d_backtrack; +public: + InstMatchTrie2(context::Context* c, QuantifiersEngine* q): d_data(0), + d_backtrack(c,q) {}; + InstMatchTrie2(const InstMatchTrie2 &) CVC4_UNDEFINED; + const InstMatchTrie2 & operator =(const InstMatchTrie2 & e) CVC4_UNDEFINED; + /** add match m in the trie, + return true if it was never seen */ + inline bool addInstMatch( InstMatch& m){ + return d_backtrack.addInstMatch(m,&d_data); + }; + +};/* class InstMatchTrie2 */ + +class Matcher +{ +public: + /** reset instantiation round (call this whenever equivalence classes have changed) */ + virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0; + /** reset the term to match, return false if there is no such term */ + virtual bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe ) = 0; + /** get the next match. If it return false once you shouldn't call + getNextMatch again before doing a reset */ + virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0; + /** If reset, or getNextMatch return false they remove from the + InstMatch the binding that they have previously created */ + + /** virtual Matcher in order to have definned behavior */ + virtual ~Matcher(){}; +}; + + +class ApplyMatcher: public Matcher{ +private: + /** What to check first: constant and variable */ + std::vector< triple< TNode,size_t,EqualityQuery* > > d_constants; + std::vector< triple< TNode,size_t,EqualityQuery* > > d_variables; + /** children generators, only the sub-pattern which are + neither a variable neither a constant appears */ + std::vector< triple< Matcher*, size_t, EqualityQuery* > > d_childrens; + /** the variable that have been set by this matcher (during its own reset) */ + std::vector< TNode > d_binded; /* TNode because the variable are already in d_pattern */ + /** the representant of the argument of the term given by the last reset */ + std::vector< Node > d_reps; +public: + /** The pattern we are producing matches for */ + Node d_pattern; +public: + /** constructors */ + ApplyMatcher( Node pat, QuantifiersEngine* qe); + /** destructor */ + ~ApplyMatcher(){/*TODO delete dandling pointers? */} + /** reset instantiation round (call this whenever equivalence classes have changed) */ + void resetInstantiationRound( QuantifiersEngine* qe ); + /** reset the term to match */ + bool reset( TNode n, InstMatch& m, QuantifiersEngine* qe ); + /** get the next match. */ + bool getNextMatch(InstMatch& m, QuantifiersEngine* qe); +private: + bool getNextMatch(InstMatch& m, QuantifiersEngine* qe, bool reset); +}; + + +/* Match literal so you don't choose the equivalence class( */ +class PatMatcher +{ +public: + /** reset instantiation round (call this whenever equivalence classes have changed) */ + virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0; + /** reset the matcher, return false if there is no such term */ + virtual bool reset( InstMatch& m, QuantifiersEngine* qe ) = 0; + /** get the next match. If it return false once you shouldn't call + getNextMatch again before doing a reset */ + virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0; + /** If reset, or getNextMatch return false they remove from the + InstMatch the binding that they have previously created */ +}; + +Matcher* mkMatcher( Node pat, QuantifiersEngine* qe ); +PatMatcher* mkPattern( Node pat, QuantifiersEngine* qe ); + +/* Match literal so you don't choose the equivalence class( */ +class PatsMatcher +{ +public: + /** reset instantiation round (call this whenever equivalence classes have changed) */ + virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0; + /** reset the matcher, return false if there is no such term */ + virtual bool getNextMatch( QuantifiersEngine* qe ) = 0; + virtual const InstMatch& getInstMatch() = 0; + /** Add directly the instantiation to quantifiers engine */ + virtual int addInstantiations( InstMatch& baseMatch, Node quant, QuantifiersEngine* qe) = 0; +}; + +PatsMatcher* mkPatterns( std::vector< Node > pat, QuantifiersEngine* qe ); +PatsMatcher* mkPatternsEfficient( std::vector< Node > pat, QuantifiersEngine* qe ); + +/** return true if whatever Node is subsituted for the variables the + given Node can't match the pattern */ +bool nonunifiable( TNode t, TNode pat, const std::vector<Node> & vars); + +class InstMatchGenerator; + +}/* CVC4::theory rrinst */ + +}/* CVC4::theory namespace */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__RR_INST_MATCH_H */ diff --git a/src/theory/rr_inst_match_impl.h b/src/theory/rr_inst_match_impl.h new file mode 100644 index 000000000..04a15d41f --- /dev/null +++ b/src/theory/rr_inst_match_impl.h @@ -0,0 +1,128 @@ +/********************* */ +/*! \file inst_match_impl.h + ** \verbatim + ** Original author: bobot + ** Major contributors: none + ** Minor contributors (to current version): taking, mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief inst match class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__RR_INST_MATCH_IMPL_H +#define __CVC4__RR_INST_MATCH_IMPL_H + +#include "theory/rr_inst_match.h" +#include "theory/theory_engine.h" +#include "theory/quantifiers_engine.h" +#include "theory/uf/theory_uf_candidate_generator.h" +#include "theory/uf/equality_engine.h" + +namespace CVC4 { +namespace theory { +namespace rrinst { + +template<bool modEq> +InstMatchTrie2Gen<modEq>::InstMatchTrie2Gen(context::Context* c, QuantifiersEngine* qe): + d_context(c), d_mods(c) { + d_eQ = qe->getEqualityQuery(); + d_cG = qe->getRRCanGenClass(); +}; + +/** add match m for quantifier f starting at index, take into account equalities q, return true if successful */ +template<bool modEq> +void InstMatchTrie2Gen<modEq>::addSubTree( Tree * root, mapIter current, mapIter end, size_t currLevel ) { + if( current == end ) return; + + Assert(root->e.find(current->second) == root->e.end()); + Tree * root2 = new Tree(currLevel); + root->e.insert(std::make_pair(current->second, root2)); + addSubTree(root2, ++current, end, currLevel ); +} + +/** exists match */ +template<bool modEq> +bool InstMatchTrie2Gen<modEq>::existsInstMatch(InstMatchTrie2Gen<modEq>::Tree * root, + mapIter & current, mapIter & end, + Tree * & e, mapIter & diverge) const{ + if( current == end ) { + Debug("Trie2") << "Trie2 Bottom " << std::endl; + --current; + return true; + }; //Already their + + if (current->first > diverge->first){ + // this point is the deepest point currently seen map are ordered + e = root; + diverge = current; + }; + + TNode n = current->second; + typename InstMatchTrie2Gen<modEq>::Tree::MLevel::iterator it = + root->e.find( n ); + if( it!=root->e.end() && + existsInstMatch( (*it).second, ++current, end, e, diverge) ){ + Debug("Trie2") << "Trie2 Directly here " << n << std::endl; + --current; + return true; + } + Assert( it==root->e.end() || e != root ); + + // Even if n is in the trie others of the equivalence class + // can also be in it since the equality can have appeared + // after they have been added + if( modEq && d_eQ->hasTerm( n ) ){ + //check modulo equality if any other instantiation match exists + d_cG->reset( d_eQ->getRepresentative( n ) ); + for(TNode en = d_cG->getNextCandidate() ; !en.isNull() ; + en = d_cG->getNextCandidate() ){ + if( en == n ) continue; // already tested + typename InstMatchTrie2Gen<modEq>::Tree::MLevel::iterator itc = + root->e.find( en ); + if( itc!=root->e.end() && + existsInstMatch( (*itc).second, ++current, end, e, diverge) ){ + Debug("Trie2") << "Trie2 Indirectly here by equality " << n << " = " << en << std::endl; + --current; + return true; + } + Assert( itc==root->e.end() || e != root ); + } + } + --current; + return false; +} + +template<bool modEq> +bool InstMatchTrie2Gen<modEq>:: +addInstMatch( InstMatch& m, InstMatchTrie2Gen<modEq>::Tree* e ) { + d_cG->resetInstantiationRound(); + mapIter begin = m.begin(); + mapIter end = m.end(); + mapIter diverge = begin; + if( !existsInstMatch(e, begin, end, e, diverge ) ){ + Assert(!diverge->second.isNull()); + size_t currLevel = d_context->getLevel(); + addSubTree( e, diverge, end, currLevel ); + if(e->level != currLevel) + //If same level that e, will be removed at the same time than e + d_mods.push_back(std::make_pair(e,diverge->second)); + return true; + }else{ + return false; + } +} + +}/* CVC4::theory::rrinst namespace */ + +}/* CVC4::theory namespace */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__RR_INST_MATCH_IMPL_H */ diff --git a/src/theory/rr_trigger.cpp b/src/theory/rr_trigger.cpp new file mode 100644 index 000000000..579608b59 --- /dev/null +++ b/src/theory/rr_trigger.cpp @@ -0,0 +1,523 @@ +/********************* */ +/*! \file trigger.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of trigger class + **/ + +#include "theory/rr_trigger.h" +#include "theory/theory_engine.h" +#include "theory/quantifiers_engine.h" +#include "theory/uf/theory_uf_instantiator.h" +#include "theory/uf/theory_uf_candidate_generator.h" +#include "theory/uf/equality_engine.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::rrinst; + +//#define NESTED_PATTERN_SELECTION + +Trigger* Trigger::TrTrie::getTrigger2( std::vector< Node >& nodes ){ + if( nodes.empty() ){ + return d_tr; + }else{ + Node n = nodes.back(); + nodes.pop_back(); + if( d_children.find( n )!=d_children.end() ){ + return d_children[n]->getTrigger2( nodes ); + }else{ + return NULL; + } + } +} +void Trigger::TrTrie::addTrigger2( std::vector< Node >& nodes, Trigger* t ){ + if( nodes.empty() ){ + d_tr = t; + }else{ + Node n = nodes.back(); + nodes.pop_back(); + if( d_children.find( n )==d_children.end() ){ + d_children[n] = new TrTrie; + } + d_children[n]->addTrigger2( nodes, t ); + } +} + +/** trigger static members */ +std::map< Node, std::vector< Node > > Trigger::d_var_contains; +int Trigger::trCount = 0; +Trigger::TrTrie Trigger::d_tr_trie; + +/** trigger class constructor */ +Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool smartTriggers ) : +d_quantEngine( qe ), d_f( f ){ + trCount++; + d_nodes.insert( d_nodes.begin(), nodes.begin(), nodes.end() ); + Debug("trigger") << "Trigger for " << f << ": " << d_nodes << std::endl; + if(matchOption == MATCH_GEN_DEFAULT) d_mg = mkPatterns( d_nodes, qe ); + else d_mg = mkPatternsEfficient( d_nodes, qe ); + if( d_nodes.size()==1 ){ + if( isSimpleTrigger( d_nodes[0] ) ){ + ++(qe->d_statistics.d_triggers); + }else{ + ++(qe->d_statistics.d_simple_triggers); + } + }else{
+ Debug("multi-trigger") << "Multi-trigger " << (*this) << std::endl; + //std::cout << "Multi-trigger for " << f << " : " << std::endl; + //std::cout << " " << (*this) << std::endl; + ++(qe->d_statistics.d_multi_triggers); + } +}
+void Trigger::computeVarContains( Node n ) {
+ if( d_var_contains.find( n )==d_var_contains.end() ){
+ d_var_contains[n].clear();
+ computeVarContains2( n, n );
+ }
+}
+
+void Trigger::computeVarContains2( Node n, Node parent ){
+ if( n.getKind()==INST_CONSTANT ){
+ if( std::find( d_var_contains[parent].begin(), d_var_contains[parent].end(), n )==d_var_contains[parent].end() ){
+ d_var_contains[parent].push_back( n );
+ }
+ }else{
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ computeVarContains2( n[i], parent );
+ }
+ }
+} +
+void Trigger::resetInstantiationRound(){
+ d_mg->resetInstantiationRound( d_quantEngine );
+}
+
+ +bool Trigger::getNextMatch(){
+ bool retVal = d_mg->getNextMatch( d_quantEngine );
+ //m.makeInternal( d_quantEngine->getEqualityQuery() );
+ return retVal;
+}
+ +// bool Trigger::getMatch( Node t, InstMatch& m ){ +// //FIXME: this assumes d_mg is an inst match generator +// return ((InstMatchGenerator*)d_mg)->getMatch( t, m, d_quantEngine ); +// } +
+ +int Trigger::addInstantiations( InstMatch& baseMatch ){
+ int addedLemmas = d_mg->addInstantiations( baseMatch, + d_nodes[0].getAttribute(InstConstantAttribute()), + d_quantEngine);
+ if( addedLemmas>0 ){
+ Debug("inst-trigger") << "Added " << addedLemmas << " lemmas, trigger was "; + for( int i=0; i<(int)d_nodes.size(); i++ ){ + Debug("inst-trigger") << d_nodes[i] << " "; + } + Debug("inst-trigger") << std::endl;
+ }
+ return addedLemmas;
+}
+
+Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool keepAll, int trOption,
+ bool smartTriggers ){
+ std::vector< Node > trNodes;
+ if( !keepAll ){
+ //only take nodes that contribute variables to the trigger when added
+ std::vector< Node > temp;
+ temp.insert( temp.begin(), nodes.begin(), nodes.end() );
+ std::map< Node, bool > vars;
+ std::map< Node, std::vector< Node > > patterns;
+ for( int i=0; i<(int)temp.size(); i++ ){
+ bool foundVar = false;
+ computeVarContains( temp[i] );
+ for( int j=0; j<(int)d_var_contains[ temp[i] ].size(); j++ ){
+ Node v = d_var_contains[ temp[i] ][j];
+ if( v.getAttribute(InstConstantAttribute())==f ){
+ if( vars.find( v )==vars.end() ){
+ vars[ v ] = true;
+ foundVar = true;
+ }
+ }
+ }
+ if( foundVar ){
+ trNodes.push_back( temp[i] );
+ for( int j=0; j<(int)d_var_contains[ temp[i] ].size(); j++ ){
+ Node v = d_var_contains[ temp[i] ][j];
+ patterns[ v ].push_back( temp[i] );
+ }
+ }
+ }
+ //now, minimalize the trigger
+ for( int i=0; i<(int)trNodes.size(); i++ ){
+ bool keepPattern = false;
+ Node n = trNodes[i];
+ for( int j=0; j<(int)d_var_contains[ n ].size(); j++ ){
+ Node v = d_var_contains[ n ][j];
+ if( patterns[v].size()==1 ){
+ keepPattern = true;
+ break;
+ }
+ }
+ if( !keepPattern ){
+ //remove from pattern vector
+ for( int j=0; j<(int)d_var_contains[ n ].size(); j++ ){
+ Node v = d_var_contains[ n ][j];
+ for( int k=0; k<(int)patterns[v].size(); k++ ){
+ if( patterns[v][k]==n ){
+ patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 );
+ break;
+ }
+ }
+ }
+ //remove from trigger nodes
+ trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 );
+ i--;
+ }
+ }
+ }else{
+ trNodes.insert( trNodes.begin(), nodes.begin(), nodes.end() );
+ }
+
+ //check for duplicate?
+ if( trOption==TR_MAKE_NEW ){
+ //static int trNew = 0;
+ //static int trOld = 0;
+ //Trigger* t = d_tr_trie.getTrigger( trNodes );
+ //if( t ){
+ // trOld++;
+ //}else{
+ // trNew++;
+ //}
+ //if( (trNew+trOld)%100==0 ){
+ // std::cout << "Trigger new old = " << trNew << " " << trOld << std::endl;
+ //}
+ }else{
+ Trigger* t = d_tr_trie.getTrigger( trNodes );
+ if( t ){
+ if( trOption==TR_GET_OLD ){
+ //just return old trigger
+ return t;
+ }else{
+ return NULL;
+ }
+ }
+ }
+ Trigger* t = new Trigger( qe, f, trNodes, matchOption, smartTriggers );
+ d_tr_trie.addTrigger( trNodes, t );
+ return t;
+}
+Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption, bool smartTriggers ){
+ std::vector< Node > nodes;
+ nodes.push_back( n );
+ return mkTrigger( qe, f, nodes, matchOption, keepAll, trOption, smartTriggers );
+}
+ +bool Trigger::isUsableTrigger( std::vector< Node >& nodes, Node f ){ + for( int i=0; i<(int)nodes.size(); i++ ){ + if( !isUsableTrigger( nodes[i], f ) ){ + return false; + } + } + return true; +}
+
+bool Trigger::isUsable( Node n, Node f ){
+ if( n.getAttribute(InstConstantAttribute())==f ){
+ if( !isAtomicTrigger( n ) && n.getKind()!=INST_CONSTANT ){
+ std::map< Node, Node > coeffs;
+ return getPatternArithmetic( f, n, coeffs );
+ }else{
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ if( !isUsable( n[i], f ) ){
+ return false;
+ }
+ }
+ return true;
+ }
+ }else{
+ return true;
+ }
+}
+ +bool Trigger::isSimpleTrigger( Node n ){ + if( isAtomicTrigger( n ) ){ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + if( n[i].getKind()!=INST_CONSTANT && n[i].hasAttribute(InstConstantAttribute()) ){ + return false; + } + } + return true; + }else{ + return false; + } +} + +/** filter all nodes that have instances */ +void Trigger::filterInstances( std::vector< Node >& nodes ){ + std::vector< bool > active; + active.resize( nodes.size(), true ); + for( int i=0; i<(int)nodes.size(); i++ ){ + for( int j=i+1; j<(int)nodes.size(); j++ ){ + if( active[i] && active[j] ){ + int result = isInstanceOf( nodes[i], nodes[j] ); + if( result==1 ){ + active[j] = false; + }else if( result==-1 ){ + active[i] = false; + } + } + } + } + std::vector< Node > temp; + for( int i=0; i<(int)nodes.size(); i++ ){ + if( active[i] ){ + temp.push_back( nodes[i] ); + } + } + nodes.clear(); + nodes.insert( nodes.begin(), temp.begin(), temp.end() ); +} + + +bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ){
+ if( patMap.find( n )==patMap.end() ){
+ patMap[ n ] = false;
+ if( tstrt==TS_MIN_TRIGGER ){
+ if( n.getKind()==FORALL ){
+#ifdef NESTED_PATTERN_SELECTION
+ //return collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt );
+ return collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt );
+#else
+ return false;
+#endif
+ }else{
+ bool retVal = false;
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){
+ retVal = true;
+ }
+ }
+ if( retVal ){
+ return true;
+ }else if( isUsableTrigger( n, f ) ){
+ patMap[ n ] = true;
+ return true;
+ }else{
+ return false;
+ }
+ }
+ }else{
+ bool retVal = false;
+ if( isUsableTrigger( n, f ) ){
+ patMap[ n ] = true;
+ if( tstrt==TS_MAX_TRIGGER ){
+ return true;
+ }else{
+ retVal = true;
+ }
+ }
+ if( n.getKind()==FORALL ){
+#ifdef NESTED_PATTERN_SELECTION
+ //if( collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt ) ){
+ // retVal = true;
+ //}
+ if( collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt ) ){
+ retVal = true;
+ }
+#endif
+ }else{
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){
+ retVal = true;
+ }
+ }
+ }
+ return retVal;
+ }
+ }else{
+ return patMap[ n ];
+ }
+} + +void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, bool filterInst ){
+ std::map< Node, bool > patMap; + if( filterInst ){ + //immediately do not consider any term t for which another term is an instance of t + std::vector< Node > patTerms2; + collectPatTerms( qe, f, n, patTerms2, TS_ALL, false ); + std::vector< Node > temp; + temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() ); + filterInstances( temp ); + if( temp.size()!=patTerms2.size() ){ + Debug("trigger-filter-instance") << "Filtered an instance: " << std::endl; + Debug("trigger-filter-instance") << "Old: "; + for( int i=0; i<(int)patTerms2.size(); i++ ){ + Debug("trigger-filter-instance") << patTerms2[i] << " "; + } + Debug("trigger-filter-instance") << std::endl << "New: "; + for( int i=0; i<(int)temp.size(); i++ ){ + Debug("trigger-filter-instance") << temp[i] << " "; + } + Debug("trigger-filter-instance") << std::endl; + } + if( tstrt==TS_ALL ){ + patTerms.insert( patTerms.begin(), temp.begin(), temp.end() ); + return; + }else{ + //do not consider terms that have instances + for( int i=0; i<(int)patTerms2.size(); i++ ){ + if( std::find( temp.begin(), temp.end(), patTerms2[i] )==temp.end() ){ + patMap[ patTerms2[i] ] = false; + } + } + } + } + collectPatTerms2( qe, f, n, patMap, tstrt ); + for( std::map< Node, bool >::iterator it = patMap.begin(); it != patMap.end(); ++it ){
+ if( it->second ){
+ patTerms.push_back( it->first );
+ }
+ } +} + +/** is n1 an instance of n2 or vice versa? */ +int Trigger::isInstanceOf( Node n1, Node n2 ){ + if( n1==n2 ){ + return 1; + }else if( n1.getKind()==n2.getKind() ){ + if( n1.getKind()==APPLY_UF ){ + if( n1.getOperator()==n2.getOperator() ){ + int result = 0; + for( int i=0; i<(int)n1.getNumChildren(); i++ ){ + if( n1[i]!=n2[i] ){ + int cResult = isInstanceOf( n1[i], n2[i] ); + if( cResult==0 ){ + return 0; + }else if( cResult!=result ){ + if( result!=0 ){ + return 0; + }else{ + result = cResult; + } + } + } + } + return result; + } + } + return 0; + }else if( n2.getKind()==INST_CONSTANT ){ + computeVarContains( n1 ); + //if( std::find( d_var_contains[ n1 ].begin(), d_var_contains[ n1 ].end(), n2 )!=d_var_contains[ n1 ].end() ){ + // return 1; + //} + if( d_var_contains[ n1 ].size()==1 && d_var_contains[ n1 ][ 0 ]==n2 ){ + return 1; + } + }else if( n1.getKind()==INST_CONSTANT ){ + computeVarContains( n2 ); + //if( std::find( d_var_contains[ n2 ].begin(), d_var_contains[ n2 ].end(), n1 )!=d_var_contains[ n2 ].end() ){ + // return -1; + //} + if( d_var_contains[ n2 ].size()==1 && d_var_contains[ n2 ][ 0 ]==n1 ){ + return 1; + } + } + return 0; +} + +bool Trigger::isVariableSubsume( Node n1, Node n2 ){ + if( n1==n2 ){ + return true; + }else{ + //std::cout << "is variable subsume ? " << n1 << " " << n2 << std::endl; + computeVarContains( n1 ); + computeVarContains( n2 ); + for( int i=0; i<(int)d_var_contains[n2].size(); i++ ){ + if( std::find( d_var_contains[n1].begin(), d_var_contains[n1].end(), d_var_contains[n2][i] )==d_var_contains[n1].end() ){ + //std::cout << "no" << std::endl; + return false; + } + } + //std::cout << "yes" << std::endl; + return true; + } +} + +void Trigger::getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains ){ + for( int i=0; i<(int)pats.size(); i++ ){ + computeVarContains( pats[i] ); + varContains[ pats[i] ].clear(); + for( int j=0; j<(int)d_var_contains[pats[i]].size(); j++ ){ + if( d_var_contains[pats[i]][j].getAttribute(InstConstantAttribute())==f ){ + varContains[ pats[i] ].push_back( d_var_contains[pats[i]][j] ); + } + } + } +} +
+void Trigger::getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ){
+ computeVarContains( n );
+ for( int j=0; j<(int)d_var_contains[n].size(); j++ ){
+ if( d_var_contains[n][j].getAttribute(InstConstantAttribute())==f ){
+ varContains.push_back( d_var_contains[n][j] );
+ }
+ }
+}
+ +bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs ){ + if( n.getKind()==PLUS ){ + Assert( coeffs.empty() ); + NodeBuilder<> t(kind::PLUS); + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + if( n[i].hasAttribute(InstConstantAttribute()) ){ + if( n[i].getKind()==INST_CONSTANT ){ + if( n[i].getAttribute(InstConstantAttribute())==f ){ + coeffs[ n[i] ] = Node::null(); + }else{ + coeffs.clear(); + return false; + } + }else if( !getPatternArithmetic( f, n[i], coeffs ) ){ + coeffs.clear(); + return false; + } + }else{ + t << n[i]; + } + } + if( t.getNumChildren()==0 ){ + coeffs[ Node::null() ] = NodeManager::currentNM()->mkConst( Rational(0) ); + }else if( t.getNumChildren()==1 ){ + coeffs[ Node::null() ] = t.getChild( 0 ); + }else{ + coeffs[ Node::null() ] = t; + } + return true; + }else if( n.getKind()==MULT ){ + if( n[0].getKind()==INST_CONSTANT && n[0].getAttribute(InstConstantAttribute())==f ){ + Assert( !n[1].hasAttribute(InstConstantAttribute()) ); + coeffs[ n[0] ] = n[1]; + return true; + }else if( n[1].getKind()==INST_CONSTANT && n[1].getAttribute(InstConstantAttribute())==f ){ + Assert( !n[0].hasAttribute(InstConstantAttribute()) ); + coeffs[ n[1] ] = n[0]; + return true; + } + } + return false; +} diff --git a/src/theory/rr_trigger.h b/src/theory/rr_trigger.h new file mode 100644 index 000000000..7ea4ee1a3 --- /dev/null +++ b/src/theory/rr_trigger.h @@ -0,0 +1,176 @@ +/********************* */ +/*! \file trigger.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief trigger class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__RR_TRIGGER_H +#define __CVC4__RR_TRIGGER_H + +#include "theory/rr_inst_match.h" + +namespace CVC4 { +namespace theory { +namespace rrinst { + +//a collect of nodes representing a trigger +class Trigger { +public: + static int trCount; +private: + /** computation of variable contains */ + static std::map< Node, std::vector< Node > > d_var_contains; + static void computeVarContains( Node n ); + static void computeVarContains2( Node n, Node parent ); +private: + /** the quantifiers engine */ + QuantifiersEngine* d_quantEngine; + /** the quantifier this trigger is for */ + Node d_f; + /** match generators */ + PatsMatcher * d_mg; +private: + /** a trie of triggers */ + class TrTrie + { + private: + Trigger* getTrigger2( std::vector< Node >& nodes ); + void addTrigger2( std::vector< Node >& nodes, Trigger* t ); + public: + TrTrie() : d_tr( NULL ){} + Trigger* d_tr; + std::map< Node, TrTrie* > d_children; + Trigger* getTrigger( std::vector< Node >& nodes ){ + std::vector< Node > temp; + temp.insert( temp.begin(), nodes.begin(), nodes.end() ); + std::sort( temp.begin(), temp.end() ); + return getTrigger2( temp ); + } + void addTrigger( std::vector< Node >& nodes, Trigger* t ){ + std::vector< Node > temp; + temp.insert( temp.begin(), nodes.begin(), nodes.end() ); + std::sort( temp.begin(), temp.end() ); + return addTrigger2( temp, t ); + } + }; + /** all triggers will be stored in this trie */ + static TrTrie d_tr_trie; +private: + /** trigger constructor */ + Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes, int matchOption = 0, bool smartTriggers = false ); +public: + ~Trigger(){} +public: + std::vector< Node > d_nodes; +public: + void debugPrint( const char* c ); + PatsMatcher* getGenerator() { return d_mg; } +public: + /** reset instantiation round (call this whenever equivalence classes have changed) */ + void resetInstantiationRound(); + /** get next match. must call reset( eqc ) once before this function. */ + bool getNextMatch(); + const InstMatch & getInstMatch(){return d_mg->getInstMatch();}; + /** return whether this is a multi-trigger */ + bool isMultiTrigger() { return d_nodes.size()>1; } +public: + /** add all available instantiations exhaustively, in any equivalence class + if limitInst>0, limitInst is the max # of instantiations to try */ + int addInstantiations( InstMatch& baseMatch); + /** mkTrigger method + ie : quantifier engine; + f : forall something .... + nodes : (multi-)trigger + matchOption : which policy to use for creating matches (one of InstMatchGenerator::MATCH_GEN_* ) + keepAll: don't remove unneeded patterns; + trOption : policy for dealing with triggers that already existed (see below) + */ + enum { + //options for producing matches + MATCH_GEN_DEFAULT = 0, + MATCH_GEN_EFFICIENT_E_MATCH, //generate matches via Efficient E + }; + enum{ + TR_MAKE_NEW, //make new trigger even if it already may exist + TR_GET_OLD, //return a previous trigger if it had already been created + TR_RETURN_NULL //return null if a duplicate is found + }; + static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, + int matchOption = 0, bool keepAll = true, int trOption = TR_MAKE_NEW, + bool smartTriggers = false ); + static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, Node n, + int matchOption = 0, bool keepAll = true, int trOption = TR_MAKE_NEW, + bool smartTriggers = false ); +private: + /** is subterm of trigger usable */ + static bool isUsable( Node n, Node f ); + /** collect all APPLY_UF pattern terms for f in n */ + static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ); +public: + //different strategies for choosing trigger terms + enum { + TS_MAX_TRIGGER = 0, + TS_MIN_TRIGGER, + TS_ALL, + }; + static void collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, bool filterInst = false ); +public: + /** is usable trigger */ + static inline bool isUsableTrigger( TNode n, TNode f ){ + //return n.getAttribute(InstConstantAttribute())==f && n.getKind()==APPLY_UF; + return n.getAttribute(InstConstantAttribute())==f && isAtomicTrigger( n ) && isUsable( n, f ); + } + static inline bool isAtomicTrigger( TNode n ){ + return + n.getKind()==kind::APPLY_UF || + n.getKind()==kind::SELECT || + n.getKind()==kind::STORE; + } + static bool isUsableTrigger( std::vector< Node >& nodes, Node f ); + static bool isSimpleTrigger( Node n ); + /** filter all nodes that have instances */ + static void filterInstances( std::vector< Node >& nodes ); + /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */ + static int isInstanceOf( Node n1, Node n2 ); + /** variables subsume, return true if n1 contains all free variables in n2 */ + static bool isVariableSubsume( Node n1, Node n2 ); + /** get var contains */ + static void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains ); + static void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ); + /** get pattern arithmetic */ + static bool getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs ); + + 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 << " )"; + } +}; + +inline std::ostream& operator<<(std::ostream& out, const Trigger & tr) { + tr.toStream(out); + return out; +} + +}/* CVC4::theory::rrinst namespace */ + +}/* CVC4::theory namespace */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__RR_TRIGGER_H */ diff --git a/src/theory/theory.h b/src/theory/theory.h index 7d003bf25..0cf7a8774 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -52,6 +52,10 @@ class InstStrategy; class QuantifiersEngine; class TheoryModel; +namespace rrinst{ +class CandidateGenerator; +} + /** * Information about an assertion for the theories. */ @@ -834,6 +838,12 @@ public: virtual bool areDisequal( Node a, Node b ) { return false; } virtual Node getRepresentative( Node a ) { return a; } virtual Node getInternalRepresentative( Node a ) { return getRepresentative( a ); } +public: + /** A Creator of CandidateGenerator for classes (one element in each + equivalence class) and class (every element of one equivalence + class) */ + virtual rrinst::CandidateGenerator* getRRCanGenClasses(){ return NULL; }; + virtual rrinst::CandidateGenerator* getRRCanGenClass(){ return NULL; }; };/* class Instantiator */ inline Assertion Theory::get() { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index f55c7c258..449f4adc3 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -450,6 +450,13 @@ public: } /** + * Get a pointer to the underlying user context. + */ + inline context::Context* getUserContext() const { + return d_userContext; + } + + /** * Get a pointer to the underlying quantifiers engine. */ theory::QuantifiersEngine* getQuantifiersEngine() const { @@ -677,8 +684,8 @@ public: } /** Get the theory for id */ - theory::Theory* getTheory(int id) { - return d_theoryTable[id]; + theory::Theory* getTheory(theory::TheoryId theoryId) { + return d_theoryTable[theoryId]; } /** diff --git a/src/theory/trigger.cpp b/src/theory/trigger.cpp index 55ca07d77..14ba88ba1 100644 --- a/src/theory/trigger.cpp +++ b/src/theory/trigger.cpp @@ -26,6 +26,7 @@ using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::theory; +using namespace CVC4::theory::inst; //#define NESTED_PATTERN_SELECTION diff --git a/src/theory/trigger.h b/src/theory/trigger.h index 476ef392e..84bc7ac2e 100644 --- a/src/theory/trigger.h +++ b/src/theory/trigger.h @@ -23,6 +23,7 @@ namespace CVC4 { namespace theory { +namespace inst { //a collect of nodes representing a trigger class Trigger { @@ -163,6 +164,8 @@ inline std::ostream& operator<<(std::ostream& out, const Trigger & tr) { return out; } +}/* CVC4::theory::inst namespace */ + }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index fe75b5f59..9376c858d 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -65,6 +65,10 @@ void EqualityEngine::init() { d_triggerDatabaseAllocatedSize = 100000; d_triggerDatabase = (char*) malloc(d_triggerDatabaseAllocatedSize); + //We can't notify during the initialization because it notifies + // QuantifiersEngine.AddTermToDatabase that try to access to the uf + // instantiator that currently doesn't exist. + ScopedBool sb(d_performNotify, false); addTerm(d_true); addTerm(d_false); diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 9228e29d4..0b461131e 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -794,7 +794,7 @@ class EqClassesIterator { public: - EqClassesIterator() { } + EqClassesIterator(): d_ee(NULL), d_it(0){ } EqClassesIterator(eq::EqualityEngine* ee) : d_ee(ee) { d_it = 0; if ( d_it < d_ee->d_nodesCount && @@ -840,7 +840,7 @@ class EqClassIterator { public: - EqClassIterator() { } + EqClassIterator(): d_ee(NULL){ } EqClassIterator(Node eqc, eq::EqualityEngine* ee) : d_ee(ee) { Assert( d_ee->getRepresentative(eqc) == eqc ); d_rep = eqc; diff --git a/src/theory/uf/inst_strategy.cpp b/src/theory/uf/inst_strategy.cpp index 669df055a..5696251ed 100644 --- a/src/theory/uf/inst_strategy.cpp +++ b/src/theory/uf/inst_strategy.cpp @@ -28,6 +28,7 @@ using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::uf; +using namespace CVC4::theory::inst; #define USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER //#define MULTI_TRIGGER_FULL_EFFORT_HALF @@ -83,7 +84,7 @@ void InstStrategyCheckCESolved::calcSolved( Node f ){ Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j ); Node rep = d_th->getInternalRepresentative( i ); if( !rep.hasAttribute(InstConstantAttribute()) ){ - d_th->d_baseMatch[f].d_map[ i ] = rep; + d_th->d_baseMatch[f].set(i,rep); }else{ d_solved[ f ] = false; } diff --git a/src/theory/uf/inst_strategy.h b/src/theory/uf/inst_strategy.h index 09b8087f2..a0091c4b4 100644 --- a/src/theory/uf/inst_strategy.h +++ b/src/theory/uf/inst_strategy.h @@ -20,6 +20,7 @@ #define __CVC4__INST_STRATEGY_H #include "theory/quantifiers_engine.h" +#include "theory/trigger.h" #include "context/context.h" #include "context/context_mm.h" @@ -59,7 +60,7 @@ private: /** InstantiatorTheoryUf class */ InstantiatorTheoryUf* d_th; /** explicitly provided patterns */ - std::map< Node, std::vector< Trigger* > > d_user_gen; + std::map< Node, std::vector< inst::Trigger* > > d_user_gen; /** counter for quantifiers */ std::map< Node, int > d_counter; /** process functions */ @@ -75,7 +76,7 @@ public: /** get num patterns */ int getNumUserGenerators( Node f ) { return (int)d_user_gen[f].size(); } /** get user pattern */ - Trigger* getUserGenerator( Node f, int i ) { return d_user_gen[f][ i ]; } + inst::Trigger* getUserGenerator( Node f, int i ) { return d_user_gen[f][ i ]; } /** identify */ std::string identify() const { return std::string("UserPatterns"); } };/* class InstStrategyUserPatterns */ @@ -99,7 +100,7 @@ private: /** generate additional triggers */ bool d_generate_additional; /** triggers for each quantifier */ - std::map< Node, std::map< Trigger*, bool > > d_auto_gen_trigger; + std::map< Node, std::map< inst::Trigger*, bool > > d_auto_gen_trigger; std::map< Node, int > d_counter; /** single, multi triggers for each quantifier */ std::map< Node, std::vector< Node > > d_patTerms[2]; @@ -120,7 +121,7 @@ public: ~InstStrategyAutoGenTriggers(){} public: /** get auto-generated trigger */ - Trigger* getAutoGenTrigger( Node f ); + inst::Trigger* getAutoGenTrigger( Node f ); /** identify */ std::string identify() const { return std::string("AutoGenTriggers"); } /** set regenerate frequency, if fr<0, turn off regenerate */ diff --git a/src/theory/uf/theory_uf_candidate_generator.cpp b/src/theory/uf/theory_uf_candidate_generator.cpp index 5342188f7..80151d1e1 100644 --- a/src/theory/uf/theory_uf_candidate_generator.cpp +++ b/src/theory/uf/theory_uf_candidate_generator.cpp @@ -26,6 +26,11 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::uf; +namespace CVC4{ +namespace theory{ +namespace uf{ +namespace inst{ + CandidateGeneratorTheoryUf::CandidateGeneratorTheoryUf( InstantiatorTheoryUf* ith, Node op ) : d_op( op ), d_ith( ith ), d_term_iter( -2 ){ Assert( !d_op.isNull() ); @@ -45,6 +50,7 @@ void CandidateGeneratorTheoryUf::reset( Node eqc ){ d_retNode = Node::null(); }else{ d_retNode = eqc; + } d_term_iter = -1; } @@ -169,3 +175,8 @@ Node CandidateGeneratorTheoryUfLitDeq::getNextCandidate(){ } return Node::null(); } + +} +} +} +} diff --git a/src/theory/uf/theory_uf_candidate_generator.h b/src/theory/uf/theory_uf_candidate_generator.h index 668d619db..a06f04f99 100644 --- a/src/theory/uf/theory_uf_candidate_generator.h +++ b/src/theory/uf/theory_uf_candidate_generator.h @@ -20,11 +20,155 @@ #define __CVC4__THEORY_UF_CANDIDATE_GENERATOR_H #include "theory/quantifiers_engine.h" +#include "theory/quantifiers/term_database.h" #include "theory/uf/theory_uf_instantiator.h" +#include "theory/rr_inst_match.h" + +using namespace CVC4::theory::quantifiers; namespace CVC4 { namespace theory { +namespace eq { + +namespace rrinst{ +typedef CVC4::theory::rrinst::CandidateGenerator CandidateGenerator; + +//New CandidateGenerator. They have a simpler semantic than the old one + +// Just iterate amoung the equivalence classes +// node::Null() must be given to reset +class CandidateGeneratorTheoryEeClasses : public CandidateGenerator{ +private: + //the equality classes iterator + eq::EqClassesIterator d_eq; + //equalityengine pointer + EqualityEngine* d_ee; +public: + CandidateGeneratorTheoryEeClasses( EqualityEngine * ee): d_ee( ee ){} + ~CandidateGeneratorTheoryEeClasses(){} + void resetInstantiationRound(){}; + void reset( TNode eqc ){ + Assert(eqc.isNull()); + d_eq = eq::EqClassesIterator( d_ee ); + }; //* the argument is not used + TNode getNextCandidate(){ + if( !d_eq.isFinished() ) return (*(d_eq++)); + else return Node::null(); + }; +}; + +// Just iterate amoung the equivalence class of the given node +// node::Null() *can't* be given to reset +class CandidateGeneratorTheoryEeClass : public CandidateGenerator{ +private: + //instantiator pointer + EqualityEngine* d_ee; + //the equality class iterator + eq::EqClassIterator d_eqc; + /* For the case where the given term doesn't exists in uf */ + Node d_retNode; +public: + CandidateGeneratorTheoryEeClass( EqualityEngine* ee): d_ee( ee ){} + ~CandidateGeneratorTheoryEeClass(){} + void resetInstantiationRound(){}; + void reset( TNode eqc ){ + Assert(!eqc.isNull()); + if( d_ee->hasTerm( eqc ) ){ + /* eqc is in uf */ + eqc = d_ee->getRepresentative( eqc ); + d_eqc = eq::EqClassIterator( eqc, d_ee ); + d_retNode = Node::null(); + }else{ + /* If eqc if not a term known by uf, it is the only one in its + equivalence class. So we will return only it */ + d_retNode = eqc; + d_eqc = eq::EqClassIterator(); + } + }; //* the argument is not used + TNode getNextCandidate(){ + if(d_retNode.isNull()){ + if( !d_eqc.isFinished() ) return (*(d_eqc++)); + else return Node::null(); + }else{ + /* the case where eqc not in uf */ + Node ret = d_retNode; + d_retNode = Node::null(); /* d_eqc.isFinished() must be true */ + return ret; + } + }; +}; + + +} /* namespace rrinst */ +} /* namespace eq */ + namespace uf { +namespace rrinst { + +typedef CVC4::theory::rrinst::CandidateGenerator CandidateGenerator; + +class CandidateGeneratorTheoryUfOp : public CandidateGenerator{ +private: + Node d_op; + //instantiator pointer + TermDb* d_tdb; + // Since new term can appears we restrict ourself to the one that + // exists at resetInstantiationRound + size_t d_term_iter_limit; + size_t d_term_iter; +public: + CandidateGeneratorTheoryUfOp(Node op, TermDb* tdb): d_op(op), d_tdb( tdb ){} + ~CandidateGeneratorTheoryUfOp(){} + void resetInstantiationRound(){ + d_term_iter_limit = d_tdb->d_op_map[d_op].size(); + }; + void reset( TNode eqc ){ + Assert(eqc.isNull()); + d_term_iter = 0; + }; //* the argument is not used + TNode getNextCandidate(){ + if( d_term_iter<d_term_iter_limit ){ + TNode n = d_tdb->d_op_map[d_op][d_term_iter]; + ++d_term_iter; + return n; + } else return Node::null(); + }; +}; + +class CandidateGeneratorTheoryUfType : public CandidateGenerator{ +private: + TypeNode d_type; + //instantiator pointer + TermDb* d_tdb; + // Since new term can appears we restrict ourself to the one that + // exists at resetInstantiationRound + size_t d_term_iter_limit; + size_t d_term_iter; +public: + CandidateGeneratorTheoryUfType(TypeNode type, TermDb* tdb): d_type(type), d_tdb( tdb ){} + ~CandidateGeneratorTheoryUfType(){} + void resetInstantiationRound(){ + d_term_iter_limit = d_tdb->d_type_map[d_type].size(); + }; + void reset( TNode eqc ){ + Assert(eqc.isNull()); + d_term_iter = 0; + }; //* the argument is not used + TNode getNextCandidate(){ + if( d_term_iter<d_term_iter_limit ){ + TNode n = d_tdb->d_type_map[d_type][d_term_iter]; + ++d_term_iter; + return n; + } else return Node::null(); + }; +}; + +} /* namespace rrinst */ + +namespace inst{ +typedef CVC4::theory::inst::CandidateGenerator CandidateGenerator; + +//Old CandidateGenerator class CandidateGeneratorTheoryUfDisequal; @@ -108,7 +252,8 @@ public: }; -} +}/* CVC4::theory::uf::inst namespace */ +}/* CVC4::theory::uf namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/uf/theory_uf_instantiator.cpp b/src/theory/uf/theory_uf_instantiator.cpp index e3999c163..257bed0a2 100644 --- a/src/theory/uf/theory_uf_instantiator.cpp +++ b/src/theory/uf/theory_uf_instantiator.cpp @@ -17,6 +17,7 @@ #include "theory/uf/theory_uf_instantiator.h" #include "theory/theory_engine.h" #include "theory/uf/theory_uf.h" +#include "theory/uf/theory_uf_candidate_generator.h" #include "theory/uf/equality_engine.h" #include "theory/quantifiers/term_database.h" @@ -26,6 +27,15 @@ using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::uf; +using namespace CVC4::theory::inst; + +namespace CVC4 { +namespace theory { +namespace uf { + +inline std::ostream& operator<<(std::ostream& out, const InstantiatorTheoryUf::Ips& ips) { + return out; +}; EqClassInfo::EqClassInfo( context::Context* c ) : d_funs( c ), d_pfuns( c ), d_disequal( c ){ @@ -33,13 +43,15 @@ EqClassInfo::EqClassInfo( context::Context* c ) : d_funs( c ), d_pfuns( c ), d_d //set member void EqClassInfo::setMember( Node n, quantifiers::TermDb* db ){ - if( n.getKind()==APPLY_UF ){ - d_funs[n.getOperator()] = true; + if( n.hasOperator() ){ + d_funs.insertAtContextLevelZero(n.getOperator(),true); } //add parent functions - for( std::map< Node, std::map< int, std::vector< Node > > >::iterator it = db->d_parents[n].begin(); + for( std::hash_map< Node, std::hash_map< int, std::vector< Node > >, NodeHashFunction >::iterator it = db->d_parents[n].begin(); it != db->d_parents[n].end(); ++it ){ - d_pfuns[ it->first ] = true; + //TODO Is it true to do it at level 0? That depend when SetMember is called + // At worst it is a good overapproximation + d_pfuns.insertAtContextLevelZero( it->first, true); } } @@ -62,6 +74,20 @@ void EqClassInfo::merge( EqClassInfo* eci ){ } } +inline void outputEqClassInfo( const char* c, const EqClassInfo* eci){ + Debug(c) << " funs:"; + for( EqClassInfo::BoolMap::iterator it = eci->d_funs.begin(); it != eci->d_funs.end(); it++ ) { + Debug(c) << (*it).first << ","; + } + Debug(c) << std::endl << "pfuns:"; + for( EqClassInfo::BoolMap::iterator it = eci->d_pfuns.begin(); it != eci->d_pfuns.end(); it++ ) { + Debug(c) << (*it).first << ","; + } + Debug(c) << std::endl; +} + + + InstantiatorTheoryUf::InstantiatorTheoryUf(context::Context* c, CVC4::theory::QuantifiersEngine* qe, Theory* th) : Instantiator( c, qe, th ) { @@ -221,21 +247,92 @@ void InstantiatorTheoryUf::newEqClass( TNode n ){ d_quantEngine->addTermToDatabase( n ); } +void InstantiatorTheoryUf::newTerms(SetNode& s){ + static NoMatchAttribute rewrittenNodeAttribute; + /* op -> nodes (if the set is empty, the op is not interesting) */ + std::hash_map< TNode, SetNode, TNodeHashFunction > h; + /* types -> nodes (if the set is empty, the type is not interesting) */ + std::hash_map< TypeNode, SetNode, TypeNodeHashFunction > tyh; + for(SetNode::iterator i=s.begin(), end=s.end(); i != end; ++i){ + if (i->getAttribute(rewrittenNodeAttribute)) continue; /* skip it */ + if( !d_cand_gens.empty() ){ + // op + TNode op = i->getOperator(); + std::hash_map< TNode, SetNode, TNodeHashFunction >::iterator + is = h.find(op); + if(is == h.end()){ + std::pair<std::hash_map< TNode, SetNode, TNodeHashFunction >::iterator,bool> + p = h.insert(make_pair(op,SetNode())); + is = p.first; + if(d_cand_gens.find(op) != d_cand_gens.end()){ + is->second.insert(*i); + } /* else we have inserted an empty set */ + }else if(!is->second.empty()){ + is->second.insert(*i); + } + } + if( !d_cand_gen_types.empty() ){ + //type + TypeNode ty = i->getType(); + std::hash_map< TypeNode, SetNode, TypeNodeHashFunction >::iterator + is = tyh.find(ty); + if(is == tyh.end()){ + std::pair<std::hash_map< TypeNode, SetNode, TypeNodeHashFunction >::iterator,bool> + p = tyh.insert(make_pair(ty,SetNode())); + is = p.first; + if(d_cand_gen_types.find(ty) != d_cand_gen_types.end()){ + is->second.insert(*i); + } /* else we have inserted an empty set */ + }else if(!is->second.empty()){ + is->second.insert(*i); + } + } + } + //op + for(std::hash_map< TNode, SetNode, TNodeHashFunction >::iterator i=h.begin(), end=h.end(); + i != end; ++i){ + //new term, add n to candidate generators + if(i->second.empty()) continue; + std::map< Node, NodeNewTermDispatcher >::iterator + inpc = d_cand_gens.find(i->first); + //we know that this op exists + Assert(inpc != d_cand_gens.end()); + inpc->second.send(i->second); + } + //type + for(std::hash_map< TypeNode, SetNode, TypeNodeHashFunction >::iterator i=tyh.begin(), end=tyh.end(); + i != end; ++i){ + //new term, add n to candidate generators + if(i->second.empty()) continue; + std::map< TypeNode, NodeNewTermDispatcher >::iterator + inpc = d_cand_gen_types.find(i->first); + //we know that this op exists + Assert(inpc != d_cand_gen_types.end()); + inpc->second.send(i->second); + } + +} + + /** merge */ void InstantiatorTheoryUf::merge( TNode a, TNode b ){ if( Options::current()->efficientEMatching ){ + //merge eqc_ops of b into a + EqClassInfo* eci_a = getOrCreateEquivalenceClassInfo( a ); + EqClassInfo* eci_b = getOrCreateEquivalenceClassInfo( b ); + if( a.getKind()!=IFF && a.getKind()!=EQUAL && b.getKind()!=IFF && b.getKind()!=EQUAL ){ Debug("efficient-e-match") << "Merging " << a << " with " << b << std::endl; //determine new candidates for instantiation - computeCandidatesPcPairs( a, b ); - computeCandidatesPcPairs( b, a ); - computeCandidatesPpPairs( a, b ); - computeCandidatesPpPairs( b, a ); + computeCandidatesPcPairs( a, eci_a, b, eci_b ); + computeCandidatesPcPairs( b, eci_b, a, eci_a ); + computeCandidatesPpPairs( a, eci_a, b, eci_b ); + computeCandidatesPpPairs( b, eci_b, a, eci_a ); } - //merge eqc_ops of b into a - EqClassInfo* eci_a = getOrCreateEquivalenceClassInfo( a ); - EqClassInfo* eci_b = getOrCreateEquivalenceClassInfo( b ); + computeCandidatesConstants( a, eci_a, b, eci_b); + computeCandidatesConstants( b, eci_b, a, eci_a); + eci_a->merge( eci_b ); } } @@ -258,97 +355,99 @@ EqClassInfo* InstantiatorTheoryUf::getOrCreateEquivalenceClassInfo( Node n ){ return d_eqc_ops[n]; } -void InstantiatorTheoryUf::computeCandidatesPcPairs( Node a, Node b ){ +void InstantiatorTheoryUf::computeCandidatesPcPairs( Node a, EqClassInfo* eci_a, Node b, EqClassInfo* eci_b ){ Debug("efficient-e-match") << "Compute candidates for pc pairs..." << std::endl; Debug("efficient-e-match") << " Eq class = ["; outputEqClass( "efficient-e-match", a); Debug("efficient-e-match") << "]" << std::endl; - EqClassInfo* eci_a = getOrCreateEquivalenceClassInfo( a ); - EqClassInfo* eci_b = getOrCreateEquivalenceClassInfo( a ); + outputEqClassInfo("efficient-e-match",eci_a); for( BoolMap::iterator it = eci_a->d_funs.begin(); it != eci_a->d_funs.end(); it++ ) { //the child function: a member of eq_class( a ) has top symbol g, in other words g is in funs( a ) Node g = (*it).first; Debug("efficient-e-match") << " Checking application " << g << std::endl; //look at all parent/child pairs - for( std::map< Node, std::map< Node, std::vector< InvertedPathString > > >::iterator itf = d_pc_pairs[g].begin(); + for( std::map< Node, std::vector< std::pair< NodePcDispatcher*, Ips > > >::iterator itf = d_pc_pairs[g].begin(); itf != d_pc_pairs[g].end(); ++itf ){ //f/g is a parent/child pair Node f = itf->first; - if( eci_b->hasParent( f ) || true ){ + if( eci_b->hasParent( f ) ){ //DO_THIS: determine if f in pfuns( b ), only do the follow if so Debug("efficient-e-match") << " Checking parent application " << f << std::endl; //scan through the list of inverted path strings/candidate generators - for( std::map< Node, std::vector< InvertedPathString > >::iterator cit = itf->second.begin(); - cit != itf->second.end(); ++cit ){ - Node pat = cit->first; - Debug("efficient-e-match") << " Checking pattern " << pat << std::endl; - for( int c=0; c<(int)cit->second.size(); c++ ){ - Debug("efficient-e-match") << " Check inverted path string for pattern "; - outputInvertedPathString( "efficient-e-match", cit->second[c] ); - Debug("efficient-e-match") << std::endl; - - //collect all new relevant terms - std::vector< Node > terms; - terms.push_back( b ); - collectTermsIps( cit->second[c], terms ); - if( !terms.empty() ){ - Debug("efficient-e-match") << " -> Added terms (" << (int)terms.size() << "): "; - //add them as candidates to the candidate generator - for( int t=0; t<(int)terms.size(); t++ ){ - Debug("efficient-e-match") << terms[t] << " "; - //Notice() << "Add candidate (PC) " << terms[t] << std::endl; - for( int cg=0; cg<(int)d_pat_cand_gens[pat].size(); cg++ ){ - d_pat_cand_gens[pat][cg]->addCandidate( terms[t] ); - } - } - Debug("efficient-e-match") << std::endl; - } + for( std::vector< std::pair< NodePcDispatcher*, Ips > >::iterator cit = itf->second.begin(); + cit != itf->second.end(); ++cit ){ +#ifdef CVC4_DEBUG + Debug("efficient-e-match") << " Checking pattern " << cit->first->pat << std::endl; +#endif + Debug("efficient-e-match") << " Check inverted path string for pattern "; + outputIps( "efficient-e-match", cit->second ); + Debug("efficient-e-match") << std::endl; + + //collect all new relevant terms + SetNode terms; + terms.insert( b ); + collectTermsIps( cit->second, terms ); + if( terms.empty() ) continue; + Debug("efficient-e-match") << " -> Added terms (" << terms.size() << "): "; + for( SetNode::const_iterator t=terms.begin(), end=terms.end(); + t!=end; ++t ){ + Debug("efficient-e-match") << (*t) << " "; } + Debug("efficient-e-match") << std::endl; + //add them as candidates to the candidate generator + cit->first->send(terms); } } } } } -void InstantiatorTheoryUf::computeCandidatesPpPairs( Node a, Node b ){ +void InstantiatorTheoryUf::computeCandidatesPpPairs( Node a, EqClassInfo* eci_a, Node b, EqClassInfo* eci_b ){ Debug("efficient-e-match") << "Compute candidates for pp pairs..." << std::endl; - EqClassInfo* eci_a = getOrCreateEquivalenceClassInfo( a ); - EqClassInfo* eci_b = getOrCreateEquivalenceClassInfo( a ); - for( std::map< Node, std::map< Node, std::map< Node, std::vector< IpsPair > > > >::iterator it = d_pp_pairs.begin(); + for( std::map< Node, std::map< Node, std::vector< triple< NodePpDispatcher*, Ips, Ips > > > >::iterator it = d_pp_pairs.begin(); it != d_pp_pairs.end(); ++it ){ Node f = it->first; if( eci_a->hasParent( f ) ){ Debug("efficient-e-match") << " Checking parent application " << f << std::endl; - for( std::map< Node, std::map< Node, std::vector< IpsPair > > >::iterator it2 = it->second.begin(); + for( std::map< Node, std::vector< triple<NodePpDispatcher*, Ips, Ips> > >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ Node g = it2->first; if( eci_b->hasParent( g ) ){ Debug("efficient-e-match") << " Checking parent application " << g << std::endl; //if f in pfuns( a ) and g is in pfuns( b ), only do the follow if so - for( std::map< Node, std::vector< IpsPair > >::iterator cit = it2->second.begin(); + for( std::vector< triple<NodePpDispatcher*, Ips, Ips> > ::iterator cit = it2->second.begin(); cit != it2->second.end(); ++cit ){ - Node pat = cit->first; - for( int c=0; c<(int)cit->second.size(); c++ ){ - std::vector< Node > a_terms; - a_terms.push_back( a ); - if( !a_terms.empty() ){ - collectTermsIps( cit->second[c].first, a_terms ); - std::vector< Node > b_terms; - b_terms.push_back( b ); - collectTermsIps( cit->second[c].first, b_terms ); - //take intersection - for( int t=0; t<(int)a_terms.size(); t++ ){ - if( std::find( b_terms.begin(), b_terms.end(), a_terms[t] )!=b_terms.end() ){ - //Notice() << "Add candidate (PP) " << a_terms[t] << std::endl; - Debug("efficient-e-match") << " -> Add term " << a_terms[t] << std::endl; - //add to all candidate generators having this term - for( int cg=0; cg<(int)d_pat_cand_gens[pat].size(); cg++ ){ - d_pat_cand_gens[pat][cg]->addCandidate( a_terms[t] ); - } - } - } - } +#ifdef CVC4_DEBUG + Debug("efficient-e-match") << " Checking pattern " << cit->first->pat1 << " and " << cit->first->pat2 << std::endl; +#endif + Debug("efficient-e-match") << " Check inverted path string "; + outputIps( "efficient-e-match", cit->second ); + SetNode a_terms; + a_terms.insert( a ); + collectTermsIps( cit->second, a_terms ); + if( a_terms.empty() ) continue; + Debug("efficient-e-match") << " And check inverted path string "; + outputIps( "efficient-e-match", cit->third ); + SetNode b_terms; + b_terms.insert( b ); + collectTermsIps( cit->third, b_terms ); + if( b_terms.empty() ) continue; + //Start debug + Debug("efficient-e-match") << " -> Possibly Added termsA (" << a_terms.size() << "): "; + for( SetNode::const_iterator t=a_terms.begin(), end=a_terms.end(); + t!=end; ++t ){ + Debug("efficient-e-match") << (*t) << " "; + } + Debug("efficient-e-match") << std::endl; + Debug("efficient-e-match") << " -> Possibly Added termsB (" << b_terms.size() << "): "; + for( SetNode::const_iterator t=b_terms.begin(), end=b_terms.end(); + t!=end; ++t ){ + Debug("efficient-e-match") << (*t) << " "; } + Debug("efficient-e-match") << std::endl; + //End debug + + cit->first->send(a_terms,b_terms); } } } @@ -356,39 +455,87 @@ void InstantiatorTheoryUf::computeCandidatesPpPairs( Node a, Node b ){ } } -void InstantiatorTheoryUf::collectTermsIps( InvertedPathString& ips, std::vector< Node >& terms, int index ){ - if( index<(int)ips.size() && !terms.empty() ){ + +void InstantiatorTheoryUf::computeCandidatesConstants( Node a, EqClassInfo* eci_a, Node b, EqClassInfo* eci_b ){ + Debug("efficient-e-match") << "Compute candidates constants for cc pairs..." << std::endl; + Debug("efficient-e-match") << " Eq class = ["; + outputEqClass( "efficient-e-match", a); + Debug("efficient-e-match") << "]" << std::endl; + outputEqClassInfo("efficient-e-match",eci_a); + for( std::map< Node, std::map< Node, NodePcDispatcher* > >::iterator + it = d_cc_pairs.begin(), end = d_cc_pairs.end(); + it != end; ++it ) { + Debug("efficient-e-match") << " Checking application " << it->first << std::endl; + if( !eci_b->hasFunction(it->first) ) continue; + for( std::map< Node, NodePcDispatcher* >::iterator + itc = it->second.begin(), end = it->second.end(); + itc != end; ++itc ) { + //The constant + Debug("efficient-e-match") << " Checking constant " << a << std::endl; + if(getRepresentative(itc->first) != a) continue; + SetNode s; + eq::EqClassIterator eqc_iter( b, &((TheoryUF*)d_th)->d_equalityEngine ); + while( !eqc_iter.isFinished() ){ + Debug("efficient-e-match-debug") << "> look at " << (*eqc_iter) + << std::endl; + if( (*eqc_iter).hasOperator() && (*eqc_iter).getOperator() == it->first ) s.insert(*eqc_iter); + eqc_iter++; + } + + if( s.empty() ) continue; + Debug("efficient-e-match") << " -> Added terms (" << s.size() << "): "; + for( SetNode::const_iterator t=s.begin(), end=s.end(); + t!=end; ++t ){ + Debug("efficient-e-match") << (*t) << " "; + } + Debug("efficient-e-match") << std::endl; + itc->second->send(s); + } + } +} + +void InstantiatorTheoryUf::collectTermsIps( Ips& ips, SetNode & terms ){ + Assert( ips.size() > 0); + return collectTermsIps( ips, terms, ips.size() - 1); +} + +void InstantiatorTheoryUf::collectTermsIps( Ips& ips, SetNode& terms, int index ){ + if( !terms.empty() ){ Debug("efficient-e-match-debug") << "> Process " << index << std::endl; Node f = ips[index].first; int arg = ips[index].second; //for each term in terms, determine if any term (modulo equality) has parent "f" from position "arg" - bool addRep = ( index!=(int)ips.size()-1 ); - std::vector< Node > newTerms; - for( int t=0; t<(int)terms.size(); t++ ){ - collectParentsTermsIps( terms[t], f, arg, newTerms, addRep ); + bool addRep = ( index!=0 ); // We want to keep the top symbol for the last + SetNode newTerms; + for( SetNode::const_iterator t=terms.begin(), end=terms.end(); + t!=end; ++t ){ + collectParentsTermsIps( *t, f, arg, newTerms, addRep ); } - terms.clear(); - terms.insert( terms.begin(), newTerms.begin(), newTerms.end() ); + terms.swap(newTerms); Debug("efficient-e-match-debug") << "> Terms are now: "; - for( int t=0; t<(int)terms.size(); t++ ){ - Debug("efficient-e-match-debug") << terms[t] << " "; + for( SetNode::const_iterator t=terms.begin(), end=terms.end(); + t!=end; ++t ){ + Debug("efficient-e-match-debug") << *t << " "; } Debug("efficient-e-match-debug") << std::endl; - collectTermsIps( ips, terms, index+1 ); + if(index!=0) collectTermsIps( ips, terms, index-1 ); } } -bool InstantiatorTheoryUf::collectParentsTermsIps( Node n, Node f, int arg, std::vector< Node >& terms, bool addRep, bool modEq ){ +bool InstantiatorTheoryUf::collectParentsTermsIps( Node n, Node f, int arg, SetNode & terms, bool addRep, bool modEq ){ //modEq default true bool addedTerm = false; - if( ((TheoryUF*)d_th)->d_equalityEngine.hasTerm( n ) && modEq ){ + + if( modEq && ((TheoryUF*)d_th)->d_equalityEngine.hasTerm( n )){ Assert( getRepresentative( n )==n ); //collect modulo equality //DO_THIS: this should (if necessary) compute a current set of (f, arg) parents for n and cache it - eq::EqClassIterator eqc_iter( getRepresentative( n ), &((TheoryUF*)d_th)->d_equalityEngine ); + eq::EqClassIterator eqc_iter( n, &((TheoryUF*)d_th)->d_equalityEngine ); while( !eqc_iter.isFinished() ){ + Debug("efficient-e-match-debug") << "> look at " << (*eqc_iter) + << std::endl; if( collectParentsTermsIps( (*eqc_iter), f, arg, terms, addRep, false ) ){ //if only one argument, we know we can stop (since all others added will be congruent) if( f.getType().getNumChildren()==2 ){ @@ -401,90 +548,263 @@ bool InstantiatorTheoryUf::collectParentsTermsIps( Node n, Node f, int arg, std: }else{ quantifiers::TermDb* db = d_quantEngine->getTermDatabase(); //see if parent f exists from argument arg - if( db->d_parents.find( n )!=db->d_parents.end() ){ - if( db->d_parents[n].find( f )!=db->d_parents[n].end() ){ - if( db->d_parents[n][f].find( arg )!=db->d_parents[n][f].end() ){ - for( int i=0; i<(int)db->d_parents[n][f][arg].size(); i++ ){ - Node t = db->d_parents[n][f][arg][i]; - if( addRep ){ - t = getRepresentative( t ); - } - if( std::find( terms.begin(), terms.end(), t )==terms.end() ){ - terms.push_back( t ); - } - addedTerm = true; - } - } - } + const std::vector<Node> & parents = db->getParents(n,f,arg); + for( size_t i=0; i<parents.size(); ++i ){ + TNode t = parents[i]; + if(!CandidateGenerator::isLegalCandidate(t)) continue; + if( addRep ) t = getRepresentative( t ); + terms.insert(t); + addedTerm = true; } } return addedTerm; } -void InstantiatorTheoryUf::registerPatternElementPairs2( Node opat, Node pat, InvertedPathString& ips, - std::map< Node, std::vector< std::pair< Node, InvertedPathString > > >& ips_map ){ - Assert( pat.getKind()==APPLY_UF ); +void InstantiatorTheoryUf::registerPatternElementPairs2( Node pat, Ips& ips, PpIpsMap & pp_ips_map, NodePcDispatcher* npc ){ + Assert( pat.hasOperator() ); //add information for possible pp-pair + ips.push_back( std::pair< Node, int >( pat.getOperator(), 0 ) ); //0 is just a dumb value + for( int i=0; i<(int)pat.getNumChildren(); i++ ){ if( pat[i].getKind()==INST_CONSTANT ){ - ips_map[ pat[i] ].push_back( std::pair< Node, InvertedPathString >( pat.getOperator(), InvertedPathString( ips ) ) ); + ips.back().second = i; + pp_ips_map[ pat[i] ].push_back( make_pair( pat.getOperator(), Ips( ips ) ) ); } } - ips.push_back( std::pair< Node, int >( pat.getOperator(), 0 ) ); + for( int i=0; i<(int)pat.getNumChildren(); i++ ){ if( pat[i].getKind()==APPLY_UF ){ ips.back().second = i; - registerPatternElementPairs2( opat, pat[i], ips, ips_map ); + registerPatternElementPairs2( pat[i], ips, pp_ips_map, npc ); Debug("pattern-element-opt") << "Found pc-pair ( " << pat.getOperator() << ", " << pat[i].getOperator() << " )" << std::endl; Debug("pattern-element-opt") << " Path = "; - outputInvertedPathString( "pattern-element-opt", ips ); + outputIps( "pattern-element-opt", ips ); Debug("pattern-element-opt") << std::endl; //pat.getOperator() and pat[i].getOperator() are a pc-pair - d_pc_pairs[ pat[i].getOperator() ][ pat.getOperator() ][opat].push_back( InvertedPathString( ips ) ); + d_pc_pairs[ pat[i].getOperator() ][ pat.getOperator() ] + .push_back( make_pair(npc,Ips(ips)) ); } } ips.pop_back(); } -void InstantiatorTheoryUf::registerPatternElementPairs( Node pat ){ - InvertedPathString ips; - std::map< Node, std::vector< std::pair< Node, InvertedPathString > > > ips_map; - registerPatternElementPairs2( pat, pat, ips, ips_map ); - for( std::map< Node, std::vector< std::pair< Node, InvertedPathString > > >::iterator it = ips_map.begin(); it != ips_map.end(); ++it ){ - for( int j=0; j<(int)it->second.size(); j++ ){ - for( int k=j+1; k<(int)it->second.size(); k++ ){ +void InstantiatorTheoryUf::registerPatternElementPairs( Node pat, PpIpsMap & pp_ips_map, + NodePcDispatcher* npc, + NodePpDispatcher* npp){ + Ips ips; + registerPatternElementPairs2( pat, ips, pp_ips_map, npc ); + for( PpIpsMap::iterator it = pp_ips_map.begin(); it != pp_ips_map.end(); ++it ){ + // for each variable construct all the pp-pair + for( size_t j=0; j<it->second.size(); j++ ){ + for( size_t k=j+1; k<it->second.size(); k++ ){ //found a pp-pair Debug("pattern-element-opt") << "Found pp-pair ( " << it->second[j].first << ", " << it->second[k].first << " )" << std::endl; Debug("pattern-element-opt") << " Paths = "; - outputInvertedPathString( "pattern-element-opt", it->second[j].second ); + outputIps( "pattern-element-opt", it->second[j].second ); Debug("pattern-element-opt") << " and "; - outputInvertedPathString( "pattern-element-opt", it->second[k].second ); + outputIps( "pattern-element-opt", it->second[k].second ); Debug("pattern-element-opt") << std::endl; - d_pp_pairs[ it->second[j].first ][ it->second[k].first ][pat].push_back( IpsPair( it->second[j].second, it->second[k].second ) ); + d_pp_pairs[ it->second[j].first ][ it->second[k].first ] + .push_back( make_triple( npp, it->second[j].second, it->second[k].second )); } } } +}; + +void findPpSite(Node pat, InstantiatorTheoryUf::Ips& ips, InstantiatorTheoryUf::PpIpsMap & pp_ips_map){ + Assert( pat.getKind()==APPLY_UF ); + //add information for possible pp-pair + + ips.push_back( make_pair( pat.getOperator(), 0) ); + for( size_t i=0; i<pat.getNumChildren(); i++ ){ + if( pat[i].getKind()==INST_CONSTANT ){ + ips.back().second = i; + pp_ips_map[ pat[i] ].push_back( make_pair( pat.getOperator(), InstantiatorTheoryUf::Ips( ips ) ) ); + } + } + + for( size_t i=0; i<pat.getNumChildren(); i++ ){ + if( pat[i].getKind()==APPLY_UF ){ + ips.back().second = i; + findPpSite( pat[i], ips, pp_ips_map ); + } + } + ips.pop_back(); } -void InstantiatorTheoryUf::registerCandidateGenerator( CandidateGenerator* cg, Node pat ){ - Debug("efficient-e-match") << "Register candidate generator..." << pat << std::endl; - if( d_pat_cand_gens.find( pat )==d_pat_cand_gens.end() ){ - registerPatternElementPairs( pat ); +void InstantiatorTheoryUf::combineMultiPpIpsMap(PpIpsMap & pp_ips_map, MultiPpIpsMap & multi_pp_ips_map, + EfficientHandler& eh, size_t index2,const std::vector<Node> & pats){ + hash_map<size_t,NodePpDispatcher*> npps; + for( PpIpsMap::iterator it = pp_ips_map.begin(); it != pp_ips_map.end(); ++it ){ + MultiPpIpsMap::iterator mit = multi_pp_ips_map.find(it->first); + if(mit == multi_pp_ips_map.end()) continue; + // for each variable construct all the pp-pair + // j the last pattern treated + for( std::vector< std::pair< Node, Ips > >::iterator j=it->second.begin(), jend = it->second.end() ; + j != jend; ++j){ + // k one of the previous one + for( std::vector< triple< size_t, Node, Ips > >::iterator k=mit->second.begin(), kend = mit->second.end() ; + k != kend; ++k){ + //found a pp-pair + Debug("pattern-element-opt") << "Found multi-pp-pair ( " << j->first + << ", " << k->second << " in "<< k->first + << " )" << std::endl; + Debug("pattern-element-opt") << " Paths = "; + outputIps( "pattern-element-opt", j->second ); + Debug("pattern-element-opt") << " and "; + outputIps( "pattern-element-opt", k->third ); + Debug("pattern-element-opt") << std::endl; + NodePpDispatcher* dispatcher; + hash_map<size_t,NodePpDispatcher*>::iterator inpp = npps.find(k->first); + if( inpp != npps.end() ) dispatcher = inpp->second; + else{ + dispatcher = new NodePpDispatcher(); +#ifdef CVC4_DEBUG + dispatcher->pat1 = pats[index2]; + dispatcher->pat2 = pats[k->first]; +#endif + dispatcher->addPpDispatcher(&eh,index2,k->first); + }; + d_pp_pairs[ j->first ][ k->second ].push_back( make_triple( dispatcher, j->second, k->third )); + } + } } - d_pat_cand_gens[pat].push_back( cg ); - //take all terms from the uf term db and add to candidate generator - Node op = pat.getOperator(); - quantifiers::TermDb* db = d_quantEngine->getTermDatabase(); - for( int i=0; i<(int)db->d_op_map[op].size(); i++ ){ - cg->addCandidate( db->d_op_map[op][i] ); + /** Put pp_ips_map to multi_pp_ips_map */ + for( PpIpsMap::iterator it = pp_ips_map.begin(); it != pp_ips_map.end(); ++it ){ + for( std::vector< std::pair< Node, Ips > >::iterator j=it->second.begin(), jend = it->second.end() ; + j != jend; ++j){ + multi_pp_ips_map[it->first].push_back(make_triple(index2, j->first, j->second)); + } + } + +} + + +void InstantiatorTheoryUf::registerEfficientHandler( EfficientHandler& handler, + const std::vector< Node > & pats ){ + Assert(pats.size() > 0); + + MultiPpIpsMap multi_pp_ips_map; + PpIpsMap pp_ips_map; + //In a multi-pattern Pattern that is only a variable are specials, + //if the variable appears in another pattern, it can be discarded. + //Otherwise new term of this term can be candidate. So we stock them + //here before adding them. + std::vector< size_t > patVars; + + Debug("pattern-element-opt") << "Register patterns" << pats << std::endl; + for(size_t i = 0; i < pats.size(); ++i){ + if( pats[i].getKind() == kind::INST_CONSTANT){ + patVars.push_back(i); + continue; + } + //to complete + if( pats[i].getKind() == kind::NOT && pats[i][0].getKind() == kind::EQUAL){ + Node cst = NodeManager::currentNM()->mkConst<bool>(false); + TNode op = pats[i][0].getOperator(); + if(d_cc_pairs[op][cst] == NULL){ + d_cc_pairs[op][cst] = new NodePcDispatcher(); + } + d_cc_pairs[op][cst]->addPcDispatcher(&handler,i); + continue; + } + //end to complete + Debug("pattern-element-opt") << " Register candidate generator..." << pats[i] << std::endl; + /* Has the pattern already been seen */ + if( d_pat_cand_gens.find( pats[i] )==d_pat_cand_gens.end() ){ + NodePcDispatcher* npc = new NodePcDispatcher(); + NodePpDispatcher* npp = new NodePpDispatcher(); +#ifdef CVC4_DEBUG + npc->pat = pats[i]; + npp->pat1 = pats[i]; + npp->pat2 = pats[i]; +#endif + d_pat_cand_gens[pats[i]] = make_pair(npc,npp); + registerPatternElementPairs( pats[i], pp_ips_map, npc, npp ); + }else{ + Ips ips; + findPpSite(pats[i],ips,pp_ips_map); + } + //Has the top operator already been seen */ + TNode op = pats[i].getOperator(); + d_pat_cand_gens[pats[i]].first->addPcDispatcher(&handler,i); + d_pat_cand_gens[pats[i]].second->addPpDispatcher(&handler,i,i); + d_cand_gens[op].addNewTermDispatcher(&handler,i); + + combineMultiPpIpsMap(pp_ips_map,multi_pp_ips_map,handler,i,pats); + + pp_ips_map.clear(); + } + + for(size_t i = 0; i < patVars.size(); ++i){ + TNode var = pats[patVars[i]]; + Assert( var.getKind() == kind::INST_CONSTANT ); + if( multi_pp_ips_map.find(var) != multi_pp_ips_map.end() ){ + //The variable appear in another pattern, skip it + continue; + }; + d_cand_gen_types[var.getType()].addNewTermDispatcher(&handler,patVars[i]); } - d_cand_gens[op].push_back( cg ); + //take all terms from the uf term db and add to candidate generator + if( pats[0].getKind() == kind::INST_CONSTANT ){ + TypeNode ty = pats[0].getType(); + rrinst::CandidateGenerator* cg = d_quantEngine->getRRCanGenClasses(ty); + cg->reset(Node::null()); + TNode c; + SetNode ele; + while( !(c = cg->getNextCandidate()).isNull() ){ + 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; + } + handler.addMonoCandidate(ele, 0); + } + + } else if( pats[0].getKind() == kind::NOT && pats[0][0].getKind() == kind::EQUAL){ + Node cst = NodeManager::currentNM()->mkConst<bool>(false); + TNode op = pats[0][0].getOperator(); + cst = getRepresentative(cst); + SetNode ele; + eq::EqClassIterator eqc_iter( cst, &((TheoryUF*)d_th)->d_equalityEngine ); + while( !eqc_iter.isFinished() ){ + Debug("efficient-e-match-debug") << "> look at " << (*eqc_iter) + << std::endl; + if( (*eqc_iter).hasOperator() && (*eqc_iter).getOperator() == op ) ele.insert(*eqc_iter); + eqc_iter++; + } + if( !ele.empty() ){ + if(Debug.isOn("efficient-e-match-stats")){ + Debug("efficient-e-match-stats") << "pattern " << pats << " initialized with " << ele.size() << " terms"<< std::endl; + } + handler.addMonoCandidate(ele, 0); + } + + } else { + Node op = pats[0].getOperator(); + TermDb* db = d_quantEngine->getTermDatabase(); + 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; + } + handler.addMonoCandidate(ele, 0); + } + } Debug("efficient-e-match") << "Done." << std::endl; } -void InstantiatorTheoryUf::registerTrigger( Trigger* tr, Node op ){ +void InstantiatorTheoryUf::registerTrigger( theory::inst::Trigger* tr, Node op ){ if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){ d_op_triggers[op].push_back( tr ); } @@ -506,9 +826,28 @@ void InstantiatorTheoryUf::outputEqClass( const char* c, Node n ){ } } -void InstantiatorTheoryUf::outputInvertedPathString( const char* c, InvertedPathString& ips ){ +void InstantiatorTheoryUf::outputIps( const char* c, Ips& ips ){ for( int i=0; i<(int)ips.size(); i++ ){ if( i>0 ){ Debug( c ) << "."; } Debug( c ) << ips[i].first << "." << ips[i].second; } } + +rrinst::CandidateGenerator* InstantiatorTheoryUf::getRRCanGenClasses(){ + uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(getTheory()); + eq::EqualityEngine* ee = + static_cast<eq::EqualityEngine*>(uf->getEqualityEngine()); + return new eq::rrinst::CandidateGeneratorTheoryEeClasses(ee); +} + +rrinst::CandidateGenerator* InstantiatorTheoryUf::getRRCanGenClass(){ + uf::TheoryUF* uf = static_cast<uf::TheoryUF*>(getTheory()); + eq::EqualityEngine* ee = + static_cast<eq::EqualityEngine*>(uf->getEqualityEngine()); + return new eq::rrinst::CandidateGeneratorTheoryEeClass(ee); +} + + +} /* namespace uf */ +} /* namespace theory */ +} /* namespace cvc4 */ diff --git a/src/theory/uf/theory_uf_instantiator.h b/src/theory/uf/theory_uf_instantiator.h index 4ddc01986..3a2a5cc0e 100644 --- a/src/theory/uf/theory_uf_instantiator.h +++ b/src/theory/uf/theory_uf_instantiator.h @@ -27,6 +27,9 @@ #include "util/stats.h" #include "theory/uf/theory_uf.h" +#include "theory/trigger.h" +#include "util/ntuple.h" +#include "context/cdqueue.h" namespace CVC4 { namespace theory { @@ -38,6 +41,300 @@ namespace quantifiers{ namespace uf { class InstantiatorTheoryUf; +class HandlerPcDispatcher; +class HandlerPpDispatcher; + +typedef std::set<Node> SetNode; + +template<class T> +class CleanUpPointer{ +public: + inline void operator()(T** e){ + delete(*e); + }; +}; + +class EfficientHandler{ +public: + typedef std::pair< Node, size_t > MonoCandidate; + typedef std::pair< MonoCandidate, MonoCandidate > MultiCandidate; + typedef std::pair< SetNode, size_t > MonoCandidates; + typedef std::pair< MonoCandidates, MonoCandidates > MultiCandidates; +private: + /* Queue of candidates */ + typedef context::CDQueue< MonoCandidates *, CleanUpPointer<MonoCandidates> > MonoCandidatesQueue; + typedef context::CDQueue< MultiCandidates *, CleanUpPointer<MultiCandidates> > MultiCandidatesQueue; + MonoCandidatesQueue d_monoCandidates; + typedef uf::SetNode::iterator SetNodeIter; + context::CDO<SetNodeIter> d_si; + context::CDO<bool> d_mono_not_first; + + MonoCandidatesQueue d_monoCandidatesNewTerm; + context::CDO<SetNodeIter> d_si_new_term; + context::CDO<bool> d_mono_not_first_new_term; + + + MultiCandidatesQueue d_multiCandidates; + context::CDO<SetNodeIter> d_si1; + context::CDO<SetNodeIter> d_si2; + context::CDO<bool> d_multi_not_first; + + + friend class InstantiatorTheoryUf; + friend class HandlerPcDispatcher; + friend class HandlerPpDispatcher; + friend class HandlerNewTermDispatcher; +protected: + void addMonoCandidate(SetNode & s, size_t index){ + Assert(!s.empty()); + d_monoCandidates.push(new MonoCandidates(s,index)); + } + void addMonoCandidateNewTerm(SetNode & s, size_t index){ + Assert(!s.empty()); + d_monoCandidatesNewTerm.push(new MonoCandidates(s,index)); + } + void addMultiCandidate(SetNode & s1, size_t index1, SetNode & s2, size_t index2){ + Assert(!s1.empty() && !s2.empty()); + d_multiCandidates.push(new MultiCandidates(MonoCandidates(s1,index1), + MonoCandidates(s2,index2))); + } +public: + EfficientHandler(context::Context * c): + //false for d_mono_not_first beacause its the default constructor + d_monoCandidates(c), d_si(c), d_mono_not_first(c,false), + d_monoCandidatesNewTerm(c), d_si_new_term(c), + d_mono_not_first_new_term(c,false), + d_multiCandidates(c) , d_si1(c), d_si2(c), d_multi_not_first(c,false) {}; + + bool getNextMonoCandidate(MonoCandidate & candidate){ + if(d_monoCandidates.empty()) return false; + const MonoCandidates * front = d_monoCandidates.front(); + SetNodeIter si_tmp; + if(!d_mono_not_first){ + Assert(front->first.begin() != front->first.end()); + d_mono_not_first = true; + si_tmp=front->first.begin(); + }else{ + si_tmp = d_si; + ++si_tmp; + }; + if(si_tmp != front->first.end()){ + candidate.first = (*si_tmp); + candidate.second = front->second; + d_si = si_tmp; + Debug("efficienthandler") << "Mono produces " << candidate.first << " for " << candidate.second << std::endl; + return true; + }; + d_monoCandidates.pop(); + d_mono_not_first = false; + return getNextMonoCandidate(candidate); + }; + + bool getNextMonoCandidateNewTerm(MonoCandidate & candidate){ + if(d_monoCandidatesNewTerm.empty()) return false; + const MonoCandidates * front = d_monoCandidatesNewTerm.front(); + SetNodeIter si_tmp; + if(!d_mono_not_first_new_term){ + Assert(front->first.begin() != front->first.end()); + d_mono_not_first_new_term = true; + si_tmp=front->first.begin(); + }else{ + si_tmp = d_si_new_term; + ++si_tmp; + }; + if(si_tmp != front->first.end()){ + candidate.first = (*si_tmp); + candidate.second = front->second; + d_si_new_term = si_tmp; + Debug("efficienthandler") << "Mono produces " << candidate.first << " for " << candidate.second << std::endl; + return true; + }; + d_monoCandidatesNewTerm.pop(); + d_mono_not_first_new_term = false; + return getNextMonoCandidateNewTerm(candidate); + }; + + bool getNextMultiCandidate(MultiCandidate & candidate){ + if(d_multiCandidates.empty()) return false; + const MultiCandidates* front = d_multiCandidates.front(); + SetNodeIter si1_tmp; + SetNodeIter si2_tmp; + if(!d_multi_not_first){ + Assert(front->first.first.begin() != front->first.first.end()); + Assert(front->second.first.begin() != front->second.first.end()); + si1_tmp = front->first.first.begin(); + si2_tmp = front->second.first.begin(); + }else{ + si1_tmp = d_si1; + si2_tmp = d_si2; + ++si2_tmp; + }; + if(si2_tmp != front->second.first.end()){ + candidate.first.first = *si1_tmp; + candidate.first.second = front->first.second; + candidate.second.first = *si2_tmp; + candidate.second.second = front->second.second; + if(!d_multi_not_first){d_si1 = si1_tmp; d_multi_not_first = true; }; + d_si2 = si2_tmp; + Debug("efficienthandler") << "Multi1 produces " + << candidate.first.first << " for " + << candidate.first.second << " and " + << candidate.second.first << " for " + << candidate.second.second << " and " + << std::endl; + return true; + }; // end of the second set + si2_tmp = front->second.first.begin(); + ++si1_tmp; + if(si1_tmp != front->first.first.end()){ + candidate.first.first = *si1_tmp; + candidate.first.second = front->first.second; + candidate.second.first = *si2_tmp; + candidate.second.second = front->second.second; + d_si1 = si1_tmp; + d_si2 = si2_tmp; + Debug("efficienthandler") << "Multi2 produces " + << candidate.first.first << " for " + << candidate.first.second << " and " + << candidate.second.first << " for " + << candidate.second.second << " and " + << std::endl; + return true; + }; // end of the first set + d_multiCandidates.pop(); + d_multi_not_first = false; + return getNextMultiCandidate(candidate); + } +}; + +class PcDispatcher{ +public: + virtual ~PcDispatcher(){}; + /* Send the node to the dispatcher */ + virtual void send(SetNode & s) = 0; +}; + + +class HandlerPcDispatcher: public PcDispatcher{ + EfficientHandler* d_handler; + size_t d_index; +public: + HandlerPcDispatcher(EfficientHandler* handler, size_t index): + d_handler(handler), d_index(index) {}; + void send(SetNode & s){ + d_handler->addMonoCandidate(s,d_index); + } +}; + + +/** All the dispatcher that correspond to this node */ +class NodePcDispatcher: public PcDispatcher{ +#ifdef CVC4_DEBUG +public: + Node pat; +#endif/* CVC4_DEBUG*/ +private: + std::vector<HandlerPcDispatcher> d_dis; +public: + void send(SetNode & s){ + Assert(!s.empty()); + for(std::vector<HandlerPcDispatcher>::iterator i = d_dis.begin(), end = d_dis.end(); + i != end; ++i){ + (*i).send(s); + } + } + void addPcDispatcher(EfficientHandler* handler, size_t index){ + d_dis.push_back(HandlerPcDispatcher(handler,index)); + } +}; + + +class HandlerNewTermDispatcher: public PcDispatcher{ + EfficientHandler* d_handler; + size_t d_index; +public: + HandlerNewTermDispatcher(EfficientHandler* handler, size_t index): + d_handler(handler), d_index(index) {}; + void send(SetNode & s){ + d_handler->addMonoCandidateNewTerm(s,d_index); + } +}; + +/** All the dispatcher that correspond to this node */ +class NodeNewTermDispatcher: public PcDispatcher{ +#ifdef CVC4_DEBUG +public: + Node pat; +#endif/* CVC4_DEBUG*/ +private: + std::vector<HandlerNewTermDispatcher> d_dis; +public: + void send(SetNode & s){ + Assert(!s.empty()); + for(std::vector<HandlerNewTermDispatcher>::iterator i = d_dis.begin(), end = d_dis.end(); + i != end; ++i){ + (*i).send(s); + } + } + void addNewTermDispatcher(EfficientHandler* handler, size_t index){ + d_dis.push_back(HandlerNewTermDispatcher(handler,index)); + } +}; + +class PpDispatcher{ +public: + virtual ~PpDispatcher(){}; + /* Send the node to the dispatcher */ + virtual void send(SetNode & s1, SetNode & s2, SetNode & sinter) = 0; +}; + + +class HandlerPpDispatcher: public PpDispatcher{ + EfficientHandler* d_handler; + size_t d_index1; + size_t d_index2; +public: + HandlerPpDispatcher(EfficientHandler* handler, size_t index1, size_t index2): + d_handler(handler), d_index1(index1), d_index2(index2) {}; + void send(SetNode & s1, SetNode & s2, SetNode & sinter){ + if(d_index1 == d_index2){ + if(!sinter.empty()) + d_handler->addMonoCandidate(sinter,d_index1); + }else{ + d_handler->addMultiCandidate(s1,d_index1,s2,d_index2); + } + } +}; + + +/** All the dispatcher that correspond to this node */ +class NodePpDispatcher: public PpDispatcher{ +#ifdef CVC4_DEBUG +public: + Node pat1; + Node pat2; +#endif/* CVC4_DEBUG */ +private: + std::vector<HandlerPpDispatcher> d_dis; + void send(SetNode & s1, SetNode & s2, SetNode & inter){ + for(std::vector<HandlerPpDispatcher>::iterator i = d_dis.begin(), end = d_dis.end(); + i != end; ++i){ + (*i).send(s1,s2,inter); + } + } +public: + void send(SetNode & s1, SetNode & s2){ + // can be done in HandlerPpDispatcher lazily + Assert(!s1.empty() && !s2.empty()); + SetNode inter; + std::set_intersection( s1.begin(), s1.end(), s2.begin(), s2.end(), + std::inserter( inter, inter.begin() ) ); + send(s1,s2,inter); + } + void addPpDispatcher(EfficientHandler* handler, size_t index1, size_t index2){ + d_dis.push_back(HandlerPpDispatcher(handler,index1,index2)); + } +}; //equivalence class info class EqClassInfo @@ -68,7 +365,7 @@ public: }; class InstantiatorTheoryUf : public Instantiator{ - friend class ::CVC4::theory::InstMatchGenerator; + friend class ::CVC4::theory::inst::InstMatchGenerator; friend class ::CVC4::theory::quantifiers::TermDb; protected: typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap; @@ -82,7 +379,14 @@ protected: InstStrategyUserPatterns* d_isup; public: InstantiatorTheoryUf(context::Context* c, CVC4::theory::QuantifiersEngine* qe, Theory* th); - ~InstantiatorTheoryUf() {} + ~InstantiatorTheoryUf() { + for(std::map< Node, std::pair<NodePcDispatcher*, NodePpDispatcher*> >::iterator + i = d_pat_cand_gens.begin(), end = d_pat_cand_gens.end(); + i != end; i++){ + delete(i->second.first); + delete(i->second.second); + } + } /** assertNode method */ void assertNode( Node assertion ); /** Pre-register a term. Done one time for a Node, ever. */ @@ -127,6 +431,9 @@ public: bool areDisequal( Node a, Node b ); Node getRepresentative( Node a ); Node getInternalRepresentative( Node a ); + /** general creators of candidate generators */ + rrinst::CandidateGenerator* getRRCanGenClasses(); + rrinst::CandidateGenerator* getRRCanGenClass(); /** new node */ void newEqClass( TNode n ); /** merge */ @@ -136,47 +443,66 @@ public: /** get equivalence class info */ EqClassInfo* getEquivalenceClassInfo( Node n ); EqClassInfo* getOrCreateEquivalenceClassInfo( Node n ); + typedef std::vector< std::pair< Node, int > > Ips; + typedef std::map< Node, std::vector< std::pair< Node, Ips > > > PpIpsMap; + typedef std::map< Node, std::vector< triple< size_t, Node, Ips > > > MultiPpIpsMap; + private: - typedef std::vector< std::pair< Node, int > > InvertedPathString; - typedef std::pair< InvertedPathString, InvertedPathString > IpsPair; /** Parent/Child Pairs (for efficient E-matching) So, for example, if we have the pattern f( g( x ) ), then d_pc_pairs[g][f][f( g( x ) )] = { f.0 }. */ - std::map< Node, std::map< Node, std::map< Node, std::vector< InvertedPathString > > > > d_pc_pairs; + std::map< Node, std::map< Node, std::vector< std::pair< NodePcDispatcher*, Ips > > > > d_pc_pairs; /** Parent/Parent Pairs (for efficient E-matching) */ - std::map< Node, std::map< Node, std::map< Node, std::vector< IpsPair > > > > d_pp_pairs; + std::map< Node, std::map< Node, std::vector< triple< NodePpDispatcher*, Ips, Ips > > > > d_pp_pairs; + /** Constants/Child Pairs + So, for example, if we have the pattern f( x ) = c, then d_pc_pairs[f][c] = ..., pcdispatcher, ... + */ + //TODO constant in pattern can use the same thing just add an Ips + std::map< Node, std::map< Node, NodePcDispatcher* > > d_cc_pairs; /** list of all candidate generators for each operator */ - std::map< Node, std::vector< CandidateGenerator* > > d_cand_gens; + std::map< Node, NodeNewTermDispatcher > d_cand_gens; + /** list of all candidate generators for each type */ + std::map< TypeNode, NodeNewTermDispatcher > d_cand_gen_types; /** map from patterns to candidate generators */ - std::map< Node, std::vector< CandidateGenerator* > > d_pat_cand_gens; + std::map< Node, std::pair<NodePcDispatcher*, NodePpDispatcher*> > d_pat_cand_gens; /** helper functions */ - void registerPatternElementPairs2( Node opat, Node pat, InvertedPathString& ips, - std::map< Node, std::vector< std::pair< Node, InvertedPathString > > >& ips_map ); - void registerPatternElementPairs( Node pat ); + void registerPatternElementPairs2( Node pat, Ips& ips, + PpIpsMap & pp_ips_map, NodePcDispatcher* npc); + void registerPatternElementPairs( Node pat, PpIpsMap & pp_ips_map, + NodePcDispatcher* npc, NodePpDispatcher* npp); + /** find the pp-pair between pattern inside multi-pattern*/ + void combineMultiPpIpsMap(PpIpsMap & pp_ips_map, MultiPpIpsMap & multi_pp_ips_map, + EfficientHandler& eh, size_t index2, + const std::vector<Node> & pats); //pats for debug /** compute candidates for pc pairs */ - void computeCandidatesPcPairs( Node a, Node b ); + void computeCandidatesPcPairs( Node a, EqClassInfo*, Node b, EqClassInfo* ); /** compute candidates for pp pairs */ - void computeCandidatesPpPairs( Node a, Node b ); + void computeCandidatesPpPairs( Node a, EqClassInfo*, Node b, EqClassInfo* ); + /** compute candidates for cc pairs */ + void computeCandidatesConstants( Node a, EqClassInfo*, Node b, EqClassInfo* ); /** collect terms based on inverted path string */ - void collectTermsIps( InvertedPathString& ips, std::vector< Node >& terms, int index = 0 ); - bool collectParentsTermsIps( Node n, Node f, int arg, std::vector< Node >& terms, bool addRep, bool modEq = true ); + void collectTermsIps( Ips& ips, SetNode& terms, int index); + bool collectParentsTermsIps( Node n, Node f, int arg, SetNode& terms, bool addRep, bool modEq = true ); public: + void collectTermsIps( Ips& ips, SetNode& terms); /** Register candidate generator cg for pattern pat. (for use with efficient e-matching) This request will ensure that calls will be made to cg->addCandidate( n ) for all ground terms n that are relevant for matching with pat. */ - void registerCandidateGenerator( CandidateGenerator* cg, Node pat ); private: /** triggers */ - std::map< Node, std::vector< Trigger* > > d_op_triggers; + std::map< Node, std::vector< inst::Trigger* > > d_op_triggers; public: /** register trigger (for eager quantifier instantiation) */ - void registerTrigger( Trigger* tr, Node op ); + void registerTrigger( inst::Trigger* tr, Node op ); + void registerEfficientHandler( EfficientHandler& eh, const std::vector<Node> & pat ); +public: + void newTerms(SetNode& s); public: /** output eq class */ void outputEqClass( const char* c, Node n ); /** output inverted path string */ - void outputInvertedPathString( const char* c, InvertedPathString& ips ); + void outputIps( const char* c, Ips& ips ); };/* class InstantiatorTheoryUf */ /** equality query object using instantiator theory uf */ |