mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
update regex membership to be slightly better tuned
This commit is contained in:
parent
f4ed432244
commit
c9cae77304
|
@ -3790,6 +3790,7 @@ expr_ref seq_rewriter::simplify_path(expr* elem, expr* path) {
|
|||
|
||||
|
||||
expr_ref seq_rewriter::mk_der_antimirov_union(expr* r1, expr* r2) {
|
||||
verbose_stream() << "union " << r1->get_id() << " " << r2->get_id() << "\n";
|
||||
return mk_der_op(_OP_RE_ANTIMIROV_UNION, r1, r2);
|
||||
}
|
||||
|
||||
|
@ -4584,7 +4585,7 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
|
|||
result = mk_in_antimirov(tl, mk_antimirov_deriv(hd, b, m().mk_true()));
|
||||
return BR_REWRITE_FULL;
|
||||
}
|
||||
|
||||
|
||||
if (get_head_tail_reversed(a, hd, tl)) {
|
||||
result = re().mk_reverse(re().mk_derivative(tl, re().mk_reverse(b)));
|
||||
result = re().mk_in_re(hd, result);
|
||||
|
|
|
@ -96,8 +96,6 @@ Equality solving using stochastic Nelson.
|
|||
#include "ast/sls/sls_context.h"
|
||||
#include "ast/ast_pp.h"
|
||||
|
||||
#include "ast/rewriter/th_rewriter.h"
|
||||
|
||||
|
||||
namespace sls {
|
||||
|
||||
|
@ -105,7 +103,8 @@ namespace sls {
|
|||
plugin(c),
|
||||
seq(c.get_manager()),
|
||||
a(c.get_manager()),
|
||||
rw(c.get_manager())
|
||||
rw(c.get_manager()),
|
||||
thrw(c.get_manager())
|
||||
{
|
||||
m_fid = seq.get_family_id();
|
||||
}
|
||||
|
@ -1705,13 +1704,17 @@ namespace sls {
|
|||
|
||||
// Regular expressions
|
||||
|
||||
bool seq_plugin::is_in_re(zstring const& s, expr* r) {
|
||||
expr_ref sval(seq.str.mk_string(s), m);
|
||||
th_rewriter rw(m);
|
||||
expr_ref in_re(seq.re.mk_in_re(sval, r), m);
|
||||
rw(in_re);
|
||||
SASSERT(m.limit().is_canceled() || m.is_true(in_re) || m.is_false(in_re));
|
||||
return m.is_true(in_re);
|
||||
bool seq_plugin::is_in_re(zstring const& s, expr* _r) {
|
||||
expr_ref r(_r, m);
|
||||
for (unsigned i = 0; i < s.length(); ++i) {
|
||||
expr_ref ch(seq.str.mk_char(s[i]), m);
|
||||
expr_ref r1 = rw.mk_derivative(ch, r);
|
||||
if (seq.re.is_empty(r1))
|
||||
return false;
|
||||
r = r1;
|
||||
}
|
||||
auto info = seq.re.get_info(r);
|
||||
return info.nullable == l_true;
|
||||
}
|
||||
|
||||
bool seq_plugin::repair_down_in_re(app* e) {
|
||||
|
@ -1721,12 +1724,8 @@ namespace sls {
|
|||
if (!info.interpreted)
|
||||
return false;
|
||||
auto s = strval0(x);
|
||||
expr_ref xval(seq.str.mk_string(s), m);
|
||||
expr_ref in_re(seq.re.mk_in_re(xval, y), m);
|
||||
th_rewriter thrw(m);
|
||||
thrw(in_re);
|
||||
SASSERT(m.limit().is_canceled() || m.is_true(in_re) || m.is_false(in_re));
|
||||
if (m.is_true(in_re) == ctx.is_true(e))
|
||||
bool in_re = is_in_re(s, y);
|
||||
if (in_re == ctx.is_true(e))
|
||||
return true;
|
||||
|
||||
if (is_value(x))
|
||||
|
|
|
@ -20,7 +20,7 @@ Author:
|
|||
#include "ast/seq_decl_plugin.h"
|
||||
#include "ast/arith_decl_plugin.h"
|
||||
#include "ast/rewriter/seq_rewriter.h"
|
||||
|
||||
#include "ast/rewriter/th_rewriter.h"
|
||||
|
||||
namespace sls {
|
||||
|
||||
|
@ -45,6 +45,7 @@ namespace sls {
|
|||
seq_util seq;
|
||||
arith_util a;
|
||||
seq_rewriter rw;
|
||||
th_rewriter thrw;
|
||||
scoped_ptr_vector<eval> m_values;
|
||||
indexed_uint_set m_chars;
|
||||
bool m_initialized = false;
|
||||
|
|
Loading…
Reference in a new issue