mirror of
https://github.com/Z3Prover/z3
synced 2025-04-28 11:25:51 +00:00
seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
6c6d1d92c4
commit
876fd1f7ba
5 changed files with 140 additions and 37 deletions
|
|
@ -520,20 +520,10 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
|
|||
result = m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), a);
|
||||
return BR_REWRITE3;
|
||||
}
|
||||
// TBD concatenation is right-associative
|
||||
expr* a1, *a2, *b1, *b2;
|
||||
if (m_util.str.is_concat(a, a1, a2) &&
|
||||
m_util.str.is_concat(b, b1, b2) && a2 == b2) {
|
||||
result = m_util.str.mk_suffix(a1, b1);
|
||||
return BR_REWRITE1;
|
||||
}
|
||||
if (m_util.str.is_concat(b, b1, b2) && b2 == a) {
|
||||
result = m().mk_true();
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
bool isc1 = false;
|
||||
bool isc2 = false;
|
||||
|
||||
expr* a1, *a2, *b1, *b2;
|
||||
if (m_util.str.is_concat(a, a1, a2) && m_util.str.is_string(a2, s1)) {
|
||||
isc1 = true;
|
||||
}
|
||||
|
|
@ -593,6 +583,37 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
|
|||
}
|
||||
}
|
||||
}
|
||||
expr_ref_vector as(m()), bs(m());
|
||||
m_util.str.get_concat(a, as);
|
||||
m_util.str.get_concat(b, bs);
|
||||
bool change = false;
|
||||
while (as.size() > 0 && bs.size() > 0 && as.back() == bs.back()) {
|
||||
as.pop_back();
|
||||
bs.pop_back();
|
||||
change = true;
|
||||
}
|
||||
if (as.size() > 0 && bs.size() > 0 && m().is_value(as.back()) && m().is_value(bs.back())) {
|
||||
result = m().mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
if (change) {
|
||||
// suffix("", bs) <- true
|
||||
if (as.empty()) {
|
||||
result = m().mk_true();
|
||||
return BR_DONE;
|
||||
}
|
||||
// suffix(as, "") iff as = ""
|
||||
if (bs.empty()) {
|
||||
for (unsigned j = 0; j < as.size(); ++j) {
|
||||
bs.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j].get()));
|
||||
}
|
||||
result = mk_and(bs);
|
||||
return BR_REWRITE3;
|
||||
}
|
||||
result = m_util.str.mk_suffix(m_util.str.mk_concat(as.size(), as.c_ptr()),
|
||||
m_util.str.mk_concat(bs.size(), bs.c_ptr()));
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -25,7 +25,6 @@ Revision History:
|
|||
zstring::zstring(encoding enc): m_encoding(enc) {}
|
||||
|
||||
zstring::zstring(char const* s, encoding enc): m_encoding(enc) {
|
||||
// TBD: epply decoding
|
||||
while (*s) {
|
||||
m_buffer.push_back(*s);
|
||||
++s;
|
||||
|
|
@ -81,6 +80,7 @@ zstring zstring::replace(zstring const& src, zstring const& dst) const {
|
|||
return result;
|
||||
}
|
||||
|
||||
// TBD: SMT-LIB 2.5 strings don't have escape characters other than "
|
||||
static char* esc_table[32] = { "\\0", "^A", "^B", "^C", "^D", "^E", "^F", "\\a", "\\b", "\\t", "\\n", "\\v", "\\f", "\\r", "^N",
|
||||
"^O", "^P", "^Q", "^R", "^S", "^T", "^U", "^V","^W","^X","^Y","^Z","\\e","^\\","^]","^^","^_"};
|
||||
|
||||
|
|
|
|||
|
|
@ -273,6 +273,7 @@ namespace datalog {
|
|||
*/
|
||||
void register_pair(app * t1, app * t2, rule * r, const var_idx_set & non_local_vars) {
|
||||
SASSERT(t1!=t2);
|
||||
std::cout << "insert: " << mk_pp(t1, m) << " - " << mk_pp(t2, m) << "\n";
|
||||
cost_map::entry * e = m_costs.insert_if_not_there2(get_key(t1, t2), 0);
|
||||
pair_info * & ptr_inf = e->get_data().m_value;
|
||||
if (ptr_inf==0) {
|
||||
|
|
@ -306,6 +307,7 @@ namespace datalog {
|
|||
}
|
||||
|
||||
void remove_rule_from_pair(app_pair key, rule * r, unsigned original_len) {
|
||||
std::cout << "remove: " << mk_pp(key.first, m) << " - " << mk_pp(key.second, m) << "\n";
|
||||
pair_info * ptr = &get_pair(key);
|
||||
if (ptr->remove_rule(r, original_len)) {
|
||||
SASSERT(ptr->m_rules.empty());
|
||||
|
|
|
|||
|
|
@ -150,6 +150,7 @@ void theory_seq::exclusion_table::display(std::ostream& out) const {
|
|||
}
|
||||
}
|
||||
|
||||
|
||||
theory_seq::theory_seq(ast_manager& m):
|
||||
theory(m.mk_family_id("seq")),
|
||||
m(m),
|
||||
|
|
@ -372,6 +373,7 @@ bool theory_seq::propagate_length_coherence(expr* e) {
|
|||
expr_ref high1(m_autil.mk_le(m_util.str.mk_length(e), m_autil.mk_numeral(hi, true)), m);
|
||||
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_trail_stack.push(push_replay(alloc(replay_length_coherence, m, e)));
|
||||
}
|
||||
|
||||
return true;
|
||||
|
|
@ -1048,12 +1050,18 @@ app* theory_seq::mk_value(app* e) {
|
|||
rational val;
|
||||
unsigned sz;
|
||||
if (bv.is_numeral(result, val, sz) && sz == zstring().num_bits()) {
|
||||
svector<bool> val_as_bits;
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
val_as_bits.push_back(!val.is_even());
|
||||
val = div(val, rational(2));
|
||||
unsigned v = val.get_unsigned();
|
||||
if ((0 <= v && v < 32) || v == 127) {
|
||||
result = m_util.str.mk_unit(result);
|
||||
}
|
||||
else {
|
||||
svector<bool> val_as_bits;
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
val_as_bits.push_back(1 == v % 2);
|
||||
v = v / 2;
|
||||
}
|
||||
result = m_util.str.mk_string(zstring(sz, val_as_bits.c_ptr()));
|
||||
}
|
||||
result = m_util.str.mk_string(zstring(sz, val_as_bits.c_ptr()));
|
||||
}
|
||||
else {
|
||||
result = m_util.str.mk_unit(result);
|
||||
|
|
@ -1113,7 +1121,7 @@ theory_var theory_seq::mk_var(enode* n) {
|
|||
}
|
||||
|
||||
bool theory_seq::can_propagate() {
|
||||
return m_axioms_head < m_axioms.size();
|
||||
return m_axioms_head < m_axioms.size() || !m_replay.empty();
|
||||
}
|
||||
|
||||
expr_ref theory_seq::canonize(expr* e, dependency*& eqs) {
|
||||
|
|
@ -1177,6 +1185,11 @@ void theory_seq::propagate() {
|
|||
deque_axiom(e);
|
||||
++m_axioms_head;
|
||||
}
|
||||
while (!m_replay.empty() && !ctx.inconsistent()) {
|
||||
(*m_replay[m_replay.size()-1])(*this);
|
||||
TRACE("seq", tout << "replay: " << ctx.get_scope_level() << "\n";);
|
||||
m_replay.pop_back();
|
||||
}
|
||||
}
|
||||
|
||||
void theory_seq::enque_axiom(expr* e) {
|
||||
|
|
@ -1733,7 +1746,9 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
|
|||
else {
|
||||
// !prefix(e1,e2) => e1 != ""
|
||||
propagate_non_empty(lit, e1);
|
||||
add_atom(e);
|
||||
if (add_prefix2prefix(e)) {
|
||||
add_atom(e);
|
||||
}
|
||||
}
|
||||
}
|
||||
else if (m_util.str.is_suffix(e, e1, e2)) {
|
||||
|
|
@ -1752,7 +1767,9 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
|
|||
f = m_util.str.mk_concat(f1, m_util.str.mk_unit(f2));
|
||||
propagate_eq(lit, e1, f, true);
|
||||
|
||||
add_atom(e);
|
||||
if (add_suffix2suffix(e)) {
|
||||
add_atom(e);
|
||||
}
|
||||
}
|
||||
}
|
||||
else if (m_util.str.is_contains(e, e1, e2)) {
|
||||
|
|
@ -1765,13 +1782,17 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
|
|||
else if (!canonizes(false, e)) {
|
||||
propagate_non_empty(lit, e2);
|
||||
propagate_lit(0, 1, &lit, ~mk_literal(m_util.str.mk_prefix(e2, e1)));
|
||||
add_atom(e);
|
||||
if (add_contains2contains(e)) {
|
||||
add_atom(e);
|
||||
}
|
||||
}
|
||||
}
|
||||
else if (is_accept(e)) {
|
||||
if (is_true) {
|
||||
propagate_acc_rej_length(lit, e);
|
||||
add_atom(e);
|
||||
if (add_accept2step(e)) {
|
||||
add_atom(e);
|
||||
}
|
||||
}
|
||||
}
|
||||
else if (is_reject(e)) {
|
||||
|
|
@ -1783,7 +1804,9 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
|
|||
else if (is_step(e)) {
|
||||
if (is_true) {
|
||||
propagate_step(lit, e);
|
||||
add_atom(e);
|
||||
if (add_step2accept(e)) {
|
||||
add_atom(e);
|
||||
}
|
||||
}
|
||||
}
|
||||
else if (m_util.str.is_in_re(e)) {
|
||||
|
|
@ -1979,10 +2002,10 @@ void theory_seq::propagate_acc_rej_length(literal lit, expr* e) {
|
|||
}
|
||||
|
||||
/**
|
||||
acc(s, idx, re, i) -> \/ step(s, idx, re, i, j, t) if i is non-final
|
||||
acc(s, idx, re, i) -> \/ step(s, idx, re, i, j, t) if i is non-final
|
||||
acc(s, idx, re, i) -> len(s) <= idx \/ step(s, idx, re, i, j, t) if i is final
|
||||
*/
|
||||
void theory_seq::add_accept2step(expr* acc) {
|
||||
bool theory_seq::add_accept2step(expr* acc) {
|
||||
context& ctx = get_context();
|
||||
SASSERT(ctx.get_assignment(acc) == l_true);
|
||||
expr *e, * idx, *re;
|
||||
|
|
@ -1990,7 +2013,9 @@ void theory_seq::add_accept2step(expr* acc) {
|
|||
unsigned src;
|
||||
eautomaton* aut = 0;
|
||||
VERIFY(is_accept(acc, e, idx, re, src, aut));
|
||||
if (!aut || m_util.str.is_length(idx)) return;
|
||||
if (!aut || m_util.str.is_length(idx)) {
|
||||
return false;
|
||||
}
|
||||
SASSERT(m_autil.is_numeral(idx));
|
||||
eautomaton::moves mvs;
|
||||
aut->get_moves_from(src, mvs);
|
||||
|
|
@ -2000,18 +2025,25 @@ void theory_seq::add_accept2step(expr* acc) {
|
|||
lits.push_back(~ctx.get_literal(acc));
|
||||
if (aut->is_final_state(src)) {
|
||||
lits.push_back(mk_literal(m_autil.mk_le(len, idx)));
|
||||
if (ctx.get_assignment(lits.back()) == l_true) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
for (unsigned i = 0; i < mvs.size(); ++i) {
|
||||
eautomaton::move mv = mvs[i];
|
||||
step = mk_step(e, idx, re, src, mv.dst(), mv.t());
|
||||
lits.push_back(mk_literal(step));
|
||||
if (ctx.get_assignment(lits.back()) == l_true) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
TRACE("seq", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";);
|
||||
//std::cout << lits << "\n";
|
||||
for (unsigned i = 0; i < lits.size(); ++i) { // TBD
|
||||
ctx.mark_as_relevant(lits[i]);
|
||||
}
|
||||
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
|
||||
add_axiom(~ctx.get_literal(acc), mk_literal(m_autil.mk_ge(len, idx)));
|
||||
return false;
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -2019,17 +2051,40 @@ void theory_seq::add_accept2step(expr* acc) {
|
|||
acc(s, idx, re, i) & step(s, idx, re, i, j, t) => acc(s, idx + 1, re, j)
|
||||
*/
|
||||
|
||||
void theory_seq::add_step2accept(expr* step) {
|
||||
bool theory_seq::add_step2accept(expr* step) {
|
||||
context& ctx = get_context();
|
||||
SASSERT(ctx.get_assignment(step) == l_true);
|
||||
rational r;
|
||||
expr* re, *t, *s, *idx, *i, *j;
|
||||
VERIFY(is_step(step, s, idx, re, i, j, t));
|
||||
VERIFY(m_autil.is_numeral(idx, r) && r.is_unsigned());
|
||||
expr_ref idx1(m_autil.mk_int(r.get_unsigned() + 1), m);
|
||||
literal acc1 = mk_accept(s, idx, re, i);
|
||||
literal acc2 = mk_accept(s, idx1, re, j);
|
||||
add_axiom(~acc1, ~ctx.get_literal(step), acc2);
|
||||
switch (ctx.get_assignment(acc1)) {
|
||||
case l_false:
|
||||
break;
|
||||
case l_undef:
|
||||
return true;
|
||||
case l_true: {
|
||||
rational r;
|
||||
VERIFY(m_autil.is_numeral(idx, r) && r.is_unsigned());
|
||||
expr_ref idx1(m_autil.mk_int(r.get_unsigned() + 1), m);
|
||||
literal acc2 = mk_accept(s, idx1, re, j);
|
||||
literal_vector lits;
|
||||
lits.push_back(acc1);
|
||||
lits.push_back(ctx.get_literal(step));
|
||||
lits.push_back(~acc2);
|
||||
switch (ctx.get_assignment(acc2)) {
|
||||
case l_undef:
|
||||
propagate_lit(0, 2, lits.c_ptr(), acc2);
|
||||
break;
|
||||
case l_true:
|
||||
break;
|
||||
case l_false:
|
||||
set_conflict(0, lits);
|
||||
break;
|
||||
}
|
||||
break;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -2257,7 +2312,7 @@ bool theory_seq::propagate_automata() {
|
|||
reQ = add_reject2reject(e);
|
||||
}
|
||||
else if (is_step(e)) {
|
||||
add_step2accept(e);
|
||||
reQ = add_step2accept(e);
|
||||
}
|
||||
else if (m_util.str.is_prefix(e)) {
|
||||
reQ = add_prefix2prefix(e);
|
||||
|
|
|
|||
|
|
@ -246,6 +246,30 @@ namespace smt {
|
|||
}
|
||||
};
|
||||
|
||||
class apply {
|
||||
public:
|
||||
virtual ~apply() {}
|
||||
virtual void operator()(theory_seq& th) = 0;
|
||||
};
|
||||
|
||||
class replay_length_coherence : public apply {
|
||||
expr_ref m_e;
|
||||
public:
|
||||
replay_length_coherence(ast_manager& m, expr* e) : m_e(e, m) {}
|
||||
virtual void operator()(theory_seq& th) {
|
||||
th.propagate_length_coherence(m_e);
|
||||
}
|
||||
};
|
||||
|
||||
class push_replay : public trail<theory_seq> {
|
||||
apply* m_apply;
|
||||
public:
|
||||
push_replay(apply* app): m_apply(app) {}
|
||||
virtual void undo(theory_seq& th) {
|
||||
th.m_replay.push_back(m_apply);
|
||||
}
|
||||
};
|
||||
|
||||
void erase_index(unsigned idx, unsigned i);
|
||||
|
||||
struct stats {
|
||||
|
|
@ -273,6 +297,7 @@ namespace smt {
|
|||
unsigned m_branch_variable_head; // index of first equation to examine.
|
||||
bool m_incomplete; // is the solver (clearly) incomplete for the fragment.
|
||||
obj_hashtable<expr> m_length; // is length applied
|
||||
scoped_ptr_vector<apply> m_replay; // set of actions to replay
|
||||
model_generator* m_mg;
|
||||
th_rewriter m_rewrite;
|
||||
seq_util m_util;
|
||||
|
|
@ -410,8 +435,8 @@ namespace smt {
|
|||
bool is_step(expr* e) const;
|
||||
void propagate_step(literal lit, expr* n);
|
||||
bool add_reject2reject(expr* rej);
|
||||
void add_accept2step(expr* acc);
|
||||
void add_step2accept(expr* step);
|
||||
bool add_accept2step(expr* acc);
|
||||
bool add_step2accept(expr* step);
|
||||
bool add_prefix2prefix(expr* e);
|
||||
bool add_suffix2suffix(expr* e);
|
||||
bool add_contains2contains(expr* e);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue