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.
}
bool ExtfSolver::hasExtendedFunctions() const { return d_hasExtf.get(); }
+std::vector<Node> ExtfSolver::getActive(Kind k) const
+{
+ return d_extt->getActive(k);
+}
+
} // namespace strings
} // namespace theory
} // namespace CVC4
const std::map<Node, ExtfInfoTmp>& 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<Node> getActive(Kind k) const;
private:
/** do reduction
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)
return NodeManager::currentNM()->mkNode(AND, c1, c2);
}
+void RegExpSolver::checkMemberships()
+{
+ // add the memberships
+ std::vector<Node> mems = d_esolver.getActive(STRING_IN_REGEXP);
+ // maps representatives to regular expression memberships in that class
+ std::map<Node, std::vector<Node> > assertedMems;
+ const std::map<Node, ExtfInfoTmp>& einfo = d_esolver.getInfo();
+ std::map<Node, ExtfInfoTmp>::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<bool>();
+ 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<Node, std::vector<Node> >& mems)
{
bool addedLemma = false;
#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"
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
* engine of the theory of strings.
*/
void check(const std::map<Node, std::vector<Node>>& mems);
-
- private:
/**
* Check memberships in equivalence class for regular expression
* inclusion.
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);
/**
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)
{
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);
return false;
}
-void TheoryStrings::checkMemberships()
-{
- // add the memberships
- std::vector<Node> mems = getExtTheory()->getActive(kind::STRING_IN_REGEXP);
- // maps representatives to regular expression memberships in that class
- std::map<Node, std::vector<Node> > assertedMems;
- const std::map<Node, ExtfInfoTmp>& einfo = d_esolver->getInfo();
- std::map<Node, ExtfInfoTmp>::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<bool>();
- 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())
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;
}
*/
std::unique_ptr<ExtfSolver> d_esolver;
/** regular expression solver module */
- RegExpSolver d_regexp_solver;
+ std::unique_ptr<RegExpSolver> d_rsolver;
/** regular expression elimination module */
RegExpElimination d_regexp_elim;
/** Strings finite model finding decision strategy */
* 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
projects / cvc5.git / commitdiff