From 6cbb7824dabd7ab8e85472a22ba30ad2498afebc Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 15 Mar 2021 13:53:33 -0500 Subject: [PATCH] Split inst match generator class to own file (#6125) --- src/CMakeLists.txt | 2 + .../quantifiers/ematching/im_generator.cpp | 43 ++++++ .../quantifiers/ematching/im_generator.h | 123 ++++++++++++++++++ .../ematching/inst_match_generator.cpp | 16 --- .../ematching/inst_match_generator.h | 94 +------------ 5 files changed, 170 insertions(+), 108 deletions(-) create mode 100644 src/theory/quantifiers/ematching/im_generator.cpp create mode 100644 src/theory/quantifiers/ematching/im_generator.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index e65e06da3..042969884 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -669,6 +669,8 @@ libcvc4_add_sources( theory/quantifiers/ematching/candidate_generator.h theory/quantifiers/ematching/ho_trigger.cpp theory/quantifiers/ematching/ho_trigger.h + theory/quantifiers/ematching/im_generator.cpp + theory/quantifiers/ematching/im_generator.h theory/quantifiers/ematching/inst_match_generator.cpp theory/quantifiers/ematching/inst_match_generator.h theory/quantifiers/ematching/inst_match_generator_multi.cpp diff --git a/src/theory/quantifiers/ematching/im_generator.cpp b/src/theory/quantifiers/ematching/im_generator.cpp new file mode 100644 index 000000000..829ccc8b1 --- /dev/null +++ b/src/theory/quantifiers/ematching/im_generator.cpp @@ -0,0 +1,43 @@ +/********************* */ +/*! \file im_generator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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 Implementation of inst match generator base class + **/ + +#include "theory/quantifiers/ematching/im_generator.h" + +#include "theory/quantifiers/ematching/trigger.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace inst { + +IMGenerator::IMGenerator(Trigger* tparent) + : d_tparent(tparent), d_qstate(tparent->d_qstate) +{ +} + +bool IMGenerator::sendInstantiation(InstMatch& m, InferenceId id) +{ + return d_tparent->sendInstantiation(m, id); +} + +QuantifiersEngine* IMGenerator::getQuantifiersEngine() +{ + return d_tparent->d_quantEngine; +} + + +}/* CVC4::theory::inst namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/quantifiers/ematching/im_generator.h b/src/theory/quantifiers/ematching/im_generator.h new file mode 100644 index 000000000..6bf472cb5 --- /dev/null +++ b/src/theory/quantifiers/ematching/im_generator.h @@ -0,0 +1,123 @@ +/********************* */ +/*! \file inst_match_generator.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Mathias Preiner, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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 inst match generator base class + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__IM_GENERATOR_H +#define CVC4__THEORY__QUANTIFIERS__IM_GENERATOR_H + +#include +#include "expr/node.h" +#include "theory/inference_id.h" +#include "theory/quantifiers/inst_match.h" + +namespace CVC4 { +namespace theory { + +class QuantifiersEngine; + +namespace quantifiers { +class QuantifiersState; +} // namespace quantifiers + +namespace inst { + +class Trigger; + +/** IMGenerator class +* +* Virtual base class for generating InstMatch objects, which correspond to +* quantifier instantiations. The main use of this class is as a backend utility +* to Trigger (see theory/quantifiers/ematching/trigger.h). +* +* Some functions below take as argument a pointer to the current quantifiers +* engine, which is used for making various queries about what terms and +* equalities exist in the current context. +* +* Some functions below take a pointer to a parent Trigger object, which is used +* to post-process and finalize the instantiations through +* sendInstantiation(...), where the parent trigger will make calls to +* qe->getInstantiate()->addInstantiation(...). The latter function is the entry +* point in which instantiate lemmas are enqueued to be sent on the output +* channel. +*/ +class IMGenerator { +public: + IMGenerator(Trigger* tparent); + virtual ~IMGenerator() {} + /** Reset instantiation round. + * + * Called once at beginning of an instantiation round. + */ + virtual void resetInstantiationRound() {} + /** Reset. + * + * eqc is the equivalence class to search in (any if eqc=null). + * Returns true if this generator can produce instantiations, and false + * otherwise. An example of when it returns false is if it can be determined + * that no appropriate matchable terms occur based on eqc. + */ + virtual bool reset(Node eqc) { return true; } + /** Get the next match. + * + * Must call reset( eqc ) before this function. This constructs an + * instantiation, which it populates in data structure m, + * based on the current context using the implemented matching algorithm. + * + * q is the quantified formula we are adding instantiations for + * m is the InstMatch object we are generating + * + * Returns a value >0 if an instantiation was successfully generated + */ + virtual int getNextMatch(Node q, InstMatch& m) { return 0; } + /** add instantiations + * + * This adds all available instantiations for q based on the current context + * using the implemented matching algorithm. It typically is implemented as a + * fixed point of getNextMatch above. + * + * It returns the number of instantiations added using calls to + * Instantiate::addInstantiation(...). + */ + virtual uint64_t addInstantiations(Node q) { return 0; } + /** get active score + * + * A heuristic value indicating how active this generator is. + */ + virtual int getActiveScore() { return 0; } + +protected: + /** send instantiation + * + * This method sends instantiation, specified by m, to the parent trigger + * object, which will in turn make a call to + * Instantiate::addInstantiation(...). This method returns true if a + * call to Instantiate::addInstantiation(...) was successfully made, + * indicating that an instantiation was enqueued in the quantifier engine's + * lemma cache. + */ + bool sendInstantiation(InstMatch& m, InferenceId id); + /** The parent trigger that owns this */ + Trigger* d_tparent; + /** The state of the quantifiers engine */ + quantifiers::QuantifiersState& d_qstate; + // !!!!!!!!! temporarily available (project #15) + QuantifiersEngine* getQuantifiersEngine(); +};/* class IMGenerator */ + +} +} +} + +#endif diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 584b3ebbf..5f47f70c3 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -22,7 +22,6 @@ #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h" #include "theory/quantifiers/ematching/inst_match_generator_simple.h" #include "theory/quantifiers/ematching/pattern_term_selector.h" -#include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/ematching/var_match_generator.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_state.h" @@ -36,21 +35,6 @@ namespace CVC4 { namespace theory { namespace inst { -IMGenerator::IMGenerator(Trigger* tparent) - : d_tparent(tparent), d_qstate(tparent->d_qstate) -{ -} - -bool IMGenerator::sendInstantiation(InstMatch& m, InferenceId id) -{ - return d_tparent->sendInstantiation(m, id); -} - -QuantifiersEngine* IMGenerator::getQuantifiersEngine() -{ - return d_tparent->d_quantEngine; -} - InstMatchGenerator::InstMatchGenerator(Trigger* tparent, Node pat) : IMGenerator(tparent) { diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index 99414c90d..3f6976ca7 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -18,104 +18,14 @@ #define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H #include -#include "expr/node_trie.h" -#include "theory/inference_id.h" +#include "expr/node.h" #include "theory/quantifiers/inst_match.h" +#include "theory/quantifiers/ematching/im_generator.h" namespace CVC4 { namespace theory { - -class QuantifiersEngine; - -namespace quantifiers { -class QuantifiersState; -} // namespace quantifiers - namespace inst { -class Trigger; - -/** IMGenerator class -* -* Virtual base class for generating InstMatch objects, which correspond to -* quantifier instantiations. The main use of this class is as a backend utility -* to Trigger (see theory/quantifiers/ematching/trigger.h). -* -* Some functions below take as argument a pointer to the current quantifiers -* engine, which is used for making various queries about what terms and -* equalities exist in the current context. -* -* Some functions below take a pointer to a parent Trigger object, which is used -* to post-process and finalize the instantiations through -* sendInstantiation(...), where the parent trigger will make calls to -* qe->getInstantiate()->addInstantiation(...). The latter function is the entry -* point in which instantiate lemmas are enqueued to be sent on the output -* channel. -*/ -class IMGenerator { -public: - IMGenerator(Trigger* tparent); - virtual ~IMGenerator() {} - /** Reset instantiation round. - * - * Called once at beginning of an instantiation round. - */ - virtual void resetInstantiationRound() {} - /** Reset. - * - * eqc is the equivalence class to search in (any if eqc=null). - * Returns true if this generator can produce instantiations, and false - * otherwise. An example of when it returns false is if it can be determined - * that no appropriate matchable terms occur based on eqc. - */ - virtual bool reset(Node eqc) { return true; } - /** Get the next match. - * - * Must call reset( eqc ) before this function. This constructs an - * instantiation, which it populates in data structure m, - * based on the current context using the implemented matching algorithm. - * - * q is the quantified formula we are adding instantiations for - * m is the InstMatch object we are generating - * - * Returns a value >0 if an instantiation was successfully generated - */ - virtual int getNextMatch(Node q, InstMatch& m) { return 0; } - /** add instantiations - * - * This add all available instantiations for q based on the current context - * using the implemented matching algorithm. It typically is implemented as a - * fixed point of getNextMatch above. - * - * It returns the number of instantiations added using calls to calls to - * Instantiate::addInstantiation(...). - */ - virtual uint64_t addInstantiations(Node q) { return 0; } - /** get active score - * - * A heuristic value indicating how active this generator is. - */ - virtual int getActiveScore() { return 0; } - -protected: - /** send instantiation - * - * This method sends instantiation, specified by m, to the parent trigger - * object, which will in turn make a call to - * Instantiate::addInstantiation(...). This method returns true if a - * call to Instantiate::addInstantiation(...) was successfully made, - * indicating that an instantiation was enqueued in the quantifier engine's - * lemma cache. - */ - bool sendInstantiation(InstMatch& m, InferenceId id); - /** The parent trigger that owns this */ - Trigger* d_tparent; - /** The state of the quantifiers engine */ - quantifiers::QuantifiersState& d_qstate; - // !!!!!!!!! temporarily available (project #15) - QuantifiersEngine* getQuantifiersEngine(); -};/* class IMGenerator */ - class CandidateGenerator; /** InstMatchGenerator class -- 2.30.2