From f48d8d6a1bc2b42608c0d9b1e5ad2cc091cb8d99 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 25 Jan 2021 08:59:18 -0600 Subject: [PATCH] Split E-matching strategies to own files (#5807) Code move + format only --- src/CMakeLists.txt | 3 + .../quantifiers/ematching/inst_strategy.h | 66 +++++++ .../ematching/inst_strategy_e_matching.cpp | 137 ++------------ .../ematching/inst_strategy_e_matching.h | 40 +--- .../inst_strategy_e_matching_user.cpp | 178 ++++++++++++++++++ .../ematching/inst_strategy_e_matching_user.h | 64 +++++++ .../ematching/instantiation_engine.cpp | 12 +- .../ematching/instantiation_engine.h | 25 +-- 8 files changed, 340 insertions(+), 185 deletions(-) create mode 100644 src/theory/quantifiers/ematching/inst_strategy.h create mode 100644 src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp create mode 100644 src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 632adae1e..60e79fbe3 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -658,8 +658,11 @@ libcvc4_add_sources( 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 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 +#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 */ diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 8947370cd..8091eded5 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -13,24 +13,16 @@ **/ #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 : @@ -65,116 +57,6 @@ struct sortTriggers { } }; -void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort ){ - Trace("inst-alg-debug") << "reset user triggers" << std::endl; - //reset triggers - for (std::pair >& 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 >& 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& 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) @@ -212,11 +94,14 @@ void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort 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) @@ -224,7 +109,7 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) : 1; if (e < peffort) { - return STATUS_UNFINISHED; + return InstStrategyStatus::STATUS_UNFINISHED; } Trace("inst-alg") << "-> Auto-gen instantiate " << f << "..." << std::endl; bool gen = false; @@ -328,7 +213,7 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) break; } } - return STATUS_UNKNOWN; + return InstStrategyStatus::STATUS_UNKNOWN; } void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h index 701d4ac74..d3c7c2c67 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h @@ -17,7 +17,7 @@ #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" @@ -25,35 +25,11 @@ namespace CVC4 { 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: @@ -91,7 +67,8 @@ class InstStrategyAutoGenTriggers : public InstStrategy 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. */ @@ -111,7 +88,6 @@ class InstStrategyAutoGenTriggers : public InstStrategy InstStrategyAutoGenTriggers(QuantifiersEngine* qe, QuantRelevance* qr); ~InstStrategyAutoGenTriggers() {} - public: /** get auto-generated trigger */ inst::Trigger* getAutoGenTrigger(Node q); /** identify */ diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp new file mode 100644 index 000000000..f7f2531bb --- /dev/null +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp @@ -0,0 +1,178 @@ +/********************* */ +/*! \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 >::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 >::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 >& 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 >& 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& 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 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 diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h new file mode 100644 index 000000000..ed0cd0ac6 --- /dev/null +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h @@ -0,0 +1,64 @@ +/********************* */ +/*! \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 +#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 > d_user_gen; + /** waiting to be generated patterns */ + std::map > > d_user_gen_wait; + /** counter for quantifiers */ + std::map d_counter; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index ad9c53e0f..7eb5a1378 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -16,6 +16,7 @@ #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" @@ -91,11 +92,16 @@ void InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ for( unsigned j=0; jidentify() << " " << 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; } } diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index f2f013f1c..9304c84ae 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -19,6 +19,7 @@ #include +#include "theory/quantifiers/ematching/inst_strategy.h" #include "theory/quantifiers/quant_relevance.h" #include "theory/quantifiers/quant_util.h" @@ -28,30 +29,6 @@ namespace quantifiers { 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: -- 2.30.2