diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp | 18 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 98 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiate.h | 59 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 5 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 5 |
5 files changed, 110 insertions, 75 deletions
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 3690cbcac..19821d347 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -473,23 +473,23 @@ Node InstStrategyCegqi::getCounterexampleLiteral(Node q) bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { Assert(!d_curr_quant.isNull()); + // check if we need virtual term substitution (if used delta or infinity) + bool usedVts = d_vtsCache->containsVtsTerm(subs, false); Instantiate* inst = d_qim.getInstantiate(); //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma if (d_qreg.getQuantAttributes().isQuantElimPartial(d_curr_quant)) { d_cbqi_set_quant_inactive = true; d_incomplete_check = true; - inst->recordInstantiation(d_curr_quant, subs, false, false); + inst->recordInstantiation(d_curr_quant, subs, usedVts); return true; } - // check if we need virtual term substitution (if used delta or infinity) - bool used_vts = d_vtsCache->containsVtsTerm(subs, false); - if (inst->addInstantiation(d_curr_quant, - subs, - InferenceId::QUANTIFIERS_INST_CEGQI, - false, - false, - used_vts)) + else if (inst->addInstantiation(d_curr_quant, + subs, + InferenceId::QUANTIFIERS_INST_CEGQI, + false, + false, + usedVts)) { return true; } diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 61c7703ed..b74f4ae0f 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -51,7 +51,7 @@ Instantiate::Instantiate(QuantifiersState& qs, d_qreg(qr), d_treg(tr), d_pnm(pnm), - d_total_inst_debug(qs.getUserContext()), + d_insts(qs.getUserContext()), d_c_inst_match_trie_dom(qs.getUserContext()), d_pfInst(pnm ? new CDProof(pnm) : nullptr) { @@ -68,24 +68,16 @@ Instantiate::~Instantiate() bool Instantiate::reset(Theory::Effort e) { - if (!d_recorded_inst.empty()) - { - Trace("quant-engine-debug") << "Removing " << d_recorded_inst.size() - << " instantiations..." << std::endl; - // remove explicitly recorded instantiations - for (std::pair<Node, std::vector<Node> >& r : d_recorded_inst) - { - removeInstantiationInternal(r.first, r.second); - } - d_recorded_inst.clear(); - } + Trace("inst-debug") << "Reset, effort " << e << std::endl; + // clear explicitly recorded instantiations + d_recordedInst.clear(); return true; } void Instantiate::registerQuantifier(Node q) {} bool Instantiate::checkComplete() { - if (!d_recorded_inst.empty()) + if (!d_recordedInst.empty()) { Trace("quant-engine-debug") << "Set incomplete due to recorded instantiations." << std::endl; @@ -337,7 +329,10 @@ bool Instantiate::addInstantiation(Node q, return false; } - d_total_inst_debug[q] = d_total_inst_debug[q] + 1; + // add to list of instantiations + InstLemmaList* ill = getOrMkInstLemmaList(q); + ill->d_list.push_back(body); + // add to temporary debug statistics (# inst on this round) d_temp_inst_debug[q]++; if (Trace.isOn("inst")) { @@ -480,12 +475,16 @@ bool Instantiate::addInstantiationExpFail(Node q, return false; } -bool Instantiate::recordInstantiation(Node q, +void Instantiate::recordInstantiation(Node q, std::vector<Node>& terms, - bool modEq, - bool addedLem) + bool doVts) { - return recordInstantiationInternal(q, terms, modEq, addedLem); + Trace("inst-debug") << "Record instantiation for " << q << std::endl; + // get the instantiation list, which ensures that q is marked as a quantified + // formula we instantiated, despite only recording an instantiation here + getOrMkInstLemmaList(q); + Node inst = getInstantiation(q, terms, doVts); + d_recordedInst[q].push_back(inst); } bool Instantiate::existsInstantiation(Node q, @@ -562,14 +561,8 @@ Node Instantiate::getInstantiation(Node q, std::vector<Node>& terms, bool doVts) bool Instantiate::recordInstantiationInternal(Node q, std::vector<Node>& terms, - bool modEq, - bool addedLem) + bool modEq) { - if (!addedLem) - { - // record the instantiation for deletion later - d_recorded_inst.push_back(std::pair<Node, std::vector<Node> >(q, terms)); - } if (options::incrementalSolving()) { Trace("inst-add-debug") @@ -607,24 +600,13 @@ bool Instantiate::removeInstantiationInternal(Node q, std::vector<Node>& terms) return d_inst_match_trie[q].removeInstMatch(q, terms); } -void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs) +void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs) const { - if (options::incrementalSolving()) - { - for (context::CDHashSet<Node, NodeHashFunction>::const_iterator it = - d_c_inst_match_trie_dom.begin(); - it != d_c_inst_match_trie_dom.end(); - ++it) - { - qs.push_back(*it); - } - } - else + for (NodeInstListMap::const_iterator it = d_insts.begin(); + it != d_insts.end(); + ++it) { - for (std::pair<const Node, InstMatchTrie>& t : d_inst_match_trie) - { - qs.push_back(t.first); - } + qs.push_back(it->first); } } @@ -671,6 +653,20 @@ void Instantiate::getInstantiationTermVectors( } } +void Instantiate::getInstantiations(Node q, std::vector<Node>& insts) +{ + Trace("inst-debug") << "get instantiations for " << q << std::endl; + InstLemmaList* ill = getOrMkInstLemmaList(q); + insts.insert(insts.end(), ill->d_list.begin(), ill->d_list.end()); + // also include recorded instantations (for qe-partial) + std::map<Node, std::vector<Node> >::const_iterator it = + d_recordedInst.find(q); + if (it != d_recordedInst.end()) + { + insts.insert(insts.end(), it->second.begin(), it->second.end()); + } +} + bool Instantiate::isProofEnabled() const { return d_pfInst != nullptr; } void Instantiate::debugPrint(std::ostream& out) @@ -705,12 +701,11 @@ void Instantiate::debugPrintModel() { if (Trace.isOn("inst-per-quant")) { - for (NodeUIntMap::iterator it = d_total_inst_debug.begin(); - it != d_total_inst_debug.end(); + for (NodeInstListMap::iterator it = d_insts.begin(); it != d_insts.end(); ++it) { - Trace("inst-per-quant") - << " * " << (*it).second << " for " << (*it).first << std::endl; + Trace("inst-per-quant") << " * " << (*it).second->d_list.size() << " for " + << (*it).first << std::endl; } } } @@ -731,6 +726,19 @@ Node Instantiate::ensureType(Node n, TypeNode tn) return Node::null(); } +InstLemmaList* Instantiate::getOrMkInstLemmaList(TNode q) +{ + NodeInstListMap::iterator it = d_insts.find(q); + if (it != d_insts.end()) + { + return it->second.get(); + } + std::shared_ptr<InstLemmaList> ill = + std::make_shared<InstLemmaList>(d_qstate.getUserContext()); + d_insts.insert(q, ill); + return ill.get(); +} + Instantiate::Statistics::Statistics() : d_instantiations("Instantiate::Instantiations_Total", 0), d_inst_duplicate("Instantiate::Duplicate_Inst", 0), diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index be410c2c8..94e16b526 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -69,6 +69,15 @@ class InstantiationRewriter bool doVts) = 0; }; +/** Context-dependent list of nodes */ +class InstLemmaList +{ + public: + InstLemmaList(context::Context* c) : d_list(c) {} + /** The list */ + context::CDList<Node> d_list; +}; + /** Instantiate * * This class is used for generating instantiation lemmas. It maintains an @@ -90,7 +99,8 @@ class InstantiationRewriter */ class Instantiate : public QuantifiersUtil { - typedef context::CDHashMap<Node, uint32_t, NodeHashFunction> NodeUIntMap; + using NodeInstListMap = context:: + CDHashMap<Node, std::shared_ptr<InstLemmaList>, NodeHashFunction>; public: Instantiate(QuantifiersState& qs, @@ -187,13 +197,13 @@ class Instantiate : public QuantifiersUtil bool expFull = true); /** record instantiation * - * Explicitly record that q has been instantiated with terms. This is the - * same as addInstantiation, but does not enqueue an instantiation lemma. + * Explicitly record that q has been instantiated with terms, with virtual + * term substitution if doVts is true. This is the same as addInstantiation, + * but does not enqueue an instantiation lemma. */ - bool recordInstantiation(Node q, + void recordInstantiation(Node q, std::vector<Node>& terms, - bool modEq = false, - bool addedLem = true); + bool doVts = false); /** exists instantiation * * Returns true if and only if the instantiation already was added or @@ -240,7 +250,7 @@ class Instantiate : public QuantifiersUtil * Get the list of quantified formulas that were instantiated in the current * user context, store them in qs. */ - void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs); + void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs) const; /** get instantiation term vectors * * Get term vectors corresponding to for all instantiations lemmas added in @@ -255,6 +265,11 @@ class Instantiate : public QuantifiersUtil */ void getInstantiationTermVectors( std::map<Node, std::vector<std::vector<Node> > >& insts); + /** + * Get instantiations for quantified formula q. If q is (forall ((x T)) (P + * x)), this is a list of the form (P t1) ... (P tn) for ground terms ti. + */ + void getInstantiations(Node q, std::vector<Node>& insts); //--------------------------------------end user-level interface utilities /** Are proofs enabled for this object? */ @@ -281,15 +296,12 @@ class Instantiate : public QuantifiersUtil private: /** record instantiation, return true if it was not a duplicate * - * addedLem : whether an instantiation lemma was added for the vector we are - * recording. If this is false, we bookkeep the vector. * modEq : whether to check for duplication modulo equality in instantiation * tries (for performance), */ bool recordInstantiationInternal(Node q, std::vector<Node>& terms, - bool modEq = false, - bool addedLem = true); + bool modEq = false); /** remove instantiation from the cache */ bool removeInstantiationInternal(Node q, std::vector<Node>& terms); /** @@ -297,6 +309,8 @@ class Instantiate : public QuantifiersUtil * if possible. */ static Node ensureType(Node n, TypeNode tn); + /** Get or make the instantiation list for quantified formula q */ + InstLemmaList* getOrMkInstLemmaList(TNode q); /** Reference to the quantifiers state */ QuantifiersState& d_qstate; @@ -311,8 +325,19 @@ class Instantiate : public QuantifiersUtil /** instantiation rewriter classes */ std::vector<InstantiationRewriter*> d_instRewrite; - /** statistics for debugging total instantiations per quantifier */ - NodeUIntMap d_total_inst_debug; + /** + * The list of all instantiation lemma bodies per quantifier. This is used + * for debugging and for quantifier elimination. + */ + NodeInstListMap d_insts; + /** explicitly recorded instantiations + * + * Sometimes an instantiation is recorded internally but not sent out as a + * lemma, for instance, for partial quantifier elimination. This is a map + * of these instantiations, for each quantified formula. This map is cleared + * on presolve, e.g. it is local to a check-sat call. + */ + std::map<Node, std::vector<Node> > d_recordedInst; /** statistics for debugging total instantiations per quantifier per round */ std::map<Node, uint32_t> d_temp_inst_debug; @@ -328,14 +353,6 @@ class Instantiate : public QuantifiersUtil * is valid. */ context::CDHashSet<Node, NodeHashFunction> d_c_inst_match_trie_dom; - - /** explicitly recorded instantiations - * - * Sometimes an instantiation is recorded internally but not sent out as a - * lemma, for instance, for partial quantifier elimination. This is a map - * of these instantiations, for each quantified formula. - */ - std::vector<std::pair<Node, std::vector<Node> > > d_recorded_inst; /** * A CDProof storing instantiation steps. */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 8d8f54768..f1ca0dd9f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -630,6 +630,11 @@ void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector d_qim.getInstantiate()->getInstantiationTermVectors(insts); } +void QuantifiersEngine::getInstantiations(Node q, std::vector<Node>& insts) +{ + d_qim.getInstantiate()->getInstantiations(q, insts); +} + void QuantifiersEngine::printSynthSolution( std::ostream& out ) { if (d_qmodules->d_synth_e) { diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 28f162ddd..d05137e80 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -155,6 +155,11 @@ public: void getInstantiationTermVectors( std::map<Node, std::vector<std::vector<Node> > >& insts); /** + * Get instantiations for quantified formula q. If q is (forall ((x T)) (P x)), + * this is a list of the form (P t1) ... (P tn) for ground terms ti. + */ + void getInstantiations(Node q, std::vector<Node>& insts); + /** * Get skolemization vectors, where for each quantified formula that was * skolemized, this is the list of skolems that were used to witness the * negation of that quantified formula. |