mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

complement regular expressions when used in negated membership constraints #1224

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-28 01:38:23 -07:00
parent 8542e4ae3d
commit 974eaab01c
5 changed files with 58 additions and 42 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/ast.cpp
View file

@ -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";);

59
src/math/automata/automaton.h
View file

@ -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 ";

3
src/math/automata/symbolic_automata.h
View file

@ -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();
}

17
src/math/automata/symbolic_automata_def.h
View file

@ -288,7 +288,7 @@ typename symbolic_automata<T, M>::automaton_t*
symbolic_automata<T, M>::mk_determinstic_param(automaton_t& a, bool flip_acceptance) {
vector<std::pair<vector<bool>, ref_t> > min_terms;
vector<ref_t> predicates;
map<uint_set, unsigned, uint_set::hash, uint_set::eq> s2id; // set of states to unique id
vector<uint_set> id2s; // unique id to set of b-states
uint_set set;
@ -296,9 +296,19 @@ symbolic_automata<T, M>::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<T, M>::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);
}

20
src/smt/theory_seq.cpp
View file

@ -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) {