mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

check that disequations are solved

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-01-08 16:07:42 -08:00
parent 3d01246f71
commit 4939957f6a
1 changed files with 17 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/smt/theory_seq.cpp
View file

@ -551,6 +551,9 @@ bool theory_seq::is_solved() {
IF_VERBOSE(10, verbose_stream() << "(seq.giveup " << m_eqs[0].ls() << " = " << m_eqs[0].rs() << " is unsolved)\n";); IF_VERBOSE(10, verbose_stream() << "(seq.giveup " << m_eqs[0].ls() << " = " << m_eqs[0].rs() << " is unsolved)\n";);
return false; return false;
} }
if (!m_nqs.empty()) {
return false;
}
for (unsigned i = 0; i < m_automata.size(); ++i) { for (unsigned i = 0; i < m_automata.size(); ++i) {
if (!m_automata[i]) { if (!m_automata[i]) {
IF_VERBOSE(10, verbose_stream() << "(seq.giveup regular expression did not compile to automaton)\n";); IF_VERBOSE(10, verbose_stream() << "(seq.giveup regular expression did not compile to automaton)\n";);
@ -967,10 +970,10 @@ bool theory_seq::solve_ne(unsigned idx) {
} }
} }
bool updated = false;
dependency* new_deps = n.dep(); dependency* new_deps = n.dep();
vector<expr_ref_vector> new_ls, new_rs; vector<expr_ref_vector> new_ls, new_rs;
literal_vector new_lits(n.lits()); literal_vector new_lits(n.lits());
bool updated = false;
for (unsigned i = 0; i < n.ls().size(); ++i) { for (unsigned i = 0; i < n.ls().size(); ++i) {
expr_ref_vector& ls = m_ls; expr_ref_vector& ls = m_ls;
expr_ref_vector& rs = m_rs; expr_ref_vector& rs = m_rs;
@ -986,8 +989,7 @@ bool theory_seq::solve_ne(unsigned idx) {
return true; return true;
} }
else if (!change) { else if (!change) {
// std::cout << n.ls(i) << " " << ls << "\n"; TRACE("seq", tout << "no change " << n.ls(i) << " " << n.rs(i) << "\n";);
// std::cout << n.rs(i) << " " << rs << "\n";
continue; continue;
} }
else { else {
@ -1041,6 +1043,16 @@ bool theory_seq::solve_ne(unsigned idx) {
new_deps = m_dm.mk_join(deps, new_deps); new_deps = m_dm.mk_join(deps, new_deps);
} }
} }
if (!updated && num_undef_lits == 0) {
return false;
}
if (!updated) {
for (unsigned j = 0; j < n.ls().size(); ++j) {
new_ls.push_back(n.ls(j));
new_rs.push_back(n.rs(j));
}
}
if (num_undef_lits == 1 && new_ls.empty()) { if (num_undef_lits == 1 && new_ls.empty()) {
literal_vector lits; literal_vector lits;
literal undef_lit = null_literal; literal undef_lit = null_literal;
@ -1064,7 +1076,7 @@ bool theory_seq::solve_ne(unsigned idx) {
propagate_lit(new_deps, lits.size(), lits.c_ptr(), ~undef_lit); propagate_lit(new_deps, lits.size(), lits.c_ptr(), ~undef_lit);
return true; return true;
} }
else if (updated) { if (updated) {
if (num_undef_lits == 0 && new_ls.empty()) { if (num_undef_lits == 0 && new_ls.empty()) {
TRACE("seq", tout << "conflict\n";); TRACE("seq", tout << "conflict\n";);
set_conflict(new_deps, new_lits); set_conflict(new_deps, new_lits);