diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-16 21:59:50 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-16 21:59:50 +0000 |
commit | d9d71e0d7885d32ef44fbd08d47b3cccd35ff6f7 (patch) | |
tree | f730bb17eba9412258c47617f144510d722d6006 /src/theory/quantifiers_engine.h | |
parent | bbcfb5208c6c0f343d1a63b129c54914f66b2701 (diff) |
more cleanup of quantifiers code
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r-- | src/theory/quantifiers_engine.h | 135 |
1 files changed, 16 insertions, 119 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index d0c5832ff..62e5d983e 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -21,6 +21,7 @@ #include "util/hash.h" #include "theory/quantifiers/inst_match.h" #include "theory/rewriterules/rr_inst_match.h" +#include "theory/quantifiers/quant_util.h" #include "util/statistics_registry.h" @@ -36,57 +37,6 @@ namespace theory { class QuantifiersEngine; -class InstStrategy { -public: - enum Status { - STATUS_UNFINISHED, - STATUS_UNKNOWN, - STATUS_SAT, - };/* enum Status */ -protected: - /** reference to the instantiation engine */ - QuantifiersEngine* d_quantEngine; -protected: - /** giving priorities */ - std::vector< InstStrategy* > d_priority_over; - /** do not instantiate list */ - std::vector< Node > d_no_instantiate; - std::vector< Node > d_no_instantiate_temp; - /** reset instantiation */ - virtual void processResetInstantiationRound( Theory::Effort effort ) = 0; - /** process method */ - virtual int process( Node f, Theory::Effort effort, int e ) = 0; -public: - InstStrategy( QuantifiersEngine* ie ) : d_quantEngine( ie ){} - virtual ~InstStrategy(){} - - /** reset instantiation */ - void resetInstantiationRound( Theory::Effort effort ); - /** do instantiation round method */ - int doInstantiation( Node f, Theory::Effort effort, int e ); - /** update status */ - static void updateStatus( int& currStatus, int addStatus ){ - if( addStatus==STATUS_UNFINISHED ){ - currStatus = STATUS_UNFINISHED; - }else if( addStatus==STATUS_UNKNOWN ){ - if( currStatus==STATUS_SAT ){ - currStatus = STATUS_UNKNOWN; - } - } - } - /** identify */ - virtual std::string identify() const { return std::string("Unknown"); } -public: - /** set priority */ - void setPriorityOver( InstStrategy* is ) { d_priority_over.push_back( is ); } - /** set no instantiate */ - void setNoInstantiate( Node n ) { d_no_instantiate.push_back( n ); } - /** should instantiate */ - bool shouldInstantiate( Node n ) { - return std::find( d_no_instantiate_temp.begin(), d_no_instantiate_temp.end(), n )==d_no_instantiate_temp.end(); - } -};/* class InstStrategy */ - class QuantifiersModule { protected: QuantifiersEngine* d_quantEngine; @@ -129,13 +79,13 @@ private: quantifiers::ModelEngine* d_model_engine; /** equality query class */ EqualityQuery* d_eq_query; -public: + /** for computing relevance of quantifiers */ + QuantRelevance d_quant_rel; + /** phase requirements for each quantifier for each instantiation literal */ + std::map< Node, QuantPhaseReq* > d_phase_reqs; +private: /** list of all quantifiers (pre-rewrite) */ std::vector< Node > d_quants; - /** list of all quantifiers (post-rewrite) */ - std::vector< Node > d_r_quants; - /** map from quantifiers to whether they are active */ - BoolMap d_active; /** lemmas produced */ std::map< Node, bool > d_lemmas_produced; /** lemmas waiting */ @@ -150,30 +100,8 @@ public: quantifiers::TermDb* d_term_db; /** extended model object */ quantifiers::FirstOrderModel* d_model; - /** has the model been set? */ - bool d_model_set; - /** has resetInstantiationRound() been called on this check(...) */ - bool d_resetInstRound; - /** universal quantifiers that have been rewritten */ - std::map< Node, std::vector< Node > > d_quant_rewritten; - /** map from rewritten universal quantifiers to the quantifier they are the consequence of */ - std::map< Node, Node > d_rewritten_quant; private: - /** for computing relavance */ - /** map from quantifiers to symbols they contain */ - std::map< Node, std::vector< Node > > d_syms; - /** map from symbols to quantifiers */ - std::map< Node, std::vector< Node > > d_syms_quants; - /** relevance for quantifiers and symbols */ - std::map< Node, int > d_relevance; - /** compute symbols */ - void computeSymbols( Node n, std::vector< Node >& syms ); -private: - /** helper functions compute phase requirements */ - static void computePhaseReqs2( Node n, bool polarity, std::map< Node, int >& phaseReqs ); - KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time"); - public: QuantifiersEngine(context::Context* c, TheoryEngine* te); ~QuantifiersEngine(); @@ -184,9 +112,7 @@ public: /** 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; - } + 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); @@ -204,14 +130,20 @@ public: OutputChannel& getOutputChannel(); /** get default valuation for the quantifiers engine */ Valuation& getValuation(); + /** get quantifier relevance */ + QuantRelevance* getQuantifierRelevance() { return &d_quant_rel; } + /** get phase requirement information */ + QuantPhaseReq* getPhaseRequirements( Node f ) { return d_phase_reqs.find( f )==d_phase_reqs.end() ? NULL : d_phase_reqs[f]; } + /** get phase requirement terms */ + void getPhaseReqTerms( Node f, std::vector< Node >& nodes ); public: /** check at level */ void check( Theory::Effort e ); - /** register (non-rewritten) quantifier */ + /** register quantifier */ void registerQuantifier( Node f ); - /** register (non-rewritten) quantifier */ + /** register quantifier */ void registerPattern( std::vector<Node> & pattern); - /** assert (universal) quantifier */ + /** assert universal quantifier */ void assertNode( Node f ); /** propagate */ void propagate( Theory::Effort level ); @@ -253,33 +185,6 @@ public: int getNumQuantifiers() { return (int)d_quants.size(); } /** get quantifier */ Node getQuantifier( int i ) { return d_quants[i]; } - /** set active */ - void setActive( Node n, bool val ) { d_active[n] = val; } - /** get active */ - bool getActive( Node n ) { return d_active.find( n )!=d_active.end() && d_active[n]; } -public: - /** phase requirements for each quantifier for each instantiation literal */ - std::map< Node, std::map< Node, bool > > d_phase_reqs; - std::map< Node, std::map< Node, bool > > d_phase_reqs_equality; - std::map< Node, std::map< Node, Node > > d_phase_reqs_equality_term; -public: - /** is phase required */ - bool isPhaseReq( Node f, Node lit ) { return d_phase_reqs[f].find( lit )!=d_phase_reqs[f].end(); } - /** get phase requirement */ - bool getPhaseReq( Node f, Node lit ) { return d_phase_reqs[f].find( lit )==d_phase_reqs[f].end() ? false : d_phase_reqs[f][ lit ]; } - /** get term req terms */ - void getPhaseReqTerms( Node f, std::vector< Node >& nodes ); - /** helper functions compute phase requirements */ - static void computePhaseReqs( Node n, bool polarity, std::map< Node, bool >& phaseReqs ); - /** compute phase requirements */ - void generatePhaseReqs( Node f, Node n ); -public: - /** has owner */ - bool hasOwner( Node f ) { return d_owner.find( f )!=d_owner.end(); } - /** get owner */ - Theory* getOwner( Node f ) { return d_owner[f]; } - /** set owner */ - void setOwner( Node f, Theory* t ) { d_owner[f] = t; } public: /** get model */ quantifiers::FirstOrderModel* getModel() { return d_model; } @@ -287,14 +192,6 @@ public: quantifiers::TermDb* getTermDatabase() { return d_term_db; } /** add term to database */ void addTermToDatabase( Node n, bool withinQuant = false ); -private: - /** set relevance */ - void setRelevance( Node s, int r ); -public: - /** get relevance */ - int getRelevance( Node s ) { return d_relevance.find( s )==d_relevance.end() ? -1 : d_relevance[s]; } - /** get number of quantifiers for symbol s */ - int getNumQuantifiersForSymbol( Node s ) { return (int)d_syms_quants[s].size(); } public: /** statistics class */ class Statistics { |