From: Andrew Reynolds Date: Mon, 22 Feb 2021 23:19:20 +0000 (-0600) Subject: Eliminate raw use of output channel and valuation in quantifiers (#5933) X-Git-Tag: cvc5-1.0.0~2242 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=13819c4ae33a103b1075e816772a305b16db9157;p=cvc5.git Eliminate raw use of output channel and valuation in quantifiers (#5933) This makes all lemmas in quantifiers sent through the inference manager. It begins adding InferenceId values for some of these calls. All uses of Valuation are replaced by calls to QuantifiersState. --- diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 884a7c428..8a787ca2d 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -169,6 +169,35 @@ enum class InferenceId DATATYPES_HEIGHT_ZERO, // ---------------------------------- end datatypes theory + //-------------------------------------- quantifiers theory + // skolemization + QUANTIFIERS_SKOLEMIZE, + // Q1 <=> Q2, where Q1 and Q2 are alpha equivalent + QUANTIFIERS_REDUCE_ALPHA_EQ, + //-------------------- counterexample-guided instantiation + // G2 => G1 where G2 is a counterexample literal for a nested quantifier whose + // counterexample literal is G1. + QUANTIFIERS_CEGQI_CEX_DEP, + // 0 < delta + QUANTIFIERS_CEGQI_VTS_LB_DELTA, + // delta < c, for positive c + QUANTIFIERS_CEGQI_VTS_UB_DELTA, + // infinity > c + QUANTIFIERS_CEGQI_VTS_LB_INF, + //-------------------- sygus solver + // preprocessing a sygus conjecture based on quantifier elimination, of the + // form Q <=> Q_preprocessed + QUANTIFIERS_SYGUS_QE_PREPROC, + // G or ~G where G is the active guard for a sygus enumerator + QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT, + // manual exclusion of a current solution + QUANTIFIERS_SYGUS_EXCLUDE_CURRENT, + // manual exclusion of a current solution for sygus-stream + QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT, + // ~Q where Q is a PBE conjecture with conflicting examples + QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA, + //-------------------------------------- end quantifiers theory + // ---------------------------------- sep theory // ensures that pto is a function: (pto x y) ^ ~(pto z w) ^ x = z => y != w SEP_PTO_NEG_PROP, diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 442532e82..a79fbb9b6 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -56,7 +56,7 @@ InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe, d_cbqi_set_quant_inactive(false), d_incomplete_check(false), d_added_cbqi_lemma(qs.getUserContext()), - d_vtsCache(new VtsTermCache(qe)), + d_vtsCache(new VtsTermCache(qim)), d_bv_invert(nullptr) { d_small_const = @@ -147,7 +147,7 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q) Node dep_lemma = nm->mkNode(IMPLIES, ceLit, nm->mkNode(AND, dep)); Trace("cegqi-lemma") << "Counterexample dependency lemma : " << dep_lemma << std::endl; - d_quantEngine->getOutputChannel().lemma(dep_lemma); + d_qim.lemma(dep_lemma, InferenceId::QUANTIFIERS_CEGQI_CEX_DEP); } //must register all sub-quantifiers of counterexample lemma, register their lemmas @@ -166,11 +166,10 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q) DecisionStrategy* dlds = nullptr; if (itds == d_dstrat.end()) { - d_dstrat[q].reset( - new DecisionStrategySingleton("CexLiteral", - ceLit, - d_qstate.getSatContext(), - d_quantEngine->getValuation())); + d_dstrat[q].reset(new DecisionStrategySingleton("CexLiteral", + ceLit, + d_qstate.getSatContext(), + d_qstate.getValuation())); dlds = d_dstrat[q].get(); } else @@ -201,10 +200,12 @@ void InstStrategyCegqi::reset_round(Theory::Effort effort) Debug("cegqi-debug") << "Check quantified formula " << q << "..." << std::endl; Node cel = getCounterexampleLiteral(q); bool value; - if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){ + if (d_qstate.getValuation().hasSatValue(cel, value)) + { Debug("cegqi-debug") << "...CE Literal has value " << value << std::endl; if( !value ){ - if( d_quantEngine->getValuation().isDecision( cel ) ){ + if (d_qstate.getValuation().isDecision(cel)) + { Trace("cegqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl; }else{ Trace("cegqi") << "Inactive : " << q << std::endl; @@ -438,14 +439,14 @@ void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) { if( !delta.isNull() ){ Trace("quant-vts-debug") << "Delta lemma for " << d_small_const << std::endl; Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_small_const ); - d_quantEngine->getOutputChannel().lemma( delta_lem_ub ); + d_qim.lemma(delta_lem_ub, InferenceId::QUANTIFIERS_CEGQI_VTS_UB_DELTA); } std::vector< Node > inf; d_vtsCache->getVtsTerms(inf, true, false, false); for( unsigned i=0; imkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst() ) ); - d_quantEngine->getOutputChannel().lemma( inf_lem_lb ); + d_qim.lemma(inf_lem_lb, InferenceId::QUANTIFIERS_CEGQI_VTS_LB_INF); } } } @@ -461,7 +462,7 @@ Node InstStrategyCegqi::getCounterexampleLiteral(Node q) NodeManager * nm = NodeManager::currentNM(); Node g = nm->mkSkolem("g", nm->booleanType()); // ensure that it is a SAT literal - Node ceLit = d_quantEngine->getValuation().ensureLiteral(g); + Node ceLit = d_qstate.getValuation().ensureLiteral(g); d_ce_lit[q] = ceLit; return ceLit; } diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp index ecc52e47c..e782a1b6f 100644 --- a/src/theory/quantifiers/cegqi/vts_term_cache.cpp +++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp @@ -16,7 +16,7 @@ #include "expr/node_algorithm.h" #include "theory/arith/arith_msum.h" -#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/quantifiers_inference_manager.h" using namespace CVC4::kind; @@ -24,7 +24,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -VtsTermCache::VtsTermCache(QuantifiersEngine* qe) : d_qe(qe) +VtsTermCache::VtsTermCache(QuantifiersInferenceManager& qim) : d_qim(qim) { d_zero = NodeManager::currentNM()->mkConst(Rational(0)); } @@ -66,7 +66,7 @@ Node VtsTermCache::getVtsDelta(bool isFree, bool create) nm->realType(), "free delta for virtual term substitution"); Node delta_lem = nm->mkNode(GT, d_vts_delta_free, d_zero); - d_qe->getOutputChannel().lemma(delta_lem); + d_qim.lemma(delta_lem, InferenceId::QUANTIFIERS_CEGQI_VTS_LB_DELTA); } if (d_vts_delta.isNull()) { diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.h b/src/theory/quantifiers/cegqi/vts_term_cache.h index b9b86dd8b..7b54412c8 100644 --- a/src/theory/quantifiers/cegqi/vts_term_cache.h +++ b/src/theory/quantifiers/cegqi/vts_term_cache.h @@ -24,8 +24,6 @@ namespace CVC4 { namespace theory { -class QuantifiersEngine; - /** Attribute to mark Skolems as virtual terms */ struct VirtualTermSkolemAttributeId { @@ -35,6 +33,8 @@ typedef expr::Attribute namespace quantifiers { +class QuantifiersInferenceManager; + /** Virtual term substitution term cache * * This class stores skolems corresponding to virtual terms (e.g. delta and @@ -70,7 +70,7 @@ namespace quantifiers { class VtsTermCache { public: - VtsTermCache(QuantifiersEngine* qe); + VtsTermCache(QuantifiersInferenceManager& qim); ~VtsTermCache() {} /** * Get vts delta. The argument isFree indicates if we are getting the @@ -122,8 +122,8 @@ class VtsTermCache bool containsVtsInfinity(Node n, bool isFree = false); private: - /** pointer to the quantifiers engine */ - QuantifiersEngine* d_qe; + /** Reference to the quantifiers inference manager */ + QuantifiersInferenceManager& d_qim; /** constants */ Node d_zero; /** The virtual term substitution delta */ diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 875c74aa4..5df350fe5 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -29,12 +29,13 @@ namespace inst { HigherOrderTrigger::HigherOrderTrigger( QuantifiersEngine* qe, + quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, quantifiers::QuantifiersRegistry& qr, Node q, std::vector& nodes, std::map >& ho_apps) - : Trigger(qe, qim, qr, q, nodes), d_ho_var_apps(ho_apps) + : Trigger(qe, qs, qim, qr, q, nodes), d_ho_var_apps(ho_apps) { NodeManager* nm = NodeManager::currentNM(); // process the higher-order variable applications diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h index af7020bfc..b99a8504d 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.h +++ b/src/theory/quantifiers/ematching/ho_trigger.h @@ -93,6 +93,7 @@ class HigherOrderTrigger : public Trigger private: HigherOrderTrigger(QuantifiersEngine* qe, + quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, quantifiers::QuantifiersRegistry& qr, Node q, diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 2a1e38c3c..e7635f200 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -283,6 +283,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ if (d_is_single_trigger[patTerms[0]]) { tr = Trigger::mkTrigger(d_quantEngine, + d_qstate, d_qim, d_qreg, f, @@ -321,6 +322,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ } // will possibly want to get an old trigger tr = Trigger::mkTrigger(d_quantEngine, + d_qstate, d_qim, d_qreg, f, @@ -364,6 +366,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ { d_single_trigger_gen[patTerms[index]] = true; Trigger* tr2 = Trigger::mkTrigger(d_quantEngine, + d_qstate, d_qim, d_qreg, f, 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 ca2f1bdc5..14913bdc1 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp @@ -107,6 +107,7 @@ InstStrategyStatus InstStrategyUserPatterns::process(Node q, for (size_t i = 0, usize = ugw.size(); i < usize; i++) { Trigger* t = Trigger::mkTrigger(d_quantEngine, + d_qstate, d_qim, d_qreg, q, @@ -170,8 +171,14 @@ void InstStrategyUserPatterns::addUserPattern(Node q, Node pat) d_user_gen_wait[q].push_back(nodes); return; } - Trigger* t = Trigger::mkTrigger( - d_quantEngine, d_qim, d_qreg, q, nodes, true, Trigger::TR_MAKE_NEW); + Trigger* t = Trigger::mkTrigger(d_quantEngine, + d_qstate, + d_qim, + d_qreg, + q, + nodes, + true, + Trigger::TR_MAKE_NEW); if (t) { d_user_gen[q].push_back(t); diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index d8d3aa098..d57c3356e 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -25,6 +25,7 @@ #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_inference_manager.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers_engine.h" using namespace CVC4::kind; @@ -35,15 +36,16 @@ namespace inst { /** trigger class constructor */ Trigger::Trigger(QuantifiersEngine* qe, + quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, quantifiers::QuantifiersRegistry& qr, Node q, std::vector& nodes) - : d_quantEngine(qe), d_qim(qim), d_qreg(qr), d_quant(q) + : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr), d_quant(q) { // We must ensure that the ground subterms of the trigger have been // preprocessed. - Valuation& val = qe->getValuation(); + Valuation& val = d_qstate.getValuation(); for (const Node& n : nodes) { Node np = ensureGroundTermPreprocessed(val, n, d_groundTerms); @@ -114,7 +116,7 @@ uint64_t Trigger::addInstantiations() { // for each ground term t that does not exist in the equality engine, we // add a purification lemma of the form (k = t). - eq::EqualityEngine* ee = d_quantEngine->getState().getEqualityEngine(); + eq::EqualityEngine* ee = d_qstate.getEqualityEngine(); for (const Node& gt : d_groundTerms) { if (!ee->hasTerm(gt)) @@ -233,6 +235,7 @@ bool Trigger::mkTriggerTerms(Node q, } Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, + quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, quantifiers::QuantifiersRegistry& qr, Node f, @@ -275,11 +278,11 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, Trigger* t; if (!ho_apps.empty()) { - t = new HigherOrderTrigger(qe, qim, qr, f, trNodes, ho_apps); + t = new HigherOrderTrigger(qe, qs, qim, qr, f, trNodes, ho_apps); } else { - t = new Trigger(qe, qim, qr, f, trNodes); + t = new Trigger(qe, qs, qim, qr, f, trNodes); } qe->getTriggerDatabase()->addTrigger( trNodes, t ); @@ -287,6 +290,7 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, } Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, + quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, quantifiers::QuantifiersRegistry& qr, Node f, @@ -297,7 +301,7 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, { std::vector< Node > nodes; nodes.push_back( n ); - return mkTrigger(qe, qim, qr, f, nodes, keepAll, trOption, useNVars); + return mkTrigger(qe, qs, qim, qr, f, nodes, keepAll, trOption, useNVars); } int Trigger::getActiveScore() { diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index 21888ff8f..014cf2185 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -30,6 +30,7 @@ namespace theory { class QuantifiersEngine; namespace quantifiers { +class QuantifiersState; class QuantifiersInferenceManager; class QuantifiersRegistry; } @@ -163,6 +164,7 @@ class Trigger { TR_RETURN_NULL //return null if a duplicate is found }; static Trigger* mkTrigger(QuantifiersEngine* qe, + quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, quantifiers::QuantifiersRegistry& qr, Node q, @@ -172,6 +174,7 @@ class Trigger { size_t useNVars = 0); /** single trigger version that calls the above function */ static Trigger* mkTrigger(QuantifiersEngine* qe, + quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, quantifiers::QuantifiersRegistry& qr, Node q, @@ -196,6 +199,7 @@ class Trigger { protected: /** trigger constructor, intentionally protected (use Trigger::mkTrigger). */ Trigger(QuantifiersEngine* ie, + quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, quantifiers::QuantifiersRegistry& qr, Node q, @@ -245,6 +249,8 @@ class Trigger { std::vector d_groundTerms; /** The quantifiers engine associated with this trigger. */ QuantifiersEngine* d_quantEngine; + /** Reference to the quantifiers state */ + quantifiers::QuantifiersState& d_qstate; /** Reference to the quantifiers inference manager */ quantifiers::QuantifiersInferenceManager& d_qim; /** The quantifiers registry */ diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index e8b9f5dea..b9a3e1f34 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -498,7 +498,7 @@ void BoundedIntegers::checkOwnership(Node f) new IntRangeDecisionHeuristic(r, d_qstate.getSatContext(), d_qstate.getUserContext(), - d_quantEngine->getValuation(), + d_qstate.getValuation(), isProxy)); d_quantEngine->getTheoryEngine() ->getDecisionManager() @@ -726,7 +726,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_quantEngine->getOutputChannel().lemma(lem); + d_qim.lemma(lem, InferenceId::UNKNOWN); } return false; }else{ diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 232499fbf..cc7f24a12 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -100,7 +100,7 @@ bool Instantiate::addInstantiation( Node q, std::vector& terms, bool mkRep, bool modEq, bool doVts) { // For resource-limiting (also does a time check). - d_qe->getOutputChannel().safePoint(ResourceManager::Resource::QuantifierStep); + d_qim.safePoint(ResourceManager::Resource::QuantifierStep); Assert(!d_qstate.isInConflict()); Assert(terms.size() == q[0].getNumChildren()); Assert(d_term_db != nullptr); diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index c09c78158..a97888d36 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -30,8 +30,10 @@ namespace CVC4 { namespace theory { namespace quantifiers { -Cegis::Cegis(QuantifiersEngine* qe, SynthConjecture* p) - : SygusModule(qe, p), d_eval_unfold(nullptr), d_usingSymCons(false) +Cegis::Cegis(QuantifiersEngine* qe, + QuantifiersInferenceManager& qim, + SynthConjecture* p) + : SygusModule(qe, qim, p), d_eval_unfold(nullptr), d_usingSymCons(false) { d_eval_unfold = qe->getTermDatabaseSygus()->getEvalUnfold(); } diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index c466afe0f..c1415d92f 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -41,7 +41,9 @@ namespace quantifiers { class Cegis : public SygusModule { public: - Cegis(QuantifiersEngine* qe, SynthConjecture* p); + Cegis(QuantifiersEngine* qe, + QuantifiersInferenceManager& qim, + SynthConjecture* p); ~Cegis() override {} /** initialize */ virtual bool initialize(Node conj, diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index 4549a0945..db2a972d5 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -69,8 +69,9 @@ bool VariadicTrie::hasSubset(const std::vector& is) const } CegisCoreConnective::CegisCoreConnective(QuantifiersEngine* qe, + QuantifiersInferenceManager& qim, SynthConjecture* p) - : Cegis(qe, p) + : Cegis(qe, qim, p) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h index d70624f0a..cdc43658d 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.h +++ b/src/theory/quantifiers/sygus/cegis_core_connective.h @@ -155,7 +155,9 @@ class VariadicTrie class CegisCoreConnective : public Cegis { public: - CegisCoreConnective(QuantifiersEngine* qe, SynthConjecture* p); + CegisCoreConnective(QuantifiersEngine* qe, + QuantifiersInferenceManager& qim, + SynthConjecture* p); ~CegisCoreConnective() {} /** * Return whether this module has the possibility to construct solutions. This diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 239fa3c94..c548f7f8f 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -30,8 +30,9 @@ namespace quantifiers { CegisUnif::CegisUnif(QuantifiersEngine* qe, QuantifiersState& qs, + QuantifiersInferenceManager& qim, SynthConjecture* p) - : Cegis(qe, p), d_sygus_unif(p), d_u_enum_manager(qe, qs, p) + : Cegis(qe, qim, p), d_sygus_unif(p), d_u_enum_manager(qe, qs, qim, p) { } @@ -216,7 +217,7 @@ bool CegisUnif::getEnumValues(const std::vector& enums, << "CegisUnif::lemma, inter-unif-enumerator " "symmetry breaking lemma : " << slem << "\n"; - d_qe->getOutputChannel().lemma(slem); + d_qim.lemma(slem, InferenceId::UNKNOWN); addedUnifEnumSymBreakLemma = true; break; } @@ -364,7 +365,7 @@ bool CegisUnif::processConstructCandidates(const std::vector& enums, { Trace("cegis-unif-lemma") << "CegisUnif::lemma, separation lemma : " << lem << "\n"; - d_qe->getOutputChannel().lemma(lem); + d_qim.lemma(lem, InferenceId::UNKNOWN); } Trace("cegis-unif") << "..failed to separate heads\n---CegisUnif Engine---\n"; return false; @@ -399,9 +400,13 @@ void CegisUnif::registerRefinementLemma(const std::vector& vars, } CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy( - QuantifiersEngine* qe, QuantifiersState& qs, SynthConjecture* parent) - : DecisionStrategyFmf(qs.getSatContext(), qe->getValuation()), + QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersInferenceManager& qim, + SynthConjecture* parent) + : DecisionStrategyFmf(qs.getSatContext(), qs.getValuation()), d_qe(qe), + d_qim(qim), d_parent(parent) { d_initialized = false; @@ -503,7 +508,7 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) // G_uq_i => size(ve) >= log_2( i-1 ) // In other words, if we use i conditions, then we allow terms in our // solution whose size is at most log_2(i-1). - d_qe->getOutputChannel().lemma(fair_lemma); + d_qim.lemma(fair_lemma, InferenceId::UNKNOWN); } } @@ -611,7 +616,7 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e, Trace("cegis-unif-enum-lemma") << "CegisUnifEnum::lemma, remove redundant ops of " << e << " : " << sym_break_red_ops << "\n"; - d_qe->getOutputChannel().lemma(sym_break_red_ops); + d_qim.lemma(sym_break_red_ops, InferenceId::UNKNOWN); } // symmetry breaking between enumerators if (!si.d_enums[index].empty() && index == 0) @@ -622,7 +627,7 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e, Node sym_break = nm->mkNode(GEQ, size_e, size_e_prev); Trace("cegis-unif-enum-lemma") << "CegisUnifEnum::lemma, enum sym break:" << sym_break << "\n"; - d_qe->getOutputChannel().lemma(sym_break); + d_qim.lemma(sym_break, InferenceId::UNKNOWN); } // register the enumerator si.d_enums[index].push_back(e); @@ -678,7 +683,7 @@ void CegisUnifEnumDecisionStrategy::registerEvalPtAtSize(Node e, Node lem = NodeManager::currentNM()->mkNode(OR, disj); Trace("cegis-unif-enum-lemma") << "CegisUnifEnum::lemma, domain:" << lem << "\n"; - d_qe->getOutputChannel().lemma(lem); + d_qim.lemma(lem, InferenceId::UNKNOWN); } } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index ee9ae0132..9db77fd95 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -49,6 +49,7 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf public: CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe, QuantifiersState& qs, + QuantifiersInferenceManager& qim, SynthConjecture* parent); /** Make the n^th literal of this strategy (G_uq_n). * @@ -101,6 +102,8 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf private: /** reference to quantifier engine */ QuantifiersEngine* d_qe; + /** Reference to the quantifiers inference manager */ + QuantifiersInferenceManager& d_qim; /** sygus term database of d_qe */ TermDbSygus* d_tds; /** reference to the parent conjecture */ @@ -204,7 +207,10 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf class CegisUnif : public Cegis { public: - CegisUnif(QuantifiersEngine* qe, QuantifiersState& qs, SynthConjecture* p); + CegisUnif(QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersInferenceManager& qim, + SynthConjecture* p); ~CegisUnif() override; /** Retrieves enumerators for constructing solutions * diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp index 807764230..49a9b1ea0 100644 --- a/src/theory/quantifiers/sygus/sygus_module.cpp +++ b/src/theory/quantifiers/sygus/sygus_module.cpp @@ -20,8 +20,10 @@ namespace CVC4 { namespace theory { namespace quantifiers { -SygusModule::SygusModule(QuantifiersEngine* qe, SynthConjecture* p) - : d_qe(qe), d_tds(qe->getTermDatabaseSygus()), d_parent(p) +SygusModule::SygusModule(QuantifiersEngine* qe, + QuantifiersInferenceManager& qim, + SynthConjecture* p) + : d_qe(qe), d_qim(qim), d_tds(qe->getTermDatabaseSygus()), d_parent(p) { } diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index 7eef6c46a..e150e52af 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -31,6 +31,7 @@ namespace quantifiers { class SynthConjecture; class TermDbSygus; +class QuantifiersInferenceManager; /** SygusModule * @@ -53,7 +54,9 @@ class TermDbSygus; class SygusModule { public: - SygusModule(QuantifiersEngine* qe, SynthConjecture* p); + SygusModule(QuantifiersEngine* qe, + QuantifiersInferenceManager& qim, + SynthConjecture* p); virtual ~SygusModule() {} /** initialize * @@ -150,8 +153,10 @@ class SygusModule protected: /** reference to quantifier engine */ QuantifiersEngine* d_qe; + /** Reference to the quantifiers inference manager */ + QuantifiersInferenceManager& d_qim; /** sygus term database of d_qe */ - quantifiers::TermDbSygus* d_tds; + TermDbSygus* d_tds; /** reference to the parent conjecture */ SynthConjecture* d_parent; }; diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index b1cb330f6..da7c0d6d4 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -28,8 +28,10 @@ namespace CVC4 { namespace theory { namespace quantifiers { -SygusPbe::SygusPbe(QuantifiersEngine* qe, SynthConjecture* p) - : SygusModule(qe, p) +SygusPbe::SygusPbe(QuantifiersEngine* qe, + QuantifiersInferenceManager& qim, + SynthConjecture* p) + : SygusModule(qe, qim, p) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index 1999f82c3..df99bc452 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -86,7 +86,9 @@ class SynthConjecture; class SygusPbe : public SygusModule { public: - SygusPbe(QuantifiersEngine* qe, SynthConjecture* p); + SygusPbe(QuantifiersEngine* qe, + QuantifiersInferenceManager& qim, + SynthConjecture* p); ~SygusPbe(); /** initialize this class diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 723f11979..0fcba916b 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -58,10 +58,10 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe, d_ceg_gc(new CegGrammarConstructor(d_tds, this)), d_sygus_rconst(new SygusRepairConst(qe)), d_exampleInfer(new ExampleInfer(d_tds)), - d_ceg_pbe(new SygusPbe(qe, this)), - d_ceg_cegis(new Cegis(qe, this)), - d_ceg_cegisUnif(new CegisUnif(qe, qs, this)), - d_sygus_ccore(new CegisCoreConnective(qe, this)), + d_ceg_pbe(new SygusPbe(qe, qim, this)), + d_ceg_cegis(new Cegis(qe, qim, this)), + d_ceg_cegisUnif(new CegisUnif(qe, qs, qim, this)), + d_sygus_ccore(new CegisCoreConnective(qe, qim, this)), d_master(nullptr), d_set_ce_sk_vars(false), d_repair_index(0), @@ -102,7 +102,7 @@ void SynthConjecture::assign(Node q) // initialize the guard d_feasible_guard = nm->mkSkolem("G", nm->booleanType()); d_feasible_guard = Rewriter::rewrite(d_feasible_guard); - d_feasible_guard = d_qe->getValuation().ensureLiteral(d_feasible_guard); + d_feasible_guard = d_qstate.getValuation().ensureLiteral(d_feasible_guard); AlwaysAssert(!d_feasible_guard.isNull()); // pre-simplify the quantified formula based on the process utility @@ -202,7 +202,7 @@ void SynthConjecture::assign(Node q) { // there is a contradictory example pair, the conjecture is infeasible. Node infLem = d_feasible_guard.negate(); - d_qe->getOutputChannel().lemma(infLem); + d_qim.lemma(infLem, InferenceId::QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA); // we don't need to continue initialization in this case return; } @@ -240,13 +240,13 @@ void SynthConjecture::assign(Node q) new DecisionStrategySingleton("sygus_feasible", d_feasible_guard, d_qstate.getSatContext(), - d_qe->getValuation())); + d_qstate.getValuation())); d_qe->getDecisionManager()->registerStrategy( DecisionManager::STRAT_QUANT_SYGUS_FEASIBLE, d_feasible_strategy.get()); // this must be called, both to ensure that the feasible guard is // decided on with true polariy, but also to ensure that output channel // has been used on this call to check. - d_qe->getOutputChannel().requirePhase(d_feasible_guard, true); + d_qim.requirePhase(d_feasible_guard, true); Node gneg = d_feasible_guard.negate(); for (unsigned i = 0; i < guarded_lemmas.size(); i++) @@ -254,7 +254,7 @@ void SynthConjecture::assign(Node q) Node lem = nm->mkNode(OR, gneg, guarded_lemmas[i]); Trace("cegqi-lemma") << "Cegqi::Lemma : initial (guarded) lemma : " << lem << std::endl; - d_qe->getOutputChannel().lemma(lem); + d_qim.lemma(lem, InferenceId::UNKNOWN); } Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation() @@ -273,7 +273,7 @@ bool SynthConjecture::needsCheck() bool value; Assert(!d_feasible_guard.isNull()); // non or fully single invocation : look at guard only - if (d_qe->getValuation().hasSatValue(d_feasible_guard, value)) + if (d_qstate.getValuation().hasSatValue(d_feasible_guard, value)) { if (!value) { @@ -610,7 +610,7 @@ bool SynthConjecture::doCheck(std::vector& lems) // We should set incomplete, since a "sat" answer should not be // interpreted as "infeasible", which would make a difference in the rare // case where e.g. we had a finite grammar and exhausted the grammar. - d_qe->getOutputChannel().setIncomplete(); + d_qim.setIncomplete(); return false; } // otherwise we are unsat, and we will process the solution below @@ -780,7 +780,7 @@ bool SynthConjecture::getEnumeratedValues(std::vector& n, Node g = d_tds->getActiveGuardForEnumerator(e); if (!g.isNull()) { - Node gstatus = d_qe->getValuation().getSatValue(g); + Node gstatus = d_qstate.getValuation().getSatValue(g); if (gstatus.isNull() || !gstatus.getConst()) { Trace("sygus-engine-debug") @@ -936,7 +936,7 @@ Node SynthConjecture::getEnumeratedValue(Node e, bool& activeIncomplete) TermDbSygus::toStreamSygus("sygus-active-gen-debug", absE); Trace("sygus-active-gen-debug") << std::endl; } - d_qe->getOutputChannel().lemma(lem); + d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_EXCLUDE_CURRENT); } else { @@ -1024,7 +1024,7 @@ void SynthConjecture::excludeCurrentSolution(const std::vector& enums, exc_lem = exc_lem.negate(); Trace("cegqi-lemma") << "Cegqi::Lemma : stream exclude current solution : " << exc_lem << std::endl; - d_qe->getOutputChannel().lemma(exc_lem); + d_qim.lemma(exc_lem, InferenceId::QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT); } } diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 3aa782272..9653c4c9d 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -94,7 +94,7 @@ void SynthEngine::check(Theory::Effort e, QEffort quant_e) Trace("sygus-engine") << "---Counterexample Guided Instantiation Engine---" << std::endl; Trace("sygus-engine-debug") << std::endl; - Valuation& valuation = d_quantEngine->getValuation(); + Valuation& valuation = d_qstate.getValuation(); std::vector activeCheckConj; for (unsigned i = 0, size = d_conjs.size(); i < size; i++) { @@ -151,7 +151,7 @@ void SynthEngine::assignConjecture(Node q) { Trace("cegqi-lemma") << "Cegqi::Lemma : qe-preprocess : " << lem << std::endl; - d_quantEngine->getOutputChannel().lemma(lem); + d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_QE_PREPROC); // we've reduced the original to a preprocessed version, return return; } diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index e800a52cf..bc5cd1fda 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -564,11 +564,11 @@ void TermDbSygus::registerEnumerator(Node e, // make the guard Node ag = nm->mkSkolem("eG", nm->booleanType()); // must ensure it is a literal immediately here - ag = d_quantEngine->getValuation().ensureLiteral(ag); + ag = d_qstate.getValuation().ensureLiteral(ag); // must ensure that it is asserted as a literal before we begin solving Node lem = nm->mkNode(OR, ag, ag.negate()); - d_quantEngine->getOutputChannel().requirePhase(ag, true); - d_quantEngine->getOutputChannel().lemma(lem); + d_qim.requirePhase(ag, true); + d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT); d_enum_to_active_guard[e] = ag; } } diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index e59b788b6..9fdf0aa7f 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -218,11 +218,11 @@ void SygusInst::reset_round(Theory::Effort e) Node lit = getCeLiteral(q); bool value; - if (d_quantEngine->getValuation().hasSatValue(lit, value)) + if (d_qstate.getValuation().hasSatValue(lit, value)) { if (!value) { - if (!d_quantEngine->getValuation().isDecision(lit)) + if (!d_qstate.getValuation().isDecision(lit)) { model->setQuantifierActive(q, false); d_active_quant.erase(q); @@ -459,7 +459,7 @@ Node SygusInst::getCeLiteral(Node q) NodeManager* nm = NodeManager::currentNM(); Node sk = nm->mkSkolem("CeLiteral", nm->booleanType()); - Node lit = d_quantEngine->getValuation().ensureLiteral(sk); + Node lit = d_qstate.getValuation().ensureLiteral(sk); d_ce_lits[q] = lit; return lit; } @@ -517,11 +517,8 @@ void SygusInst::registerCeLemma(Node q, std::vector& types) * counterexample literal is decided on first. It is user-context dependent. */ Assert(d_dstrat.find(q) == d_dstrat.end()); - DecisionStrategy* ds = - new DecisionStrategySingleton("CeLiteral", - lit, - d_qstate.getSatContext(), - d_quantEngine->getValuation()); + DecisionStrategy* ds = new DecisionStrategySingleton( + "CeLiteral", lit, d_qstate.getSatContext(), d_qstate.getValuation()); d_dstrat[q].reset(ds); d_quantEngine->getDecisionManager()->registerStrategy( diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index f9edbda35..ec4cb7905 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -127,12 +127,6 @@ DecisionManager* QuantifiersEngine::getDecisionManager() return d_decManager; } -OutputChannel& QuantifiersEngine::getOutputChannel() -{ - return d_te->theoryOf(THEORY_QUANTIFIERS)->getOutputChannel(); -} -Valuation& QuantifiersEngine::getValuation() { return d_qstate.getValuation(); } - quantifiers::QuantifiersState& QuantifiersEngine::getState() { return d_qstate; @@ -591,7 +585,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ { if( setIncomplete ){ Trace("quant-engine") << "Set incomplete flag." << std::endl; - getOutputChannel().setIncomplete(); + d_qim.setIncomplete(); } //output debug stats d_instantiate->debugPrintModel(); @@ -609,6 +603,7 @@ bool QuantifiersEngine::reduceQuantifier( Node q ) { BoolMap::const_iterator it = d_quants_red.find( q ); if( it==d_quants_red.end() ){ Node lem; + InferenceId id = InferenceId::UNKNOWN; std::map< Node, Node >::iterator itr = d_quants_red_lem.find( q ); if( itr==d_quants_red_lem.end() ){ if (d_qmodules->d_alpha_equiv) @@ -616,6 +611,7 @@ bool QuantifiersEngine::reduceQuantifier( Node q ) { Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl; //add equivalence with another quantified formula lem = d_qmodules->d_alpha_equiv->reduceQuantifier(q); + id = InferenceId::QUANTIFIERS_REDUCE_ALPHA_EQ; if( !lem.isNull() ){ Trace("quant-engine-red") << "...alpha equivalence success." << std::endl; ++(d_statistics.d_red_alpha_equiv); @@ -626,7 +622,7 @@ bool QuantifiersEngine::reduceQuantifier( Node q ) { lem = itr->second; } if( !lem.isNull() ){ - getOutputChannel().lemma( lem ); + d_qim.lemma(lem, id); } d_quants_red[q] = !lem.isNull(); return !lem.isNull(); @@ -721,7 +717,9 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ Trace("quantifiers-sk-debug") << "Skolemize lemma : " << slem << std::endl; } - getOutputChannel().trustedLemma(lem, LemmaProperty::NEEDS_JUSTIFY); + d_qim.trustedLemma(lem, + InferenceId::QUANTIFIERS_SKOLEMIZE, + LemmaProperty::NEEDS_JUSTIFY); } return; } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index f01158ee2..c8f9cd6ad 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -69,10 +69,6 @@ class QuantifiersEngine { TheoryEngine* getTheoryEngine() const; /** Get the decision manager */ DecisionManager* getDecisionManager(); - /** get default output channel for the quantifiers engine */ - OutputChannel& getOutputChannel(); - /** get default valuation for the quantifiers engine */ - Valuation& getValuation(); /** The quantifiers state object */ quantifiers::QuantifiersState& getState(); /** The quantifiers inference manager */