From 974eaab01c752df9d61d53887709a5eb9a71ef1d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 28 Aug 2017 01:38:23 -0700 Subject: [PATCH] complement regular expressions when used in negated membership constraints #1224 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 1 + src/math/automata/automaton.h | 59 +++++++++++------------ src/math/automata/symbolic_automata.h | 3 +- src/math/automata/symbolic_automata_def.h | 17 +++++-- src/smt/theory_seq.cpp | 20 +++++--- 5 files changed, 58 insertions(+), 42 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index f347a8e49..4f9a88490 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1726,6 +1726,7 @@ ast * ast_manager::register_node_core(ast * n) { } n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk(); + static unsigned s_counter = 0; TRACE("ast", tout << "Object " << n->m_id << " was created.\n";); diff --git a/src/math/automata/automaton.h b/src/math/automata/automaton.h index cf4dcbfc6..2f55d5cc2 100644 --- a/src/math/automata/automaton.h +++ b/src/math/automata/automaton.h @@ -107,11 +107,10 @@ public: m_init = init; m_delta.push_back(moves()); m_delta_inv.push_back(moves()); - for (unsigned i = 0; i < final.size(); ++i) { - add_to_final_states(final[i]); + for (unsigned f : final) { + add_to_final_states(f); } - for (unsigned i = 0; i < mvs.size(); ++i) { - move const& mv = mvs[i]; + for (move const& mv : mvs) { unsigned n = std::max(mv.src(), mv.dst()); if (n >= m_delta.size()) { m_delta.resize(n+1, moves()); @@ -280,8 +279,8 @@ public: } else { init = a.num_states(); - for (unsigned i = 0; i < a.m_final_states.size(); ++i) { - mvs.push_back(move(m, init, a.m_final_states[i])); + for (unsigned st : a.m_final_states) { + mvs.push_back(move(m, init, st)); } } return alloc(automaton, m, init, final, mvs); @@ -471,18 +470,17 @@ public: moves const& get_moves_to(unsigned state) const { return m_delta_inv[state]; } bool initial_state_is_source() const { return m_delta_inv[m_init].empty(); } bool is_final_state(unsigned s) const { return m_final_set.contains(s); } - bool is_final_configuration(uint_set s) const { - for (uint_set::iterator it = s.begin(), end = s.end(); it != end; ++it) { - if (is_final_state(*it)) - return true; - } - return false; - } + bool is_final_configuration(uint_set s) const { + for (unsigned i : s) { + if (is_final_state(i)) + return true; + } + return false; + } bool is_epsilon_free() const { - for (unsigned i = 0; i < m_delta.size(); ++i) { - moves const& mvs = m_delta[i]; - for (unsigned j = 0; j < mvs.size(); ++j) { - if (!mvs[j].t()) return false; + for (moves const& mvs : m_delta) { + for (move const & m : mvs) { + if (!m.t()) return false; } } return true; @@ -490,8 +488,8 @@ public: bool all_epsilon_in(unsigned s) { moves const& mvs = m_delta_inv[s]; - for (unsigned j = 0; j < mvs.size(); ++j) { - if (mvs[j].t()) return false; + for (move const& m : mvs) { + if (m.t()) return false; } return true; } @@ -504,15 +502,15 @@ public: bool is_loop_state(unsigned s) const { moves mvs; get_moves_from(s, mvs); - for (unsigned i = 0; i < mvs.size(); ++i) { - if (s == mvs[i].dst()) return true; + for (move const& m : mvs) { + if (s == m.dst()) return true; } return false; } unsigned move_count() const { unsigned result = 0; - for (unsigned i = 0; i < m_delta.size(); result += m_delta[i].size(), ++i) {} + for (moves const& mvs : m_delta) result += mvs.size(); return result; } void get_epsilon_closure(unsigned state, unsigned_vector& states) { @@ -524,13 +522,13 @@ public: void get_moves_from(unsigned state, moves& mvs, bool epsilon_closure = true) const { get_moves(state, m_delta, mvs, epsilon_closure); } - void get_moves_from_states(uint_set states, moves& mvs, bool epsilon_closure = true) const { - for (uint_set::iterator it = states.begin(), end = states.end(); it != end; ++it) { - moves curr; - get_moves(*it, m_delta, curr, epsilon_closure); - mvs.append(curr); - } - } + void get_moves_from_states(uint_set states, moves& mvs, bool epsilon_closure = true) const { + for (unsigned i : states) { + moves curr; + get_moves(i, m_delta, curr, epsilon_closure); + mvs.append(curr); + } + } void get_moves_to(unsigned state, moves& mvs, bool epsilon_closure = true) { get_moves(state, m_delta_inv, mvs, epsilon_closure); } @@ -543,8 +541,7 @@ public: out << "\n"; for (unsigned i = 0; i < m_delta.size(); ++i) { moves const& mvs = m_delta[i]; - for (unsigned j = 0; j < mvs.size(); ++j) { - move const& mv = mvs[j]; + for (move const& mv : mvs) { out << i << " -> " << mv.dst() << " "; if (mv.t()) { out << "if "; diff --git a/src/math/automata/symbolic_automata.h b/src/math/automata/symbolic_automata.h index 4a8e7a74d..35545e975 100644 --- a/src/math/automata/symbolic_automata.h +++ b/src/math/automata/symbolic_automata.h @@ -136,7 +136,8 @@ private: //false case curr_bv.push_back(false); - ref_t new_pred_neg(m_ba.mk_and(curr_pred, m_ba.mk_not(constraints[i])), m); + ref_t neg(m_ba.mk_not(constraints[i]), m); + ref_t new_pred_neg(m_ba.mk_and(curr_pred, neg), m); generate_min_terms_rec(constraints, min_terms, i + 1, curr_bv, new_pred_neg); curr_bv.pop_back(); } diff --git a/src/math/automata/symbolic_automata_def.h b/src/math/automata/symbolic_automata_def.h index c1ee53214..aa8dd34fd 100644 --- a/src/math/automata/symbolic_automata_def.h +++ b/src/math/automata/symbolic_automata_def.h @@ -288,7 +288,7 @@ typename symbolic_automata::automaton_t* symbolic_automata::mk_determinstic_param(automaton_t& a, bool flip_acceptance) { vector, ref_t> > min_terms; vector predicates; - + map s2id; // set of states to unique id vector id2s; // unique id to set of b-states uint_set set; @@ -296,9 +296,19 @@ symbolic_automata::mk_determinstic_param(automaton_t& a, bool flip_accepta moves_t new_mvs; // moves in the resulting automaton unsigned_vector new_final_states; // new final states unsigned p_state_id = 0; // next state identifier - + + TRACE("seq", tout << "mk-deterministic " << flip_acceptance << " " << set << " " << a.is_final_configuration(set) << "\n";); // adds non-final states of a to final if flipping and and final otherwise - if (a.is_final_configuration(set) != flip_acceptance) { + unsigned_vector init_states; + a.get_epsilon_closure(a.init(), init_states); + bool found_final = false; + for (unsigned s : init_states) { + if (a.is_final_state(s)) { + found_final = true; + break; + } + } + if (found_final != flip_acceptance) { new_final_states.push_back(p_state_id); } @@ -342,6 +352,7 @@ symbolic_automata::mk_determinstic_param(automaton_t& a, bool flip_accepta bool is_new = !s2id.contains(set); if (is_new) { + TRACE("seq", tout << "mk-deterministic " << flip_acceptance << " " << set << " " << a.is_final_configuration(set) << "\n";); if (a.is_final_configuration(set) != flip_acceptance) { new_final_states.push_back(p_state_id); } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index c91882dad..a32a4833a 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3391,15 +3391,22 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) { return; } - eautomaton* a = get_automaton(e2); + expr_ref e3(e2, m); + context& ctx = get_context(); + literal lit = ctx.get_literal(n); + if (!is_true) { + e3 = m_util.re.mk_complement(e2); + is_true = true; + lit.neg(); + } + eautomaton* a = get_automaton(e3); if (!a) return; - context& ctx = get_context(); expr_ref len(m_util.str.mk_length(e1), m); for (unsigned i = 0; i < a->num_states(); ++i) { - literal acc = mk_accept(e1, len, e2, i); - literal rej = mk_reject(e1, len, e2, i); + literal acc = mk_accept(e1, len, e3, i); + literal rej = mk_reject(e1, len, e3, i); add_axiom(a->is_final_state(i)?acc:~acc); add_axiom(a->is_final_state(i)?~rej:rej); } @@ -3408,17 +3415,16 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) { unsigned_vector states; a->get_epsilon_closure(a->init(), states); literal_vector lits; - literal lit = ctx.get_literal(n); if (is_true) { lits.push_back(~lit); } for (unsigned i = 0; i < states.size(); ++i) { if (is_true) { - lits.push_back(mk_accept(e1, zero, e2, states[i])); + lits.push_back(mk_accept(e1, zero, e3, states[i])); } else { literal nlit = ~lit; - propagate_lit(0, 1, &nlit, mk_reject(e1, zero, e2, states[i])); + propagate_lit(0, 1, &nlit, mk_reject(e1, zero, e3, states[i])); } } if (is_true) {