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.
return retVal;
}
-bool NlExtTheoryCallback::isExtfReduced(int effort,
- Node n,
- Node on,
- std::vector<Node>& exp)
+bool NlExtTheoryCallback::isExtfReduced(
+ int effort, Node n, Node on, std::vector<Node>& 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")
bool isExtfReduced(int effort,
Node n,
Node on,
- std::vector<Node>& exp) override;
+ std::vector<Node>& exp,
+ ExtReducedId& id) override;
private:
/** The underlying equality engine. */
Trace("nl-ext") << "NonlinearExtension::check, effort = " << e << std::endl;
if (e == Theory::EFFORT_FULL)
{
- d_extTheory.clearCache();
d_needsLastCall = true;
if (options::nlExtRewrites())
{
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<Node>& vars,
{
return false;
}
-bool ExtTheoryCallback::isExtfReduced(int effort,
- Node n,
- Node on,
- std::vector<Node>& exp)
+bool ExtTheoryCallback::isExtfReduced(
+ int effort, Node n, Node on, std::vector<Node>& exp, ExtReducedId& id)
{
+ id = ExtReducedId::SR_CONST;
return n.isConst();
}
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);
}
Node ExtTheory::getSubstitutedTerm(int effort,
Node term,
- std::vector<Node>& exp,
- bool useCache)
+ std::vector<Node>& 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<Node> terms;
terms.push_back(term);
std::vector<Node> sterms;
std::vector<std::vector<Node> > 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());
void ExtTheory::getSubstitutedTerms(int effort,
const std::vector<Node>& terms,
std::vector<Node>& sterms,
- std::vector<std::vector<Node> >& exp,
- bool useCache)
+ std::vector<std::vector<Node> >& 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<Node> vars;
+ std::vector<Node> sub;
+ std::map<Node, std::vector<Node> > 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<Node>());
- 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<Node> vars;
- std::vector<Node> sub;
- std::map<Node, std::vector<Node> > expc;
- for (const Node& n : terms)
+ // do substitution, rewrite
+ std::map<Node, ExtfInfo>::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<Node, ExtfInfo>::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<Node> expn;
+ if (useSubs)
{
- Node ns = n;
- std::vector<Node> 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<Node, ExtfInfo>::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<Node, ExtfInfo>::iterator iti = d_extf_info.find(n);
- Assert(iti != d_extf_info.end());
- for (const Node& v : iti->second.d_vars)
+ std::map<Node, std::vector<Node> >::iterator itx = expc.find(v);
+ if (itx != expc.end())
{
- std::map<Node, std::vector<Node> >::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);
}
}
}
addedLemma = true;
}
}
- markReduced(n, satDep);
+ markReduced(n, ExtReducedId::REDUCTION, satDep);
}
}
}
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.
}
// 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
}
}
-// 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<Node>& 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;
}
return active;
}
-void ExtTheory::clearCache() { d_gst_cache.clear(); }
-
} // namespace theory
} // namespace cvc5
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.
* @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<Node>& exp);
+ virtual bool isExtfReduced(
+ int effort, Node n, Node on, std::vector<Node>& exp, ExtReducedId& id);
/**
* Get reduction for node n.
*/
class ExtTheory
{
- typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
- typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+ using NodeBoolMap = context::CDHashMap<Node, bool, NodeHashFunction>;
+ using NodeExtReducedIdMap =
+ context::CDHashMap<Node, ExtReducedId, NodeHashFunction>;
+ using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
public:
/** constructor
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; }
* 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
*
* 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<Node>& terms,
std::vector<Node>& sterms,
- std::vector<std::vector<Node> >& exp,
- bool useCache = false);
+ std::vector<std::vector<Node> >& 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<Node>& exp,
- bool useCache = false);
- /** clear the cache for getSubstitutedTerm */
- void clearCache();
+ Node getSubstitutedTerm(int effort, Node term, std::vector<Node>& exp);
/** doInferences
*
* This function performs "context-dependent simplification". The method takes
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<Node> getActive() const;
/** get the set of active terms from d_ext_func_terms of kind k */
static std::vector<Node> 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<Node>& terms,
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.
// 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<Node> 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<int, std::map<Node, SubsTermInfo> > d_gst_cache;
};
} // namespace theory
}
// 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
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)
{
{
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<Node> exps;
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);
}
}
}
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)
{
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)
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
/**
{
// ~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
{
// 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
{
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;
}
projects / cvc5.git / commitdiff