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/instantiation_engine.h | |
parent | aaf1bbbdc6e42910e07db64441885ee3476d86df (diff) |
Promote InstStrategyCbqi to quantifier module. Cleanup unused code.
Diffstat (limited to 'src/theory/quantifiers/instantiation_engine.h')
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.h | 33 |
1 files changed, 1 insertions, 32 deletions
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 51daef9dc..bc1199588 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -27,9 +27,6 @@ namespace quantifiers { class InstStrategyUserPatterns; class InstStrategyAutoGenTriggers; class InstStrategyFreeVariable; -class InstStrategyCbqi; -class InstStrategySimplex; -class InstStrategyCegqi; /** instantiation strategy class */ class InstStrategy { @@ -53,9 +50,7 @@ public: /** identify */ virtual std::string identify() const { return std::string("Unknown"); } /** register quantifier */ - virtual void registerQuantifier( Node q ) {} - /** get next decision request */ - virtual Node getNextDecisionRequest() { return Node::null(); } + //virtual void registerQuantifier( Node q ) {} };/* class InstStrategy */ class InstantiationEngine : public QuantifiersModule @@ -63,17 +58,10 @@ class InstantiationEngine : public QuantifiersModule private: /** instantiation strategies */ std::vector< InstStrategy* > d_instStrategies; - /** instantiation strategies active */ - //std::map< InstStrategy*, bool > d_instStrategyActive; /** user-pattern instantiation strategy */ InstStrategyUserPatterns* d_isup; /** auto gen triggers; only kept for destructor cleanup */ InstStrategyAutoGenTriggers* d_i_ag; - InstStrategyCbqi * d_i_cbqi; - /** simplex (cbqi) */ - InstStrategySimplex * d_i_splx; - /** generic cegqi */ - InstStrategyCegqi * d_i_cegqi; private: typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; /** current processing quantified formulas */ @@ -90,34 +78,15 @@ public: void finishInit(); void presolve(); 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 ); - void assertNode( Node f ); Node explain(TNode n){ return Node::null(); } - Node getNextDecisionRequest(); /** add user pattern */ void addUserPattern( Node f, Node pat ); void addUserNoPattern( Node f, Node pat ); public: - /** statistics class */ - class Statistics { - public: - IntStat d_instantiations_user_patterns; - IntStat d_instantiations_auto_gen; - IntStat d_instantiations_guess; - IntStat d_instantiations_cbqi_arith; - IntStat d_instantiations_cbqi_arith_minus; - IntStat d_instantiations_cbqi_datatypes; - IntStat d_instantiations_lte; - IntStat d_instantiation_rounds; - Statistics(); - ~Statistics(); - }; - Statistics d_statistics; /** Identify this module */ std::string identify() const { return "InstEngine"; } };/* class InstantiationEngine */ |