From 1c0d2738941e948d67c696e0c96e3463da9807d2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 13 Apr 2021 16:33:07 -0500 Subject: [PATCH] Add pool instantiation strategy (#6308) Adds an instantiation strategy based on user-provided pool annotations. The next PR will connect this to quantifiers engine. --- src/CMakeLists.txt | 2 + src/options/quantifiers_options.toml | 8 + src/theory/inference_id.cpp | 1 + src/theory/inference_id.h | 2 + src/theory/quantifiers/inst_strategy_pool.cpp | 168 ++++++++++++++++++ src/theory/quantifiers/inst_strategy_pool.h | 73 ++++++++ src/theory/quantifiers/quant_util.h | 4 +- .../quantifiers/quantifiers_modules.cpp | 6 + src/theory/quantifiers/quantifiers_modules.h | 3 + .../quantifiers/term_tuple_enumerator.cpp | 50 ++++++ .../quantifiers/term_tuple_enumerator.h | 5 + 11 files changed, 320 insertions(+), 2 deletions(-) create mode 100644 src/theory/quantifiers/inst_strategy_pool.cpp create mode 100644 src/theory/quantifiers/inst_strategy_pool.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c33110cc3..ee59d5d31 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -745,6 +745,8 @@ libcvc4_add_sources( theory/quantifiers/inst_match_trie.h theory/quantifiers/inst_strategy_enumerative.cpp theory/quantifiers/inst_strategy_enumerative.h + theory/quantifiers/inst_strategy_pool.cpp + theory/quantifiers/inst_strategy_pool.h theory/quantifiers/instantiate.cpp theory/quantifiers/instantiate.h theory/quantifiers/instantiation_list.cpp diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index db7100e9c..bbdf030a1 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -586,6 +586,14 @@ header = "options/quantifiers_options.h" name = "agg" help = "Consider the phase requirements aggressively for all triggers." +[[option]] + name = "poolInst" + category = "regular" + long = "pool-inst" + type = "bool" + default = "true" + help = "pool-based instantiation: instantiate with ground terms occurring in user-specified pools" + ### Finite model finding options [[option]] diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index c1c751800..ceca32a8d 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -174,6 +174,7 @@ const char* toString(InferenceId i) case InferenceId::QUANTIFIERS_INST_CEGQI: return "QUANTIFIERS_INST_CEGQI"; case InferenceId::QUANTIFIERS_INST_SYQI: return "QUANTIFIERS_INST_SYQI"; case InferenceId::QUANTIFIERS_INST_ENUM: return "QUANTIFIERS_INST_ENUM"; + case InferenceId::QUANTIFIERS_INST_POOL: return "QUANTIFIERS_INST_POOL"; case InferenceId::QUANTIFIERS_BINT_PROXY: return "QUANTIFIERS_BINT_PROXY"; case InferenceId::QUANTIFIERS_BINT_MIN_NG: return "QUANTIFIERS_BINT_MIN_NG"; case InferenceId::QUANTIFIERS_CEGQI_CEX: return "QUANTIFIERS_CEGQI_CEX"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 985d90738..7730a7d14 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -265,6 +265,8 @@ enum class InferenceId QUANTIFIERS_INST_SYQI, // instantiations from enumerative instantiation QUANTIFIERS_INST_ENUM, + // instantiations from pool instantiation + QUANTIFIERS_INST_POOL, //-------------------- bounded integers // a proxy lemma from bounded integers, used to control bounds on ground terms QUANTIFIERS_BINT_PROXY, diff --git a/src/theory/quantifiers/inst_strategy_pool.cpp b/src/theory/quantifiers/inst_strategy_pool.cpp new file mode 100644 index 000000000..0e32c246e --- /dev/null +++ b/src/theory/quantifiers/inst_strategy_pool.cpp @@ -0,0 +1,168 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 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. + * **************************************************************************** + * + * Pool-based instantiation strategy + */ + +#include "theory/quantifiers/inst_strategy_pool.h" + +#include "options/quantifiers_options.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/instantiate.h" +#include "theory/quantifiers/quantifiers_inference_manager.h" +#include "theory/quantifiers/term_pools.h" +#include "theory/quantifiers/term_registry.h" +#include "theory/quantifiers/term_tuple_enumerator.h" + +using namespace cvc5::kind; +using namespace cvc5::context; + +namespace cvc5 { +namespace theory { +namespace quantifiers { + +InstStrategyPool::InstStrategyPool(QuantifiersState& qs, + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, + TermRegistry& tr) + : QuantifiersModule(qs, qim, qr, tr) +{ +} + +void InstStrategyPool::presolve() {} + +bool InstStrategyPool::needsCheck(Theory::Effort e) +{ + return d_qstate.getInstWhenNeedsCheck(e); +} + +void InstStrategyPool::reset_round(Theory::Effort e) {} + +void InstStrategyPool::registerQuantifier(Node q) +{ + // take into account user pools + if (q.getNumChildren() == 3) + { + Node subsPat = d_qreg.substituteBoundVariablesToInstConstants(q[2], q); + // add patterns + for (const Node& p : subsPat) + { + if (p.getKind() == INST_POOL) + { + d_userPools[q].push_back(p); + } + } + } +} + +void InstStrategyPool::check(Theory::Effort e, QEffort quant_e) +{ + if (d_userPools.empty()) + { + return; + } + double clSet = 0; + if (Trace.isOn("pool-engine")) + { + clSet = double(clock()) / double(CLOCKS_PER_SEC); + Trace("pool-engine") << "---Pool instantiation, effort = " << e << "---" + << std::endl; + } + FirstOrderModel* fm = d_treg.getModel(); + bool inConflict = false; + uint64_t addedLemmas = 0; + size_t nquant = fm->getNumAssertedQuantifiers(); + std::map >::iterator uit; + for (size_t i = 0; i < nquant; i++) + { + Node q = fm->getAssertedQuantifier(i, true); + uit = d_userPools.find(q); + if (uit == d_userPools.end()) + { + // no user pools for this + continue; + } + if (!d_qreg.hasOwnership(q, this) || !fm->isQuantifierActive(q)) + { + // quantified formula is not owned by this or is inactive + continue; + } + // process with each user pool + for (const Node& p : uit->second) + { + inConflict = process(q, p, addedLemmas); + if (inConflict) + { + break; + } + } + if (inConflict) + { + break; + } + } + if (Trace.isOn("pool-engine")) + { + Trace("pool-engine") << "Added lemmas = " << addedLemmas << std::endl; + double clSet2 = double(clock()) / double(CLOCKS_PER_SEC); + Trace("pool-engine") << "Finished pool instantiation, time = " + << (clSet2 - clSet) << std::endl; + } +} + +std::string InstStrategyPool::identify() const +{ + return std::string("InstStrategyPool"); +} + +bool InstStrategyPool::process(Node q, Node p, uint64_t& addedLemmas) +{ + TermTupleEnumeratorEnv ttec; + ttec.d_fullEffort = true; + ttec.d_increaseSum = options::fullSaturateSum(); + TermPools* tp = d_treg.getTermPools(); + std::shared_ptr enumerator( + mkTermTupleEnumeratorPool(q, &ttec, tp, p)); + Instantiate* ie = d_qim.getInstantiate(); + std::vector terms; + std::vector failMask; + // we instantiate exhaustively + enumerator->init(); + while (enumerator->hasNext()) + { + if (d_qstate.isInConflict()) + { + // could be conflicting for an internal reason + return true; + } + enumerator->next(terms); + // try instantiation + failMask.clear(); + if (ie->addInstantiationExpFail( + q, terms, failMask, InferenceId::QUANTIFIERS_INST_POOL)) + { + Trace("pool-inst") << "Success with " << terms << std::endl; + addedLemmas++; + } + else + { + Trace("pool-inst") << "Fail with " << terms << std::endl; + // notify the enumerator of the failure + enumerator->failureReason(failMask); + } + } + return false; +} + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/quantifiers/inst_strategy_pool.h b/src/theory/quantifiers/inst_strategy_pool.h new file mode 100644 index 000000000..e45f08bc2 --- /dev/null +++ b/src/theory/quantifiers/inst_strategy_pool.h @@ -0,0 +1,73 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 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. + * **************************************************************************** + * + * Pool-based instantiation strategy + */ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H +#define CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H + +#include "theory/quantifiers/quant_module.h" + +namespace cvc5 { +namespace theory { +namespace quantifiers { + +/** + * Pool-based instantiation. This implements a strategy for instantiating + * quantifiers based on user-provided pool annotations. + * + * When check is invoked, this strategy considers each + * INST_POOL annotation on quantified formulas. For each annotation, it + * instantiates the associated quantified formula with the Cartesian + * product of terms currently in the pool, using efficient techniques for + * enumerating over tuples of terms, as implemented in the term tuple + * enumerator utilities (see quantifiers/term_tuple_enumerator.h). + */ +class InstStrategyPool : public QuantifiersModule +{ + public: + InstStrategyPool(QuantifiersState& qs, + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, + TermRegistry& tr); + ~InstStrategyPool() {} + /** Presolve */ + void presolve() override; + /** Needs check. */ + bool needsCheck(Theory::Effort e) override; + /** Reset round. */ + void reset_round(Theory::Effort e) override; + /** Register quantified formula q */ + void registerQuantifier(Node q) override; + /** Check. + * Adds instantiations for all currently asserted + * quantified formulas via calls to process(...) + */ + void check(Theory::Effort e, QEffort quant_e) override; + /** Identify. */ + std::string identify() const override; + + private: + /** Process quantified formula with user pool */ + bool process(Node q, Node p, uint64_t& addedLemmas); + /** Map from quantified formulas to user pools */ + std::map > d_userPools; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 + +#endif diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index a70cc2c8e..85c891117 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -43,9 +43,9 @@ public: * Returns false if the reset failed. When reset fails, the utility should * have added a lemma via a call to d_qim.addPendingLemma. */ - virtual bool reset( Theory::Effort e ) = 0; + virtual bool reset(Theory::Effort e) { return true; } /* Called for new quantifiers */ - virtual void registerQuantifier(Node q) = 0; + virtual void registerQuantifier(Node q) {} /** Identify this module (for debugging, dynamic configuration, etc..) */ virtual std::string identify() const = 0; /** Check complete? diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp index a9871d643..704a65bfb 100644 --- a/src/theory/quantifiers/quantifiers_modules.cpp +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -34,6 +34,7 @@ QuantifiersModules::QuantifiersModules() d_sg_gen(nullptr), d_synth_e(nullptr), d_fs(nullptr), + d_ipool(nullptr), d_i_cbqi(nullptr), d_qsplit(nullptr), d_sygus_inst(nullptr) @@ -114,6 +115,11 @@ void QuantifiersModules::initialize(QuantifiersState& qs, d_fs.reset(new InstStrategyEnum(qs, qim, qr, tr, d_rel_dom.get())); modules.push_back(d_fs.get()); } + if (options::poolInst()) + { + d_ipool.reset(new InstStrategyPool(qs, qim, qr, tr)); + modules.push_back(d_ipool.get()); + } if (options::sygusInst()) { d_sygus_inst.reset(new SygusInst(qs, qim, qr, tr)); diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h index d42c60c31..dabee00f9 100644 --- a/src/theory/quantifiers/quantifiers_modules.h +++ b/src/theory/quantifiers/quantifiers_modules.h @@ -26,6 +26,7 @@ #include "theory/quantifiers/fmf/model_builder.h" #include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/inst_strategy_enumerative.h" +#include "theory/quantifiers/inst_strategy_pool.h" #include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/quant_split.h" #include "theory/quantifiers/sygus/synth_engine.h" @@ -85,6 +86,8 @@ class QuantifiersModules std::unique_ptr d_synth_e; /** full saturation */ std::unique_ptr d_fs; + /** pool-based instantiation */ + std::unique_ptr d_ipool; /** counterexample-based quantifier instantiation */ std::unique_ptr d_i_cbqi; /** quantifiers splitting */ diff --git a/src/theory/quantifiers/term_tuple_enumerator.cpp b/src/theory/quantifiers/term_tuple_enumerator.cpp index 169d2afea..4b714419f 100644 --- a/src/theory/quantifiers/term_tuple_enumerator.cpp +++ b/src/theory/quantifiers/term_tuple_enumerator.cpp @@ -28,6 +28,7 @@ #include "theory/quantifiers/index_trie.h" #include "theory/quantifiers/quant_module.h" #include "theory/quantifiers/relevant_domain.h" +#include "theory/quantifiers/term_pools.h" #include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" #include "util/statistics_registry.h" @@ -491,6 +492,48 @@ Node TermTupleEnumeratorBasic::getTerm(size_t variableIx, size_t term_index) return d_termDbList[type_node][term_index]; } +/** + * Enumerate ground terms as they come from a user-provided term pool + */ +class TermTupleEnumeratorPool : public TermTupleEnumeratorBase +{ + public: + TermTupleEnumeratorPool(Node quantifier, + const TermTupleEnumeratorEnv* env, + TermPools* tp, + Node pool) + : TermTupleEnumeratorBase(quantifier, env), d_tp(tp), d_pool(pool) + { + Assert(d_pool.getKind() == kind::INST_POOL); + } + + virtual ~TermTupleEnumeratorPool() = default; + + protected: + /** Pointer to the term pool utility */ + TermPools* d_tp; + /** The pool annotation */ + Node d_pool; + /** a list of terms for each id */ + std::map > d_poolList; + /** gets the terms from the pool */ + size_t prepareTerms(size_t variableIx) override + { + Assert(d_pool.getNumChildren() > variableIx); + // prepare terms from pool + d_poolList[variableIx].clear(); + d_tp->getTermsForPool(d_pool[variableIx], d_poolList[variableIx]); + Trace("pool-inst") << "Instantiation Terms for child " << variableIx << ": " + << d_poolList[variableIx] << std::endl; + return d_poolList[variableIx].size(); + } + Node getTerm(size_t variableIx, size_t term_index) override + { + Assert(term_index < d_poolList[variableIx].size()); + return d_poolList[variableIx][term_index]; + } +}; + TermTupleEnumeratorInterface* mkTermTupleEnumerator( Node q, const TermTupleEnumeratorEnv* env, QuantifiersState& qs, TermDb* td) { @@ -504,6 +547,13 @@ TermTupleEnumeratorInterface* mkTermTupleEnumeratorRd( new TermTupleEnumeratorRD(q, env, rd)); } +TermTupleEnumeratorInterface* mkTermTupleEnumeratorPool( + Node q, const TermTupleEnumeratorEnv* env, TermPools* tp, Node pool) +{ + return static_cast( + new TermTupleEnumeratorPool(q, env, tp, pool)); +} + } // namespace quantifiers } // namespace theory } // namespace cvc5 diff --git a/src/theory/quantifiers/term_tuple_enumerator.h b/src/theory/quantifiers/term_tuple_enumerator.h index c7f71481e..3306ee430 100644 --- a/src/theory/quantifiers/term_tuple_enumerator.h +++ b/src/theory/quantifiers/term_tuple_enumerator.h @@ -24,6 +24,7 @@ namespace cvc5 { namespace theory { namespace quantifiers { +class TermPools; class QuantifiersState; class TermDb; class RelevantDomain; @@ -94,6 +95,10 @@ TermTupleEnumeratorInterface* mkTermTupleEnumerator( TermTupleEnumeratorInterface* mkTermTupleEnumeratorRd( Node q, const TermTupleEnumeratorEnv* env, RelevantDomain* rd); +/** Make term pool enumerator */ +TermTupleEnumeratorInterface* mkTermTupleEnumeratorPool( + Node q, const TermTupleEnumeratorEnv* env, TermPools* tp, Node p); + } // namespace quantifiers } // namespace theory } // namespace cvc5 -- 2.30.2