diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-22 08:59:03 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-22 08:59:09 +0100 |
commit | 48bc3c425947542ca1a337e08044c8f745600690 (patch) | |
tree | cc08928a21cb4d8c81d2d8ab338a65fe7cca5128 /src/theory/quantifiers/instantiation_engine.h | |
parent | d2b44175c45a6d2c2fa9c3f8ec1ca1c433cb399b (diff) |
New trigger options. --inst-no-entail on by default. Misc cleanup.
Diffstat (limited to 'src/theory/quantifiers/instantiation_engine.h')
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.h | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 2d427ae0a..c69136933 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -40,21 +40,9 @@ public: protected: /** reference to the instantiation engine */ QuantifiersEngine* d_quantEngine; - /** should process a quantifier */ - std::map< Node, bool > d_quantActive; - /** calculate should process */ - virtual bool calculateShouldProcess( Node f ) { return true; } public: InstStrategy( QuantifiersEngine* qe ) : d_quantEngine( qe ){} virtual ~InstStrategy(){} - - /** should process quantified formula f? */ - bool shouldProcess( Node f ) { - if( d_quantActive.find( f )==d_quantActive.end() ){ - d_quantActive[f] = calculateShouldProcess( f ); - } - return d_quantActive[f]; - } /** reset instantiation */ virtual void processResetInstantiationRound( Theory::Effort effort ) = 0; /** process method, returns a status */ @@ -131,7 +119,6 @@ public: public: IntStat d_instantiations_user_patterns; IntStat d_instantiations_auto_gen; - IntStat d_instantiations_auto_gen_min; IntStat d_instantiations_guess; IntStat d_instantiations_cbqi_arith; IntStat d_instantiations_cbqi_arith_minus; |