From f74bdbd182d95a8e6395aaaf348ca0e41baa3bf4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 14 Apr 2021 11:49:50 -0500 Subject: [PATCH] Add internal API methods for pool-based instantiation (#6350) --- src/smt/smt_engine.cpp | 8 ++++++++ src/smt/smt_engine.h | 11 +++++++++++ src/theory/quantifiers/inst_strategy_pool.h | 4 ++-- src/theory/quantifiers/instantiate.cpp | 1 + .../quantifiers/quantifiers_attributes.cpp | 16 +++++++++++++--- src/theory/quantifiers/quantifiers_attributes.h | 3 +++ .../quantifiers_inference_manager.cpp | 2 +- src/theory/quantifiers/skolemize.cpp | 8 +++++++- src/theory/quantifiers/skolemize.h | 8 ++++---- src/theory/quantifiers/term_pools.cpp | 3 ++- src/theory/quantifiers/term_pools.h | 2 +- src/theory/quantifiers_engine.cpp | 5 +++++ src/theory/quantifiers_engine.h | 3 ++- 13 files changed, 60 insertions(+), 14 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 55bf68b9f..3eedfdf53 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1135,6 +1135,14 @@ Result SmtEngine::checkSynth() -------------------------------------------------------------------------- */ +void SmtEngine::declarePool(const Node& p, const std::vector& initValue) +{ + Assert(p.isVar() && p.getType().isSet()); + finishInit(); + QuantifiersEngine* qe = getAvailableQuantifiersEngine("declareTermPool"); + qe->declarePool(p, initValue); +} + Node SmtEngine::simplify(const Node& ex) { SmtScope smts(this); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 51eed32b2..3ef190447 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -496,6 +496,17 @@ class CVC4_EXPORT SmtEngine /*------------------------- end of sygus commands ------------------------*/ + /** + * Declare pool whose initial value is the terms in initValue. A pool is + * a variable of type (Set T) that is used in quantifier annotations and does + * not occur in constraints. + * + * @param p The pool to declare, which should be a variable of type (Set T) + * for some type T. + * @param initValue The initial value of p, which should be a vector of terms + * of type T. + */ + void declarePool(const Node& p, const std::vector& initValue); /** * Simplify a formula without doing "much" work. Does not involve * the SAT Engine in the simplification, but uses the current diff --git a/src/theory/quantifiers/inst_strategy_pool.h b/src/theory/quantifiers/inst_strategy_pool.h index e45f08bc2..8eceaf35a 100644 --- a/src/theory/quantifiers/inst_strategy_pool.h +++ b/src/theory/quantifiers/inst_strategy_pool.h @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H -#define CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H +#ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H +#define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H #include "theory/quantifiers/quant_module.h" diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index b45380f5e..5f83578df 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -378,6 +378,7 @@ bool Instantiate::addInstantiation(Node q, orig_body, q[1], maxInstLevel + 1); } } + d_treg.processInstantiation(q, terms); Trace("inst-add-debug") << " --> Success." << std::endl; ++(d_statistics.d_instantiations); return true; diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index 64dc70246..f89bdf1f2 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -186,10 +186,20 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){ if( q.getNumChildren()==3 ){ qa.d_ipl = q[2]; for( unsigned i=0; i NodeNodeMap; public: - Skolemize(QuantifiersState& qs, ProofNodeManager* pnm); + Skolemize(QuantifiersState& qs, TermRegistry& tr, ProofNodeManager* pnm); ~Skolemize() {} /** skolemize quantified formula q * If the return value ret of this function is non-null, then ret is a trust @@ -143,6 +141,8 @@ class Skolemize std::vector& selfSel); /** Reference to the quantifiers state */ QuantifiersState& d_qstate; + /** Reference to the term registry */ + TermRegistry& d_treg; /** quantified formulas that have been skolemized */ NodeNodeMap d_skolemized; /** map from quantified formulas to the list of skolem constants */ diff --git a/src/theory/quantifiers/term_pools.cpp b/src/theory/quantifiers/term_pools.cpp index 43eec9499..aa0fbd06d 100644 --- a/src/theory/quantifiers/term_pools.cpp +++ b/src/theory/quantifiers/term_pools.cpp @@ -81,6 +81,7 @@ void TermPools::registerPool(Node p, const std::vector& initValue) d.initialize(); for (const Node& i : initValue) { + Assert(i.getType().isComparableTo(p.getType().getSetElementType())); d.add(i); } } @@ -156,4 +157,4 @@ void TermPools::processInternal(Node q, } // namespace quantifiers } // namespace theory -} // namespace CVC4 +} // namespace cvc5 diff --git a/src/theory/quantifiers/term_pools.h b/src/theory/quantifiers/term_pools.h index 4e34d6074..0664340a7 100644 --- a/src/theory/quantifiers/term_pools.h +++ b/src/theory/quantifiers/term_pools.h @@ -103,6 +103,6 @@ class TermPools : public QuantifiersUtil } // namespace quantifiers } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC5__THEORY__QUANTIFIERS__TERM_POOLS_H */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 5a582cea8..5916390a6 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -65,6 +65,7 @@ QuantifiersEngine::QuantifiersEngine( d_util.push_back(&d_qreg); d_util.push_back(tr.getTermDatabase()); d_util.push_back(qim.getInstantiate()); + d_util.push_back(tr.getTermPools()); } QuantifiersEngine::~QuantifiersEngine() {} @@ -653,6 +654,10 @@ bool QuantifiersEngine::getSynthSolutions( { return d_qmodules->d_synth_e->getSynthSolutions(sol_map); } +void QuantifiersEngine::declarePool(Node p, const std::vector& initValue) +{ + d_treg.declarePool(p, initValue); +} } // namespace theory } // namespace cvc5 diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 0a54f37ea..bed73d1fb 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -172,7 +172,8 @@ public: * SynthConjecture::getSynthSolutions. */ bool getSynthSolutions(std::map >& sol_map); - + /** Declare pool */ + void declarePool(Node p, const std::vector& initValue); //----------end user interface for instantiations private: -- 2.30.2