diff options
Diffstat (limited to 'src/theory')
28 files changed, 166 insertions, 94 deletions
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; i<inf.size(); i++ ){ Trace("quant-vts-debug") << "Infinity lemma for " << inf[i] << " " << d_small_const << std::endl; Node inf_lem_lb = NodeManager::currentNM()->mkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst<Rational>() ) ); - 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<VirtualTermSkolemAttributeId, bool> 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<Node>& nodes, std::map<Node, std::vector<Node> >& 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<Node>& 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<Node> 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<Node>& 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<Node>& 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<Node>& 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<Node>& 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<Node>& 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<Node>& 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<Node>& 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<bool>()) { 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<Node>& 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<SynthConjecture*> 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<TypeNode>& 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 */ |