diff options
Diffstat (limited to 'src/theory/strings')
-rw-r--r-- | src/theory/strings/extf_solver.cpp | 13 | ||||
-rw-r--r-- | src/theory/strings/inference_manager.cpp | 13 | ||||
-rw-r--r-- | src/theory/strings/inference_manager.h | 9 | ||||
-rw-r--r-- | src/theory/strings/regexp_solver.cpp | 12 |
4 files changed, 16 insertions, 31 deletions
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<Node> 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 @@ -220,18 +220,11 @@ class InferenceManager : public InferenceManagerBuffered // ------------------------------------------------- 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<Node>& 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<Node>& 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<Node>& 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; } |