theory/quantifiers/ematching/ho_trigger.h
theory/quantifiers/ematching/inst_match_generator.cpp
theory/quantifiers/ematching/inst_match_generator.h
+ theory/quantifiers/ematching/inst_strategy.h
theory/quantifiers/ematching/inst_strategy_e_matching.cpp
theory/quantifiers/ematching/inst_strategy_e_matching.h
+ theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
+ theory/quantifiers/ematching/inst_strategy_e_matching_user.h
theory/quantifiers/ematching/instantiation_engine.cpp
theory/quantifiers/ematching/instantiation_engine.h
theory/quantifiers/ematching/trigger.cpp
--- /dev/null
+/********************* */
+/*! \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 */
**/
#include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
-#include "theory/quantifiers/ematching/inst_match_generator.h"
+
#include "theory/quantifiers/quant_relevance.h"
-#include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
-#include "theory/theory_engine.h"
#include "util/random.h"
-namespace CVC4 {
-
-using namespace kind;
-using namespace context;
+using namespace CVC4::kind;
+using namespace CVC4::theory::inst;
+namespace CVC4 {
namespace theory {
-
-using namespace inst;
-
namespace quantifiers {
//priority levels :
}
};
-void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort ){
- Trace("inst-alg-debug") << "reset user triggers" << std::endl;
- //reset triggers
- for (std::pair<const Node, std::vector<Trigger*> >& u : d_user_gen)
- {
- for (Trigger* t : u.second)
- {
- t->resetInstantiationRound();
- t->reset(Node::null());
- }
- }
- Trace("inst-alg-debug") << "done reset user triggers" << std::endl;
-}
-
-int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
- if( e==0 ){
- return STATUS_UNFINISHED;
- }
- options::UserPatMode upm = d_quantEngine->getInstUserPatMode();
- int peffort = upm == options::UserPatMode::RESORT ? 2 : 1;
- if (e < peffort)
- {
- return STATUS_UNFINISHED;
- }
- if (e != peffort)
- {
- return STATUS_UNKNOWN;
- }
- d_counter[f]++;
-
- Trace("inst-alg") << "-> User-provided instantiate " << f << "..."
- << std::endl;
- if (upm == options::UserPatMode::RESORT)
- {
- std::vector<std::vector<Node> >& ugw = d_user_gen_wait[f];
- for (size_t i = 0, usize = ugw.size(); i < usize; i++)
- {
- Trigger* t = Trigger::mkTrigger(
- d_quantEngine, f, ugw[i], true, Trigger::TR_RETURN_NULL);
- if (t)
- {
- d_user_gen[f].push_back(t);
- }
- }
- ugw.clear();
- }
-
- std::vector<inst::Trigger*>& ug = d_user_gen[f];
- for (Trigger* t : ug)
- {
- if (Trace.isOn("process-trigger"))
- {
- Trace("process-trigger") << " Process (user) ";
- t->debugPrint("process-trigger");
- Trace("process-trigger") << "..." << std::endl;
- }
- unsigned numInst = t->addInstantiations();
- Trace("process-trigger")
- << " Done, numInst = " << numInst << "." << std::endl;
- d_quantEngine->d_statistics.d_instantiations_user_patterns += numInst;
- if (t->isMultiTrigger())
- {
- d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
- }
- if (d_quantEngine->inConflict())
- {
- // we are already in conflict
- break;
- }
- }
- return STATUS_UNKNOWN;
-}
-
-void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){
- Assert(pat.getKind() == INST_PATTERN);
- //add to generators
- std::vector< Node > nodes;
- for (const Node& p : pat)
- {
- Node pat_use = Trigger::getIsUsableTrigger(p, q);
- if( pat_use.isNull() ){
- Trace("trigger-warn") << "User-provided trigger is not usable : " << pat
- << " because of " << p << std::endl;
- return;
- }else{
- nodes.push_back( pat_use );
- }
- }
- Trace("user-pat") << "Add user pattern: " << pat << " for " << q << std::endl;
- // check match option
- if (d_quantEngine->getInstUserPatMode() == options::UserPatMode::RESORT)
- {
- d_user_gen_wait[q].push_back(nodes);
- }
- else
- {
- Trigger* t =
- Trigger::mkTrigger(d_quantEngine, q, nodes, true, Trigger::TR_MAKE_NEW);
- if (t)
- {
- d_user_gen[q].push_back(t);
- }
- else
- {
- Trace("trigger-warn") << "Failed to construct trigger : " << pat
- << " due to variable mismatch" << std::endl;
- }
- }
-}
-
InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers(QuantifiersEngine* qe,
QuantRelevance* qr)
: InstStrategy(qe), d_quant_rel(qr)
Trace("inst-alg-debug") << "done reset auto-gen triggers" << std::endl;
}
-int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){
+InstStrategyStatus InstStrategyAutoGenTriggers::process(Node f,
+ Theory::Effort effort,
+ int e)
+{
options::UserPatMode upMode = d_quantEngine->getInstUserPatMode();
if (hasUserPatterns(f) && upMode == options::UserPatMode::TRUST)
{
- return STATUS_UNKNOWN;
+ return InstStrategyStatus::STATUS_UNKNOWN;
}
int peffort = (hasUserPatterns(f) && upMode != options::UserPatMode::IGNORE
&& upMode != options::UserPatMode::RESORT)
: 1;
if (e < peffort)
{
- return STATUS_UNFINISHED;
+ return InstStrategyStatus::STATUS_UNFINISHED;
}
Trace("inst-alg") << "-> Auto-gen instantiate " << f << "..." << std::endl;
bool gen = false;
break;
}
}
- return STATUS_UNKNOWN;
+ return InstStrategyStatus::STATUS_UNKNOWN;
}
void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
#ifndef CVC4__INST_STRATEGY_E_MATCHING_H
#define CVC4__INST_STRATEGY_E_MATCHING_H
-#include "theory/quantifiers/ematching/instantiation_engine.h"
+#include "theory/quantifiers/ematching/inst_strategy.h"
#include "theory/quantifiers/ematching/trigger.h"
#include "theory/quantifiers/quant_relevance.h"
namespace theory {
namespace quantifiers {
-//instantiation strategies
-
-class InstStrategyUserPatterns : public InstStrategy{
-private:
- /** explicitly provided patterns */
- std::map< Node, std::vector< inst::Trigger* > > d_user_gen;
- /** waiting to be generated patterns */
- std::map< Node, std::vector< std::vector< Node > > > d_user_gen_wait;
- /** counter for quantifiers */
- std::map< Node, int > d_counter;
- /** process functions */
- void processResetInstantiationRound(Theory::Effort effort) override;
- int process(Node f, Theory::Effort effort, int e) override;
-
- public:
- InstStrategyUserPatterns( QuantifiersEngine* ie ) :
- InstStrategy( ie ){}
- ~InstStrategyUserPatterns(){}
-public:
- /** add pattern */
- void addUserPattern( Node q, Node pat );
- /** get num patterns */
- size_t getNumUserGenerators(Node q) { return d_user_gen[q].size(); }
- /** get user pattern */
- inst::Trigger* getUserGenerator(Node q, size_t i) { return d_user_gen[q][i]; }
- /** identify */
- std::string identify() const override { return std::string("UserPatterns"); }
-};/* class InstStrategyUserPatterns */
-
+/**
+ * This class is responsible for instantiating quantifiers based on
+ * automatically generated triggers. It selects pattern terms, generates
+ * and manages triggers, and uses a strategy for processing them.
+ */
class InstStrategyAutoGenTriggers : public InstStrategy
{
public:
private:
/** process functions */
void processResetInstantiationRound(Theory::Effort effort) override;
- int process(Node q, Theory::Effort effort, int e) override;
+ /** Process */
+ InstStrategyStatus process(Node q, Theory::Effort effort, int e) override;
/**
* Generate triggers for quantified formula q.
*/
InstStrategyAutoGenTriggers(QuantifiersEngine* qe, QuantRelevance* qr);
~InstStrategyAutoGenTriggers() {}
- public:
/** get auto-generated trigger */
inst::Trigger* getAutoGenTrigger(Node q);
/** identify */
--- /dev/null
+/********************* */
+/*! \file inst_strategy_e_matching_user.cpp
+ ** \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 Implementation of e matching instantiation strategies
+ **/
+
+#include "theory/quantifiers/ematching/inst_strategy_e_matching_user.h"
+
+#include "theory/quantifiers_engine.h"
+
+using namespace CVC4::kind;
+using namespace CVC4::theory::inst;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+InstStrategyUserPatterns::InstStrategyUserPatterns(QuantifiersEngine* ie)
+ : InstStrategy(ie)
+{
+}
+InstStrategyUserPatterns::~InstStrategyUserPatterns() {}
+
+size_t InstStrategyUserPatterns::getNumUserGenerators(Node q) const
+{
+ std::map<Node, std::vector<inst::Trigger*> >::const_iterator it =
+ d_user_gen.find(q);
+ if (it == d_user_gen.end())
+ {
+ return 0;
+ }
+ return it->second.size();
+}
+
+inst::Trigger* InstStrategyUserPatterns::getUserGenerator(Node q,
+ size_t i) const
+{
+ std::map<Node, std::vector<inst::Trigger*> >::const_iterator it =
+ d_user_gen.find(q);
+ if (it == d_user_gen.end())
+ {
+ return nullptr;
+ }
+ Assert(i < it->second.size());
+ return it->second[i];
+}
+
+std::string InstStrategyUserPatterns::identify() const
+{
+ return std::string("UserPatterns");
+}
+
+void InstStrategyUserPatterns::processResetInstantiationRound(
+ Theory::Effort effort)
+{
+ Trace("inst-alg-debug") << "reset user triggers" << std::endl;
+ // reset triggers
+ for (std::pair<const Node, std::vector<Trigger*> >& u : d_user_gen)
+ {
+ for (Trigger* t : u.second)
+ {
+ t->resetInstantiationRound();
+ t->reset(Node::null());
+ }
+ }
+ Trace("inst-alg-debug") << "done reset user triggers" << std::endl;
+}
+
+InstStrategyStatus InstStrategyUserPatterns::process(Node q,
+ Theory::Effort effort,
+ int e)
+{
+ if (e == 0)
+ {
+ return InstStrategyStatus::STATUS_UNFINISHED;
+ }
+ options::UserPatMode upm = d_quantEngine->getInstUserPatMode();
+ int peffort = upm == options::UserPatMode::RESORT ? 2 : 1;
+ if (e < peffort)
+ {
+ return InstStrategyStatus::STATUS_UNFINISHED;
+ }
+ if (e != peffort)
+ {
+ return InstStrategyStatus::STATUS_UNKNOWN;
+ }
+ d_counter[q]++;
+
+ Trace("inst-alg") << "-> User-provided instantiate " << q << "..."
+ << std::endl;
+ if (upm == options::UserPatMode::RESORT)
+ {
+ std::vector<std::vector<Node> >& ugw = d_user_gen_wait[q];
+ for (size_t i = 0, usize = ugw.size(); i < usize; i++)
+ {
+ Trigger* t = Trigger::mkTrigger(
+ d_quantEngine, q, ugw[i], true, Trigger::TR_RETURN_NULL);
+ if (t)
+ {
+ d_user_gen[q].push_back(t);
+ }
+ }
+ ugw.clear();
+ }
+
+ std::vector<inst::Trigger*>& ug = d_user_gen[q];
+ for (Trigger* t : ug)
+ {
+ if (Trace.isOn("process-trigger"))
+ {
+ Trace("process-trigger") << " Process (user) ";
+ t->debugPrint("process-trigger");
+ Trace("process-trigger") << "..." << std::endl;
+ }
+ unsigned numInst = t->addInstantiations();
+ Trace("process-trigger")
+ << " Done, numInst = " << numInst << "." << std::endl;
+ d_quantEngine->d_statistics.d_instantiations_user_patterns += numInst;
+ if (t->isMultiTrigger())
+ {
+ d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
+ }
+ if (d_quantEngine->inConflict())
+ {
+ // we are already in conflict
+ break;
+ }
+ }
+ return InstStrategyStatus::STATUS_UNKNOWN;
+}
+
+void InstStrategyUserPatterns::addUserPattern(Node q, Node pat)
+{
+ Assert(pat.getKind() == INST_PATTERN);
+ // add to generators
+ std::vector<Node> nodes;
+ for (const Node& p : pat)
+ {
+ Node pat_use = Trigger::getIsUsableTrigger(p, q);
+ if (pat_use.isNull())
+ {
+ Trace("trigger-warn") << "User-provided trigger is not usable : " << pat
+ << " because of " << p << std::endl;
+ return;
+ }
+ nodes.push_back(pat_use);
+ }
+ Trace("user-pat") << "Add user pattern: " << pat << " for " << q << std::endl;
+ // check match option
+ if (d_quantEngine->getInstUserPatMode() == options::UserPatMode::RESORT)
+ {
+ d_user_gen_wait[q].push_back(nodes);
+ return;
+ }
+ Trigger* t =
+ Trigger::mkTrigger(d_quantEngine, q, nodes, true, Trigger::TR_MAKE_NEW);
+ if (t)
+ {
+ d_user_gen[q].push_back(t);
+ }
+ else
+ {
+ Trace("trigger-warn") << "Failed to construct trigger : " << pat
+ << " due to variable mismatch" << std::endl;
+ }
+}
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file inst_strategy_e_matching_user.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Morgan Deters, Andrew Reynolds, 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 The user-provided E matching instantiation strategy
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__INST_STRATEGY_E_MATCHING_USER_H
+#define CVC4__INST_STRATEGY_E_MATCHING_USER_H
+
+#include <map>
+#include "expr/node.h"
+#include "theory/quantifiers/ematching/inst_strategy.h"
+#include "theory/quantifiers/ematching/trigger.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/**
+ * This class is responsible for adding instantiations based on user-provided
+ * triggers.
+ */
+class InstStrategyUserPatterns : public InstStrategy
+{
+ public:
+ InstStrategyUserPatterns(QuantifiersEngine* qe);
+ ~InstStrategyUserPatterns();
+ /** add pattern */
+ void addUserPattern(Node q, Node pat);
+ /** get num patterns */
+ size_t getNumUserGenerators(Node q) const;
+ /** get user pattern */
+ inst::Trigger* getUserGenerator(Node q, size_t i) const;
+ /** identify */
+ std::string identify() const override;
+
+ private:
+ /** reset instantiation round for the given effort */
+ void processResetInstantiationRound(Theory::Effort effort) override;
+ /** Process quantified formula q at the given effort */
+ InstStrategyStatus process(Node f, Theory::Effort effort, int e) override;
+ /** explicitly provided patterns */
+ std::map<Node, std::vector<inst::Trigger*> > d_user_gen;
+ /** waiting to be generated patterns */
+ std::map<Node, std::vector<std::vector<Node> > > d_user_gen_wait;
+ /** counter for quantifiers */
+ std::map<Node, int> d_counter;
+};
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
+
+#endif
#include "options/quantifiers_options.h"
#include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
+#include "theory/quantifiers/ematching/inst_strategy_e_matching_user.h"
#include "theory/quantifiers/ematching/trigger.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/quantifiers_attributes.h"
for( unsigned j=0; j<d_instStrategies.size(); j++ ){
InstStrategy* is = d_instStrategies[j];
Trace("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl;
- int quantStatus = is->process( q, effort, e_use );
- Trace("inst-engine-debug") << " -> status is " << quantStatus << ", conflict=" << d_quantEngine->inConflict() << std::endl;
+ InstStrategyStatus quantStatus = is->process(q, effort, e_use);
+ Trace("inst-engine-debug")
+ << " -> unfinished= "
+ << (quantStatus == InstStrategyStatus::STATUS_UNFINISHED)
+ << ", conflict=" << d_quantEngine->inConflict() << std::endl;
if( d_quantEngine->inConflict() ){
return;
- }else if( quantStatus==InstStrategy::STATUS_UNFINISHED ){
+ }
+ else if (quantStatus == InstStrategyStatus::STATUS_UNFINISHED)
+ {
finished = false;
}
}
#include <vector>
+#include "theory/quantifiers/ematching/inst_strategy.h"
#include "theory/quantifiers/quant_relevance.h"
#include "theory/quantifiers/quant_util.h"
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:
projects / cvc5.git / commitdiff