diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-26 16:11:00 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-26 16:11:00 +0100 |
commit | af86e5a8dc7a64fb5f7b4ca7bd3b2bedf5e8fe32 (patch) | |
tree | d86858d67279e940a225e7ca693172685532d6d7 /src/theory/quantifiers/inst_strategy_cbqi.h | |
parent | aaf1bbbdc6e42910e07db64441885ee3476d86df (diff) |
Promote InstStrategyCbqi to quantifier module. Cleanup unused code.
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_cbqi.h')
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.h | 26 |
1 files changed, 17 insertions, 9 deletions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index adbb2a5e4..6619860e0 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -33,11 +33,12 @@ namespace arith { namespace quantifiers { -class InstStrategyCbqi : public InstStrategy { +class InstStrategyCbqi : public QuantifiersModule { + typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; protected: bool d_cbqi_set_quant_inactive; /** whether we have added cbqi lemma */ - std::map< Node, bool > d_added_cbqi_lemma; + NodeSet d_added_cbqi_lemma; /** whether to do cbqi for this quantified formula */ std::map< Node, bool > d_do_cbqi; /** register ce lemma */ @@ -47,17 +48,24 @@ protected: /** helper functions */ bool hasNonCbqiVariable( Node q ); bool hasNonCbqiOperator( Node n, std::map< Node, bool >& visited ); + /** process functions */ + virtual void processResetInstantiationRound( Theory::Effort effort ) = 0; + virtual void process( Node q, Theory::Effort effort, int e ) = 0; public: InstStrategyCbqi( QuantifiersEngine * qe ); ~InstStrategyCbqi() throw() {} + /** whether to do CBQI for quantifier q */ + bool doCbqi( Node q ); /** process functions */ - void processResetInstantiationRound( Theory::Effort effort ); + bool needsCheck( Theory::Effort e ); + unsigned needsModel( Theory::Effort e ); + void reset_round( Theory::Effort e ); + void check( Theory::Effort e, unsigned quant_e ); + bool checkComplete(); + void preRegisterQuantifier( Node q ); + void registerQuantifier( Node q ); /** get next decision request */ Node getNextDecisionRequest(); - //set quant inactive - bool setQuantifierInactive() { return d_cbqi_set_quant_inactive; } - /** whether to do CBQI for quantifier q */ - bool doCbqi( Node q ); }; @@ -95,7 +103,7 @@ private: Node d_negOne; /** process functions */ void processResetInstantiationRound( Theory::Effort effort ); - int process( Node f, Theory::Effort effort, int e ); + void process( Node f, Theory::Effort effort, int e ); public: InstStrategySimplex( arith::TheoryArith* th, QuantifiersEngine* ie ); ~InstStrategySimplex() throw() {} @@ -126,7 +134,7 @@ protected: bool d_check_vts_lemma_lc; /** process functions */ void processResetInstantiationRound( Theory::Effort effort ); - int process( Node f, Theory::Effort effort, int e ); + void process( Node f, Theory::Effort effort, int e ); /** register ce lemma */ void registerCounterexampleLemma( Node q, Node lem ); public: |