From 6923f0cb9930332a61e187d3b4d1a7ec7e65b15c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 9 Apr 2021 14:21:11 -0500 Subject: [PATCH] Add identifiers for extended function reductions (#6314) This adds identifiers for extended function reductions, which are reasons for why an extended term no longer needs to be processed. The motivation is help understand check-model failures. This PR adds identifiers to the ExtTheory utility. It also cleans up some unused parts of this utility. Some blocks of code changed indentation in this class. --- src/theory/arith/nl/ext_theory_callback.cpp | 14 +- src/theory/arith/nl/ext_theory_callback.h | 3 +- src/theory/arith/nl/nonlinear_extension.cpp | 1 - src/theory/ext_theory.cpp | 228 ++++++++++---------- src/theory/ext_theory.h | 116 ++++++---- src/theory/strings/extf_solver.cpp | 13 +- src/theory/strings/inference_manager.cpp | 13 +- src/theory/strings/inference_manager.h | 9 +- src/theory/strings/regexp_solver.cpp | 12 +- 9 files changed, 208 insertions(+), 201 deletions(-) diff --git a/src/theory/arith/nl/ext_theory_callback.cpp b/src/theory/arith/nl/ext_theory_callback.cpp index 72848ac89..8fa1a56c9 100644 --- a/src/theory/arith/nl/ext_theory_callback.cpp +++ b/src/theory/arith/nl/ext_theory_callback.cpp @@ -69,17 +69,21 @@ bool NlExtTheoryCallback::getCurrentSubstitution( return retVal; } -bool NlExtTheoryCallback::isExtfReduced(int effort, - Node n, - Node on, - std::vector& exp) +bool NlExtTheoryCallback::isExtfReduced( + int effort, Node n, Node on, std::vector& exp, ExtReducedId& id) { if (n != d_zero) { Kind k = n.getKind(); - return k != NONLINEAR_MULT && !isTranscendentalKind(k) && k != IAND; + if (k != NONLINEAR_MULT && !isTranscendentalKind(k) && k != IAND) + { + id = ExtReducedId::ARITH_SR_LINEAR; + return true; + } + return false; } Assert(n == d_zero); + id = ExtReducedId::ARITH_SR_ZERO; if (on.getKind() == NONLINEAR_MULT) { Trace("nl-ext-zero-exp") diff --git a/src/theory/arith/nl/ext_theory_callback.h b/src/theory/arith/nl/ext_theory_callback.h index 0e0e1411b..78ea3b2b6 100644 --- a/src/theory/arith/nl/ext_theory_callback.h +++ b/src/theory/arith/nl/ext_theory_callback.h @@ -72,7 +72,8 @@ class NlExtTheoryCallback : public ExtTheoryCallback bool isExtfReduced(int effort, Node n, Node on, - std::vector& exp) override; + std::vector& exp, + ExtReducedId& id) override; private: /** The underlying equality engine. */ diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 16142886f..20d64b0d5 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -248,7 +248,6 @@ void NonlinearExtension::check(Theory::Effort e) Trace("nl-ext") << "NonlinearExtension::check, effort = " << e << std::endl; if (e == Theory::EFFORT_FULL) { - d_extTheory.clearCache(); d_needsLastCall = true; if (options::nlExtRewrites()) { diff --git a/src/theory/ext_theory.cpp b/src/theory/ext_theory.cpp index 80fafe92c..5cd38e4e0 100644 --- a/src/theory/ext_theory.cpp +++ b/src/theory/ext_theory.cpp @@ -30,6 +30,34 @@ using namespace std; namespace cvc5 { namespace theory { +const char* toString(ExtReducedId id) +{ + switch (id) + { + case ExtReducedId::SR_CONST: return "SR_CONST"; + case ExtReducedId::REDUCTION: return "REDUCTION"; + case ExtReducedId::ARITH_SR_ZERO: return "ARITH_SR_ZERO"; + case ExtReducedId::ARITH_SR_LINEAR: return "ARITH_SR_LINEAR"; + case ExtReducedId::STRINGS_SR_CONST: return "STRINGS_SR_CONST"; + case ExtReducedId::STRINGS_NEG_CTN_DEQ: return "STRINGS_NEG_CTN_DEQ"; + case ExtReducedId::STRINGS_POS_CTN: return "STRINGS_POS_CTN"; + case ExtReducedId::STRINGS_CTN_DECOMPOSE: return "STRINGS_CTN_DECOMPOSE"; + case ExtReducedId::STRINGS_REGEXP_INTER: return "STRINGS_REGEXP_INTER"; + case ExtReducedId::STRINGS_REGEXP_INTER_SUBSUME: + return "STRINGS_REGEXP_INTER_SUBSUME"; + case ExtReducedId::STRINGS_REGEXP_INCLUDE: return "STRINGS_REGEXP_INCLUDE"; + case ExtReducedId::STRINGS_REGEXP_INCLUDE_NEG: + return "STRINGS_REGEXP_INCLUDE_NEG"; + default: return "?ExtReducedId?"; + } +} + +std::ostream& operator<<(std::ostream& out, ExtReducedId id) +{ + out << toString(id); + return out; +} + bool ExtTheoryCallback::getCurrentSubstitution( int effort, const std::vector& vars, @@ -38,11 +66,10 @@ bool ExtTheoryCallback::getCurrentSubstitution( { return false; } -bool ExtTheoryCallback::isExtfReduced(int effort, - Node n, - Node on, - std::vector& exp) +bool ExtTheoryCallback::isExtfReduced( + int effort, Node n, Node on, std::vector& exp, ExtReducedId& id) { + id = ExtReducedId::SR_CONST; return n.isConst(); } bool ExtTheoryCallback::getReduction(int effort, @@ -56,16 +83,15 @@ bool ExtTheoryCallback::getReduction(int effort, ExtTheory::ExtTheory(ExtTheoryCallback& p, context::Context* c, context::UserContext* u, - OutputChannel& out, - bool cacheEnabled) + OutputChannel& out) : d_parent(p), d_out(out), d_ext_func_terms(c), + d_extfExtReducedIdMap(c), d_ci_inactive(u), d_has_extf(c), d_lemmas(u), - d_pp_lemmas(u), - d_cacheEnabled(cacheEnabled) + d_pp_lemmas(u) { d_true = NodeManager::currentNM()->mkConst(true); } @@ -103,23 +129,13 @@ std::vector ExtTheory::collectVars(Node n) Node ExtTheory::getSubstitutedTerm(int effort, Node term, - std::vector& exp, - bool useCache) + std::vector& exp) { - if (useCache) - { - Assert(d_gst_cache[effort].find(term) != d_gst_cache[effort].end()); - exp.insert(exp.end(), - d_gst_cache[effort][term].d_exp.begin(), - d_gst_cache[effort][term].d_exp.end()); - return d_gst_cache[effort][term].d_sterm; - } - std::vector terms; terms.push_back(term); std::vector sterms; std::vector > exps; - getSubstitutedTerms(effort, terms, sterms, exps, useCache); + getSubstitutedTerms(effort, terms, sterms, exps); Assert(sterms.size() == 1); Assert(exps.size() == 1); exp.insert(exp.end(), exps[0].begin(), exps[0].end()); @@ -130,92 +146,67 @@ Node ExtTheory::getSubstitutedTerm(int effort, void ExtTheory::getSubstitutedTerms(int effort, const std::vector& terms, std::vector& sterms, - std::vector >& exp, - bool useCache) + std::vector >& exp) { - if (useCache) + Trace("extt-debug") << "getSubstitutedTerms for " << terms.size() << " / " + << d_ext_func_terms.size() << " extended functions." + << std::endl; + if (!terms.empty()) { + // all variables we need to find a substitution for + std::vector vars; + std::vector sub; + std::map > expc; for (const Node& n : terms) { - Assert(d_gst_cache[effort].find(n) != d_gst_cache[effort].end()); - sterms.push_back(d_gst_cache[effort][n].d_sterm); - exp.push_back(std::vector()); - exp[0].insert(exp[0].end(), - d_gst_cache[effort][n].d_exp.begin(), - d_gst_cache[effort][n].d_exp.end()); - } - } - else - { - Trace("extt-debug") << "getSubstitutedTerms for " << terms.size() << " / " - << d_ext_func_terms.size() << " extended functions." - << std::endl; - if (!terms.empty()) - { - // all variables we need to find a substitution for - std::vector vars; - std::vector sub; - std::map > expc; - for (const Node& n : terms) + // do substitution, rewrite + std::map::iterator iti = d_extf_info.find(n); + Assert(iti != d_extf_info.end()); + for (const Node& v : iti->second.d_vars) { - // do substitution, rewrite - std::map::iterator iti = d_extf_info.find(n); - Assert(iti != d_extf_info.end()); - for (const Node& v : iti->second.d_vars) + if (std::find(vars.begin(), vars.end(), v) == vars.end()) { - if (std::find(vars.begin(), vars.end(), v) == vars.end()) - { - vars.push_back(v); - } + vars.push_back(v); } } - bool useSubs = d_parent.getCurrentSubstitution(effort, vars, sub, expc); - // get the current substitution for all variables - Assert(!useSubs || vars.size() == sub.size()); - for (const Node& n : terms) + } + bool useSubs = d_parent.getCurrentSubstitution(effort, vars, sub, expc); + // get the current substitution for all variables + Assert(!useSubs || vars.size() == sub.size()); + for (const Node& n : terms) + { + Node ns = n; + std::vector expn; + if (useSubs) { - Node ns = n; - std::vector expn; - if (useSubs) + // do substitution + ns = n.substitute(vars.begin(), vars.end(), sub.begin(), sub.end()); + if (ns != n) { - // do substitution - ns = n.substitute(vars.begin(), vars.end(), sub.begin(), sub.end()); - if (ns != n) + // build explanation: explanation vars = sub for each vars in FV(n) + std::map::iterator iti = d_extf_info.find(n); + Assert(iti != d_extf_info.end()); + for (const Node& v : iti->second.d_vars) { - // build explanation: explanation vars = sub for each vars in FV(n) - std::map::iterator iti = d_extf_info.find(n); - Assert(iti != d_extf_info.end()); - for (const Node& v : iti->second.d_vars) + std::map >::iterator itx = expc.find(v); + if (itx != expc.end()) { - std::map >::iterator itx = expc.find(v); - if (itx != expc.end()) + for (const Node& e : itx->second) { - for (const Node& e : itx->second) + if (std::find(expn.begin(), expn.end(), e) == expn.end()) { - if (std::find(expn.begin(), expn.end(), e) == expn.end()) - { - expn.push_back(e); - } + expn.push_back(e); } } } } - Trace("extt-debug") - << " have " << n << " == " << ns << ", exp size=" << expn.size() - << "." << std::endl; - } - // add to vector - sterms.push_back(ns); - exp.push_back(expn); - // add to cache - if (d_cacheEnabled) - { - d_gst_cache[effort][n].d_sterm = ns; - d_gst_cache[effort][n].d_exp.clear(); - d_gst_cache[effort][n].d_exp.insert( - d_gst_cache[effort][n].d_exp.end(), expn.begin(), expn.end()); } + Trace("extt-debug") << " have " << n << " == " << ns + << ", exp size=" << expn.size() << "." << std::endl; } + // add to vector + sterms.push_back(ns); + exp.push_back(expn); } } } @@ -252,7 +243,7 @@ bool ExtTheory::doInferencesInternal(int effort, addedLemma = true; } } - markReduced(n, satDep); + markReduced(n, ExtReducedId::REDUCTION, satDep); } } } @@ -271,10 +262,11 @@ bool ExtTheory::doInferencesInternal(int effort, Node sr = Rewriter::rewrite(sterms[i]); // ask the theory if this term is reduced, e.g. is it constant or it // is a non-extf term. - if (d_parent.isExtfReduced(effort, sr, terms[i], exp[i])) + ExtReducedId id; + if (d_parent.isExtfReduced(effort, sr, terms[i], exp[i], id)) { processed = true; - markReduced(terms[i]); + markReduced(terms[i], id); // We have exp[i] => terms[i] = sr, convert this to a clause. // This ensures the proof infrastructure can process this as a // normal theory lemma. @@ -441,15 +433,16 @@ void ExtTheory::registerTerm(Node n) } // mark reduced -void ExtTheory::markReduced(Node n, bool satDep) +void ExtTheory::markReduced(Node n, ExtReducedId rid, bool satDep) { Trace("extt-debug") << "Mark reduced " << n << std::endl; registerTerm(n); Assert(d_ext_func_terms.find(n) != d_ext_func_terms.end()); d_ext_func_terms[n] = false; + d_extfExtReducedIdMap[n] = rid; if (!satDep) { - d_ci_inactive.insert(n); + d_ci_inactive[n] = rid; } // update has_extf @@ -468,34 +461,21 @@ void ExtTheory::markReduced(Node n, bool satDep) } } -// mark congruent -void ExtTheory::markCongruent(Node a, Node b) +bool ExtTheory::isContextIndependentInactive(Node n) const { - Trace("extt-debug") << "Mark congruent : " << a << " " << b << std::endl; - registerTerm(a); - registerTerm(b); - NodeBoolMap::const_iterator it = d_ext_func_terms.find(b); - if (it != d_ext_func_terms.end()) - { - if (d_ext_func_terms.find(a) != d_ext_func_terms.end()) - { - d_ext_func_terms[a] = d_ext_func_terms[a] && (*it).second; - } - else - { - Assert(false); - } - d_ext_func_terms[b] = false; - } - else - { - Assert(false); - } + ExtReducedId rid = ExtReducedId::UNKNOWN; + return isContextIndependentInactive(n, rid); } -bool ExtTheory::isContextIndependentInactive(Node n) const +bool ExtTheory::isContextIndependentInactive(Node n, ExtReducedId& rid) const { - return d_ci_inactive.find(n) != d_ci_inactive.end(); + NodeExtReducedIdMap::iterator it = d_ci_inactive.find(n); + if (it != d_ci_inactive.end()) + { + rid = it->second; + return true; + } + return false; } void ExtTheory::getTerms(std::vector& terms) @@ -510,13 +490,25 @@ void ExtTheory::getTerms(std::vector& terms) bool ExtTheory::hasActiveTerm() const { return !d_has_extf.get().isNull(); } -// is active bool ExtTheory::isActive(Node n) const +{ + ExtReducedId rid = ExtReducedId::UNKNOWN; + return isActive(n, rid); +} + +bool ExtTheory::isActive(Node n, ExtReducedId& rid) const { NodeBoolMap::const_iterator it = d_ext_func_terms.find(n); if (it != d_ext_func_terms.end()) { - return (*it).second && !isContextIndependentInactive(n); + if ((*it).second) + { + return !isContextIndependentInactive(n, rid); + } + NodeExtReducedIdMap::const_iterator itr = d_extfExtReducedIdMap.find(n); + Assert(itr != d_extfExtReducedIdMap.end()); + rid = itr->second; + return false; } return false; } @@ -555,7 +547,5 @@ std::vector ExtTheory::getActive(Kind k) const return active; } -void ExtTheory::clearCache() { d_gst_cache.clear(); } - } // namespace theory } // namespace cvc5 diff --git a/src/theory/ext_theory.h b/src/theory/ext_theory.h index b44f2b852..0beca705d 100644 --- a/src/theory/ext_theory.h +++ b/src/theory/ext_theory.h @@ -46,6 +46,52 @@ namespace theory { class OutputChannel; +/** Reasons for why a term was marked reduced */ +enum class ExtReducedId +{ + UNKNOWN, + // the extended function substitutes+rewrites to a constant + SR_CONST, + // the extended function was reduced by the callback + REDUCTION, + // the extended function substitutes+rewrites to zero + ARITH_SR_ZERO, + // the extended function substitutes+rewrites to a linear (non-zero) term + ARITH_SR_LINEAR, + // an extended string function substitutes+rewrites to a constant + STRINGS_SR_CONST, + // a negative str.contains was reduced to a disequality + STRINGS_NEG_CTN_DEQ, + // a positive str.contains was reduced to an equality + STRINGS_POS_CTN, + // a str.contains was subsumed by another based on a decomposition + STRINGS_CTN_DECOMPOSE, + // reduced via an intersection inference + STRINGS_REGEXP_INTER, + // subsumed due to intersection reasoning + STRINGS_REGEXP_INTER_SUBSUME, + // subsumed due to RE inclusion reasoning for positive memberships + STRINGS_REGEXP_INCLUDE, + // subsumed due to RE inclusion reasoning for negative memberships + STRINGS_REGEXP_INCLUDE_NEG, +}; +/** + * Converts an ext reduced identifier to a string. + * + * @param id The ext reduced identifier + * @return The name of the ext reduced identifier + */ +const char* toString(ExtReducedId id); + +/** + * Writes an ext reduced identifier to a stream. + * + * @param out The stream to write to + * @param id The ext reduced identifier to write to the stream + * @return The stream + */ +std::ostream& operator<<(std::ostream& out, ExtReducedId id); + /** * A callback class for ExtTheory below. This class is responsible for * determining how to apply context-dependent simplification. @@ -78,12 +124,12 @@ class ExtTheoryCallback * @param n The term to reduce * @param on The original form of n, before substitution * @param exp The explanation of on = n + * @param id If this method returns true, then id is updated to the reason + * why n was reduced. * @return true if n is reduced. */ - virtual bool isExtfReduced(int effort, - Node n, - Node on, - std::vector& exp); + virtual bool isExtfReduced( + int effort, Node n, Node on, std::vector& exp, ExtReducedId& id); /** * Get reduction for node n. @@ -117,8 +163,10 @@ class ExtTheoryCallback */ class ExtTheory { - typedef context::CDHashMap NodeBoolMap; - typedef context::CDHashSet NodeSet; + using NodeBoolMap = context::CDHashMap; + using NodeExtReducedIdMap = + context::CDHashMap; + using NodeSet = context::CDHashSet; public: /** constructor @@ -128,8 +176,7 @@ class ExtTheory ExtTheory(ExtTheoryCallback& p, context::Context* c, context::UserContext* u, - OutputChannel& out, - bool cacheEnabled = false); + OutputChannel& out); virtual ~ExtTheory() {} /** Tells this class to treat terms with Kind k as extended functions */ void addFunctionKind(Kind k) { d_extf_kind[k] = true; } @@ -150,12 +197,7 @@ class ExtTheory * If satDep = false, then n remains inactive in the duration of this * user-context level */ - void markReduced(Node n, bool satDep = true); - /** - * Mark that a and b are congruent terms. This sets b inactive, and sets a to - * inactive if b was inactive. - */ - void markCongruent(Node a, Node b); + void markReduced(Node n, ExtReducedId rid, bool satDep = true); /** getSubstitutedTerms * * input : effort, terms @@ -163,27 +205,17 @@ class ExtTheory * * For each i, sterms[i] = term[i] * sigma for some "derivable substitution" * sigma. We obtain derivable substitutions and their explanations via calls - * to the underlying theory's Theory::getCurrentSubstitution method. This - * also - * - * If useCache is true, we cache the result in d_gst_cache. This is a context - * independent cache that can be cleared using clearCache() below. + * to the underlying theory's Theory::getCurrentSubstitution method. */ void getSubstitutedTerms(int effort, const std::vector& terms, std::vector& sterms, - std::vector >& exp, - bool useCache = false); + std::vector >& exp); /** * Same as above, but for a single term. We return the substituted form of * term and add its explanation to exp. */ - Node getSubstitutedTerm(int effort, - Node term, - std::vector& exp, - bool useCache = false); - /** clear the cache for getSubstitutedTerm */ - void clearCache(); + Node getSubstitutedTerm(int effort, Node term, std::vector& exp); /** doInferences * * This function performs "context-dependent simplification". The method takes @@ -232,6 +264,11 @@ class ExtTheory bool hasActiveTerm() const; /** is n an active extended function term? */ bool isActive(Node n) const; + /** + * Same as above, but rid is updated to the reason if this method returns + * false. + */ + bool isActive(Node n, ExtReducedId& rid) const; /** get the set of active terms from d_ext_func_terms */ std::vector getActive() const; /** get the set of active terms from d_ext_func_terms of kind k */ @@ -242,6 +279,11 @@ class ExtTheory static std::vector collectVars(Node n); /** is n context dependent inactive? */ bool isContextIndependentInactive(Node n) const; + /** + * Same as above, but rid is updated to the reason if this method returns + * true. + */ + bool isContextIndependentInactive(Node n, ExtReducedId& rid) const; /** do inferences internal */ bool doInferencesInternal(int effort, const std::vector& terms, @@ -258,12 +300,14 @@ class ExtTheory Node d_true; /** extended function terms, map to whether they are active */ NodeBoolMap d_ext_func_terms; + /** mapping to why extended function terms are inactive */ + NodeExtReducedIdMap d_extfExtReducedIdMap; /** * The set of terms from d_ext_func_terms that are SAT-context-independent * inactive. For instance, a term t is SAT-context-independent inactive if * a reduction lemma of the form t = t' was added in this user-context level. */ - NodeSet d_ci_inactive; + NodeExtReducedIdMap d_ci_inactive; /** * Watched term for checking if any non-reduced extended functions exist. * This is an arbitrary active member of d_ext_func_terms. @@ -283,22 +327,6 @@ class ExtTheory // cache of all lemmas sent NodeSet d_lemmas; NodeSet d_pp_lemmas; - /** whether we enable caching for getSubstitutedTerm */ - bool d_cacheEnabled; - /** Substituted term info */ - class SubsTermInfo - { - public: - /** the substituted term */ - Node d_sterm; - /** an explanation */ - std::vector d_exp; - }; - /** - * This maps an (effort, term) to the information above. It is used as a - * cache for getSubstitutedTerm when d_cacheEnabled is true. - */ - std::map > d_gst_cache; }; } // namespace theory diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index fd50e78ee..6051bc4ca 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -132,7 +132,7 @@ bool ExtfSolver::doReduction(int effort, Node n) } // this depends on the current assertions, so this // inference is context-dependent - d_extt.markReduced(n, true); + d_extt.markReduced(n, ExtReducedId::STRINGS_NEG_CTN_DEQ, true); return true; } else @@ -183,7 +183,7 @@ bool ExtfSolver::doReduction(int effort, Node n) Trace("strings-red-lemma") << "Reduction (positive contains) lemma : " << n << " => " << eq << std::endl; // context-dependent because it depends on the polarity of n itself - d_extt.markReduced(n, true); + d_extt.markReduced(n, ExtReducedId::STRINGS_POS_CTN, true); } else if (k != kind::STRING_TO_CODE) { @@ -297,7 +297,7 @@ void ExtfSolver::checkExtfEval(int effort) { if (effort < 3) { - d_extt.markReduced(n); + d_extt.markReduced(n, ExtReducedId::STRINGS_SR_CONST); Trace("strings-extf-debug") << " resolvable by evaluation..." << std::endl; std::vector exps; @@ -549,7 +549,7 @@ void ExtfSolver::checkExtfInference(Node n, else if (d_extt.hasFunctionKind(conc.getKind())) { // can mark as reduced, since model for n implies model for conc - d_extt.markReduced(conc); + d_extt.markReduced(conc, ExtReducedId::STRINGS_CTN_DECOMPOSE); } } } @@ -730,9 +730,10 @@ std::string ExtfSolver::debugPrintModel() for (const Node& n : extf) { ss << "- " << n; - if (!d_extt.isActive(n)) + ExtReducedId id; + if (!d_extt.isActive(n, id)) { - ss << " :extt-inactive"; + ss << " :extt-inactive " << id; } if (!d_extfInfoTmp[n].d_modelActive) { diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 8a0429fae..6f218e5be 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -268,18 +268,9 @@ bool InferenceManager::hasProcessed() const return d_state.isInConflict() || hasPending(); } -void InferenceManager::markCongruent(Node a, Node b) +void InferenceManager::markReduced(Node n, ExtReducedId id, bool contextDepend) { - Assert(a.getKind() == b.getKind()); - if (d_extt.hasFunctionKind(a.getKind())) - { - d_extt.markCongruent(a, b); - } -} - -void InferenceManager::markReduced(Node n, bool contextDepend) -{ - d_extt.markReduced(n, contextDepend); + d_extt.markReduced(n, id, contextDepend); } void InferenceManager::processConflict(const InferInfo& ii) diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index cfb8614ca..abc5c5709 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -219,19 +219,12 @@ class InferenceManager : public InferenceManagerBuffered bool hasProcessed() const; // ------------------------------------------------- extended theory - /** - * Mark that terms a and b are congruent in the current context. - * This makes a call to markCongruent in the extended theory object of - * the parent theory if the kind of a (and b) is owned by the extended - * theory. - */ - void markCongruent(Node a, Node b); /** * Mark that extended function is reduced. If contextDepend is true, * then this mark is SAT-context dependent, otherwise it is user-context * dependent (see ExtTheory::markReduced). */ - void markReduced(Node n, bool contextDepend = true); + void markReduced(Node n, ExtReducedId id, bool contextDepend = true); // ------------------------------------------------- end extended theory /** diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 85d66cd54..151761329 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -361,14 +361,14 @@ bool RegExpSolver::checkEqcInclusion(std::vector& mems) { // ~str.in.re(x, R1) includes ~str.in.re(x, R2) ---> // mark ~str.in.re(x, R2) as reduced - d_im.markReduced(m2Lit); + d_im.markReduced(m2Lit, ExtReducedId::STRINGS_REGEXP_INCLUDE_NEG); remove.insert(m2); } else { // str.in.re(x, R1) includes str.in.re(x, R2) ---> // mark str.in.re(x, R1) as reduced - d_im.markReduced(m1Lit); + d_im.markReduced(m1Lit, ExtReducedId::STRINGS_REGEXP_INCLUDE); remove.insert(m1); // We don't need to process m1 anymore @@ -489,12 +489,12 @@ bool RegExpSolver::checkEqcIntersect(const std::vector& mems) { // if R1 = intersect( R1, R2 ), then x in R1 ^ x in R2 is equivalent // to x in R1, hence x in R2 can be marked redundant. - d_im.markReduced(m); + d_im.markReduced(m, ExtReducedId::STRINGS_REGEXP_INTER_SUBSUME); } else if (mresr == m) { // same as above, opposite direction - d_im.markReduced(mi); + d_im.markReduced(mi, ExtReducedId::STRINGS_REGEXP_INTER_SUBSUME); } else { @@ -510,8 +510,8 @@ bool RegExpSolver::checkEqcIntersect(const std::vector& mems) d_im.sendInference( vec_nodes, mres, InferenceId::STRINGS_RE_INTER_INFER, false, true); // both are reduced - d_im.markReduced(m); - d_im.markReduced(mi); + d_im.markReduced(m, ExtReducedId::STRINGS_REGEXP_INTER); + d_im.markReduced(mi, ExtReducedId::STRINGS_REGEXP_INTER); // do not send more than one lemma for this class return true; } -- 2.30.2