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

#6646

Browse source 
- always enable special-relations theory to deal with default setting and push
- fix bugs related to equality and transitivity.
This commit is contained in:
Nikolaj Bjorner 2023-03-25 17:37:59 -07:00
parent cd2ea6b703
commit ce501e0b6e
2 changed files with 21 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/smt_setup.cpp
View file

@ -802,7 +802,7 @@ namespace smt {
setup_dl();
setup_seq_str(st);
setup_fpa();
if (st.m_has_sr) setup_special_relations();
setup_special_relations();
}
void setup::setup_unknown(static_features & st) {
@ -818,7 +818,7 @@ namespace smt {
setup_seq_str(st);
setup_fpa();
setup_recfuns();
if (st.m_has_sr) setup_special_relations();
setup_special_relations();
return;
}

39
src/smt/theory_special_relations.cpp
View file

@ -71,7 +71,7 @@ namespace smt {
ensure_var(v1);
ensure_var(v2);
literal_vector ls;
ls.push_back(l);
ls.push_back(l);
return m_graph.add_non_strict_edge(v1, v2, ls) && m_graph.add_non_strict_edge(v2, v1, ls);
}
@ -130,6 +130,7 @@ namespace smt {
}
bool theory_special_relations::internalize_term(app * term) {
verbose_stream() << mk_pp(term, m) << "\n";
return false;
}
@ -156,9 +157,8 @@ namespace smt {
}
theory_var theory_special_relations::mk_var(expr* e) {
if (!ctx.e_internalized(e)) {
if (!ctx.e_internalized(e))
ctx.internalize(e, false);
}
enode * n = ctx.get_enode(e);
theory_var v = n->get_th_var(get_id());
if (null_theory_var == v) {
@ -582,18 +582,18 @@ namespace smt {
lbool theory_special_relations::final_check_po(relation& r) {
for (atom* ap : r.m_asserted_atoms) {
atom& a = *ap;
if (!a.phase() && r.m_uf.find(a.v1()) == r.m_uf.find(a.v2())) {
// v1 !-> v2
// find v1 -> v3 -> v4 -> v2 path
r.m_explanation.reset();
unsigned timestamp = r.m_graph.get_timestamp();
bool found_path = r.m_graph.find_shortest_reachable_path(a.v1(), a.v2(), timestamp, r);
if (found_path) {
TRACE("special_relations", tout << "check po conflict\n";);
r.m_explanation.push_back(a.explanation());
set_conflict(r);
return l_false;
}
if (a.phase())
continue;
// v1 !-> v2
// find v1 -> v3 -> v4 -> v2 path
r.m_explanation.reset();
unsigned timestamp = r.m_graph.get_timestamp();
bool found_path = a.v1() == a.v2() || r.m_graph.find_shortest_reachable_path(a.v1(), a.v2(), timestamp, r);
if (found_path) {
TRACE("special_relations", tout << "check po conflict\n";);
r.m_explanation.push_back(a.explanation());
set_conflict(r);
return l_false;
}
}
return l_true;
@ -601,9 +601,8 @@ namespace smt {
void theory_special_relations::propagate() {
if (m_can_propagate) {
for (auto const& kv : m_relations) {
for (auto const& kv : m_relations)
propagate(*kv.m_value);
}
m_can_propagate = false;
}
}
@ -1124,12 +1123,12 @@ namespace smt {
}
void theory_special_relations::display(std::ostream & out) const {
if (m_relations.empty()) return;
if (m_relations.empty())
return;
out << "Theory Special Relations\n";
display_var2enode(out);
for (auto const& kv : m_relations) {
for (auto const& kv : m_relations)
kv.m_value->display(*this, out);
}
}
void theory_special_relations::collect_asserted_po_atoms(vector<std::pair<bool_var, bool>>& atoms) const {