diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-11 17:08:07 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-11 17:08:07 -0500 |
commit | 81cd457d729f845f1b76d457359a0ae9963c0f88 (patch) | |
tree | c521ed630f3514b26bfbce227a1e1e41b8dac01a /src/theory/quantifiers/instantiate.h | |
parent | 3e6de62d11dcb3cf266f58e68def2f2c2ce728c3 (diff) |
Infrastructure for instantiation rewriter (#3262)
Diffstat (limited to 'src/theory/quantifiers/instantiate.h')
-rw-r--r-- | src/theory/quantifiers/instantiate.h | 32 |
1 files changed, 31 insertions, 1 deletions
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 769ae4ea3..4936693d1 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -69,6 +69,32 @@ class InstantiationNotify virtual void filterInstantiations() = 0; }; +/** Instantiation rewriter + * + * This class is used for cases where instantiation lemmas can be rewritten by + * external utilities. Examples of this include virtual term substitution and + * nested quantifier elimination techniques. + */ +class InstantiationRewriter +{ + public: + InstantiationRewriter() {} + virtual ~InstantiationRewriter() {} + + /** rewrite instantiation + * + * The node inst is the instantiation of quantified formula q for terms. + * This method returns the rewritten form of the instantiation. + * + * The flag doVts is whether we must apply virtual term substitution to the + * instantiation. + */ + virtual Node rewriteInstantiation(Node q, + std::vector<Node>& terms, + Node inst, + bool doVts) = 0; +}; + /** Instantiate * * This class is used for generating instantiation lemmas. It maintains an @@ -103,7 +129,7 @@ class Instantiate : public QuantifiersUtil /** check incomplete */ bool checkComplete() override; - //--------------------------------------notify objects + //--------------------------------------notify/rewrite objects /** add instantiation notify * * Adds an instantiation notify class to listen to the instantiations reported @@ -112,6 +138,8 @@ class Instantiate : public QuantifiersUtil void addNotify(InstantiationNotify* in); /** get number of instantiation notify added to this class */ bool hasNotify() const { return !d_inst_notify.empty(); } + /** add instantiation rewriter */ + void addRewriter(InstantiationRewriter* ir); /** notify flush lemmas * * This is called just before the quantifiers engine flushes its lemmas to @@ -342,6 +370,8 @@ class Instantiate : public QuantifiersUtil TermUtil* d_term_util; /** instantiation notify classes */ std::vector<InstantiationNotify*> d_inst_notify; + /** instantiation rewriter classes */ + std::vector<InstantiationRewriter*> d_instRewrite; /** statistics for debugging total instantiation */ int d_total_inst_count_debug; |