diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-25 08:59:18 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-01-25 08:59:18 -0600 |
commit | f48d8d6a1bc2b42608c0d9b1e5ad2cc091cb8d99 (patch) | |
tree | 1b080e9c287eb757eb42bf2d320e41aa3adff1ff /src/theory/quantifiers/ematching/instantiation_engine.h | |
parent | 865fb413bf91d395a90cf0cc502e1dbc7d2d8ebb (diff) |
Split E-matching strategies to own files (#5807)
Code move + format only
Diffstat (limited to 'src/theory/quantifiers/ematching/instantiation_engine.h')
-rw-r--r-- | src/theory/quantifiers/ematching/instantiation_engine.h | 25 |
1 files changed, 1 insertions, 24 deletions
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index f2f013f1c..9304c84ae 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -19,6 +19,7 @@ #include <vector> +#include "theory/quantifiers/ematching/inst_strategy.h" #include "theory/quantifiers/quant_relevance.h" #include "theory/quantifiers/quant_util.h" @@ -28,30 +29,6 @@ namespace quantifiers { class InstStrategyUserPatterns; class InstStrategyAutoGenTriggers; -class InstStrategyFreeVariable; - -/** instantiation strategy class */ -class InstStrategy { -public: - enum Status { - STATUS_UNFINISHED, - STATUS_UNKNOWN, - };/* enum Status */ -protected: - /** reference to the instantiation engine */ - QuantifiersEngine* d_quantEngine; -public: - InstStrategy( QuantifiersEngine* qe ) : d_quantEngine( qe ){} - virtual ~InstStrategy(){} - /** presolve */ - virtual void presolve() {} - /** reset instantiation */ - virtual void processResetInstantiationRound( Theory::Effort effort ) = 0; - /** process method, returns a status */ - virtual int process( Node f, Theory::Effort effort, int e ) = 0; - /** identify */ - virtual std::string identify() const { return std::string("Unknown"); } -};/* class InstStrategy */ class InstantiationEngine : public QuantifiersModule { private: |