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/inst_strategy.h | |
parent | 865fb413bf91d395a90cf0cc502e1dbc7d2d8ebb (diff) |
Split E-matching strategies to own files (#5807)
Code move + format only
Diffstat (limited to 'src/theory/quantifiers/ematching/inst_strategy.h')
-rw-r--r-- | src/theory/quantifiers/ematching/inst_strategy.h | 66 |
1 files changed, 66 insertions, 0 deletions
diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h new file mode 100644 index 000000000..0a4c1b76f --- /dev/null +++ b/src/theory/quantifiers/ematching/inst_strategy.h @@ -0,0 +1,66 @@ +/********************* */ +/*! \file inst_strategy.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters, Mathias Preiner + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Instantiation Engine classes + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_H +#define CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_H + +#include <vector> +#include "expr/node.h" +#include "theory/theory.h" + +namespace CVC4 { +namespace theory { + +class QuantifiersEngine; + +namespace quantifiers { + +/** A status response to process */ +enum class InstStrategyStatus +{ + // the strategy is not finished + STATUS_UNFINISHED, + // the status of the strategy is unknown + STATUS_UNKNOWN, +}; + +/** + * A base class for instantiation strategies within E-matching. + */ +class InstStrategy +{ + 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 InstStrategyStatus process(Node f, Theory::Effort effort, int e) = 0; + /** identify */ + virtual std::string identify() const { return std::string("Unknown"); } + + protected: + /** reference to the instantiation engine */ + QuantifiersEngine* d_quantEngine; +}; /* class InstStrategy */ + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */ |