diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-30 20:38:45 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-11-30 20:38:45 +0000 |
commit | f28bab562105548413cfca93de5c9b047157a076 (patch) | |
tree | bfbe95b9aed35f91b6bd9e3af50fad03ab86f23b /src/theory/uf | |
parent | 6369830eec077ef112e6cc806cd910c7209eb2db (diff) |
quantifiers now uses master equality engine, preparation work to cleanup code
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/inst_strategy.cpp | 56 | ||||
-rw-r--r-- | src/theory/uf/inst_strategy.h | 28 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 9 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_instantiator.cpp | 49 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_instantiator.h | 52 |
5 files changed, 82 insertions, 112 deletions
diff --git a/src/theory/uf/inst_strategy.cpp b/src/theory/uf/inst_strategy.cpp index 433ceee85..8c90d569a 100644 --- a/src/theory/uf/inst_strategy.cpp +++ b/src/theory/uf/inst_strategy.cpp @@ -75,10 +75,11 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){ if( processTrigger ){ //if( d_user_gen[f][i]->isMultiTrigger() ) //Notice() << " Process (user) " << (*d_user_gen[f][i]) << " for " << f << "..." << std::endl; - int numInst = d_user_gen[f][i]->addInstantiations( d_th->d_baseMatch[f] ); + InstMatch baseMatch; + int numInst = d_user_gen[f][i]->addInstantiations( baseMatch ); //if( d_user_gen[f][i]->isMultiTrigger() ) //Notice() << " Done, numInst = " << numInst << "." << std::endl; - d_th->d_statistics.d_instantiations_user_pattern += numInst; + //d_statistics.d_instantiations += numInst; if( d_user_gen[f][i]->isMultiTrigger() ){ d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst; } @@ -106,6 +107,17 @@ void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){ options::smartTriggers() ) ); } } +/* +InstStrategyUserPatterns::Statistics::Statistics(): + d_instantiations("InstStrategyUserPatterns::Instantiations", 0) +{ + StatisticsRegistry::registerStat(&d_instantiations); +} + +InstStrategyUserPatterns::Statistics::~Statistics(){ + StatisticsRegistry::unregisterStat(&d_instantiations); +} +*/ void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){ //reset triggers @@ -153,14 +165,15 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) if( processTrigger ){ //if( tr->isMultiTrigger() ) Debug("quant-uf-strategy-auto-gen-triggers") << " Process " << (*tr) << "..." << std::endl; - int numInst = tr->addInstantiations( d_th->d_baseMatch[f] ); + InstMatch baseMatch; + int numInst = tr->addInstantiations( baseMatch ); //if( tr->isMultiTrigger() ) Debug("quant-uf-strategy-auto-gen-triggers") << " Done, numInst = " << numInst << "." << std::endl; - if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){ - d_th->d_statistics.d_instantiations_auto_gen_min += numInst; - }else{ - d_th->d_statistics.d_instantiations_auto_gen += numInst; - } + //if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){ + // d_statistics.d_instantiations_min += numInst; + //}else{ + // d_statistics.d_instantiations += numInst; + //} if( tr->isMultiTrigger() ){ d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst; } @@ -321,6 +334,20 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ } } } +/* +InstStrategyAutoGenTriggers::Statistics::Statistics(): + d_instantiations("InstStrategyAutoGenTriggers::Instantiations", 0), + d_instantiations_min("InstStrategyAutoGenTriggers::Instantiations_min", 0) +{ + StatisticsRegistry::registerStat(&d_instantiations); + StatisticsRegistry::registerStat(&d_instantiations_min); +} + +InstStrategyAutoGenTriggers::Statistics::~Statistics(){ + StatisticsRegistry::unregisterStat(&d_instantiations); + StatisticsRegistry::unregisterStat(&d_instantiations_min); +} +*/ void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){ } @@ -334,10 +361,21 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){ Debug("quant-uf-alg") << "Add guessed instantiation" << std::endl; InstMatch m; if( d_quantEngine->addInstantiation( f, m ) ){ - ++(d_th->d_statistics.d_instantiations_guess); + //++(d_statistics.d_instantiations); //d_quantEngine->d_hasInstantiated[f] = true; } } return STATUS_UNKNOWN; } } +/* +InstStrategyFreeVariable::Statistics::Statistics(): + d_instantiations("InstStrategyGuess::Instantiations", 0) +{ + StatisticsRegistry::registerStat(&d_instantiations); +} + +InstStrategyFreeVariable::Statistics::~Statistics(){ + StatisticsRegistry::unregisterStat(&d_instantiations); +} +*/
\ No newline at end of file diff --git a/src/theory/uf/inst_strategy.h b/src/theory/uf/inst_strategy.h index aaa5f27a1..42d401126 100644 --- a/src/theory/uf/inst_strategy.h +++ b/src/theory/uf/inst_strategy.h @@ -58,6 +58,15 @@ public: inst::Trigger* getUserGenerator( Node f, int i ) { return d_user_gen[f][ i ]; } /** identify */ std::string identify() const { return std::string("UserPatterns"); } +public: + /** statistics class */ + //class Statistics { + //public: + // IntStat d_instantiations; + // Statistics(); + // ~Statistics(); + //}; + //Statistics d_statistics; };/* class InstStrategyUserPatterns */ class InstStrategyAutoGenTriggers : public InstStrategy{ @@ -114,6 +123,16 @@ public: } /** set generate additional */ void setGenerateAdditional( bool val ) { d_generate_additional = val; } +public: + /** statistics class */ + //class Statistics { + //public: + // IntStat d_instantiations; + // IntStat d_instantiations_min; + // Statistics(); + // ~Statistics(); + //}; + //Statistics d_statistics; };/* class InstStrategyAutoGenTriggers */ class InstStrategyFreeVariable : public InstStrategy{ @@ -131,6 +150,15 @@ public: ~InstStrategyFreeVariable(){} /** identify */ std::string identify() const { return std::string("FreeVariable"); } +public: + /** statistics class */ + //class Statistics { + //public: + // IntStat d_instantiations; + // Statistics(); + // ~Statistics(); + //}; + //Statistics d_statistics; };/* class InstStrategyFreeVariable */ }/* CVC4::theory::uf namespace */ diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index e6ae3747c..23f100f74 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -22,6 +22,8 @@ #include "theory/uf/theory_uf_strong_solver.h" #include "theory/model.h" #include "theory/type_enumerator.h" +//included since efficient e matching needs notifications from UF +#include "theory/rewriterules/efficient_e_matching.h" using namespace std; using namespace CVC4; @@ -479,13 +481,13 @@ void TheoryUF::eqNotifyNewClass(TNode t) { } // this can be called very early, during initialization if (!getLogicInfo().isLocked() || getLogicInfo().isQuantified()) { - ((InstantiatorTheoryUf*) getInstantiator())->newEqClass(t); + //getQuantifiersEngine()->addTermToDatabase( t ); } } void TheoryUF::eqNotifyPreMerge(TNode t1, TNode t2) { if (getLogicInfo().isQuantified()) { - ((InstantiatorTheoryUf*) getInstantiator())->merge(t1, t2); + getQuantifiersEngine()->getEfficientEMatcher()->merge( t1, t2 ); } } @@ -499,9 +501,6 @@ void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { if (d_thss != NULL) { d_thss->assertDisequal(t1, t2, reason); } - if (getLogicInfo().isQuantified()) { - ((InstantiatorTheoryUf*) getInstantiator())->assertDisequal(t1, t2, reason); - } } Node TheoryUF::ppRewrite(TNode node) { diff --git a/src/theory/uf/theory_uf_instantiator.cpp b/src/theory/uf/theory_uf_instantiator.cpp index e45842481..9ae6bbd37 100644 --- a/src/theory/uf/theory_uf_instantiator.cpp +++ b/src/theory/uf/theory_uf_instantiator.cpp @@ -41,6 +41,7 @@ Instantiator( c, qe, th ) //if( options::cbqi() ){ // addInstStrategy( new InstStrategyCheckCESolved( this, qe ) ); //} + //these are the instantiation strategies for basic E-matching if( options::userPatternsQuant() ){ d_isup = new InstStrategyUserPatterns( this, qe ); addInstStrategy( d_isup ); @@ -69,7 +70,7 @@ void InstantiatorTheoryUf::assertNode( Node assertion ) { Debug("quant-uf-assert") << "InstantiatorTheoryUf::check: " << assertion << std::endl; //preRegisterTerm( assertion ); - d_quantEngine->addTermToDatabase( assertion ); + //INST_ELIM_TRY//d_quantEngine->addTermToDatabase( assertion ); if( options::cbqi() ){ if( assertion.hasAttribute(InstConstantAttribute()) ){ setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) ); @@ -150,52 +151,6 @@ void InstantiatorTheoryUf::getEquivalenceClass( Node a, std::vector< Node >& eqc } } -InstantiatorTheoryUf::Statistics::Statistics(): - //d_instantiations("InstantiatorTheoryUf::Total_Instantiations", 0), - d_instantiations_ce_solved("InstantiatorTheoryUf::Instantiations_CE-Solved", 0), - d_instantiations_e_induced("InstantiatorTheoryUf::Instantiations_E-Induced", 0), - d_instantiations_user_pattern("InstantiatorTheoryUf::Instantiations_User_Pattern", 0), - d_instantiations_guess("InstantiatorTheoryUf::Instantiations_Free_Var", 0), - d_instantiations_auto_gen("InstantiatorTheoryUf::Instantiations_Auto_Gen", 0), - d_instantiations_auto_gen_min("InstantiatorTheoryUf::Instantiations_Auto_Gen_Min", 0), - d_splits("InstantiatorTheoryUf::Total_Splits", 0) -{ - //StatisticsRegistry::registerStat(&d_instantiations); - StatisticsRegistry::registerStat(&d_instantiations_ce_solved); - StatisticsRegistry::registerStat(&d_instantiations_e_induced); - StatisticsRegistry::registerStat(&d_instantiations_user_pattern ); - StatisticsRegistry::registerStat(&d_instantiations_guess ); - StatisticsRegistry::registerStat(&d_instantiations_auto_gen ); - StatisticsRegistry::registerStat(&d_instantiations_auto_gen_min ); - StatisticsRegistry::registerStat(&d_splits); -} - -InstantiatorTheoryUf::Statistics::~Statistics(){ - //StatisticsRegistry::unregisterStat(&d_instantiations); - StatisticsRegistry::unregisterStat(&d_instantiations_ce_solved); - StatisticsRegistry::unregisterStat(&d_instantiations_e_induced); - StatisticsRegistry::unregisterStat(&d_instantiations_user_pattern ); - StatisticsRegistry::unregisterStat(&d_instantiations_guess ); - StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen ); - StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen_min ); - StatisticsRegistry::unregisterStat(&d_splits); -} - -/** new node */ -void InstantiatorTheoryUf::newEqClass( TNode n ){ - d_quantEngine->addTermToDatabase( n ); -} - -/** merge */ -void InstantiatorTheoryUf::merge( TNode a, TNode b ){ - d_quantEngine->getEfficientEMatcher()->merge( a, b ); -} - -/** assert terms are disequal */ -void InstantiatorTheoryUf::assertDisequal( TNode a, TNode b, TNode reason ){ - -} - void InstantiatorTheoryUf::outputEqClass( const char* c, Node n ){ if( ((TheoryUF*)d_th)->d_equalityEngine.hasTerm( n ) ){ eq::EqClassIterator eqc_iter( getRepresentative( n ), diff --git a/src/theory/uf/theory_uf_instantiator.h b/src/theory/uf/theory_uf_instantiator.h index b5a3aa765..fe34c9487 100644 --- a/src/theory/uf/theory_uf_instantiator.h +++ b/src/theory/uf/theory_uf_instantiator.h @@ -40,15 +40,6 @@ namespace quantifiers{ namespace uf { class InstantiatorTheoryUf : public Instantiator{ - friend class ::CVC4::theory::inst::InstMatchGenerator; - friend class ::CVC4::theory::quantifiers::TermDb; -protected: - typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap; - typedef context::CDHashMap<Node, int, NodeHashFunction> IntMap; - typedef context::CDChunkList<Node> NodeList; - typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeLists; - /** map to representatives used */ - //std::map< Node, Node > d_ground_reps; protected: /** instantiation strategies */ InstStrategyUserPatterns* d_isup; @@ -71,25 +62,6 @@ private: /** calculate matches for quantifier f at effort */ int process( Node f, Theory::Effort effort, int e ); public: - /** statistics class */ - class Statistics { - public: - //IntStat d_instantiations; - IntStat d_instantiations_ce_solved; - IntStat d_instantiations_e_induced; - IntStat d_instantiations_user_pattern; - IntStat d_instantiations_guess; - IntStat d_instantiations_auto_gen; - IntStat d_instantiations_auto_gen_min; - IntStat d_splits; - Statistics(); - ~Statistics(); - }; - Statistics d_statistics; -public: - /** the base match */ - std::map< Node, InstMatch > d_baseMatch; -public: /** general queries about equality */ bool hasTerm( Node a ); bool areEqual( Node a, Node b ); @@ -101,34 +73,12 @@ public: /** general creators of candidate generators */ rrinst::CandidateGenerator* getRRCanGenClasses(); rrinst::CandidateGenerator* getRRCanGenClass(); - /** new node */ - void newEqClass( TNode n ); - /** merge */ - void merge( TNode a, TNode b ); - /** assert terms are disequal */ - void assertDisequal( TNode a, TNode b, TNode reason ); public: /** output eq class */ void outputEqClass( const char* c, Node n ); };/* class InstantiatorTheoryUf */ -/** equality query object using instantiator theory uf */ -class EqualityQueryInstantiatorTheoryUf : public EqualityQuery -{ -private: - /** pointer to instantiator uf class */ - InstantiatorTheoryUf* d_ith; -public: - EqualityQueryInstantiatorTheoryUf( InstantiatorTheoryUf* ith ) : d_ith( ith ){} - ~EqualityQueryInstantiatorTheoryUf(){} - /** general queries about equality */ - bool hasTerm( Node a ) { return d_ith->hasTerm( a ); } - Node getRepresentative( Node a ) { return d_ith->getRepresentative( a ); } - bool areEqual( Node a, Node b ) { return d_ith->areEqual( a, b ); } - bool areDisequal( Node a, Node b ) { return d_ith->areDisequal( a, b ); } - eq::EqualityEngine* getEngine() { return d_ith->getEqualityEngine(); } - void getEquivalenceClass( Node a, std::vector< Node >& eqc ) { d_ith->getEquivalenceClass( a, eqc ); } -}; /* EqualityQueryInstantiatorTheoryUf */ + } }/* CVC4::theory namespace */ |