From: Andrew Reynolds Date: Thu, 11 Mar 2021 20:59:40 +0000 (-0600) Subject: Introduce inference ids for quantifier instantiation (#6119) X-Git-Tag: cvc5-1.0.0~2096 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3d9daccc198844c24c8014f1fff31a64714b3dff;p=cvc5.git Introduce inference ids for quantifier instantiation (#6119) This makes quantifiers use standard inference ids. This eliminates the need to track ad-hoc statistics, per instantiation type. This makes minor modifications to a few interfaces in quantifiers to enable this. --- diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 7acf2e861..7eeba8497 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -123,6 +123,55 @@ const char* toString(InferenceId i) return "DATATYPES_SYGUS_MT_BOUND"; case InferenceId::DATATYPES_SYGUS_MT_POS: return "DATATYPES_SYGUS_MT_POS"; + case InferenceId::QUANTIFIERS_INST_E_MATCHING: + return "QUANTIFIERS_INST_E_MATCHING"; + case InferenceId::QUANTIFIERS_INST_E_MATCHING_SIMPLE: + return "QUANTIFIERS_INST_E_MATCHING_SIMPLE"; + case InferenceId::QUANTIFIERS_INST_E_MATCHING_MT: + return "QUANTIFIERS_INST_E_MATCHING_MT"; + case InferenceId::QUANTIFIERS_INST_E_MATCHING_MTL: + return "QUANTIFIERS_INST_E_MATCHING_MTL"; + case InferenceId::QUANTIFIERS_INST_E_MATCHING_HO: + return "QUANTIFIERS_INST_E_MATCHING_HO"; + case InferenceId::QUANTIFIERS_INST_E_MATCHING_VAR_GEN: + return "QUANTIFIERS_INST_E_MATCHING_VAR_GEN"; + case InferenceId::QUANTIFIERS_INST_CBQI_CONFLICT: + return "QUANTIFIERS_INST_CBQI_CONFLICT"; + case InferenceId::QUANTIFIERS_INST_CBQI_PROP: + return "QUANTIFIERS_INST_CBQI_PROP"; + case InferenceId::QUANTIFIERS_INST_FMF_EXH: + return "QUANTIFIERS_INST_FMF_EXH"; + case InferenceId::QUANTIFIERS_INST_FMF_FMC: + return "QUANTIFIERS_INST_FMF_FMC"; + case InferenceId::QUANTIFIERS_INST_FMF_FMC_EXH: + return "QUANTIFIERS_INST_FMF_FMC_EXH"; + 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_CEGQI_CEX_DEP: + return "QUANTIFIERS_CEGQI_CEX_DEP"; + case InferenceId::QUANTIFIERS_CEGQI_VTS_LB_DELTA: + return "QUANTIFIERS_CEGQI_VTS_LB_DELTA"; + case InferenceId::QUANTIFIERS_CEGQI_VTS_UB_DELTA: + return "QUANTIFIERS_CEGQI_VTS_UB_DELTA"; + case InferenceId::QUANTIFIERS_CEGQI_VTS_LB_INF: + return "QUANTIFIERS_CEGQI_VTS_LB_INF"; + case InferenceId::QUANTIFIERS_SYQI_EVAL_UNFOLD: + return "QUANTIFIERS_SYQI_EVAL_UNFOLD"; + case InferenceId::QUANTIFIERS_SYGUS_QE_PREPROC: + return "QUANTIFIERS_SYGUS_QE_PREPROC"; + case InferenceId::QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT: + return "QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT"; + case InferenceId::QUANTIFIERS_SYGUS_EXCLUDE_CURRENT: + return "QUANTIFIERS_SYGUS_EXCLUDE_CURRENT"; + case InferenceId::QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT: + return "QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT"; + case InferenceId::QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA: + return "QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA"; + case InferenceId::QUANTIFIERS_SKOLEMIZE: return "QUANTIFIERS_SKOLEMIZE"; + case InferenceId::QUANTIFIERS_REDUCE_ALPHA_EQ: + return "QUANTIFIERS_REDUCE_ALPHA_EQ"; + case InferenceId::SEP_PTO_NEG_PROP: return "SEP_PTO_NEG_PROP"; case InferenceId::SEP_PTO_PROP: return "SEP_PTO_PROP"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 8cc678162..f5fda1747 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -201,10 +201,40 @@ enum class InferenceId // ---------------------------------- end datatypes theory //-------------------------------------- quantifiers theory - // skolemization - QUANTIFIERS_SKOLEMIZE, - // Q1 <=> Q2, where Q1 and Q2 are alpha equivalent - QUANTIFIERS_REDUCE_ALPHA_EQ, + //-------------------- types of instantiations. + // Notice the identifiers in this section cover all the techniques used for + // quantifier instantiation. The subcategories below are for specific lemmas + // that are not instantiation lemmas added, per technique. + // instantiation from E-matching + QUANTIFIERS_INST_E_MATCHING, + // E-matching using simple trigger implementation + QUANTIFIERS_INST_E_MATCHING_SIMPLE, + // E-matching using multi-triggers + QUANTIFIERS_INST_E_MATCHING_MT, + // E-matching using linear implementation of multi-triggers + QUANTIFIERS_INST_E_MATCHING_MTL, + // instantiation due to higher-order matching on top of e-matching + QUANTIFIERS_INST_E_MATCHING_HO, + // E-matching based on variable triggers + QUANTIFIERS_INST_E_MATCHING_VAR_GEN, + // conflicting instantiation from conflict-based instantiation + QUANTIFIERS_INST_CBQI_CONFLICT, + // propagating instantiation from conflict-based instantiation + QUANTIFIERS_INST_CBQI_PROP, + // instantiation from naive exhaustive instantiation in finite model finding + QUANTIFIERS_INST_FMF_EXH, + // instantiation from finite model finding based on its model-based algorithm + QUANTIFIERS_INST_FMF_FMC, + // instantiation from running exhaustive instantiation on a subdomain of + // the quantified formula in finite model finding based on its model-based + // algorithm + QUANTIFIERS_INST_FMF_FMC_EXH, + // instantiations from counterexample-guided instantiation + QUANTIFIERS_INST_CEGQI, + // instantiations from syntax-guided instantiation + QUANTIFIERS_INST_SYQI, + // instantiations from enumerative instantiation + QUANTIFIERS_INST_ENUM, //-------------------- counterexample-guided instantiation // G2 => G1 where G2 is a counterexample literal for a nested quantifier whose // counterexample literal is G1. @@ -215,6 +245,9 @@ enum class InferenceId QUANTIFIERS_CEGQI_VTS_UB_DELTA, // infinity > c QUANTIFIERS_CEGQI_VTS_LB_INF, + //-------------------- syntax-guided instantiation + // evaluation unfolding for syntax-guided instantiation + QUANTIFIERS_SYQI_EVAL_UNFOLD, //-------------------- sygus solver // preprocessing a sygus conjecture based on quantifier elimination, of the // form Q <=> Q_preprocessed @@ -227,6 +260,11 @@ enum class InferenceId QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT, // ~Q where Q is a PBE conjecture with conflicting examples QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA, + //-------------------- reductions + // skolemization + QUANTIFIERS_SKOLEMIZE, + // Q1 <=> Q2, where Q1 and Q2 are alpha equivalent + QUANTIFIERS_REDUCE_ALPHA_EQ, //-------------------------------------- end quantifiers theory // ---------------------------------- sep theory diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 56bd14b33..dcc0e885b 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -483,10 +483,13 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { //check if we need virtual term substitution (if used delta or infinity) bool used_vts = d_vtsCache->containsVtsTerm(subs, false); if (d_quantEngine->getInstantiate()->addInstantiation( - d_curr_quant, subs, false, false, used_vts)) + d_curr_quant, + subs, + InferenceId::QUANTIFIERS_INST_CEGQI, + false, + false, + used_vts)) { - ++(d_quantEngine->d_statistics.d_instantiations_cbqi); - //d_added_inst.insert( d_curr_quant ); return true; }else{ //this should never happen for monotonic selection strategies diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index d69b3f19c..953693f59 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -198,7 +198,7 @@ uint64_t HigherOrderTrigger::addInstantiations() return addedHoLemmas + addedFoLemmas; } -bool HigherOrderTrigger::sendInstantiation(InstMatch& m) +bool HigherOrderTrigger::sendInstantiation(std::vector& m, InferenceId id) { if (options::hoMatching()) { @@ -207,7 +207,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m) std::vector subs; for (unsigned i = 0, size = d_quant[0].getNumChildren(); i < size; i++) { - subs.push_back(m.d_vals[i]); + subs.push_back(m[i]); vars.push_back(d_qreg.getInstantiationConstant(d_quant, i)); } @@ -238,7 +238,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m) { TNode var = ha.first; unsigned vnum = var.getAttribute(InstVarNumAttribute()); - TNode value = m.d_vals[vnum]; + TNode value = m[vnum]; Trace("ho-unif-debug") << " val[" << var << "] = " << value << std::endl; Trace("ho-unif-debug2") << "initialize lambda information..." @@ -372,27 +372,29 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m) else { // do not run higher-order matching - return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m.d_vals); + return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m, id); } } // recursion depth limited by number of arguments of higher order variables // occurring as pattern operators (very small) -bool HigherOrderTrigger::sendInstantiation(InstMatch& m, unsigned var_index) +bool HigherOrderTrigger::sendInstantiation(std::vector& m, + size_t var_index) { Trace("ho-unif-debug2") << "send inst " << var_index << " / " << d_ho_var_list.size() << std::endl; if (var_index == d_ho_var_list.size()) { // we now have an instantiation to try - return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m.d_vals); + return d_quantEngine->getInstantiate()->addInstantiation( + d_quant, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_HO); } else { Node var = d_ho_var_list[var_index]; unsigned vnum = var.getAttribute(InstVarNumAttribute()); - Assert(vnum < m.d_vals.size()); - Node value = m.d_vals[vnum]; + Assert(vnum < m.size()); + Node value = m[vnum]; Assert(d_lchildren[vnum][0] == value); Assert(d_ho_var_bvl.find(var) != d_ho_var_bvl.end()); @@ -402,13 +404,13 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m, unsigned var_index) sendInstantiationArg(m, var_index, vnum, 0, d_ho_var_bvl[var], false); // reset the value - m.d_vals[vnum] = value; + m[vnum] = value; return ret; } } -bool HigherOrderTrigger::sendInstantiationArg(InstMatch& m, +bool HigherOrderTrigger::sendInstantiationArg(std::vector& m, unsigned var_index, unsigned vnum, unsigned arg_index, @@ -428,7 +430,7 @@ bool HigherOrderTrigger::sendInstantiationArg(InstMatch& m, NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_lchildren[vnum]); Trace("ho-unif-debug2") << " got " << body << std::endl; Node lam = NodeManager::currentNM()->mkNode(kind::LAMBDA, lbvl, body); - m.d_vals[vnum] = lam; + m[vnum] = lam; Trace("ho-unif-debug2") << " try " << vnum << " -> " << lam << std::endl; } return sendInstantiation(m, var_index + 1); diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h index 3f9ca1507..fcb3cbfee 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.h +++ b/src/theory/quantifiers/ematching/ho_trigger.h @@ -34,15 +34,15 @@ class Trigger; /** HigherOrder trigger * * This extends the trigger class with techniques that post-process - * instantiations, specified by InstMatch objects, according to a variant of + * instantiations, specified by vectors of terms, according to a variant of * Huet's algorithm. For details, see Chapter 16 of the Handbook of Automated * Reasoning (vol. 2), by Gilles Dowek. * * The main difference between HigherOrderTrigger and Trigger is the function * sendInstantiation(...). Recall that this function is called when its - * underlying IMGenerator generates an InstMatch m using E-matching technique. - * We enumerate additional instantiations based on m, when the domain of m - * contains variables of function type. + * underlying IMGenerator generates a vectors of terms m using E-matching + * technique. We enumerate additional instantiations based on m, when the + * domain of m contains variables of function type. * * Examples below (f, x, y are universal variables): * @@ -170,7 +170,7 @@ class HigherOrderTrigger : public Trigger * matching ground terms to function applications with variable heads. * See examples (EX1)-(EX3) above. */ - bool sendInstantiation(InstMatch& m) override; + bool sendInstantiation(std::vector& m, InferenceId id) override; private: //-------------------- current information about the match @@ -235,7 +235,7 @@ class HigherOrderTrigger : public Trigger * when var_index = 0,1, we are processing possibilities for * instantiation of f1,f2 respectively. */ - bool sendInstantiation(InstMatch& m, unsigned var_index); + bool sendInstantiation(std::vector& m, size_t var_index); /** higher-order pattern unification algorithm * Sends an instantiation that is equivalent to m via * d_quantEngine->addInstantiation(...). @@ -266,7 +266,7 @@ class HigherOrderTrigger : public Trigger * arg_changed is true, since we modified at least one previous * argument of f1 or f2. */ - bool sendInstantiationArg(InstMatch& m, + bool sendInstantiationArg(std::vector& m, unsigned var_index, unsigned vnum, unsigned arg_index, diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 30fb8d49b..719451d1e 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -42,9 +42,11 @@ IMGenerator::IMGenerator(quantifiers::QuantifiersState& qs, { } -bool IMGenerator::sendInstantiation(Trigger* tparent, InstMatch& m) +bool IMGenerator::sendInstantiation(Trigger* tparent, + InstMatch& m, + InferenceId id) { - return tparent->sendInstantiation(m); + return tparent->sendInstantiation(m, id); } InstMatchGenerator::InstMatchGenerator( @@ -426,7 +428,8 @@ int InstMatchGenerator::getMatch( if (success) { Trace("matching-debug2") << "Continue next " << d_next << std::endl; - ret_val = continueNextMatch(f, m, qe, tparent); + ret_val = continueNextMatch( + f, m, qe, tparent, InferenceId::QUANTIFIERS_INST_E_MATCHING); } } if (ret_val < 0) @@ -442,14 +445,15 @@ int InstMatchGenerator::getMatch( int InstMatchGenerator::continueNextMatch(Node q, InstMatch& m, QuantifiersEngine* qe, - Trigger* tparent) + Trigger* tparent, + InferenceId id) { if( d_next!=NULL ){ return d_next->getNextMatch(q, m, qe, tparent); } if (d_active_add) { - return sendInstantiation(tparent, m) ? 1 : -1; + return sendInstantiation(tparent, m, id) ? 1 : -1; } return 1; } @@ -559,7 +563,7 @@ uint64_t InstMatchGenerator::addInstantiations(Node f, while (getNextMatch(f, m, qe, tparent) > 0) { if( !d_active_add ){ - if (sendInstantiation(tparent, m)) + if (sendInstantiation(tparent, m, InferenceId::UNKNOWN)) { addedLemmas++; if (d_qstate.isInConflict()) diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index 892096224..7a22a5ded 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -19,6 +19,7 @@ #include #include "expr/node_trie.h" +#include "theory/inference_id.h" #include "theory/quantifiers/inst_match.h" namespace CVC4 { @@ -118,7 +119,7 @@ public: * indicating that an instantiation was enqueued in the quantifier engine's * lemma cache. */ - bool sendInstantiation(Trigger* tparent, InstMatch& m); + bool sendInstantiation(Trigger* tparent, InstMatch& m, InferenceId id); /** The state of the quantifiers engine */ quantifiers::QuantifiersState& d_qstate; /** The quantifiers inference manager */ @@ -426,7 +427,8 @@ class InstMatchGenerator : public IMGenerator { int continueNextMatch(Node q, InstMatch& m, QuantifiersEngine* qe, - Trigger* tparent); + Trigger* tparent, + InferenceId id); /** Get inst match generator * * Gets the InstMatchGenerator that implements the diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp index 8d89c25d8..a1674e89f 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp @@ -232,7 +232,8 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe, if (childIndex == endChildIndex) { // m is an instantiation - if (sendInstantiation(tparent, m)) + if (sendInstantiation( + tparent, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_MT)) { addedLemmas++; Trace("multi-trigger-cache-debug") diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp index 41f83269c..d70011bfb 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp @@ -158,7 +158,8 @@ int InstMatchGeneratorMultiLinear::getNextMatch(Node q, << "InstMatchGeneratorMultiLinear::getNextMatch : continue match " << std::endl; Assert(d_next != nullptr); - int ret_val = continueNextMatch(q, m, qe, tparent); + int ret_val = continueNextMatch( + q, m, qe, tparent, InferenceId::QUANTIFIERS_INST_E_MATCHING_MTL); if (ret_val > 0) { Trace("multi-trigger-linear") diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp index 91cb6e929..879bd50b9 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp @@ -101,7 +101,7 @@ uint64_t InstMatchGeneratorSimple::addInstantiations(Node q, if (t.first != r) { InstMatch m(q); - addInstantiations(m, qe, addedLemmas, 0, &(t.second)); + addInstantiations(m, qe, addedLemmas, 0, &(t.second), tparent); if (qs.isInConflict()) { break; @@ -118,7 +118,7 @@ uint64_t InstMatchGeneratorSimple::addInstantiations(Node q, if (tat && !qs.isInConflict()) { InstMatch m(q); - addInstantiations(m, qe, addedLemmas, 0, tat); + addInstantiations(m, qe, addedLemmas, 0, tat, tparent); } return addedLemmas; } @@ -127,7 +127,8 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, QuantifiersEngine* qe, uint64_t& addedLemmas, size_t argIndex, - TNodeTrie* tat) + TNodeTrie* tat, + Trigger* tparent) { Debug("simple-trigger-debug") << "Add inst " << argIndex << " " << d_match_pattern << std::endl; @@ -149,7 +150,8 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, } // we do not need the trigger parent for simple triggers (no post-processing // required) - if (qe->getInstantiate()->addInstantiation(d_quant, m.d_vals)) + if (sendInstantiation( + tparent, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_SIMPLE)) { addedLemmas++; Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl; @@ -171,7 +173,8 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, if (prev.isNull() || prev == t) { m.setValue(v, t); - addInstantiations(m, qe, addedLemmas, argIndex + 1, &(tt.second)); + addInstantiations( + m, qe, addedLemmas, argIndex + 1, &(tt.second), tparent); m.setValue(v, prev); if (qs.isInConflict()) { @@ -187,7 +190,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, std::map::iterator it = tat->d_data.find(r); if (it != tat->d_data.end()) { - addInstantiations(m, qe, addedLemmas, argIndex + 1, &(it->second)); + addInstantiations(m, qe, addedLemmas, argIndex + 1, &(it->second), tparent); } } diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.h b/src/theory/quantifiers/ematching/inst_match_generator_simple.h index 72a3b4959..dd8746f71 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.h @@ -104,7 +104,8 @@ class InstMatchGeneratorSimple : public IMGenerator QuantifiersEngine* qe, uint64_t& addedLemmas, size_t argIndex, - TNodeTrie* tat); + TNodeTrie* tat, + Trigger* tparent); }; } // namespace inst diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 9855441f1..257684704 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -204,11 +204,6 @@ InstStrategyStatus InstStrategyAutoGenTriggers::process(Node f, hasInst = numInst > 0 || hasInst; Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl; - d_quantEngine->d_statistics.d_instantiations_auto_gen += numInst; - if (r == 1) - { - d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst; - } if (d_qstate.isInConflict()) { break; diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp index 289c5150b..c9e566b77 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp @@ -135,11 +135,6 @@ InstStrategyStatus InstStrategyUserPatterns::process(Node q, unsigned numInst = t->addInstantiations(); Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl; - d_quantEngine->d_statistics.d_instantiations_user_patterns += numInst; - if (t->isMultiTrigger()) - { - d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst; - } if (d_qstate.isInConflict()) { // we are already in conflict diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index ef9b8063f..7d397403d 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -150,9 +150,14 @@ uint64_t Trigger::addInstantiations() return gtAddedLemmas + addedLemmas; } -bool Trigger::sendInstantiation(InstMatch& m) +bool Trigger::sendInstantiation(std::vector& m, InferenceId id) { - return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m.d_vals); + return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m, id); +} + +bool Trigger::sendInstantiation(InstMatch& m, InferenceId id) +{ + return sendInstantiation(m.d_vals, id); } bool Trigger::mkTriggerTerms(Node q, diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index 892f453ea..31661e611 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -18,6 +18,7 @@ #define CVC4__THEORY__QUANTIFIERS__TRIGGER_H #include "expr/node.h" +#include "theory/inference_id.h" namespace CVC4 { namespace theory { @@ -208,7 +209,9 @@ class Trigger { * but in some cases (e.g. higher-order) we may modify m before calling * Instantiate::addInstantiation(...). */ - virtual bool sendInstantiation(InstMatch& m); + virtual bool sendInstantiation(std::vector& m, InferenceId id); + /** inst match version, calls the above method */ + bool sendInstantiation(InstMatch& m, InferenceId id); /** * Ensure that all ground subterms of n have been preprocessed. This makes * calls to the provided valuation to obtain the preprocessed form of these diff --git a/src/theory/quantifiers/ematching/var_match_generator.cpp b/src/theory/quantifiers/ematching/var_match_generator.cpp index 1795ec8d3..20e157808 100644 --- a/src/theory/quantifiers/ematching/var_match_generator.cpp +++ b/src/theory/quantifiers/ematching/var_match_generator.cpp @@ -67,7 +67,8 @@ int VarMatchGeneratorTermSubs::getNextMatch(Node q, } else { - ret_val = continueNextMatch(q, m, qe, tparent); + ret_val = continueNextMatch( + q, m, qe, tparent, InferenceId::QUANTIFIERS_INST_E_MATCHING_VAR_GEN); if (ret_val > 0) { return ret_val; diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 2ecf3673f..46c27df3d 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -610,7 +610,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i // just exhaustive instantiate Node c = mkCondDefault(fmfmc, f); d_quant_models[f].addEntry(fmfmc, c, d_false); - if (!exhaustiveInstantiate(fmfmc, f, c, -1)) + if (!exhaustiveInstantiate(fmfmc, f, c)) { return 0; } @@ -697,7 +697,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i // (should only add one instance) Node c = mkCond(cond); unsigned prevInst = d_addedLemmas; - exhaustiveInstantiate(fmfmc, f, c, -1); + exhaustiveInstantiate(fmfmc, f, c); if (d_addedLemmas == prevInst) { d_star_insts[f].push_back(i); @@ -706,7 +706,8 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i } // just add the instance d_triedLemmas++; - if (instq->addInstantiation(f, inst, true)) + if (instq->addInstantiation( + f, inst, InferenceId::QUANTIFIERS_INST_FMF_FMC, true)) { Trace("fmc-debug-inst") << "** Added instantiation." << std::endl; d_addedLemmas++; @@ -746,7 +747,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i int j = d_star_insts[f][i]; if (temp.addEntry(fmfmc, mcond[j], d_quant_models[f].d_value[j])) { - if (!exhaustiveInstantiate(fmfmc, f, mcond[j], j)) + if (!exhaustiveInstantiate(fmfmc, f, mcond[j])) { // something went wrong, resort to exhaustive instantiation return 0; @@ -810,8 +811,11 @@ class RepBoundFmcEntry : public QRepBoundExt FirstOrderModelFmc* d_fm; }; -bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index) { - Trace("fmc-exh") << "----Exhaustive instantiate based on index " << c_index << " : " << c << " "; +bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc* fm, + Node f, + Node c) +{ + Trace("fmc-exh") << "----Exhaustive instantiate based on " << c << " "; debugPrintCond("fmc-exh", c, true); Trace("fmc-exh")<< std::endl; RepBoundFmcEntry rbfe(d_qe, c, fm); @@ -848,7 +852,8 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No if (ev!=d_true) { Trace("fmc-exh-debug") << ", add!"; //add as instantiation - if (d_qe->getInstantiate()->addInstantiation(f, inst, true)) + if (d_qe->getInstantiate()->addInstantiation( + f, inst, InferenceId::QUANTIFIERS_INST_FMF_FMC_EXH, true)) { Trace("fmc-exh-debug") << " ...success."; addedLemmas++; diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h index 370a88488..6cad3fff5 100644 --- a/src/theory/quantifiers/fmf/full_model_check.h +++ b/src/theory/quantifiers/fmf/full_model_check.h @@ -119,8 +119,13 @@ protected: std::map d_preinitialized_types; //--------------------end for preinitialization Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n); - bool exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index); -private: + /** + * Exhaustively instantiate quantified formula q based on condition c, which + * indicate the domain to instantiate. + */ + bool exhaustiveInstantiate(FirstOrderModelFmc* fm, Node q, Node c); + + private: void doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n ); void doNegate( Def & dc ); diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 297a3ffcc..6cfb31c53 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -261,8 +261,6 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ } d_triedLemmas += mb->getNumTriedLemmas()-prev_tlem; d_addedLemmas += mb->getNumAddedLemmas()-prev_alem; - d_quantEngine->d_statistics.d_instantiations_fmf_mbqi += - (mb->getNumAddedLemmas() - prev_alem); }else{ if( Trace.isOn("fmf-exh-inst-debug") ){ Trace("fmf-exh-inst-debug") << " Instantiation Constants: "; @@ -291,7 +289,8 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; triedLemmas++; //add as instantiation - if (inst->addInstantiation(f, m.d_vals, true)) + if (inst->addInstantiation( + f, m.d_vals, InferenceId::QUANTIFIERS_INST_FMF_EXH, true)) { addedLemmas++; if (d_qstate.isInConflict()) @@ -305,7 +304,6 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ } d_addedLemmas += addedLemmas; d_triedLemmas += triedLemmas; - d_quantEngine->d_statistics.d_instantiations_fmf_exh += addedLemmas; } }else{ Trace("fmf-exh-inst") << "...exhaustive instantiation did set, incomplete=" << riter.isIncomplete() << "..." << std::endl; diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index 0595484fa..6efcd2adf 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -207,10 +207,10 @@ bool InstStrategyEnum::process(Node quantifier, bool fullEffort, bool isRd) // try instantiation failMask.clear(); /* if (ie->addInstantiation(quantifier, terms)) */ - if (ie->addInstantiationExpFail(quantifier, terms, failMask, false)) + if (ie->addInstantiationExpFail( + quantifier, terms, failMask, InferenceId::QUANTIFIERS_INST_ENUM)) { Trace("inst-alg-rd") << "Success!" << std::endl; - ++(d_quantEngine->d_statistics.d_instantiations_guess); return true; } else diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index f6fb9ed75..6c8d826cb 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -100,8 +100,12 @@ void Instantiate::addRewriter(InstantiationRewriter* ir) d_instRewrite.push_back(ir); } -bool Instantiate::addInstantiation( - Node q, std::vector& terms, bool mkRep, bool modEq, bool doVts) +bool Instantiate::addInstantiation(Node q, + std::vector& terms, + InferenceId id, + bool mkRep, + bool modEq, + bool doVts) { // For resource-limiting (also does a time check). d_qim.safePoint(ResourceManager::Resource::QuantifierStep); @@ -319,11 +323,12 @@ bool Instantiate::addInstantiation( if (hasProof) { // use proof generator - addedLem = d_qim.addPendingLemma(lem, InferenceId::UNKNOWN, LemmaProperty::NONE, d_pfInst.get()); + addedLem = + d_qim.addPendingLemma(lem, id, LemmaProperty::NONE, d_pfInst.get()); } else { - addedLem = d_qim.addPendingLemma(lem, InferenceId::UNKNOWN); + addedLem = d_qim.addPendingLemma(lem, id); } if (!addedLem) @@ -386,12 +391,13 @@ bool Instantiate::addInstantiation( bool Instantiate::addInstantiationExpFail(Node q, std::vector& terms, std::vector& failMask, + InferenceId id, bool mkRep, bool modEq, bool doVts, bool expFull) { - if (addInstantiation(q, terms, mkRep, modEq, doVts)) + if (addInstantiation(q, terms, id, mkRep, modEq, doVts)) { return true; } diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index e55e677df..abdee69ef 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -22,6 +22,7 @@ #include "context/cdhashset.h" #include "expr/node.h" #include "expr/proof.h" +#include "theory/inference_id.h" #include "theory/quantifiers/inst_match_trie.h" #include "theory/quantifiers/quant_util.h" #include "util/statistics_registry.h" @@ -126,12 +127,16 @@ class Instantiate : public QuantifiersUtil * This function returns true if the instantiation lemma for quantified * formula q for the substitution specified by terms is successfully enqueued * via a call to QuantifiersInferenceManager::addPendingLemma. - * mkRep : whether to take the representatives of the terms in the range of - * the substitution m, - * modEq : whether to check for duplication modulo equality in instantiation - * tries (for performance), - * doVts : whether we must apply virtual term substitution to the - * instantiation lemma. + * @param q the quantified formula to instantiate + * @param terms the terms to instantiate with + * @param id the identifier of the instantiation lemma sent via the inference + * manager + * @param mkRep whether to take the representatives of the terms in the + * range of the substitution m, + * @param modEq whether to check for duplication modulo equality in + * instantiation tries (for performance), + * @param doVts whether we must apply virtual term substitution to the + * instantiation lemma. * * This call may fail if it can be determined that the instantiation is not * relevant or legal in the current context. This happens if: @@ -147,6 +152,7 @@ class Instantiate : public QuantifiersUtil */ bool addInstantiation(Node q, std::vector& terms, + InferenceId id, bool mkRep = false, bool modEq = false, bool doVts = false); @@ -176,6 +182,7 @@ class Instantiate : public QuantifiersUtil bool addInstantiationExpFail(Node q, std::vector& terms, std::vector& failMask, + InferenceId id, bool mkRep = false, bool modEq = false, bool doVts = false, diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 0aafbde56..7bf7cc09b 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -2164,7 +2164,10 @@ void QuantConflictFind::checkQuantifiedFormula(Node q, } // Process the lemma: either add an instantiation or specific lemmas // constructed during the isTConstraintSpurious call, or both. - if (!qinst->addInstantiation(q, terms)) + InferenceId id = (d_effort == EFFORT_CONFLICT + ? InferenceId::QUANTIFIERS_INST_CBQI_CONFLICT + : InferenceId::QUANTIFIERS_INST_CBQI_PROP); + if (!qinst->addInstantiation(q, terms, id)) { Trace("qcf-inst") << " ... Failed to add instantiation" << std::endl; // This should only happen if the algorithm generates the same @@ -2188,7 +2191,6 @@ void QuantConflictFind::checkQuantifiedFormula(Node q, // ensure that quantified formulas that are more likely to have // conflicting instances are checked earlier. d_quantEngine->markRelevant(q); - ++(d_quantEngine->d_statistics.d_instantiations_qcf); if (options::qcfAllConflict()) { isConflict = true; @@ -2202,7 +2204,6 @@ void QuantConflictFind::checkQuantifiedFormula(Node q, else if (d_effort == EFFORT_PROP_EQ) { d_quantEngine->markRelevant(q); - ++(d_quantEngine->d_statistics.d_instantiations_qcf); } } // clean up assigned diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index fa6d80085..bbc13b463 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -286,7 +286,7 @@ void SygusInst::check(Theory::Effort e, QEffort quant_e) if (mode == options::SygusInstMode::PRIORITY_INST) { - if (!inst->addInstantiation(q, terms)) + if (!inst->addInstantiation(q, terms, InferenceId::QUANTIFIERS_INST_SYQI)) { sendEvalUnfoldLemmas(eval_unfold_lemmas); } @@ -295,13 +295,13 @@ void SygusInst::check(Theory::Effort e, QEffort quant_e) { if (!sendEvalUnfoldLemmas(eval_unfold_lemmas)) { - inst->addInstantiation(q, terms); + inst->addInstantiation(q, terms, InferenceId::QUANTIFIERS_INST_SYQI); } } else { Assert(mode == options::SygusInstMode::INTERLEAVE); - inst->addInstantiation(q, terms); + inst->addInstantiation(q, terms, InferenceId::QUANTIFIERS_INST_SYQI); sendEvalUnfoldLemmas(eval_unfold_lemmas); } } @@ -313,7 +313,8 @@ bool SygusInst::sendEvalUnfoldLemmas(const std::vector& lemmas) for (const Node& lem : lemmas) { Trace("sygus-inst") << "Evaluation unfolding: " << lem << std::endl; - added_lemma |= d_qim.addPendingLemma(lem, InferenceId::UNKNOWN); + added_lemma |= + d_qim.addPendingLemma(lem, InferenceId::QUANTIFIERS_SYQI_EVAL_UNFOLD); } return added_lemma; } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 401857206..24919fae0 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -767,21 +767,12 @@ QuantifiersEngine::Statistics::Statistics() d_ematching_time("theory::QuantifiersEngine::time_ematching"), d_num_quant("QuantifiersEngine::Num_Quantifiers", 0), d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0), - d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0), + d_instantiation_rounds_lc( + "QuantifiersEngine::Rounds_Instantiation_Last_Call", 0), d_triggers("QuantifiersEngine::Triggers", 0), d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0), d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0), - d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0), - d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0), - d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0), - d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0), - d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0), - d_instantiations_qcf("QuantifiersEngine::Instantiations_Qcf_Conflict", 0), - d_instantiations_qcf_prop("QuantifiersEngine::Instantiations_Qcf_Prop", 0), - d_instantiations_fmf_exh("QuantifiersEngine::Instantiations_Fmf_Exh", 0), - d_instantiations_fmf_mbqi("QuantifiersEngine::Instantiations_Fmf_Mbqi", 0), - d_instantiations_cbqi("QuantifiersEngine::Instantiations_Cbqi", 0), - d_instantiations_rr("QuantifiersEngine::Instantiations_Rewrite_Rules", 0) + d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0) { smtStatisticsRegistry()->registerStat(&d_time); smtStatisticsRegistry()->registerStat(&d_qcf_time); @@ -792,17 +783,7 @@ QuantifiersEngine::Statistics::Statistics() smtStatisticsRegistry()->registerStat(&d_triggers); smtStatisticsRegistry()->registerStat(&d_simple_triggers); smtStatisticsRegistry()->registerStat(&d_multi_triggers); - smtStatisticsRegistry()->registerStat(&d_multi_trigger_instantiations); smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv); - smtStatisticsRegistry()->registerStat(&d_instantiations_user_patterns); - smtStatisticsRegistry()->registerStat(&d_instantiations_auto_gen); - smtStatisticsRegistry()->registerStat(&d_instantiations_guess); - smtStatisticsRegistry()->registerStat(&d_instantiations_qcf); - smtStatisticsRegistry()->registerStat(&d_instantiations_qcf_prop); - smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_exh); - smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_mbqi); - smtStatisticsRegistry()->registerStat(&d_instantiations_cbqi); - smtStatisticsRegistry()->registerStat(&d_instantiations_rr); } QuantifiersEngine::Statistics::~Statistics(){ @@ -815,17 +796,7 @@ QuantifiersEngine::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(&d_triggers); smtStatisticsRegistry()->unregisterStat(&d_simple_triggers); smtStatisticsRegistry()->unregisterStat(&d_multi_triggers); - smtStatisticsRegistry()->unregisterStat(&d_multi_trigger_instantiations); smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv); - smtStatisticsRegistry()->unregisterStat(&d_instantiations_user_patterns); - smtStatisticsRegistry()->unregisterStat(&d_instantiations_auto_gen); - smtStatisticsRegistry()->unregisterStat(&d_instantiations_guess); - smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf); - smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf_prop); - smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_exh); - smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_mbqi); - smtStatisticsRegistry()->unregisterStat(&d_instantiations_cbqi); - smtStatisticsRegistry()->unregisterStat(&d_instantiations_rr); } Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 5fca96f0d..91c21a650 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -247,17 +247,7 @@ public: IntStat d_triggers; IntStat d_simple_triggers; IntStat d_multi_triggers; - IntStat d_multi_trigger_instantiations; IntStat d_red_alpha_equiv; - IntStat d_instantiations_user_patterns; - IntStat d_instantiations_auto_gen; - IntStat d_instantiations_guess; - IntStat d_instantiations_qcf; - IntStat d_instantiations_qcf_prop; - IntStat d_instantiations_fmf_exh; - IntStat d_instantiations_fmf_mbqi; - IntStat d_instantiations_cbqi; - IntStat d_instantiations_rr; Statistics(); ~Statistics(); };/* class QuantifiersEngine::Statistics */