diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/strings/extf_solver.cpp | 27 | ||||
-rw-r--r-- | src/theory/strings/extf_solver.h | 11 |
2 files changed, 23 insertions, 15 deletions
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index 8ce2a3e81..0f4af2458 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -47,7 +47,8 @@ ExtfSolver::ExtfSolver(context::Context* c, d_statistics(statistics), d_preproc(&skc, u, statistics), d_hasExtf(c, false), - d_extfInferCache(c) + d_extfInferCache(c), + d_reduced(u) { d_extt->addFunctionKind(kind::STRING_SUBSTR); d_extt->addFunctionKind(kind::STRING_STRIDOF); @@ -69,7 +70,7 @@ ExtfSolver::ExtfSolver(context::Context* c, ExtfSolver::~ExtfSolver() {} -bool ExtfSolver::doReduction(int effort, Node n, bool& isCd) +bool ExtfSolver::doReduction(int effort, Node n) { Assert(d_extfInfoTmp.find(n) != d_extfInfoTmp.end()); if (!d_extfInfoTmp[n].d_modelActive) @@ -77,6 +78,11 @@ bool ExtfSolver::doReduction(int effort, Node n, bool& isCd) // n is not active in the model, no need to reduce return false; } + if (d_reduced.find(n)!=d_reduced.end()) + { + // already sent a reduction lemma + return false; + } // determine the effort level to process the extf at // 0 - at assertion time, 1+ - after no other reduction is applicable int r_effort = -1; @@ -118,9 +124,9 @@ bool ExtfSolver::doReduction(int effort, Node n, bool& isCd) Node xneqs = x.eqNode(s).negate(); d_im.sendInference(lexp, xneqs, Inference::CTN_NEG_EQUAL, true); } - // this depends on the current assertions, so we set that this - // inference is context-dependent. - isCd = true; + // this depends on the current assertions, so this + // inference is context-dependent + d_extt->markReduced(n, true); return true; } else @@ -168,7 +174,7 @@ bool ExtfSolver::doReduction(int effort, Node n, bool& isCd) Trace("strings-red-lemma") << "Reduction (positive contains) lemma : " << n << " => " << eq << std::endl; // context-dependent because it depends on the polarity of n itself - isCd = true; + d_extt->markReduced(n, true); } else if (k != kind::STRING_TO_CODE) { @@ -190,7 +196,8 @@ bool ExtfSolver::doReduction(int effort, Node n, bool& isCd) d_im.sendInference(d_emptyVec, nnlem, Inference::REDUCTION, true); Trace("strings-extf-debug") << " resolve extf : " << n << " based on reduction." << std::endl; - isCd = false; + // add as reduction lemma + d_reduced.insert(n); } return true; } @@ -209,12 +216,10 @@ void ExtfSolver::checkExtfReductions(int effort) Trace("strings-process") << " check " << n << ", active in model=" << d_extfInfoTmp[n].d_modelActive << std::endl; - // whether the reduction was context-dependent - bool isCd = false; - bool ret = doReduction(effort, n, isCd); + bool ret = doReduction(effort, n); if (ret) { - d_extt->markReduced(n, isCd); + // we do not mark as reduced, since we may want to evaluate if (d_im.hasProcessed()) { return; diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h index e7e2512bd..f0f0d790b 100644 --- a/src/theory/strings/extf_solver.h +++ b/src/theory/strings/extf_solver.h @@ -161,11 +161,12 @@ class ExtfSolver * This is called when an extended function application n is not able to be * simplified by context-depdendent simplification, and we are resorting to * expanding n to its full semantics via a reduction. This method returns - * true if it successfully reduced n by some reduction and sets isCd to - * true if the reduction was (SAT)-context-dependent, and false otherwise. - * The argument effort has the same meaning as in checkExtfReductions. + * true if it successfully reduced n by some reduction. If so, it either + * caches that the reduction lemma was sent, or marks n as reduced in this + * SAT-context. The argument effort has the same meaning as in + * checkExtfReductions. */ - bool doReduction(int effort, Node n, bool& isCd); + bool doReduction(int effort, Node n); /** check extended function inferences * * This function makes additional inferences for n that do not contribute @@ -205,6 +206,8 @@ class ExtfSolver context::CDO<bool> d_hasExtf; /** extended functions inferences cache */ NodeSet d_extfInferCache; + /** The set of extended functions we have sent reduction lemmas for */ + NodeSet d_reduced; }; } // namespace strings |