diff options
-rw-r--r-- | src/smt/smt_engine.cpp | 8 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 11 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_pool.h | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.cpp | 16 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_inference_manager.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/skolemize.cpp | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/skolemize.h | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/term_pools.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/term_pools.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 5 | ||||
-rw-r--r-- | 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<Node>& 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 @@ -497,6 +497,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<Node>& initValue); + /** * Simplify a formula without doing "much" work. Does not involve * the SAT Engine in the simplification, but uses the current * definitions, assertions, and the current partial model, if one 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<q[2].getNumChildren(); i++ ){ - Trace("quant-attr-debug") << "Check : " << q[2][i] << " " << q[2][i].getKind() << std::endl; - if( q[2][i].getKind()==INST_PATTERN || q[2][i].getKind()==INST_NO_PATTERN ){ + Kind k = q[2][i].getKind(); + Trace("quant-attr-debug") + << "Check : " << q[2][i] << " " << k << std::endl; + if (k == INST_PATTERN || k == INST_NO_PATTERN) + { qa.d_hasPattern = true; - }else if( q[2][i].getKind()==INST_ATTRIBUTE ){ + } + else if (k == INST_POOL || k == INST_ADD_TO_POOL + || k == SKOLEM_ADD_TO_POOL) + { + qa.d_hasPool = true; + } + else if (k == INST_ATTRIBUTE) + { Node avar = q[2][i][0]; if( avar.getAttribute(FunDefAttribute()) ){ Trace("quant-attr") << "Attribute : function definition : " << q << std::endl; diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 2f3d0bdcf..0a72945c1 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -119,6 +119,7 @@ struct QAttributes public: QAttributes() : d_hasPattern(false), + d_hasPool(false), d_sygus(false), d_qinstLevel(-1), d_quant_elim(false), @@ -129,6 +130,8 @@ struct QAttributes ~QAttributes(){} /** does the quantified formula have a pattern? */ bool d_hasPattern; + /** does the quantified formula have a pool? */ + bool d_hasPool; /** if non-null, this quantified formula is a function definition for function * d_fundef_f */ Node d_fundef_f; diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp index d0825f1f5..0f7c65924 100644 --- a/src/theory/quantifiers/quantifiers_inference_manager.cpp +++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp @@ -30,7 +30,7 @@ QuantifiersInferenceManager::QuantifiersInferenceManager( ProofNodeManager* pnm) : InferenceManagerBuffered(t, state, pnm, "theory::quantifiers"), d_instantiate(new Instantiate(state, *this, qr, tr, pnm)), - d_skolemize(new Skolemize(state, pnm)) + d_skolemize(new Skolemize(state, tr, pnm)) { } diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index ece2ce568..90e780c44 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -24,6 +24,7 @@ #include "options/smt_options.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_state.h" +#include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" #include "theory/sort_inference.h" @@ -34,8 +35,11 @@ namespace cvc5 { namespace theory { namespace quantifiers { -Skolemize::Skolemize(QuantifiersState& qs, ProofNodeManager* pnm) +Skolemize::Skolemize(QuantifiersState& qs, + TermRegistry& tr, + ProofNodeManager* pnm) : d_qstate(qs), + d_treg(tr), d_skolemized(qs.getUserContext()), d_pnm(pnm), d_epg(pnm == nullptr ? nullptr @@ -91,6 +95,8 @@ TrustNode Skolemize::process(Node q) lem = nb; } d_skolemized[q] = lem; + // triggered when skolemizing + d_treg.processSkolemization(q, d_skolem_constants[q]); return TrustNode::mkTrustLemma(lem, pg); } diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index f72228c5b..148dff1b6 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -32,12 +32,10 @@ namespace cvc5 { class DTypeConstructor; namespace theory { - -class SortInference; - namespace quantifiers { class QuantifiersState; +class TermRegistry; /** Skolemization utility * @@ -70,7 +68,7 @@ class Skolemize typedef context::CDHashMap<Node, Node, NodeHashFunction> 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<Node>& 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<Node>& 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<Node>& 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<Node, std::map<Node, Node> >& sol_map); - + /** Declare pool */ + void declarePool(Node p, const std::vector<Node>& initValue); //----------end user interface for instantiations private: |