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

issues #963 #912

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-04-17 03:03:59 -07:00
parent 8b5627e361
commit 66e61b8a31
3 changed files with 64 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

41
src/smt/theory_seq.cpp
View file

@ -255,6 +255,11 @@ final_check_status theory_seq::final_check_eh() {
TRACE("seq", tout << ">>solve_eqs\n";);
return FC_CONTINUE;
}
if (check_contains()) {
++m_stats.m_propagate_contains;
TRACE("seq", tout << ">>propagate_contains\n";);
return FC_CONTINUE;
}
if (solve_nqs(0)) {
++m_stats.m_solve_nqs;
TRACE("seq", tout << ">>solve_nqs\n";);
@ -290,11 +295,6 @@ final_check_status theory_seq::final_check_eh() {
TRACE("seq", tout << ">>propagate_automata\n";);
return FC_CONTINUE;
}
if (check_contains()) {
++m_stats.m_propagate_contains;
TRACE("seq", tout << ">>propagate_contains\n";);
return FC_CONTINUE;
}
if (is_solved()) {
TRACE("seq", tout << ">>is_solved\n";);
return FC_DONE;
@ -1159,7 +1159,7 @@ bool theory_seq::check_extensionality() {
}
/*
\brief check negated contains constriants.
\brief check negated contains constraints.
*/
bool theory_seq::check_contains() {
context & ctx = get_context();
@ -1199,6 +1199,11 @@ bool theory_seq::is_solved() {
IF_VERBOSE(10, display_disequation(verbose_stream() << "(seq.giveup ", m_nqs[0]); verbose_stream() << " is unsolved)\n";);
return false;
}
if (!m_ncs.empty()) {
TRACE("seq", display_nc(tout << "(seq.giveup ", m_ncs[0]); tout << " is unsolved)\n";);
IF_VERBOSE(10, display_nc(verbose_stream() << "(seq.giveup ", m_ncs[0]); verbose_stream() << " is unsolved)\n";);
return false;
}
return true;
}
@ -1984,6 +1989,22 @@ bool theory_seq::solve_nc(unsigned idx) {
m_new_propagation = true;
return true;
}
expr* e1, *e2;
if (m.is_eq(c, e1, e2)) {
literal eq = mk_eq(e1, e2, false);
propagate_lit(deps, 0, 0, ~eq);
return true;
}
if (m.is_or(c)) {
for (unsigned i = 0; i < to_app(c)->get_num_args(); ++i) {
expr_ref ci(to_app(c)->get_arg(i), m);
m_ncs.push_back(nc(ci, deps));
}
m_new_propagation = true;
return true;
}
return false;
}
@ -2418,13 +2439,17 @@ void theory_seq::display(std::ostream & out) const {
if (!m_ncs.empty()) {
out << "Non contains:\n";
for (unsigned i = 0; i < m_ncs.size(); ++i) {
out << "not " << mk_pp(m_ncs[i].contains(), m) << "\n";
display_deps(out << " <- ", m_ncs[i].deps()); out << "\n";
display_nc(out, m_ncs[i]);
}
}
}
void theory_seq::display_nc(std::ostream& out, nc const& nc) const {
out << "not " << mk_pp(nc.contains(), m) << "\n";
display_deps(out << " <- ", nc.deps()); out << "\n";
}
void theory_seq::display_equations(std::ostream& out) const {
for (unsigned i = 0; i < m_eqs.size(); ++i) {
display_equation(out, m_eqs[i]);

1
src/smt/theory_seq.h
View file

@ -570,6 +570,7 @@ namespace smt {
void display_disequation(std::ostream& out, ne const& e) const;
void display_deps(std::ostream& out, dependency* deps) const;
void display_deps(std::ostream& out, literal_vector const& lits, enode_pair_vector const& eqs) const;
void display_nc(std::ostream& out, nc const& nc) const;
public:
theory_seq(ast_manager& m);
virtual ~theory_seq();