mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 03:07:07 +00:00
Code Activity

fix #1233

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-21 11:52:15 -08:00
parent c5f231acdf
commit d520557ad9
6 changed files with 41 additions and 58 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/smt/smt_b_justification.h
View file

@ -93,6 +93,16 @@ namespace smt {
const b_justification null_b_justification(static_cast<clause*>(0));
inline std::ostream& operator<<(std::ostream& out, b_justification::kind k) {
switch (k) {
case b_justification::CLAUSE: return out << "clause";
case b_justification::BIN_CLAUSE: return out << "bin_clause";
case b_justification::AXIOM: return out << "axiom";
case b_justification::JUSTIFICATION: return out << "theory";
}
return out;
}
typedef std::pair<literal, b_justification> justified_literal;
};

14
src/smt/smt_conflict_resolution.cpp
View file

@ -468,20 +468,6 @@ namespace smt {
}
bool conflict_resolution::resolve(b_justification conflict, literal not_l) {
#if 0
// for debugging #1233
if (not_l == to_literal(22267)) {
std::cout << not_l << "\n";
enable_trace("conflict");
enable_trace("conflict_verbose");
TRACE("conflict",
unsigned idx = 0;
for (literal lit : m_assigned_literals) {
m_ctx.display_literal(tout << (idx++) << ":", lit); tout << "\n";
});
}
#endif
b_justification js;
literal consequent;

8
src/smt/smt_context.cpp
View file

@ -285,15 +285,7 @@ namespace smt {
d.set_justification(j);
}
void context::assign_core(literal l, b_justification j, bool decision) {
#if 0
// for debugging #1233
if (l.var() == 11133 && l.sign()) {
std::cout << l << "\n";
UNREACHABLE();
}
#endif
TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " ";
display_literal_verbose(tout, l); tout << " level: " << m_scope_lvl << "\n";
display(tout, j););

2
src/smt/smt_context_pp.cpp
View file

@ -601,7 +601,7 @@ namespace smt {
out << "justification " << j.get_justification()->get_from_theory() << ": ";
literal_vector lits;
const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
display_literals(out, lits.size(), lits.c_ptr());
display_literals(out, lits);
break;
}
default:

63
src/smt/theory_seq.cpp
View file

@ -1228,18 +1228,25 @@ bool theory_seq::is_solved() {
return true;
}
void theory_seq::linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const {
/**
\brief while extracting dependency literals ensure that they have all been asserted on the context.
*/
bool theory_seq::linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const {
context & ctx = get_context();
DEBUG_CODE(for (literal lit : lits) SASSERT(ctx.get_assignment(lit) == l_true); );
bool asserted = true;
svector<assumption> assumptions;
const_cast<dependency_manager&>(m_dm).linearize(dep, assumptions);
for (unsigned i = 0; i < assumptions.size(); ++i) {
assumption const& a = assumptions[i];
for (assumption const& a : assumptions) {
if (a.lit != null_literal) {
lits.push_back(a.lit);
asserted &= ctx.get_assignment(a.lit) == l_true;
}
if (a.n1 != 0) {
eqs.push_back(enode_pair(a.n1, a.n2));
}
}
return asserted;
}
@ -1257,7 +1264,8 @@ void theory_seq::propagate_lit(dependency* dep, unsigned n, literal const* _lits
ctx.mark_as_relevant(lit);
enode_pair_vector eqs;
linearize(dep, eqs, lits);
if (!linearize(dep, eqs, lits))
return;
TRACE("seq",
tout << "assert:";
ctx.display_detailed_literal(tout, lit);
@ -1276,7 +1284,8 @@ void theory_seq::set_conflict(dependency* dep, literal_vector const& _lits) {
context& ctx = get_context();
enode_pair_vector eqs;
literal_vector lits(_lits);
linearize(dep, eqs, lits);
if (!linearize(dep, eqs, lits))
return;
TRACE("seq", display_deps(tout << "assert conflict:", lits, eqs););
m_new_propagation = true;
ctx.set_conflict(
@ -1292,27 +1301,13 @@ void theory_seq::propagate_eq(dependency* dep, enode* n1, enode* n2) {
context& ctx = get_context();
literal_vector lits;
enode_pair_vector eqs;
linearize(dep, eqs, lits);
if (!linearize(dep, eqs, lits))
return;
TRACE("seq",
tout << "assert: " << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << " <-\n";
display_deps(tout, dep);
);
#if 0
//std::cout << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << "\n";
//display_deps(std::cout, dep);
for (literal lit : lits) {
SASSERT(ctx.get_assignment(lit) == l_true);
}
for (enode_pair p : eqs) {
if (p.first->get_root() != p.second->get_root()) {
std::cout << mk_pp(p.first->get_owner(), m) << " " << mk_pp(p.second->get_owner(), m) << "\n";
}
SASSERT(p.first->get_root() == p.second->get_root());
}
#endif
justification* js = ctx.mk_justification(
ext_theory_eq_propagation_justification(
get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), n1, n2));
@ -1858,12 +1853,12 @@ bool theory_seq::solve_ne(unsigned idx) {
ne const& n = m_nqs[idx];
unsigned num_undef_lits = 0;
for (unsigned i = 0; i < n.lits().size(); ++i) {
switch (ctx.get_assignment(n.lits(i))) {
for (literal lit : n.lits()) {
switch (ctx.get_assignment(lit)) {
case l_false:
TRACE("seq", display_disequation(tout << "has false literal\n", n);
ctx.display_literal_verbose(tout, n.lits(i));
tout << "\n" << n.lits(i) << " " << ctx.is_relevant(n.lits(i)) << "\n";
ctx.display_literal_verbose(tout, lit);
tout << "\n" << lit << " " << ctx.is_relevant(lit) << "\n";
);
return true;
case l_true:
@ -1967,8 +1962,7 @@ bool theory_seq::solve_ne(unsigned idx) {
if (num_undef_lits == 1 && new_ls.empty()) {
literal_vector lits;
literal undef_lit = null_literal;
for (unsigned i = 0; i < new_lits.size(); ++i) {
literal lit = new_lits[i];
for (literal lit : new_lits) {
switch (ctx.get_assignment(lit)) {
case l_true:
lits.push_back(lit);
@ -2574,8 +2568,8 @@ void theory_seq::display_disequations(std::ostream& out) const {
}
void theory_seq::display_disequation(std::ostream& out, ne const& e) const {
for (unsigned j = 0; j < e.lits().size(); ++j) {
out << e.lits(j) << " ";
for (literal lit : e.lits()) {
out << lit << " ";
}
if (e.lits().size() > 0) {
out << "\n";
@ -3820,11 +3814,11 @@ literal theory_seq::mk_eq_empty(expr* _e, bool phase) {
}
expr_ref_vector concats(m);
m_util.str.get_concat(e, concats);
for (unsigned i = 0; i < concats.size(); ++i) {
if (m_util.str.is_unit(concats[i].get())) {
for (expr* c : concats) {
if (m_util.str.is_unit(c)) {
return false_literal;
}
if (m_util.str.is_string(concats[i].get(), s) && s.length() > 0) {
if (m_util.str.is_string(c, s) && s.length() > 0) {
return false_literal;
}
}
@ -3895,8 +3889,9 @@ void theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp
literal_vector lits(_lits);
enode_pair_vector eqs;
linearize(deps, eqs, lits);
if (!linearize(deps, eqs, lits))
return;
if (add_to_eqs) {
deps = mk_join(deps, _lits);
new_eq_eh(deps, n1, n2);

2
src/smt/theory_seq.h
View file

@ -431,7 +431,7 @@ namespace smt {
bool explain_empty(expr_ref_vector& es, dependency*& dep);
// asserting consequences
void linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const;
bool linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const;
void propagate_lit(dependency* dep, literal lit) { propagate_lit(dep, 0, 0, lit); }
void propagate_lit(dependency* dep, unsigned n, literal const* lits, literal lit);
void propagate_eq(dependency* dep, enode* n1, enode* n2);