std::map<Node, std::vector<PairNodes> > d_split_cache;
void simplifyPRegExp(Node s, Node r, std::vector<Node> &new_nodes);
void simplifyNRegExp(Node s, Node r, std::vector<Node> &new_nodes);
- std::string niceChar(Node r);
+ /**
+ * Helper function for mkString, pretty prints constant or variable regular
+ * expression r.
+ */
+ static std::string niceChar(Node r);
Node mkAllExceptOne(unsigned c);
bool isPairNodesInSet(std::set<PairNodes> &s, Node n1, Node n2);
RegExpOpr();
~RegExpOpr();
+ /**
+ * Returns true if r is a "constant" regular expression, that is, a set
+ * of regular expression operators whose subterms of the form (str.to.re t)
+ * are such that t is a constant (or rewrites to one).
+ */
bool checkConstRegExp( Node r );
void simplify(Node t, std::vector< Node > &new_nodes, bool polarity);
int delta( Node r, Node &exp );
int derivativeS( Node r, CVC4::String c, Node &retNode );
Node derivativeSingle( Node r, CVC4::String c );
+ /**
+ * Returns the regular expression intersection of r1 and r2. If r1 or r2 is
+ * not constant, then this method returns null and sets spflag to true.
+ */
Node intersect(Node r1, Node r2, bool &spflag);
-
- std::string mkString( Node r );
+ /** Get the pretty printed version of the regular expression r */
+ static std::string mkString(Node r);
};
}/* CVC4::theory::strings namespace */
#include <cmath>
#include "options/strings_options.h"
+#include "theory/ext_theory.h"
#include "theory/strings/theory_strings.h"
#include "theory/strings/theory_strings_rewriter.h"
#include "theory/strings/theory_strings_utils.h"
context::UserContext* u)
: d_parent(p),
d_im(im),
- d_regexp_memberships(c),
d_regexp_ucached(u),
d_regexp_ccached(c),
- d_pos_memberships(c),
- d_neg_memberships(c),
- d_inter_cache(c),
- d_inter_index(c),
d_processed_memberships(c)
{
d_emptyString = NodeManager::currentNM()->mkConst(::CVC4::String(""));
d_false = NodeManager::currentNM()->mkConst(false);
}
-unsigned RegExpSolver::getNumMemberships(Node n, bool isPos)
-{
- if (isPos)
- {
- NodeUIntMap::const_iterator it = d_pos_memberships.find(n);
- if (it != d_pos_memberships.end())
- {
- return (*it).second;
- }
- }
- else
- {
- NodeUIntMap::const_iterator it = d_neg_memberships.find(n);
- if (it != d_neg_memberships.end())
- {
- return (*it).second;
- }
- }
- return 0;
-}
-
-Node RegExpSolver::getMembership(Node n, bool isPos, unsigned i)
-{
- return isPos ? d_pos_memberships_data[n][i] : d_neg_memberships_data[n][i];
-}
-
Node RegExpSolver::mkAnd(Node c1, Node c2)
{
return NodeManager::currentNM()->mkNode(AND, c1, c2);
}
-void RegExpSolver::check()
+void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
{
bool addedLemma = false;
bool changed = false;
std::vector<Node> processed;
std::vector<Node> cprocessed;
- Trace("regexp-debug") << "Checking Memberships ... " << std::endl;
- for (NodeUIntMap::const_iterator itr_xr = d_pos_memberships.begin();
- itr_xr != d_pos_memberships.end();
- ++itr_xr)
+ Trace("regexp-process") << "Checking Memberships ... " << std::endl;
+ for (const std::pair<const Node, std::vector<Node> >& mr : mems)
{
- bool spflag = false;
- Node x = (*itr_xr).first;
- Trace("regexp-debug") << "Checking Memberships for " << x << std::endl;
- if (d_inter_index.find(x) == d_inter_index.end())
+ Trace("regexp-process")
+ << "Memberships(" << mr.first << ") = " << mr.second << std::endl;
+ if (!checkEqcIntersect(mr.second))
{
- d_inter_index[x] = 0;
- }
- int cur_inter_idx = d_inter_index[x];
- unsigned n_pmem = (*itr_xr).second;
- Assert(getNumMemberships(x, true) == n_pmem);
- if (cur_inter_idx != (int)n_pmem)
- {
- if (n_pmem == 1)
- {
- d_inter_cache[x] = getMembership(x, true, 0);
- d_inter_index[x] = 1;
- Trace("regexp-debug") << "... only one choice " << std::endl;
- }
- else if (n_pmem > 1)
- {
- Node r;
- if (d_inter_cache.find(x) != d_inter_cache.end())
- {
- r = d_inter_cache[x];
- }
- if (r.isNull())
- {
- r = getMembership(x, true, 0);
- cur_inter_idx = 1;
- }
-
- unsigned k_start = cur_inter_idx;
- Trace("regexp-debug") << "... staring from : " << cur_inter_idx
- << ", we have " << n_pmem << std::endl;
- for (unsigned k = k_start; k < n_pmem; k++)
- {
- Node r2 = getMembership(x, true, k);
- r = d_regexp_opr.intersect(r, r2, spflag);
- if (spflag)
- {
- break;
- }
- else if (r == d_emptyRegexp)
- {
- std::vector<Node> vec_nodes;
- for (unsigned kk = 0; kk <= k; kk++)
- {
- Node rr = getMembership(x, true, kk);
- Node n =
- NodeManager::currentNM()->mkNode(STRING_IN_REGEXP, x, rr);
- vec_nodes.push_back(n);
- }
- Node conc;
- d_im.sendInference(vec_nodes, conc, "INTERSECT CONFLICT", true);
- addedLemma = true;
- break;
- }
- if (d_im.hasConflict())
- {
- break;
- }
- }
- // updates
- if (!d_im.hasConflict() && !spflag)
- {
- d_inter_cache[x] = r;
- d_inter_index[x] = (int)n_pmem;
- }
- }
+ // conflict discovered, return
+ return;
}
}
<< std::endl;
if (!addedLemma)
{
+ // get all memberships
+ std::vector<Node> allMems;
+ for (const std::pair<const Node, std::vector<Node> >& mr : mems)
+ {
+ for (const Node& m : mr.second)
+ {
+ bool polarity = m.getKind() != NOT;
+ if (polarity || !options::stringIgnNegMembership())
+ {
+ allMems.push_back(m);
+ }
+ }
+ }
+
NodeManager* nm = NodeManager::currentNM();
// representatives of strings that are the LHS of positive memberships that
// we unfolded
// check positive (e=0), then negative (e=1) memberships
for (unsigned e = 0; e < 2; e++)
{
- for (const Node& assertion : d_regexp_memberships)
+ for (const Node& assertion : allMems)
{
// check regular expression membership
Trace("regexp-debug")
}
}
+bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems)
+{
+ if (mems.empty())
+ {
+ // nothing to do
+ return true;
+ }
+ // the initial regular expression membership
+ Node mi;
+ NodeManager* nm = NodeManager::currentNM();
+ for (const Node& m : mems)
+ {
+ if (m.getKind() != STRING_IN_REGEXP)
+ {
+ // do not do negative
+ Assert(m.getKind() == NOT && m[0].getKind() == STRING_IN_REGEXP);
+ continue;
+ }
+ if (!d_regexp_opr.checkConstRegExp(m))
+ {
+ // cannot do intersection on RE with variables
+ continue;
+ }
+ if (mi.isNull())
+ {
+ // first regular expression seen
+ mi = m;
+ continue;
+ }
+ bool spflag = false;
+ Node resR = d_regexp_opr.intersect(mi[1], m[1], spflag);
+ // intersection should be computable
+ Assert(!resR.isNull());
+ Assert(!spflag);
+ if (resR == d_emptyRegexp)
+ {
+ // conflict, explain
+ std::vector<Node> vec_nodes;
+ vec_nodes.push_back(mi);
+ vec_nodes.push_back(m);
+ if (mi[0] != m[0])
+ {
+ vec_nodes.push_back(mi[0].eqNode(m[0]));
+ }
+ Node conc;
+ d_im.sendInference(vec_nodes, conc, "INTERSECT CONFLICT", true);
+ // conflict, return
+ return false;
+ }
+ // rewrite to ensure the equality checks below are precise
+ Node mres = Rewriter::rewrite(nm->mkNode(STRING_IN_REGEXP, mi[0], resR));
+ if (mres == mi)
+ {
+ // 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_parent.getExtTheory()->markReduced(m);
+ }
+ else if (mres == m)
+ {
+ // same as above, opposite direction
+ d_parent.getExtTheory()->markReduced(mi);
+ }
+ else
+ {
+ // new conclusion
+ // (x in R ^ y in R2 ^ x = y) => (x in intersect(R1,R2))
+ std::vector<Node> vec_nodes;
+ vec_nodes.push_back(mi);
+ vec_nodes.push_back(m);
+ if (mi[0] != m[0])
+ {
+ vec_nodes.push_back(mi[0].eqNode(m[0]));
+ }
+ d_im.sendInference(vec_nodes, mres, "INTERSECT INFER", true);
+ // both are reduced
+ d_parent.getExtTheory()->markReduced(m);
+ d_parent.getExtTheory()->markReduced(mi);
+ // do not send more than one lemma for this class
+ return true;
+ }
+ }
+ return true;
+}
+
bool RegExpSolver::checkPDerivative(
Node x, Node r, Node atom, bool& addedLemma, std::vector<Node>& nf_exp)
{
return false;
}
-void RegExpSolver::addMembership(Node assertion)
-{
- bool polarity = assertion.getKind() != NOT;
- TNode atom = polarity ? assertion : assertion[0];
- Node x = atom[0];
- Node r = atom[1];
- if (polarity)
- {
- unsigned index = 0;
- NodeUIntMap::const_iterator it = d_pos_memberships.find(x);
- if (it != d_pos_memberships.end())
- {
- index = (*it).second;
- for (unsigned k = 0; k < index; k++)
- {
- if (k < d_pos_memberships_data[x].size())
- {
- if (d_pos_memberships_data[x][k] == r)
- {
- return;
- }
- }
- else
- {
- break;
- }
- }
- }
- d_pos_memberships[x] = index + 1;
- if (index < d_pos_memberships_data[x].size())
- {
- d_pos_memberships_data[x][index] = r;
- }
- else
- {
- d_pos_memberships_data[x].push_back(r);
- }
- }
- else if (!options::stringIgnNegMembership())
- {
- unsigned index = 0;
- NodeUIntMap::const_iterator it = d_neg_memberships.find(x);
- if (it != d_neg_memberships.end())
- {
- index = (*it).second;
- for (unsigned k = 0; k < index; k++)
- {
- if (k < d_neg_memberships_data[x].size())
- {
- if (d_neg_memberships_data[x][k] == r)
- {
- return;
- }
- }
- else
- {
- break;
- }
- }
- }
- d_neg_memberships[x] = index + 1;
- if (index < d_neg_memberships_data[x].size())
- {
- d_neg_memberships_data[x][index] = r;
- }
- else
- {
- d_neg_memberships_data[x].push_back(r);
- }
- }
- // old
- if (polarity || !options::stringIgnNegMembership())
- {
- d_regexp_memberships.push_back(assertion);
- }
-}
-
Node RegExpSolver::getNormalSymRegExp(Node r, std::vector<Node>& nf_exp)
{
Node ret = r;
context::UserContext* u);
~RegExpSolver() {}
- /** add membership
- *
- * This informs this class that assertion is asserted in the current context.
- * We expect that assertion is a (possibly negated) regular expression
- * membership.
- */
- void addMembership(Node assertion);
/** check
*
- * Tells this solver to check whether the regular expressions asserted to it
+ * Tells this solver to check whether the regular expressions in mems
* are consistent. If they are not, then this class will call the
* sendInference method of its parent TheoryString object, indicating that
* it requires a conflict or lemma to be processed.
+ *
+ * The argument mems maps representative string terms r to memberships of the
+ * form (t in R) or ~(t in R), where t = r currently holds in the equality
+ * engine of the theory of strings.
*/
- void check();
+ void check(const std::map<Node, std::vector<Node>>& mems);
private:
+ /**
+ * Check memberships for equivalence class.
+ * The vector mems is a vector of memberships of the form:
+ * (~) (x1 in R1 ) ... (~) (xn in Rn)
+ * where x1 = ... = xn in the current context.
+ *
+ * This method may add lemmas or conflicts via the inference manager.
+ *
+ * This method returns false if it discovered a conflict for this set of
+ * assertions, and true otherwise. It discovers a conflict e.g. if mems
+ * contains (xi in Ri) and (xj in Rj) and intersect(xi,xj) is empty.
+ */
+ bool checkEqcIntersect(const std::vector<Node>& mems);
// Constants
Node d_emptyString;
Node d_emptyRegexp;
bool deriveRegExp(Node x, Node r, Node atom, std::vector<Node>& ant);
Node getNormalSymRegExp(Node r, std::vector<Node>& nf_exp);
// regular expression memberships
- NodeList d_regexp_memberships;
NodeSet d_regexp_ucached;
NodeSet d_regexp_ccached;
- // stored assertions
- NodeUIntMap d_pos_memberships;
- std::map<Node, std::vector<Node> > d_pos_memberships_data;
- NodeUIntMap d_neg_memberships;
- std::map<Node, std::vector<Node> > d_neg_memberships_data;
// semi normal forms for symbolic expression
std::map<Node, Node> d_nf_regexps;
std::map<Node, std::vector<Node> > d_nf_regexps_exp;
- // intersection
- NodeNodeMap d_inter_cache;
- NodeIntMap d_inter_index;
// processed memberships
NodeSet d_processed_memberships;
/** regular expression operation module */
projects / cvc5.git / commitdiff