mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

fix #3935

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-13 10:00:42 -07:00
parent 01c12c951c
commit 5c4f775b1b
3 changed files with 11 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -120,6 +120,9 @@ private:
}
void generate_min_terms_rec(vector<ref_t> &constraints, vector<std::pair<vector<bool>, ref_t> > &min_terms, unsigned i, vector<bool> &curr_bv, ref_t &curr_pred) {
lbool is_sat = m_ba.is_sat(curr_pred);
if (is_sat == l_undef)
throw default_exception("incomplete theory: unable to generate min-terms");
if (is_sat != l_true) {
return;
}

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

@ -44,7 +44,7 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_total
ref_t cond(m_ba.mk_not(m_ba.mk_or(vs.size(), vs.c_ptr())), m);
lbool is_sat = m_ba.is_sat(cond);
if (is_sat == l_undef) {
return 0;
return nullptr;
}
if (is_sat == l_true) {
new_mvs.push_back(move_t(m, i, dead_state, cond));
@ -191,7 +191,7 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_minim
p1.insert(q);
break;
case l_undef:
return 0;
return nullptr;
default:
break;
}
@ -200,7 +200,7 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_minim
ref_t psi_min_phi(m_ba.mk_and(psi, m_ba.mk_not(phi)), m);
lbool is_sat = m_ba.is_sat(psi_min_phi);
if (is_sat == l_undef) {
return 0;
return nullptr;
}
if (is_sat == l_true) {
psi = psi_min_phi;
@ -211,7 +211,7 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_minim
ref_t phi_min_psi(m_ba.mk_and(phi, m_ba.mk_not(psi)), m);
is_sat = m_ba.is_sat(phi_min_psi);
if (is_sat == l_undef) {
return 0;
return nullptr;
}
else if (is_sat == l_false) {
p1.insert(q); // psi and phi are equivalent

7
src/smt/theory_seq.cpp
View file

@ -6366,8 +6366,8 @@ bool theory_seq::is_accept(expr* e, expr*& s, expr*& idx, expr*& re, unsigned& i
VERIFY(m_autil.is_numeral(to_app(e)->get_arg(3), r));
SASSERT(r.is_unsigned());
i = r.get_unsigned();
aut = get_automaton(re);
return true;
aut = get_automaton(re);
return aut != nullptr;
}
else {
return false;
@ -6444,7 +6444,8 @@ void theory_seq::propagate_accept(literal lit, expr* acc) {
context& ctx = get_context();
rational _idx;
eautomaton* aut = nullptr;
VERIFY(is_accept(acc, e, idx, re, src, aut));
if (!is_accept(acc, e, idx, re, src, aut))
return;
VERIFY(m_autil.is_numeral(idx, _idx));
VERIFY(aut);
if (aut->is_sink_state(src)) {