3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00

Add outline of elimination for regex membership constraints

This commit is contained in:
Nikolaj Bjorner 2025-01-07 14:17:20 -08:00
parent b6c0e6fe4b
commit ab9ea4e6e7
3 changed files with 41 additions and 1 deletions

View file

@ -21,6 +21,7 @@ Author:
#include "ast/arith_decl_plugin.h"
#include "ast/seq_decl_plugin.h"
#include "ast/pb_decl_plugin.h"
#include "ast/rewriter/seq_rewriter.h"
#include "ast/converters/expr_inverter.h"
class basic_expr_inverter : public iexpr_inverter {
@ -825,8 +826,9 @@ public:
class seq_expr_inverter : public iexpr_inverter {
seq_util seq;
seq_rewriter rw;
public:
seq_expr_inverter(ast_manager& m) : iexpr_inverter(m), seq(m) {}
seq_expr_inverter(ast_manager& m) : iexpr_inverter(m), seq(m), rw(m) {}
family_id get_fid() const override { return seq.get_family_id(); }
@ -878,7 +880,42 @@ public:
return true;
}
return false;
case OP_SEQ_IN_RE:
if (uncnstr(args[0]) && seq.re.is_ground(args[1])) {
#if 0
// requires auxiliary functions
// is_empty
// find_member
expr* r = args[1];
expr_ref not_r(seq.re.mk_complement(r), m);
lbool emp_r = rw.is_empty(r);
if (emp_r == l_undef)
return false;
if (emp_r == l_true) {
r = m.mk_false();
return true;
}
lbool emp_not_r = rw.is_empty(not_r);
if (emp_not_r == l_true) {
r = m.mk_true();
return true;
}
if (emp_not_r == l_false) {
mk_fresh_uncnstr_var_for(f, r);
expr_ref witness1 = rw.find_member(r);
expr_ref witness2 = rw.find_member(not_r);
if (!witness1 || !witness2)
return false;
if (m_mc)
add_def(args[0], m.mk_ite(r, witness1, witness2));
return true;
}
#endif
}
return false;
default:
verbose_stream() << mk_pp(f, m) << "\n";
return false;
}

View file

@ -594,6 +594,7 @@ public:
info get_info(expr* r) const;
std::string to_str(expr* r) const;
std::string to_strh(expr* r) const;
bool is_ground(expr* r) const { return get_info(r).interpreted; }
expr_ref mk_ite_simplify(expr* c, expr* t, expr* e)
{

View file

@ -243,6 +243,8 @@ elim_unconstrained::node& elim_unconstrained::get_node(expr* t) {
node& ch = get_node(arg);
SASSERT(ch.is_root());
ch.add_parent(*n);
if (is_uninterp_const(arg))
m_heap.increased(arg->get_id());
}
}
else if (is_quantifier(t)) {