summaryrefslogtreecommitdiff
path: root/src/theory/ext_theory.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2021-04-09 14:21:11 -0500
committerGitHub <noreply@github.com>2021-04-09 19:21:11 +0000
commit6923f0cb9930332a61e187d3b4d1a7ec7e65b15c (patch)
treedc6712e1b30352c60c9ca2f091b38136e2e92108 /src/theory/ext_theory.h
parente5358e498db6d934d0b8704cfd023b0f67b6fbc0 (diff)
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.
Diffstat (limited to 'src/theory/ext_theory.h')
-rw-r--r--src/theory/ext_theory.h116
1 files changed, 72 insertions, 44 deletions
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<Node>& exp);
+ virtual bool isExtfReduced(
+ int effort, Node n, Node on, std::vector<Node>& exp, ExtReducedId& id);
/**
* Get reduction for node n.
@@ -117,8 +163,10 @@ class ExtTheoryCallback
*/
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
@@ -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<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
@@ -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<Node> 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<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,
@@ -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<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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback