From 8838a4e8ac47f94089044e2c638376c28a0fd7cd Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 7 Apr 2021 14:30:58 -0500 Subject: [PATCH] Add term pools utility (#6243) This utility will be used to track pools for pool-based instantiation. --- src/CMakeLists.txt | 2 + src/theory/quantifiers/term_pools.cpp | 158 +++++++++++++++++++++++ src/theory/quantifiers/term_pools.h | 107 +++++++++++++++ src/theory/quantifiers/term_registry.cpp | 20 +++ src/theory/quantifiers/term_registry.h | 14 ++ 5 files changed, 301 insertions(+) create mode 100644 src/theory/quantifiers/term_pools.cpp create mode 100644 src/theory/quantifiers/term_pools.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 04ad27b5c..2bcda537c 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -786,6 +786,8 @@ libcvc4_add_sources( theory/quantifiers/skolemize.h theory/quantifiers/solution_filter.cpp theory/quantifiers/solution_filter.h + theory/quantifiers/term_pools.cpp + theory/quantifiers/term_pools.h theory/quantifiers/term_tuple_enumerator.cpp theory/quantifiers/term_tuple_enumerator.h theory/quantifiers/sygus/ce_guided_single_inv.cpp diff --git a/src/theory/quantifiers/term_pools.cpp b/src/theory/quantifiers/term_pools.cpp new file mode 100644 index 000000000..e90fd69b3 --- /dev/null +++ b/src/theory/quantifiers/term_pools.cpp @@ -0,0 +1,158 @@ +/********************* */ +/*! \file term_pools.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** 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 utilities for term enumeration + **/ + +#include "theory/quantifiers/term_pools.h" + +#include "theory/quantifiers/quantifiers_state.h" + +namespace cvc5 { +namespace theory { +namespace quantifiers { + +void TermPoolDomain::initialize() { d_terms.clear(); } +void TermPoolDomain::add(Node n) +{ + if (std::find(d_terms.begin(), d_terms.end(), n) == d_terms.end()) + { + d_terms.push_back(n); + } +} + +void TermPoolQuantInfo::initialize() +{ + d_instAddToPool.clear(); + d_skolemAddToPool.clear(); +} + +TermPools::TermPools(QuantifiersState& qs) : d_qs(qs) {} + +bool TermPools::reset(Theory::Effort e) +{ + for (std::pair& p : d_pools) + { + p.second.d_currTerms.clear(); + } + return true; +} + +void TermPools::registerQuantifier(Node q) +{ + if (q.getNumChildren() < 3) + { + return; + } + TermPoolQuantInfo& qi = d_qinfo[q]; + qi.initialize(); + for (const Node& p : q[2]) + { + Kind pk = p.getKind(); + if (pk == kind::INST_ADD_TO_POOL) + { + qi.d_instAddToPool.push_back(p); + } + else if (pk == kind::SKOLEM_ADD_TO_POOL) + { + qi.d_skolemAddToPool.push_back(p); + } + } + if (qi.d_instAddToPool.empty() && qi.d_skolemAddToPool.empty()) + { + d_qinfo.erase(q); + } +} + +std::string TermPools::identify() const { return "TermPools"; } + +void TermPools::registerPool(Node p, const std::vector& initValue) +{ + TermPoolDomain& d = d_pools[p]; + d.initialize(); + for (const Node& i : initValue) + { + d.add(i); + } +} + +void TermPools::getTermsForPool(Node p, std::vector& terms) +{ + // for now, we assume p is a variable + Assert(p.isVar()); + TermPoolDomain& dom = d_pools[p]; + if (dom.d_terms.empty()) + { + return; + } + // if we have yet to compute terms on this round + if (dom.d_currTerms.empty()) + { + std::unordered_set reps; + // eliminate modulo equality + for (const Node& t : dom.d_terms) + { + Node r = d_qs.getRepresentative(t); + if (reps.find(r) == reps.end()) + { + reps.insert(r); + dom.d_currTerms.push_back(t); + } + } + Trace("pool-terms") << "* Domain for pool " << p << " is " + << dom.d_currTerms << std::endl; + } + terms.insert(terms.end(), dom.d_currTerms.begin(), dom.d_currTerms.end()); +} + +void TermPools::processInstantiation(Node q, const std::vector& terms) +{ + processInternal(q, terms, true); +} + +void TermPools::processSkolemization(Node q, const std::vector& skolems) +{ + processInternal(q, skolems, false); +} + +void TermPools::processInternal(Node q, + const std::vector& ts, + bool isInst) +{ + Assert(q.getKind() == kind::FORALL); + std::map::iterator it = d_qinfo.find(q); + if (it == d_qinfo.end()) + { + // does not impact + return; + } + std::vector vars(q[0].begin(), q[0].end()); + Assert(vars.size() == ts.size()); + std::vector& cmds = + isInst ? it->second.d_instAddToPool : it->second.d_skolemAddToPool; + for (const Node& c : cmds) + { + Assert(c.getNumChildren() == 2); + Node t = c[0]; + // substitute the term + Node st = t.substitute(vars.begin(), vars.end(), ts.begin(), ts.end()); + // add to pool + Trace("pool-terms") << "Due to " + << (isInst ? "instantiation" : "skolemization") + << ", add " << st << " to pool " << c[1] << std::endl; + TermPoolDomain& dom = d_pools[c[1]]; + dom.d_terms.push_back(st); + } +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/term_pools.h b/src/theory/quantifiers/term_pools.h new file mode 100644 index 000000000..117cffc42 --- /dev/null +++ b/src/theory/quantifiers/term_pools.h @@ -0,0 +1,107 @@ +/********************* */ +/*! \file term_pools.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** 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 utilities for term enumeration + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__TERM_POOLS_H +#define CVC4__THEORY__QUANTIFIERS__TERM_POOLS_H + +#include +#include + +#include "expr/node.h" +#include "theory/quantifiers/quant_util.h" + +namespace cvc5 { +namespace theory { +namespace quantifiers { + +class QuantifiersState; + +/** + * Information concerning a pool variable. + */ +class TermPoolDomain +{ + public: + /** initialize, which clears the data below */ + void initialize(); + /** add node to this pool */ + void add(Node n); + /** The list in this pool */ + std::vector d_terms; + /** + * The list of terms on this round. This is cleared at the beginning of an + * instantiation round. The members are unique modulo equality. + */ + std::vector d_currTerms; +}; + +/** + * Contains all annotations that pertain to pools for a given quantified + * formula. + */ +class TermPoolQuantInfo +{ + public: + /** initialize, which clears the data below */ + void initialize(); + /** Annotations of kind INST_ADD_TO_POOL */ + std::vector d_instAddToPool; + /** Annotations of kind SKOLEM_ADD_TO_POOL */ + std::vector d_skolemAddToPool; +}; + +/** + * Term pools, which tracks the values of "pools", which are used for + * pool-based instantiation. + */ +class TermPools : public QuantifiersUtil +{ + public: + TermPools(QuantifiersState& qs); + ~TermPools() {} + /** reset, which resets the current values of pools */ + bool reset(Theory::Effort e) override; + /** Called for new quantifiers, which computes TermPoolQuantInfo above */ + void registerQuantifier(Node q) override; + /** Identify this module (for debugging, dynamic configuration, etc..) */ + std::string identify() const override; + /** Register pool p with initial value initValue. */ + void registerPool(Node p, const std::vector& initValue); + /** Get terms for pool p, adds them to the vector terms. */ + void getTermsForPool(Node p, std::vector& terms); + /** + * Process instantiation, called at the moment we successfully instantiate + * q with terms. This adds terms to pools based on INST_ADD_TO_POOL + * annotations. + */ + void processInstantiation(Node q, const std::vector& terms); + /** Same as above, for SKOLEM_ADD_TO_POOL. */ + void processSkolemization(Node q, const std::vector& skolems); + private: + void processInternal(Node q, const std::vector& ts, bool isInst); + /** reference to the quantifiers state */ + QuantifiersState& d_qs; + /** Maps pools to a domain */ + std::map d_pools; + /** Maps quantifiers to info */ + std::map d_qinfo; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC5 + +#endif /* CVC4__THEORY__QUANTIFIERS__TERM_POOLS_H */ diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp index 8317271f9..96bde733a 100644 --- a/src/theory/quantifiers/term_registry.cpp +++ b/src/theory/quantifiers/term_registry.cpp @@ -18,7 +18,9 @@ #include "options/smt_options.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/first_order_model_fmc.h" +#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_state.h" +#include "theory/quantifiers/term_util.h" namespace cvc5 { namespace theory { @@ -29,6 +31,7 @@ TermRegistry::TermRegistry(QuantifiersState& qs, QuantifiersRegistry& qr) d_useFmcModel(false), d_presolveCache(qs.getUserContext()), d_termEnum(new TermEnumeration), + d_termPools(new TermPools(qs)), d_termDb(new TermDb(qs, qr)), d_sygusTdb(nullptr) { @@ -116,6 +119,21 @@ Node TermRegistry::getTermForType(TypeNode tn) return d_termDb->getOrMakeTypeGroundTerm(tn); } +void TermRegistry::declarePool(Node p, const std::vector& initValue) +{ + d_termPools->registerPool(p, initValue); +} + +void TermRegistry::processInstantiation(Node q, const std::vector& terms) +{ + d_termPools->processInstantiation(q, terms); +} +void TermRegistry::processSkolemization(Node q, + const std::vector& skolems) +{ + d_termPools->processSkolemization(q, skolems); +} + TermDb* TermRegistry::getTermDatabase() const { return d_termDb.get(); } TermDbSygus* TermRegistry::getTermDatabaseSygus() const @@ -128,6 +146,8 @@ TermEnumeration* TermRegistry::getTermEnumeration() const return d_termEnum.get(); } +TermPools* TermRegistry::getTermPools() const { return d_termPools.get(); } + FirstOrderModel* TermRegistry::getModel() const { return d_qmodel.get(); } bool TermRegistry::useFmcModel() const { return d_useFmcModel; } diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h index 79070fae8..e6b577f4e 100644 --- a/src/theory/quantifiers/term_registry.h +++ b/src/theory/quantifiers/term_registry.h @@ -24,6 +24,7 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" +#include "theory/quantifiers/term_pools.h" namespace cvc5 { namespace theory { @@ -67,6 +68,15 @@ class TermRegistry * one exists, or otherwise a fresh variable. */ Node getTermForType(TypeNode tn); + /** + * Declare pool p with initial value initValue. + */ + void declarePool(Node p, const std::vector& initValue); + /** + * Process instantiation + */ + void processInstantiation(Node q, const std::vector& terms); + void processSkolemization(Node q, const std::vector& skolems); /** Whether we use the full model check builder and corresponding model */ bool useFmcModel() const; @@ -77,6 +87,8 @@ class TermRegistry TermDbSygus* getTermDatabaseSygus() const; /** get term enumeration utility */ TermEnumeration* getTermEnumeration() const; + /** get the term pools utility */ + TermPools* getTermPools() const; /** get the model utility */ FirstOrderModel* getModel() const; @@ -89,6 +101,8 @@ class TermRegistry NodeSet d_presolveCache; /** term enumeration utility */ std::unique_ptr d_termEnum; + /** term enumeration utility */ + std::unique_ptr d_termPools; /** term database */ std::unique_ptr d_termDb; /** sygus term database */ -- 2.30.2