diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-18 17:39:05 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-18 17:39:14 +0100 |
commit | 3a2aed30267a33ff78006aec6a5b36aad96feb09 (patch) | |
tree | fa5a61a9c0e071c0d9d438de9150e3a90b4ff583 /src/theory/quantifiers/instantiation_engine.h | |
parent | d9923e1928a158c915a71ce0addb766a1e9986ca (diff) |
Add local theory extensions instantiation strategy (incomplete). Refactor how default options are set for quantifiers. Minor improvement to datatypes. Add unsat co-datatype regression. Clean up instantiation engine. Set inst level 0 on introduced constants for types with no ground terms. Return introduced constant for variable trigger when no ground terms exist.
Diffstat (limited to 'src/theory/quantifiers/instantiation_engine.h')
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.h | 36 |
1 files changed, 13 insertions, 23 deletions
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index bf0bb03e1..2fa37ac35 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -26,6 +26,9 @@ namespace quantifiers { class InstStrategyUserPatterns; class InstStrategyAutoGenTriggers; +class InstStrategyLocalTheoryExt; +class InstStrategyFreeVariable; +class InstStrategySimplex; /** instantiation strategy class */ class InstStrategy { @@ -33,7 +36,6 @@ public: enum Status { STATUS_UNFINISHED, STATUS_UNKNOWN, - STATUS_SAT, };/* enum Status */ protected: /** reference to the instantiation engine */ @@ -57,16 +59,6 @@ public: virtual void processResetInstantiationRound( Theory::Effort effort ) = 0; /** process method, returns a status */ virtual int process( Node f, Theory::Effort effort, int e ) = 0; - /** 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"); } };/* class InstStrategy */ @@ -77,24 +69,19 @@ private: /** instantiation strategies */ std::vector< InstStrategy* > d_instStrategies; /** instantiation strategies active */ - std::map< InstStrategy*, bool > d_instStrategyActive; + //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; - /** is instantiation strategy active */ - bool isActiveStrategy( InstStrategy* is ) { - return d_instStrategyActive.find( is )!=d_instStrategyActive.end() && d_instStrategyActive[is]; - } - /** add inst strategy */ - void addInstStrategy( InstStrategy* is ){ - d_instStrategies.push_back( is ); - d_instStrategyActive[is] = true; - } + /** local theory extensions */ + InstStrategyLocalTheoryExt * d_i_lte; + /** full saturate */ + InstStrategyFreeVariable * d_i_fs; + /** simplex (cbqi) */ + InstStrategySimplex * d_i_splx; private: typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; - /** status of instantiation round (one of InstStrategy::STATUS_*) */ - int d_inst_round_status; /** whether the instantiation engine should set incomplete if it cannot answer SAT */ bool d_setIncomplete; /** inst round counter */ @@ -111,6 +98,8 @@ private: bool hasApplyUf( Node f ); /** whether to do CBQI for quantifier f */ bool doCbqi( Node f ); + /** is the engine incomplete for this quantifier */ + bool isIncomplete( Node f ); private: /** do instantiation round */ bool doInstantiationRound( Theory::Effort effort ); @@ -149,6 +138,7 @@ public: 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(); |