From c28829ce6fc9861b8f0e902952c9983bba10820a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 31 Mar 2021 04:21:12 -0500 Subject: Add missing inference ids (#6242) Towards having complete stats on inference ids for each lemma, fact, and conflict. --- src/theory/arith/simplex.cpp | 2 +- src/theory/arith/soi_simplex.cpp | 3 ++- src/theory/inference_id.cpp | 31 ++++++++++++++++++++++ src/theory/inference_id.h | 31 +++++++++++++++++++++- .../quantifiers/cegqi/ceg_arith_instantiator.cpp | 6 +---- .../quantifiers/cegqi/ceg_arith_instantiator.h | 3 +-- src/theory/quantifiers/cegqi/ceg_instantiator.cpp | 18 +++++-------- src/theory/quantifiers/cegqi/ceg_instantiator.h | 8 +++--- .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 13 +++------ src/theory/quantifiers/cegqi/inst_strategy_cegqi.h | 2 -- src/theory/quantifiers/ematching/ho_trigger.cpp | 3 ++- .../ematching/inst_strategy_e_matching.cpp | 2 +- src/theory/quantifiers/fmf/bounded_integers.cpp | 4 +-- src/theory/quantifiers/quant_split.cpp | 2 +- src/theory/quantifiers/sygus_inst.cpp | 2 +- src/theory/sets/cardinality_extension.cpp | 2 +- src/theory/theory_inference_manager.cpp | 4 +-- 17 files changed, 90 insertions(+), 46 deletions(-) diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index d93e42215..49267034c 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -94,7 +94,7 @@ void SimplexDecisionProcedure::reportConflict(ArithVar basic){ ConstraintCP conflicted = generateConflictForBasic(basic); Assert(conflicted != NullConstraint); - d_conflictChannel.raiseConflict(conflicted, InferenceId::UNKNOWN); + d_conflictChannel.raiseConflict(conflicted, InferenceId::ARITH_CONF_SIMPLEX); d_conflictVariables.add(basic); } diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index 2ea3fd546..eef0ede43 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -846,7 +846,8 @@ bool SumOfInfeasibilitiesSPD::generateSOIConflict(const ArithVarVec& subset){ d_conflictBuilder->addConstraint(c, coeff); } ConstraintCP conflicted = d_conflictBuilder->commitConflict(); - d_conflictChannel.raiseConflict(conflicted, InferenceId::UNKNOWN); + d_conflictChannel.raiseConflict(conflicted, + InferenceId::ARITH_CONF_SOI_SIMPLEX); } tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization, d_soiVar); diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index c786117f3..50ede2726 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -23,6 +23,23 @@ const char* toString(InferenceId i) { switch (i) { + case InferenceId::EQ_CONSTANT_MERGE: return "EQ_CONSTANT_MERGE"; + case InferenceId::ARITH_BLACK_BOX: return "ARITH_BLACK_BOX"; + case InferenceId::ARITH_CONF_EQ: return "ARITH_CONF_EQ"; + case InferenceId::ARITH_CONF_LOWER: return "ARITH_CONF_LOWER"; + case InferenceId::ARITH_CONF_TRICHOTOMY: return "ARITH_CONF_TRICHOTOMY"; + case InferenceId::ARITH_CONF_UPPER: return "ARITH_CONF_UPPER"; + case InferenceId::ARITH_CONF_SIMPLEX: return "ARITH_CONF_SIMPLEX"; + case InferenceId::ARITH_CONF_SOI_SIMPLEX: return "ARITH_CONF_SOI_SIMPLEX"; + case InferenceId::ARITH_SPLIT_DEQ: return "ARITH_SPLIT_DEQ"; + case InferenceId::ARITH_TIGHTEN_CEIL: return "ARITH_TIGHTEN_CEIL"; + case InferenceId::ARITH_TIGHTEN_FLOOR: return "ARITH_TIGHTEN_FLOOR"; + case InferenceId::ARITH_APPROX_CUT: return "ARITH_APPROX_CUT"; + case InferenceId::ARITH_BB_LEMMA: return "ARITH_BB_LEMMA"; + case InferenceId::ARITH_DIO_CUT: return "ARITH_DIO_CUT"; + case InferenceId::ARITH_DIO_DECOMPOSITION: return "ARITH_DIO_DECOMPOSITION"; + case InferenceId::ARITH_SPLIT_FOR_NL_MODEL: + return "ARITH_SPLIT_FOR_NL_MODEL"; case InferenceId::ARITH_PP_ELIM_OPERATORS: return "ARITH_PP_ELIM_OPERATORS"; case InferenceId::ARITH_PP_ELIM_OPERATORS_LEMMA: return "ARITH_PP_ELIM_OPERATORS_LEMMA"; @@ -148,6 +165,13 @@ const char* toString(InferenceId i) 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_BINT_PROXY: return "QUANTIFIERS_BINT_PROXY"; + case InferenceId::QUANTIFIERS_BINT_MIN_NG: return "QUANTIFIERS_BINT_MIN_NG"; + case InferenceId::QUANTIFIERS_CEGQI_CEX: return "QUANTIFIERS_CEGQI_CEX"; + case InferenceId::QUANTIFIERS_CEGQI_CEX_AUX: + return "QUANTIFIERS_CEGQI_CEX_AUX"; + case InferenceId::QUANTIFIERS_CEGQI_NESTED_QE: + return "QUANTIFIERS_CEGQI_NESTED_QE"; case InferenceId::QUANTIFIERS_CEGQI_CEX_DEP: return "QUANTIFIERS_CEGQI_CEX_DEP"; case InferenceId::QUANTIFIERS_CEGQI_VTS_LB_DELTA: @@ -156,6 +180,7 @@ const char* toString(InferenceId i) return "QUANTIFIERS_CEGQI_VTS_UB_DELTA"; case InferenceId::QUANTIFIERS_CEGQI_VTS_LB_INF: return "QUANTIFIERS_CEGQI_VTS_LB_INF"; + case InferenceId::QUANTIFIERS_SYQI_CEX: return "QUANTIFIERS_SYQI_CEX"; case InferenceId::QUANTIFIERS_SYQI_EVAL_UNFOLD: return "QUANTIFIERS_SYQI_EVAL_UNFOLD"; case InferenceId::QUANTIFIERS_SYGUS_QE_PREPROC: @@ -168,9 +193,14 @@ const char* toString(InferenceId i) return "QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT"; case InferenceId::QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA: return "QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA"; + case InferenceId::QUANTIFIERS_DSPLIT: return "QUANTIFIERS_DSPLIT"; case InferenceId::QUANTIFIERS_SKOLEMIZE: return "QUANTIFIERS_SKOLEMIZE"; case InferenceId::QUANTIFIERS_REDUCE_ALPHA_EQ: return "QUANTIFIERS_REDUCE_ALPHA_EQ"; + case InferenceId::QUANTIFIERS_HO_MATCH_PRED: + return "QUANTIFIERS_HO_MATCH_PRED"; + case InferenceId::QUANTIFIERS_PARTIAL_TRIGGER_REDUCE: + return "QUANTIFIERS_PARTIAL_TRIGGER_REDUCE"; case InferenceId::SEP_PTO_NEG_PROP: return "SEP_PTO_NEG_PROP"; case InferenceId::SEP_PTO_PROP: return "SEP_PTO_PROP"; @@ -200,6 +230,7 @@ const char* toString(InferenceId i) case InferenceId::SETS_UP_CLOSURE_2: return "SETS_UP_CLOSURE_2"; case InferenceId::SETS_UP_UNIV: return "SETS_UP_UNIV"; case InferenceId::SETS_UNIV_TYPE: return "SETS_UNIV_TYPE"; + case InferenceId::SETS_CARD_SPLIT_EMPTY: return "SETS_CARD_SPLIT_EMPTY"; case InferenceId::SETS_CARD_CYCLE: return "SETS_CARD_CYCLE"; case InferenceId::SETS_CARD_EQUAL: return "SETS_CARD_EQUAL"; case InferenceId::SETS_CARD_GRAPH_EMP: return "SETS_CARD_GRAPH_EMP"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 380b5eca6..1b57e966f 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -37,6 +37,9 @@ namespace theory { */ enum class InferenceId { + // ---------------------------------- core + // a conflict when two constants merge in the equality engine (of any theory) + EQ_CONSTANT_MERGE, // ---------------------------------- arith theory //-------------------- linear core // black box conflicts. It's magic. @@ -49,6 +52,10 @@ enum class InferenceId ARITH_CONF_TRICHOTOMY, // conflicting upper bound ARITH_CONF_UPPER, + // conflict from simplex + ARITH_CONF_SIMPLEX, + // conflict from sum-of-infeasibility simplex + ARITH_CONF_SOI_SIMPLEX, // introduces split on a disequality ARITH_SPLIT_DEQ, // tighten integer inequalities to ceiling @@ -257,7 +264,18 @@ enum class InferenceId QUANTIFIERS_INST_SYQI, // instantiations from enumerative instantiation QUANTIFIERS_INST_ENUM, + //-------------------- bounded integers + // a proxy lemma from bounded integers, used to control bounds on ground terms + QUANTIFIERS_BINT_PROXY, + // a proxy lemma to minimize an instantiation of non-ground terms + QUANTIFIERS_BINT_MIN_NG, //-------------------- counterexample-guided instantiation + // a counterexample lemma + QUANTIFIERS_CEGQI_CEX, + // an auxiliary lemma from counterexample lemma + QUANTIFIERS_CEGQI_CEX_AUX, + // a reduction lemma for nested quantifier elimination + QUANTIFIERS_CEGQI_NESTED_QE, // G2 => G1 where G2 is a counterexample literal for a nested quantifier whose // counterexample literal is G1. QUANTIFIERS_CEGQI_CEX_DEP, @@ -268,6 +286,8 @@ enum class InferenceId // infinity > c QUANTIFIERS_CEGQI_VTS_LB_INF, //-------------------- syntax-guided instantiation + // a counterexample lemma + QUANTIFIERS_SYQI_CEX, // evaluation unfolding for syntax-guided instantiation QUANTIFIERS_SYQI_EVAL_UNFOLD, //-------------------- sygus solver @@ -282,11 +302,18 @@ enum class InferenceId QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT, // ~Q where Q is a PBE conjecture with conflicting examples QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA, - //-------------------- reductions + //-------------------- dynamic splitting + // a dynamic split from quantifiers + QUANTIFIERS_DSPLIT, + //-------------------- miscellaneous // skolemization QUANTIFIERS_SKOLEMIZE, // Q1 <=> Q2, where Q1 and Q2 are alpha equivalent QUANTIFIERS_REDUCE_ALPHA_EQ, + // a higher-order match predicate lemma + QUANTIFIERS_HO_MATCH_PRED, + // reduction of quantifiers that don't have triggers that cover all variables + QUANTIFIERS_PARTIAL_TRIGGER_REDUCE, //-------------------------------------- end quantifiers theory // ---------------------------------- sep theory @@ -336,6 +363,8 @@ enum class InferenceId SETS_UP_UNIV, SETS_UNIV_TYPE, //-------------------- sets cardinality solver + // split on emptyset + SETS_CARD_SPLIT_EMPTY, // cycle of cardinalities, hence all sets have the same SETS_CARD_CYCLE, // two sets have the same cardinality diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index 94c8b87e6..aa5512f5f 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -697,11 +697,7 @@ bool ArithInstantiator::needsPostProcessInstantiationForVariable( } bool ArithInstantiator::postProcessInstantiationForVariable( - CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort, - std::vector& lemmas) + CegInstantiator* ci, SolvedForm& sf, Node pv, CegInstEffort effort) { Assert(std::find(sf.d_non_basic.begin(), sf.d_non_basic.end(), pv) != sf.d_non_basic.end()); diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h index 34985cd51..00b23307e 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h @@ -125,8 +125,7 @@ class ArithInstantiator : public Instantiator bool postProcessInstantiationForVariable(CegInstantiator* ci, SolvedForm& sf, Node pv, - CegInstEffort effort, - std::vector& lemmas) override; + CegInstEffort effort) override; std::string identify() const override { return "Arith"; } private: diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 38b9c739e..26cb1d53c 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -562,7 +562,6 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i) sf.d_vars.size() > d_input_vars.size() || !d_var_order_index.empty(); std::vector< Instantiator * > pp_inst; std::map< Instantiator *, Node > pp_inst_to_var; - std::vector< Node > lemmas; for( std::map< Node, Instantiator * >::iterator ita = d_active_instantiators.begin(); ita != d_active_instantiators.end(); ++ita ){ if (ita->second->needsPostProcessInstantiationForVariable( this, sf, ita->first, d_effort)) @@ -577,19 +576,19 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i) bool postProcessSuccess = true; for( std::map< Instantiator *, Node >::iterator itp = pp_inst_to_var.begin(); itp != pp_inst_to_var.end(); ++itp ){ if (!itp->first->postProcessInstantiationForVariable( - this, sf_tmp, itp->second, d_effort, lemmas)) + this, sf_tmp, itp->second, d_effort)) { postProcessSuccess = false; break; } } if( postProcessSuccess ){ - return doAddInstantiation( sf_tmp.d_vars, sf_tmp.d_subs, lemmas ); + return doAddInstantiation(sf_tmp.d_vars, sf_tmp.d_subs); }else{ return false; } }else{ - return doAddInstantiation( sf.d_vars, sf.d_subs, lemmas ); + return doAddInstantiation(sf.d_vars, sf.d_subs); } }else{ bool is_sv = false; @@ -1050,7 +1049,9 @@ bool CegInstantiator::constructInstantiationInc(Node pv, } } -bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& lemmas ) { +bool CegInstantiator::doAddInstantiation(std::vector& vars, + std::vector& subs) +{ if (vars.size() > d_input_vars.size() || !d_var_order_index.empty()) { Trace("cegqi-inst-debug") << "Reconstructing instantiations...." << std::endl; @@ -1082,12 +1083,7 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector } } Trace("cegqi-inst-debug") << "Do the instantiation...." << std::endl; - bool ret = d_parent->doAddInstantiation(subs); - for (const Node& l : lemmas) - { - d_parent->addPendingLemma(l); - } - return ret; + return d_parent->doAddInstantiation(subs); } bool CegInstantiator::isEligibleForInstantiation(Node n) const diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h index bca62f2ef..800398fb9 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -20,6 +20,7 @@ #include #include "expr/node.h" +#include "theory/inference_id.h" #include "util/statistics_registry.h" namespace CVC4 { @@ -554,9 +555,7 @@ class CegInstantiator { * It returns true if a successful call to the output channel's * doAddInstantiation was made. */ - bool doAddInstantiation(std::vector& vars, - std::vector& subs, - std::vector& lemmas); + bool doAddInstantiation(std::vector& vars, std::vector& subs); //------------------------------------ static queries /** is cbqi sort @@ -771,8 +770,7 @@ public: virtual bool postProcessInstantiationForVariable(CegInstantiator* ci, SolvedForm& sf, Node pv, - CegInstEffort effort, - std::vector& lemmas) + CegInstEffort effort) { return true; } diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 19821d347..6390feec0 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -380,7 +380,7 @@ void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem) ce_vars.push_back(d_qreg.getInstantiationConstant(q, i)); } // send the lemma - d_qim.lemma(lem, InferenceId::UNKNOWN); + d_qim.lemma(lem, InferenceId::QUANTIFIERS_CEGQI_CEX); // get the preprocessed form of the lemma we just sent std::vector skolems; std::vector skAsserts; @@ -394,11 +394,11 @@ void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem) std::vector auxLems; CegInstantiator* cinst = getInstantiator(q); cinst->registerCounterexampleLemma(ppLem, ce_vars, auxLems); - for (unsigned i = 0, size = auxLems.size(); i < size; i++) + for (size_t i = 0, size = auxLems.size(); i < size; i++) { Trace("cegqi-debug") << "Auxiliary CE lemma " << i << " : " << auxLems[i] << std::endl; - d_qim.addPendingLemma(auxLems[i], InferenceId::UNKNOWN); + d_qim.addPendingLemma(auxLems[i], InferenceId::QUANTIFIERS_CEGQI_CEX_AUX); } } @@ -498,11 +498,6 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { return false; } -bool InstStrategyCegqi::addPendingLemma(Node lem) const -{ - return d_qim.addPendingLemma(lem, InferenceId::UNKNOWN); -} - CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) { std::map>::iterator it = d_cinst.find(q); @@ -541,7 +536,7 @@ bool InstStrategyCegqi::processNestedQe(Node q, bool isPreregister) // add lemmas to process for (const Node& lem : lems) { - d_qim.addPendingLemma(lem, InferenceId::UNKNOWN); + d_qim.addPendingLemma(lem, InferenceId::QUANTIFIERS_CEGQI_NESTED_QE); } // don't need to process this, since it has been reduced return true; diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index 6db755246..db3997865 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -123,8 +123,6 @@ class InstStrategyCegqi : public QuantifiersModule //------------------- interface for CegqiOutputInstStrategy /** Instantiate the current quantified formula forall x. Q with x -> subs. */ bool doAddInstantiation(std::vector& subs); - /** Add pending lemma lem via the inference manager of this class. */ - bool addPendingLemma(Node lem) const; //------------------- end interface for CegqiOutputInstStrategy protected: diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index a2885cdec..f197e50ee 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -505,7 +505,8 @@ uint64_t HigherOrderTrigger::addHoTypeMatchPredicateLemmas() { Node u = tdb->getHoTypeMatchPredicate(tn); Node au = nm->mkNode(kind::APPLY_UF, u, f); - if (d_qim.addPendingLemma(au, InferenceId::UNKNOWN)) + if (d_qim.addPendingLemma(au, + InferenceId::QUANTIFIERS_HO_MATCH_PRED)) { // this forces f to be a first-class member of the quantifier-free // equality engine, which in turn forces the quantifier-free diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index d489869ae..45d5f13a7 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -624,7 +624,7 @@ void InstStrategyAutoGenTriggers::addTrigger( inst::Trigger * tr, Node q ) { << "Make partially specified user pattern: " << std::endl; Trace("auto-gen-trigger-partial") << " " << qq << std::endl; Node lem = nm->mkNode(OR, q.negate(), qq); - d_qim.addPendingLemma(lem, InferenceId::UNKNOWN); + d_qim.addPendingLemma(lem, InferenceId::QUANTIFIERS_PARTIAL_TRIGGER_REDUCE); return; } unsigned tindex; diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 8fcbeca4f..9222c4c93 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -296,7 +296,7 @@ void BoundedIntegers::check(Theory::Effort e, QEffort quant_e) { Trace("bound-int-lemma") << "*** bound int : proxy lemma : " << prangeLem << std::endl; - d_qim.addPendingLemma(prangeLem, InferenceId::UNKNOWN); + d_qim.addPendingLemma(prangeLem, InferenceId::QUANTIFIERS_BINT_PROXY); addedLemma = true; } } @@ -727,7 +727,7 @@ bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& va nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[q][v] ); Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl; - d_qim.lemma(lem, InferenceId::UNKNOWN); + d_qim.lemma(lem, InferenceId::QUANTIFIERS_BINT_MIN_NG); } return false; }else{ diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index 23087286b..f9b0a1e80 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -203,7 +203,7 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e) for (const Node& lem : lemmas) { Trace("quant-dsplit") << "QuantDSplit lemma : " << lem << std::endl; - d_qim.addPendingLemma(lem, InferenceId::UNKNOWN); + d_qim.addPendingLemma(lem, InferenceId::QUANTIFIERS_DSPLIT); } Trace("quant-dsplit") << "QuantDSplit::check finished" << std::endl; } diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index 1baf50045..36d2978a5 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -548,7 +548,7 @@ void SygusInst::addCeLemma(Node q) if (d_ce_lemma_added.find(q) != d_ce_lemma_added.end()) return; Node lem = d_ce_lemmas[q]; - d_qim.addPendingLemma(lem, InferenceId::UNKNOWN); + d_qim.addPendingLemma(lem, InferenceId::QUANTIFIERS_SYQI_CEX); d_ce_lemma_added.insert(q); Trace("sygus-inst") << "Add CE Lemma: " << lem << std::endl; } diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index 5c3e2d38d..ef1b3e8d5 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -560,7 +560,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, { // split on empty Trace("sets-nf") << "Split empty : " << n << std::endl; - d_im.split(n.eqNode(emp_set), InferenceId::UNKNOWN, 1); + d_im.split(n.eqNode(emp_set), InferenceId::SETS_CARD_SPLIT_EMPTY, 1); } Assert(d_im.hasSent()); return; diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index db917daea..11a889a6b 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -107,8 +107,7 @@ void TheoryInferenceManager::conflictEqConstantMerge(TNode a, TNode b) if (!d_theoryState.isInConflict()) { TrustNode tconf = explainConflictEqConstantMerge(a, b); - d_theoryState.notifyInConflict(); - d_out.trustedConflict(tconf); + trustedConflict(tconf, InferenceId::EQ_CONSTANT_MERGE); } } @@ -125,6 +124,7 @@ void TheoryInferenceManager::trustedConflict(TrustNode tconf, InferenceId id) d_conflictIdStats << id; d_theoryState.notifyInConflict(); d_out.trustedConflict(tconf); + ++d_numConflicts; } void TheoryInferenceManager::conflictExp(InferenceId id, -- cgit v1.2.3