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
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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 <map>
+#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
#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"
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)
{
#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
#include <map>
-#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
projects / cvc5.git / commitdiff