mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 09:05:31 +00:00
add intersection using symbolic automata facility
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
4cf72e23e6
commit
df2d7e7628
8 changed files with 561 additions and 28 deletions
|
|
@ -25,6 +25,8 @@ Notes:
|
|||
#include"automaton.h"
|
||||
#include"well_sorted.h"
|
||||
#include"var_subst.h"
|
||||
#include"symbolic_automata_def.h"
|
||||
|
||||
|
||||
expr_ref sym_expr::accept(expr* e) {
|
||||
ast_manager& m = m_t.get_manager();
|
||||
|
|
@ -37,6 +39,7 @@ expr_ref sym_expr::accept(expr* e) {
|
|||
}
|
||||
case t_char:
|
||||
SASSERT(m.get_sort(e) == m.get_sort(m_t));
|
||||
SASSERT(m.get_sort(e) == m_sort);
|
||||
result = m.mk_eq(e, m_t);
|
||||
break;
|
||||
case t_range: {
|
||||
|
|
@ -67,8 +70,114 @@ struct display_expr1 {
|
|||
}
|
||||
};
|
||||
|
||||
class sym_expr_boolean_algebra : public boolean_algebra<sym_expr*> {
|
||||
ast_manager& m;
|
||||
expr_solver& m_solver;
|
||||
typedef sym_expr* T;
|
||||
public:
|
||||
sym_expr_boolean_algebra(ast_manager& m, expr_solver& s):
|
||||
m(m), m_solver(s) {}
|
||||
|
||||
virtual T mk_false() {
|
||||
expr_ref fml(m.mk_false(), m);
|
||||
return sym_expr::mk_pred(fml, m.mk_bool_sort()); // use of Bool sort for bound variable is arbitrary
|
||||
}
|
||||
virtual T mk_true() {
|
||||
expr_ref fml(m.mk_true(), m);
|
||||
return sym_expr::mk_pred(fml, m.mk_bool_sort());
|
||||
}
|
||||
virtual T mk_and(T x, T y) {
|
||||
if (x->is_char() && y->is_char()) {
|
||||
if (x->get_char() == y->get_char()) {
|
||||
return x;
|
||||
}
|
||||
if (m.are_distinct(x->get_char(), y->get_char())) {
|
||||
expr_ref fml(m.mk_false(), m);
|
||||
return sym_expr::mk_pred(fml, x->sort());
|
||||
}
|
||||
}
|
||||
var_ref v(m.mk_var(0, x->sort()), m);
|
||||
expr_ref fml1 = x->accept(v);
|
||||
expr_ref fml2 = y->accept(v);
|
||||
if (m.is_true(fml1)) return y;
|
||||
if (m.is_true(fml2)) return x;
|
||||
expr_ref fml(m.mk_and(fml1, fml2), m);
|
||||
return sym_expr::mk_pred(fml, x->sort());
|
||||
}
|
||||
virtual T mk_or(T x, T y) {
|
||||
if (x->is_char() && y->is_char() &&
|
||||
x->get_char() == y->get_char()) {
|
||||
return x;
|
||||
}
|
||||
var_ref v(m.mk_var(0, x->sort()), m);
|
||||
expr_ref fml1 = x->accept(v);
|
||||
expr_ref fml2 = y->accept(v);
|
||||
if (m.is_false(fml1)) return y;
|
||||
if (m.is_false(fml2)) return x;
|
||||
expr_ref fml(m.mk_or(fml1, fml2), m);
|
||||
return sym_expr::mk_pred(fml, x->sort());
|
||||
}
|
||||
|
||||
virtual T mk_and(unsigned sz, T const* ts) {
|
||||
switch (sz) {
|
||||
case 0: return mk_true();
|
||||
case 1: return ts[0];
|
||||
default: {
|
||||
T t = ts[0];
|
||||
for (unsigned i = 1; i < sz; ++i) {
|
||||
t = mk_and(t, ts[i]);
|
||||
}
|
||||
return t;
|
||||
}
|
||||
}
|
||||
}
|
||||
virtual T mk_or(unsigned sz, T const* ts) {
|
||||
switch (sz) {
|
||||
case 0: return mk_false();
|
||||
case 1: return ts[0];
|
||||
default: {
|
||||
T t = ts[0];
|
||||
for (unsigned i = 1; i < sz; ++i) {
|
||||
t = mk_or(t, ts[i]);
|
||||
}
|
||||
return t;
|
||||
}
|
||||
}
|
||||
}
|
||||
virtual lbool is_sat(T x) {
|
||||
if (x->is_char()) {
|
||||
return l_true;
|
||||
}
|
||||
if (x->is_range()) {
|
||||
// TBD check lower is below upper.
|
||||
}
|
||||
expr_ref v(m.mk_fresh_const("x", x->sort()), m);
|
||||
expr_ref fml = x->accept(v);
|
||||
if (m.is_true(fml)) {
|
||||
return l_true;
|
||||
}
|
||||
if (m.is_false(fml)) {
|
||||
return l_false;
|
||||
}
|
||||
return m_solver.check_sat(fml);
|
||||
}
|
||||
virtual T mk_not(T x) {
|
||||
var_ref v(m.mk_var(0, x->sort()), m);
|
||||
expr_ref fml(m.mk_not(x->accept(v)), m);
|
||||
return sym_expr::mk_pred(fml, x->sort());
|
||||
}
|
||||
};
|
||||
|
||||
re2automaton::re2automaton(ast_manager& m): m(m), u(m), bv(m), m_ba(0), m_sa(0) {}
|
||||
|
||||
re2automaton::~re2automaton() {}
|
||||
|
||||
void re2automaton::set_solver(expr_solver* solver) {
|
||||
m_solver = solver;
|
||||
m_ba = alloc(sym_expr_boolean_algebra, m, *solver);
|
||||
m_sa = alloc(symbolic_automata_t, sm, *m_ba.get());
|
||||
}
|
||||
|
||||
re2automaton::re2automaton(ast_manager& m): m(m), u(m), bv(m) {}
|
||||
|
||||
eautomaton* re2automaton::operator()(expr* e) {
|
||||
eautomaton* r = re2aut(e);
|
||||
|
|
@ -136,7 +245,7 @@ eautomaton* re2automaton::re2aut(expr* e) {
|
|||
expr_ref _start(bv.mk_numeral(start, nb), m);
|
||||
expr_ref _stop(bv.mk_numeral(stop, nb), m);
|
||||
expr_ref _pred(m.mk_not(m.mk_and(bv.mk_ule(_start, v), bv.mk_ule(v, _stop))), m);
|
||||
a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred));
|
||||
a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred, s));
|
||||
return a.detach();
|
||||
}
|
||||
else if (u.re.is_to_re(e0, e1) && u.str.is_string(e1, s1) && s1.length() == 1) {
|
||||
|
|
@ -145,13 +254,14 @@ eautomaton* re2automaton::re2aut(expr* e) {
|
|||
expr_ref v(m.mk_var(0, s), m);
|
||||
expr_ref _ch(bv.mk_numeral(s1[0], nb), m);
|
||||
expr_ref _pred(m.mk_not(m.mk_eq(v, _ch)), m);
|
||||
a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred));
|
||||
a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred, s));
|
||||
return a.detach();
|
||||
}
|
||||
else if (u.re.is_to_re(e0, e1) && u.str.is_unit(e1, e2)) {
|
||||
expr_ref v(m.mk_var(0, m.get_sort(e2)), m);
|
||||
sort* s = m.get_sort(e2);
|
||||
expr_ref v(m.mk_var(0, s), m);
|
||||
expr_ref _pred(m.mk_not(m.mk_eq(v, e2)), m);
|
||||
a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred));
|
||||
a = alloc(eautomaton, sm, sym_expr::mk_pred(_pred, s));
|
||||
return a.detach();
|
||||
}
|
||||
else {
|
||||
|
|
@ -187,14 +297,15 @@ eautomaton* re2automaton::re2aut(expr* e) {
|
|||
}
|
||||
else if (u.re.is_full(e)) {
|
||||
expr_ref tt(m.mk_true(), m);
|
||||
sym_expr* _true = sym_expr::mk_pred(tt);
|
||||
sort* seq_s, *char_s;
|
||||
VERIFY (u.is_re(m.get_sort(e), seq_s));
|
||||
VERIFY (u.is_seq(seq_s, char_s));
|
||||
sym_expr* _true = sym_expr::mk_pred(tt, char_s);
|
||||
return eautomaton::mk_loop(sm, _true);
|
||||
}
|
||||
#if 0
|
||||
else if (u.re.is_intersect(e, e1, e2)) {
|
||||
// maybe later
|
||||
else if (u.re.is_intersection(e, e1, e2) && m_sa && (a = re2aut(e1)) && (b = re2aut(e2))) {
|
||||
return m_sa->mk_product(*a, *b);
|
||||
}
|
||||
#endif
|
||||
|
||||
return 0;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -25,6 +25,7 @@ Notes:
|
|||
#include"params.h"
|
||||
#include"lbool.h"
|
||||
#include"automaton.h"
|
||||
#include"symbolic_automata.h"
|
||||
|
||||
class sym_expr {
|
||||
enum ty {
|
||||
|
|
@ -33,21 +34,24 @@ class sym_expr {
|
|||
t_range
|
||||
};
|
||||
ty m_ty;
|
||||
sort* m_sort;
|
||||
expr_ref m_t;
|
||||
expr_ref m_s;
|
||||
unsigned m_ref;
|
||||
sym_expr(ty ty, expr_ref& t, expr_ref& s) : m_ty(ty), m_t(t), m_s(s), m_ref(0) {}
|
||||
sym_expr(ty ty, expr_ref& t, expr_ref& s, sort* srt) : m_ty(ty), m_sort(srt), m_t(t), m_s(s), m_ref(0) {}
|
||||
public:
|
||||
expr_ref accept(expr* e);
|
||||
static sym_expr* mk_char(expr_ref& t) { return alloc(sym_expr, t_char, t, t); }
|
||||
static sym_expr* mk_char(expr_ref& t) { return alloc(sym_expr, t_char, t, t, t.get_manager().get_sort(t)); }
|
||||
static sym_expr* mk_char(ast_manager& m, expr* t) { expr_ref tr(t, m); return mk_char(tr); }
|
||||
static sym_expr* mk_pred(expr_ref& t) { return alloc(sym_expr, t_pred, t, t); }
|
||||
static sym_expr* mk_range(expr_ref& lo, expr_ref& hi) { return alloc(sym_expr, t_range, lo, hi); }
|
||||
static sym_expr* mk_pred(expr_ref& t, sort* s) { return alloc(sym_expr, t_pred, t, t, s); }
|
||||
static sym_expr* mk_range(expr_ref& lo, expr_ref& hi) { return alloc(sym_expr, t_range, lo, hi, lo.get_manager().get_sort(hi)); }
|
||||
void inc_ref() { ++m_ref; }
|
||||
void dec_ref() { --m_ref; if (m_ref == 0) dealloc(this); }
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
bool is_char() const { return m_ty == t_char; }
|
||||
bool is_pred() const { return !is_char(); }
|
||||
bool is_range() const { return m_ty == t_range; }
|
||||
sort* sort() const { return m_sort; }
|
||||
expr* get_char() const { SASSERT(is_char()); return m_t; }
|
||||
|
||||
};
|
||||
|
|
@ -58,17 +62,31 @@ public:
|
|||
void dec_ref(sym_expr* s) { if (s) s->dec_ref(); }
|
||||
};
|
||||
|
||||
class expr_solver {
|
||||
public:
|
||||
virtual ~expr_solver() {}
|
||||
virtual lbool check_sat(expr* e) = 0;
|
||||
};
|
||||
|
||||
typedef automaton<sym_expr, sym_expr_manager> eautomaton;
|
||||
class re2automaton {
|
||||
typedef boolean_algebra<sym_expr*> boolean_algebra_t;
|
||||
typedef symbolic_automata<sym_expr, sym_expr_manager> symbolic_automata_t;
|
||||
ast_manager& m;
|
||||
sym_expr_manager sm;
|
||||
seq_util u;
|
||||
bv_util bv;
|
||||
scoped_ptr<expr_solver> m_solver;
|
||||
scoped_ptr<boolean_algebra_t> m_ba;
|
||||
scoped_ptr<symbolic_automata_t> m_sa;
|
||||
|
||||
eautomaton* re2aut(expr* e);
|
||||
eautomaton* seq2aut(expr* e);
|
||||
public:
|
||||
public:
|
||||
re2automaton(ast_manager& m);
|
||||
~re2automaton();
|
||||
eautomaton* operator()(expr* e);
|
||||
void set_solver(expr_solver* solver);
|
||||
};
|
||||
|
||||
/**
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue