From 25d2ed390bf5ad825fadbc4ed21676100b01de68 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 22 Feb 2020 10:07:44 -0600 Subject: [PATCH] Move check memberships to reg exp solver (#3793) There was previously a function in TheoryStrings to make the proper call to checkMembership. In the refactored code, this is no longer necessary and the interface to RegExp can be simplified. --- src/theory/strings/extf_solver.cpp | 5 ++++ src/theory/strings/extf_solver.h | 5 ++++ src/theory/strings/regexp_solver.cpp | 33 ++++++++++++++++++++++++ src/theory/strings/regexp_solver.h | 17 +++++++++++-- src/theory/strings/theory_strings.cpp | 36 +++------------------------ src/theory/strings/theory_strings.h | 11 +------- 6 files changed, 62 insertions(+), 45 deletions(-) diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index e22528490..6ab74cf9a 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -668,6 +668,11 @@ const std::map& ExtfSolver::getInfo() const } bool ExtfSolver::hasExtendedFunctions() const { return d_hasExtf.get(); } +std::vector ExtfSolver::getActive(Kind k) const +{ + return d_extt->getActive(k); +} + } // namespace strings } // namespace theory } // namespace CVC4 diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h index e0e41bc3d..4c848f430 100644 --- a/src/theory/strings/extf_solver.h +++ b/src/theory/strings/extf_solver.h @@ -145,6 +145,11 @@ class ExtfSolver const std::map& getInfo() const; /** Are there any active extended functions? */ bool hasExtendedFunctions() const; + /** + * Get the function applications of kind k that are active in the current + * context (see ExtTheory::getActive). + */ + std::vector getActive(Kind k) const; private: /** do reduction diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index e4fe2cf17..5b41feacb 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -36,11 +36,13 @@ namespace strings { RegExpSolver::RegExpSolver(TheoryStrings& p, SolverState& s, InferenceManager& im, + ExtfSolver& es, context::Context* c, context::UserContext* u) : d_parent(p), d_state(s), d_im(im), + d_esolver(es), d_regexp_ucached(u), d_regexp_ccached(c), d_processed_memberships(c) @@ -57,6 +59,37 @@ Node RegExpSolver::mkAnd(Node c1, Node c2) return NodeManager::currentNM()->mkNode(AND, c1, c2); } +void RegExpSolver::checkMemberships() +{ + // add the memberships + std::vector mems = d_esolver.getActive(STRING_IN_REGEXP); + // maps representatives to regular expression memberships in that class + std::map > assertedMems; + const std::map& einfo = d_esolver.getInfo(); + std::map::const_iterator it; + for (unsigned i = 0; i < mems.size(); i++) + { + Node n = mems[i]; + Assert(n.getKind() == STRING_IN_REGEXP); + it = einfo.find(n); + Assert(it != einfo.end()); + if (!it->second.d_const.isNull()) + { + bool pol = it->second.d_const.getConst(); + Trace("strings-process-debug") + << " add membership : " << n << ", pol = " << pol << std::endl; + Node r = d_state.getRepresentative(n[0]); + assertedMems[r].push_back(pol ? n : n.negate()); + } + else + { + Trace("strings-process-debug") + << " irrelevant (non-asserted) membership : " << n << std::endl; + } + } + check(assertedMems); +} + void RegExpSolver::check(const std::map >& mems) { bool addedLemma = false; diff --git a/src/theory/strings/regexp_solver.h b/src/theory/strings/regexp_solver.h index a43ea516a..4880af905 100644 --- a/src/theory/strings/regexp_solver.h +++ b/src/theory/strings/regexp_solver.h @@ -23,6 +23,7 @@ #include "context/cdlist.h" #include "context/context.h" #include "expr/node.h" +#include "theory/strings/extf_solver.h" #include "theory/strings/inference_manager.h" #include "theory/strings/regexp_operation.h" #include "theory/strings/solver_state.h" @@ -47,10 +48,22 @@ class RegExpSolver RegExpSolver(TheoryStrings& p, SolverState& s, InferenceManager& im, + ExtfSolver& es, context::Context* c, context::UserContext* u); ~RegExpSolver() {} + /** check regular expression memberships + * + * This checks the satisfiability of all regular expression memberships + * of the form (not) s in R. We use various heuristic techniques based on + * unrolling, combined with techniques from Liang et al, "A Decision Procedure + * for Regular Membership and Length Constraints over Unbounded Strings", + * FroCoS 2015. + */ + void checkMemberships(); + + private: /** check * * Tells this solver to check whether the regular expressions in mems @@ -63,8 +76,6 @@ class RegExpSolver * engine of the theory of strings. */ void check(const std::map>& mems); - - private: /** * Check memberships in equivalence class for regular expression * inclusion. @@ -106,6 +117,8 @@ class RegExpSolver SolverState& d_state; /** the output channel of the parent of this object */ InferenceManager& d_im; + /** reference to the extended function solver of the parent */ + ExtfSolver& d_esolver; // check membership constraints Node mkAnd(Node c1, Node c2); /** diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 5be2f96d4..d3d75a98d 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -79,7 +79,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_bsolver(c, u, d_state, d_im), d_csolver(c, u, d_state, d_im, d_sk_cache, d_bsolver), d_esolver(nullptr), - d_regexp_solver(*this, d_state, d_im, c, u), + d_rsolver(nullptr), d_stringsFmf(c, u, valuation, d_sk_cache), d_strategy_init(false) { @@ -87,6 +87,7 @@ TheoryStrings::TheoryStrings(context::Context* c, ExtTheory* extt = getExtTheory(); d_esolver.reset(new ExtfSolver( c, u, d_state, d_im, d_sk_cache, d_bsolver, d_csolver, extt)); + d_rsolver.reset(new RegExpSolver(*this, d_state, d_im, *d_esolver, c, u)); getExtTheory()->addFunctionKind(kind::STRING_SUBSTR); getExtTheory()->addFunctionKind(kind::STRING_STRIDOF); getExtTheory()->addFunctionKind(kind::STRING_ITOS); @@ -726,37 +727,6 @@ bool TheoryStrings::needsCheckLastEffort() { return false; } -void TheoryStrings::checkMemberships() -{ - // add the memberships - std::vector mems = getExtTheory()->getActive(kind::STRING_IN_REGEXP); - // maps representatives to regular expression memberships in that class - std::map > assertedMems; - const std::map& einfo = d_esolver->getInfo(); - std::map::const_iterator it; - for (unsigned i = 0; i < mems.size(); i++) - { - Node n = mems[i]; - Assert(n.getKind() == STRING_IN_REGEXP); - it = einfo.find(n); - Assert(it != einfo.end()); - if (!it->second.d_const.isNull()) - { - bool pol = it->second.d_const.getConst(); - Trace("strings-process-debug") - << " add membership : " << n << ", pol = " << pol << std::endl; - Node r = d_state.getRepresentative(n[0]); - assertedMems[r].push_back(pol ? n : n.negate()); - } - else - { - Trace("strings-process-debug") - << " irrelevant (non-asserted) membership : " << n << std::endl; - } - } - d_regexp_solver.check(assertedMems); -} - /** Conflict when merging two constants */ void TheoryStrings::conflict(TNode a, TNode b){ if (!d_state.isInConflict()) @@ -1223,7 +1193,7 @@ void TheoryStrings::runInferStep(InferStep s, int effort) case CHECK_LENGTH_EQC: d_csolver.checkLengthsEqc(); break; case CHECK_REGISTER_TERMS_NF: checkRegisterTermsNormalForms(); break; case CHECK_EXTF_REDUCTION: d_esolver->checkExtfReductions(effort); break; - case CHECK_MEMBERSHIP: checkMemberships(); break; + case CHECK_MEMBERSHIP: d_rsolver->checkMemberships(); break; case CHECK_CARDINALITY: d_bsolver.checkCardinality(); break; default: Unreachable(); break; } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index f40af6e67..e0fca1b2e 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -344,7 +344,7 @@ private: */ std::unique_ptr d_esolver; /** regular expression solver module */ - RegExpSolver d_regexp_solver; + std::unique_ptr d_rsolver; /** regular expression elimination module */ RegExpElimination d_regexp_elim; /** Strings finite model finding decision strategy */ @@ -392,15 +392,6 @@ private: * there does not exist a term of the form str.len(si) in the current context. */ void checkRegisterTermsNormalForms(); - /** check regular expression memberships - * - * This checks the satisfiability of all regular expression memberships - * of the form (not) s in R. We use various heuristic techniques based on - * unrolling, combined with techniques from Liang et al, "A Decision Procedure - * for Regular Membership and Length Constraints over Unbounded Strings", - * FroCoS 2015. - */ - void checkMemberships(); //-----------------------end inference steps //-----------------------representation of the strategy -- 2.30.2