mirror of
https://github.com/Z3Prover/z3
synced 2025-10-31 19:52:29 +00:00
seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
e2fab0a555
commit
bd9b5b5735
5 changed files with 133 additions and 54 deletions
|
|
@ -39,7 +39,10 @@ re2automaton::re2automaton(ast_manager& m): m(m), u(m) {}
|
|||
eautomaton* re2automaton::operator()(expr* e) {
|
||||
eautomaton* r = re2aut(e);
|
||||
if (r) {
|
||||
//display_expr1 disp(m);
|
||||
//r->display(std::cout, disp);
|
||||
r->compress();
|
||||
//r->display(std::cout, disp);
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
|
@ -61,6 +64,7 @@ eautomaton* re2automaton::re2aut(expr* e) {
|
|||
else if (u.re.is_star(e, e1) && (a = re2aut(e1))) {
|
||||
a->add_final_to_init_moves();
|
||||
a->add_init_to_final_states();
|
||||
|
||||
return a.detach();
|
||||
}
|
||||
else if (u.re.is_plus(e, e1) && (a = re2aut(e1))) {
|
||||
|
|
|
|||
|
|
@ -209,24 +209,16 @@ public:
|
|||
moves mvs;
|
||||
unsigned_vector final;
|
||||
unsigned init = 0;
|
||||
if (a.has_single_final_sink() && b.initial_state_is_source() && b.init() == 0) {
|
||||
unsigned offset2 = a.num_states();
|
||||
init = a.init();
|
||||
append_moves(0, a, mvs);
|
||||
append_moves(offset2, b, mvs);
|
||||
append_final(offset2, b, final);
|
||||
}
|
||||
else {
|
||||
unsigned offset1 = 1;
|
||||
unsigned offset2 = a.num_states() + offset1;
|
||||
mvs.push_back(move(m, 0, a.init() + offset1));
|
||||
append_moves(offset1, a, mvs);
|
||||
for (unsigned i = 0; i < a.m_final_states.size(); ++i) {
|
||||
mvs.push_back(move(m, a.m_final_states[i], b.init() + offset2));
|
||||
}
|
||||
append_moves(offset2, b, mvs);
|
||||
append_final(offset2, b, final);
|
||||
unsigned offset1 = 1;
|
||||
unsigned offset2 = a.num_states() + offset1;
|
||||
mvs.push_back(move(m, 0, a.init() + offset1));
|
||||
append_moves(offset1, a, mvs);
|
||||
for (unsigned i = 0; i < a.m_final_states.size(); ++i) {
|
||||
mvs.push_back(move(m, a.m_final_states[i] + offset1, b.init() + offset2));
|
||||
}
|
||||
append_moves(offset2, b, mvs);
|
||||
append_final(offset2, b, final);
|
||||
|
||||
return alloc(automaton, m, init, final, mvs);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -361,6 +361,7 @@ namespace smt {
|
|||
}
|
||||
else {
|
||||
enode * child = d.get_enode();
|
||||
TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " (" << mk_pp(n->get_owner(), m_manager) << "): " << mk_pp(child->get_owner(), m_manager) << " " << mk_pp(child->get_root()->get_owner(), m_manager) << "\n";);
|
||||
child = child->get_root();
|
||||
app * val = 0;
|
||||
m_root2value.find(child, val);
|
||||
|
|
|
|||
|
|
@ -77,6 +77,14 @@ expr* theory_seq::solution_map::find(expr* e, enode_pair_dependency*& d) {
|
|||
return result;
|
||||
}
|
||||
|
||||
expr* theory_seq::solution_map::find(expr* e) {
|
||||
std::pair<expr*, enode_pair_dependency*> value;
|
||||
while (m_map.find(e, value)) {
|
||||
e = value.first;
|
||||
}
|
||||
return e;
|
||||
}
|
||||
|
||||
void theory_seq::solution_map::pop_scope(unsigned num_scopes) {
|
||||
if (num_scopes == 0) return;
|
||||
m_cache.reset();
|
||||
|
|
@ -185,26 +193,32 @@ final_check_status theory_seq::final_check_eh() {
|
|||
context & ctx = get_context();
|
||||
TRACE("seq", display(tout););
|
||||
if (!check_ineqs()) {
|
||||
++m_stats.m_check_ineqs;
|
||||
TRACE("seq", tout << ">>check_ineqs\n";);
|
||||
return FC_CONTINUE;
|
||||
}
|
||||
if (simplify_and_solve_eqs()) {
|
||||
++m_stats.m_solve_eqs;
|
||||
TRACE("seq", tout << ">>solve_eqs\n";);
|
||||
return FC_CONTINUE;
|
||||
}
|
||||
if (solve_nqs()) {
|
||||
++m_stats.m_solve_nqs;
|
||||
TRACE("seq", tout << ">>solve_nqs\n";);
|
||||
return FC_CONTINUE;
|
||||
}
|
||||
if (branch_variable()) {
|
||||
++m_stats.m_branch_variable;
|
||||
TRACE("seq", tout << ">>branch_variable\n";);
|
||||
return FC_CONTINUE;
|
||||
}
|
||||
if (!check_length_coherence()) {
|
||||
++m_stats.m_check_length_coherence;
|
||||
TRACE("seq", tout << ">>check_length_coherence\n";);
|
||||
return FC_CONTINUE;
|
||||
}
|
||||
if (propagate_automata()) {
|
||||
++m_stats.m_propagate_automata;
|
||||
TRACE("seq", tout << ">>propagate_automata\n";);
|
||||
return FC_CONTINUE;
|
||||
}
|
||||
|
|
@ -312,23 +326,27 @@ bool theory_seq::assume_equality(expr* l, expr* r) {
|
|||
}
|
||||
|
||||
bool theory_seq::propagate_length_coherence(expr* e) {
|
||||
expr_ref head(m), tail(m), emp(m);
|
||||
expr_ref head(m), tail(m);
|
||||
rational lo, hi;
|
||||
|
||||
if (!is_var(e) || !m_rep.is_root(e)) {
|
||||
return false;
|
||||
}
|
||||
if (!lower_bound(e, lo) || !lo.is_pos() || lo >= rational(2048)) {
|
||||
return false;
|
||||
}
|
||||
TRACE("seq", tout << "Unsolved " << mk_pp(e, m);
|
||||
if (!lower_bound(e, lo)) lo = -rational::one();
|
||||
if (!upper_bound(e, hi)) hi = -rational::one();
|
||||
tout << " lo: " << lo << " hi: " << hi << "\n";
|
||||
);
|
||||
|
||||
if (!lower_bound(e, lo) || !lo.is_pos() || lo >= rational(2048)) {
|
||||
return false;
|
||||
}
|
||||
literal low(mk_literal(m_autil.mk_ge(m_util.str.mk_length(e), m_autil.mk_numeral(lo, true))));
|
||||
expr_ref seq(e, m);
|
||||
expr_ref_vector elems(m);
|
||||
unsigned _lo = lo.get_unsigned();
|
||||
for (unsigned j = 0; j < _lo; ++j) {
|
||||
mk_decompose(seq, emp, head, tail);
|
||||
mk_decompose(seq, head, tail);
|
||||
elems.push_back(head);
|
||||
seq = tail;
|
||||
}
|
||||
|
|
@ -342,6 +360,10 @@ bool theory_seq::propagate_length_coherence(expr* e) {
|
|||
expr_ref high2(m_autil.mk_le(m_util.str.mk_length(seq), m_autil.mk_numeral(hi-lo, true)), m);
|
||||
add_axiom(~mk_literal(high1), mk_literal(high2));
|
||||
}
|
||||
|
||||
//m_replay_length_coherence.push_back(e);
|
||||
//m_replay_length_coherence_qhead = m_replay_length_coherence.size();
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
|
|
@ -357,14 +379,12 @@ bool theory_seq::check_length_coherence() {
|
|||
expr_ref head(m), tail(m);
|
||||
|
||||
if (propagate_length_coherence(e)) {
|
||||
//m_replay_length_coherence.push_back(e);
|
||||
//m_replay_length_coherence_qhead = m_replay_length_coherence.size();
|
||||
}
|
||||
else if (!assume_equality(e, emp)) {
|
||||
mk_decompose(e, emp, head, tail);
|
||||
mk_decompose(e, head, tail);
|
||||
// e = emp \/ e = unit(head.elem(e))*tail(e)
|
||||
expr_ref conc(m_util.str.mk_concat(head, tail), m);
|
||||
add_axiom(mk_eq(e, emp, false), mk_eq(e, conc, false));
|
||||
add_axiom(mk_eq_empty(e), mk_eq(e, conc, false));
|
||||
assume_equality(tail, emp);
|
||||
}
|
||||
return false;
|
||||
|
|
@ -379,10 +399,9 @@ expr_ref theory_seq::mk_nth(expr* s, expr* idx) {
|
|||
return mk_skolem(m_nth, s, idx, 0, char_sort);
|
||||
}
|
||||
|
||||
void theory_seq::mk_decompose(expr* e, expr_ref& emp, expr_ref& head, expr_ref& tail) {
|
||||
void theory_seq::mk_decompose(expr* e, expr_ref& head, expr_ref& tail) {
|
||||
expr* e1, *e2;
|
||||
zstring s;
|
||||
emp = m_util.str.mk_empty(m.get_sort(e));
|
||||
if (m_util.str.is_empty(e)) {
|
||||
head = m_util.str.mk_unit(mk_nth(e, m_autil.mk_int(0)));
|
||||
tail = e;
|
||||
|
|
@ -393,7 +412,7 @@ void theory_seq::mk_decompose(expr* e, expr_ref& emp, expr_ref& head, expr_ref&
|
|||
}
|
||||
else if (m_util.str.is_unit(e)) {
|
||||
head = e;
|
||||
tail = emp;
|
||||
tail = m_util.str.mk_empty(m.get_sort(e));
|
||||
}
|
||||
else if (m_util.str.is_concat(e, e1, e2) && m_util.str.is_unit(e1)) {
|
||||
head = e1;
|
||||
|
|
@ -585,7 +604,7 @@ bool theory_seq::is_var(expr* a) {
|
|||
}
|
||||
|
||||
|
||||
bool theory_seq::is_head_elem(expr* e) const {
|
||||
bool theory_seq::is_nth(expr* e) const {
|
||||
return is_skolem(m_nth, e);
|
||||
}
|
||||
|
||||
|
|
@ -884,6 +903,13 @@ void theory_seq::display_deps(std::ostream& out, enode_pair_dependency* dep) con
|
|||
void theory_seq::collect_statistics(::statistics & st) const {
|
||||
st.update("seq num splits", m_stats.m_num_splits);
|
||||
st.update("seq num reductions", m_stats.m_num_reductions);
|
||||
st.update("e", m_stats.m_propagate_automata);
|
||||
st.update("seq length coherence", m_stats.m_check_length_coherence);
|
||||
st.update("seq branch", m_stats.m_branch_variable);
|
||||
st.update("seq solve !=", m_stats.m_solve_nqs);
|
||||
st.update("seq solve =", m_stats.m_solve_eqs);
|
||||
st.update("seq check negations", m_stats.m_check_ineqs);
|
||||
|
||||
}
|
||||
|
||||
void theory_seq::init_model(model_generator & mg) {
|
||||
|
|
@ -910,7 +936,6 @@ public:
|
|||
if (values.empty()) {
|
||||
return th.mk_value(n);
|
||||
}
|
||||
SASSERT(values.size() == n->get_num_args());
|
||||
return th.mk_value(mg.get_manager().mk_app(n->get_decl(), values.size(), values.c_ptr()));
|
||||
}
|
||||
};
|
||||
|
|
@ -918,13 +943,35 @@ public:
|
|||
|
||||
model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
|
||||
context& ctx = get_context();
|
||||
enode_pair_dependency* dep = 0;
|
||||
expr* e = m_rep.find(n->get_owner(), dep);
|
||||
expr* e1, *e2;
|
||||
expr_ref e(m);
|
||||
expr* e1;
|
||||
ptr_vector<expr> concats;
|
||||
get_concat(n->get_owner(), concats);
|
||||
switch (concats.size()) {
|
||||
case 0:
|
||||
e = m_util.str.mk_empty(m.get_sort(n->get_owner()));
|
||||
break;
|
||||
case 1:
|
||||
e = concats[0];
|
||||
SASSERT(!m_util.str.is_concat(e));
|
||||
break;
|
||||
default:
|
||||
e = m_rep.find(n->get_owner());
|
||||
SASSERT(m_util.str.is_concat(e));
|
||||
break;
|
||||
}
|
||||
seq_value_proc* sv = alloc(seq_value_proc, *this, to_app(e));
|
||||
if (m_util.str.is_concat(e, e1, e2)) {
|
||||
sv->add_dependency(ctx.get_enode(e1));
|
||||
sv->add_dependency(ctx.get_enode(e2));
|
||||
TRACE("seq", tout << mk_pp(n->get_owner(), m) << " ";
|
||||
for (unsigned i = 0; i < concats.size(); ++i) {
|
||||
tout << mk_pp(concats[i], m) << " ";
|
||||
}
|
||||
tout << "\n";
|
||||
);
|
||||
|
||||
if (concats.size() > 1) {
|
||||
for (unsigned i = 0; i < concats.size(); ++i) {
|
||||
sv->add_dependency(ctx.get_enode(concats[i]));
|
||||
}
|
||||
}
|
||||
else if (m_util.str.is_unit(e, e1)) {
|
||||
sv->add_dependency(ctx.get_enode(e1));
|
||||
|
|
@ -932,6 +979,22 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
|
|||
return sv;
|
||||
}
|
||||
|
||||
void theory_seq::get_concat(expr* e, ptr_vector<expr>& concats) {
|
||||
expr* e1, *e2;
|
||||
while (true) {
|
||||
e = m_rep.find(e);
|
||||
if (m_util.str.is_concat(e, e1, e2)) {
|
||||
get_concat(e1, concats);
|
||||
e = e2;
|
||||
continue;
|
||||
}
|
||||
if (!m_util.str.is_empty(e)) {
|
||||
concats.push_back(e);
|
||||
}
|
||||
return;
|
||||
}
|
||||
}
|
||||
|
||||
app* theory_seq::mk_value(app* e) {
|
||||
expr* e1;
|
||||
expr_ref result(e, m);
|
||||
|
|
@ -964,7 +1027,7 @@ app* theory_seq::mk_value(app* e) {
|
|||
result = e;
|
||||
}
|
||||
}
|
||||
else if (is_head_elem(e)) {
|
||||
else if (is_nth(e)) {
|
||||
enode* n = get_context().get_enode(e)->get_root();
|
||||
enode* n0 = n;
|
||||
bool found_value = false;
|
||||
|
|
@ -1088,6 +1151,9 @@ void theory_seq::deque_axiom(expr* n) {
|
|||
if (m_util.str.is_length(n)) {
|
||||
add_length_axiom(n);
|
||||
}
|
||||
else if (m_util.str.is_empty(n) && !has_length(n)) {
|
||||
enforce_length(get_context().get_enode(n));
|
||||
}
|
||||
else if (m_util.str.is_index(n)) {
|
||||
add_indexof_axiom(n);
|
||||
}
|
||||
|
|
@ -1120,8 +1186,7 @@ void theory_seq::tightest_prefix(expr* s, expr* x, literal lit1, literal lit2) {
|
|||
expr_ref s1c(m_util.str.mk_concat(s1, c), m);
|
||||
expr_ref lc(m_util.str.mk_length(c), m);
|
||||
expr_ref one(m_autil.mk_int(1), m);
|
||||
expr_ref emp(m_util.str.mk_empty(m.get_sort(s)), m);
|
||||
literal s_eq_emp = mk_eq(s, emp, false);
|
||||
literal s_eq_emp = mk_eq_empty(s);
|
||||
add_axiom(lit1, lit2, s_eq_emp, mk_eq(s, s1c, false));
|
||||
add_axiom(lit1, lit2, s_eq_emp, mk_eq(lc, one, false));
|
||||
add_axiom(lit1, lit2, s_eq_emp, ~mk_literal(m_util.str.mk_contains(s, m_util.str.mk_concat(x, s1))));
|
||||
|
|
@ -1160,7 +1225,6 @@ void theory_seq::add_indexof_axiom(expr* i) {
|
|||
expr_ref emp(m), minus_one(m), zero(m), xsy(m);
|
||||
minus_one = m_autil.mk_int(-1);
|
||||
zero = m_autil.mk_int(0);
|
||||
emp = m_util.str.mk_empty(m.get_sort(s));
|
||||
literal offset_ne_zero = null_literal;
|
||||
bool is_num = m_autil.is_numeral(offset, r);
|
||||
if (is_num && r.is_zero()) {
|
||||
|
|
@ -1174,7 +1238,7 @@ void theory_seq::add_indexof_axiom(expr* i) {
|
|||
expr_ref y = mk_skolem(m_contains_right, t, s);
|
||||
xsy = m_util.str.mk_concat(x,s,y);
|
||||
literal cnt = mk_literal(m_util.str.mk_contains(t, s));
|
||||
literal eq_empty = mk_eq(s, emp, false);
|
||||
literal eq_empty = mk_eq_empty(s);
|
||||
add_axiom(offset_ne_zero, cnt, mk_eq(i, minus_one, false));
|
||||
add_axiom(offset_ne_zero, ~eq_empty, mk_eq(i, zero, false));
|
||||
add_axiom(offset_ne_zero, ~cnt, eq_empty, mk_eq(t, xsy, false));
|
||||
|
|
@ -1263,12 +1327,12 @@ void theory_seq::add_length_axiom(expr* n) {
|
|||
}
|
||||
else {
|
||||
expr_ref zero(m_autil.mk_int(0), m);
|
||||
expr_ref emp(m_util.str.mk_empty(m.get_sort(x)), m);
|
||||
literal eq1(mk_eq(zero, n, false));
|
||||
literal eq2(mk_eq(x, emp, false));
|
||||
add_axiom(mk_literal(m_autil.mk_ge(n, zero)));
|
||||
add_axiom(~eq1, eq2);
|
||||
add_axiom(~eq2, eq1);
|
||||
|
||||
//expr_ref emp(m_util.str.mk_empty(m.get_sort(x)), m);
|
||||
//literal eq1(mk_eq(zero, n, false));
|
||||
//literal eq2(mk_eq(x, emp, false));
|
||||
//add_axiom(~eq1, eq2);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -1510,6 +1574,17 @@ literal theory_seq::mk_literal(expr* _e) {
|
|||
return ctx.get_literal(e);
|
||||
}
|
||||
|
||||
literal theory_seq::mk_eq_empty(expr* _e) {
|
||||
expr_ref e(_e, m);
|
||||
context& ctx = get_context();
|
||||
SASSERT(m_util.is_seq(e));
|
||||
expr_ref emp(m);
|
||||
emp = m_util.str.mk_empty(m.get_sort(e));
|
||||
literal lit = mk_eq(e, emp, false);
|
||||
ctx.force_phase(lit);
|
||||
return lit;
|
||||
}
|
||||
|
||||
void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4) {
|
||||
context& ctx = get_context();
|
||||
literal_vector lits;
|
||||
|
|
@ -1681,8 +1756,8 @@ void theory_seq::relevant_eh(app* n) {
|
|||
m_util.str.is_replace(n) ||
|
||||
m_util.str.is_extract(n) ||
|
||||
m_util.str.is_at(n) ||
|
||||
m_util.str.is_string(n) ||
|
||||
is_step(n)) {
|
||||
m_util.str.is_empty(n) ||
|
||||
m_util.str.is_string(n)) {
|
||||
enque_axiom(n);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -72,6 +72,7 @@ namespace smt {
|
|||
void add_cache(expr* v, expr_dep& r) { m_cache.insert(v, r); }
|
||||
bool find_cache(expr* v, expr_dep& r) { return m_cache.find(v, r); }
|
||||
expr* find(expr* e, enode_pair_dependency*& d);
|
||||
expr* find(expr* e);
|
||||
bool is_root(expr* e) const;
|
||||
void cache(expr* e, expr* r, enode_pair_dependency* d);
|
||||
void reset_cache() { m_cache.reset(); }
|
||||
|
|
@ -246,6 +247,12 @@ namespace smt {
|
|||
void reset() { memset(this, 0, sizeof(stats)); }
|
||||
unsigned m_num_splits;
|
||||
unsigned m_num_reductions;
|
||||
unsigned m_propagate_automata;
|
||||
unsigned m_check_length_coherence;
|
||||
unsigned m_branch_variable;
|
||||
unsigned m_solve_nqs;
|
||||
unsigned m_solve_eqs;
|
||||
unsigned m_check_ineqs;
|
||||
};
|
||||
ast_manager& m;
|
||||
enode_pair_dependency_manager m_dm;
|
||||
|
|
@ -335,13 +342,13 @@ namespace smt {
|
|||
bool occurs(expr* a, expr* b);
|
||||
bool is_var(expr* b);
|
||||
bool add_solution(expr* l, expr* r, enode_pair_dependency* dep);
|
||||
bool is_left_select(expr* a, expr*& b);
|
||||
bool is_right_select(expr* a, expr*& b);
|
||||
bool is_head_elem(expr* a) const;
|
||||
bool is_nth(expr* a) const;
|
||||
expr_ref mk_nth(expr* s, expr* idx);
|
||||
expr_ref canonize(expr* e, enode_pair_dependency*& eqs);
|
||||
expr_ref expand(expr* e, enode_pair_dependency*& eqs);
|
||||
void add_dependency(enode_pair_dependency*& dep, enode* a, enode* b);
|
||||
|
||||
void get_concat(expr* e, ptr_vector<expr>& concats);
|
||||
|
||||
// terms whose meaning are encoded using axioms.
|
||||
void enque_axiom(expr* e);
|
||||
|
|
@ -360,6 +367,7 @@ namespace smt {
|
|||
void add_at_axiom(expr* n);
|
||||
void add_in_re_axiom(expr* n);
|
||||
literal mk_literal(expr* n);
|
||||
literal mk_eq_empty(expr* n);
|
||||
void tightest_prefix(expr* s, expr* x, literal lit, literal lit2 = null_literal);
|
||||
expr_ref mk_sub(expr* a, expr* b);
|
||||
enode* ensure_enode(expr* a);
|
||||
|
|
@ -369,9 +377,8 @@ namespace smt {
|
|||
bool upper_bound(expr* s, rational& hi);
|
||||
bool get_length(expr* s, rational& val);
|
||||
|
||||
void mk_decompose(expr* e, expr_ref& emp, expr_ref& head, expr_ref& tail);
|
||||
void mk_decompose(expr* e, expr_ref& head, expr_ref& tail);
|
||||
expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = 0, expr* e3 = 0, sort* range = 0);
|
||||
expr_ref mk_nth(expr* s, expr* idx);
|
||||
bool is_skolem(symbol const& s, expr* e) const;
|
||||
|
||||
void set_incomplete(app* term);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue