mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-13 14:40:55 +00:00
Code Activity

explain conflict

Browse source
This commit is contained in:
Jakob Rath 2023-07-18 11:26:18 +02:00
parent 5e5164ed2c
commit 4049716946
1 changed files with 22 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

31
src/math/polysat/slicing.cpp
View file

@ -320,15 +320,6 @@ namespace polysat {
return m_bv->is_numeral(s->get_app()->get_arg(0), val); return m_bv->is_numeral(s->get_app()->get_arg(0), val);
} }
bool slicing::merge_base(enode* s1, enode* s2, dep_t dep) {
SASSERT_EQ(width(s1), width(s2));
SASSERT(!has_sub(s1));
SASSERT(!has_sub(s2));
m_egraph.merge(s1, s2, encode_dep(dep));
m_egraph.propagate(); // TODO: could do this later maybe
return !m_egraph.inconsistent();
}
void slicing::begin_explain() { void slicing::begin_explain() {
SASSERT(m_marked_lits.empty()); SASSERT(m_marked_lits.empty());
SASSERT(m_marked_vars.empty()); SASSERT(m_marked_vars.empty());
@ -420,6 +411,28 @@ namespace polysat {
end_explain(); end_explain();
} }
void slicing::explain(sat::literal_vector& out_lits, unsigned_vector& out_vars) {
SASSERT(is_conflict());
begin_explain();
SASSERT(m_tmp_justifications.empty());
m_egraph.begin_explain();
m_egraph.explain(m_tmp_justifications, nullptr);
m_egraph.end_explain();
for (void* dp : m_tmp_justifications)
push_dep(dp, out_lits, out_vars);
m_tmp_justifications.reset();
end_explain();
}
bool slicing::merge_base(enode* s1, enode* s2, dep_t dep) {
SASSERT_EQ(width(s1), width(s2));
SASSERT(!has_sub(s1));
SASSERT(!has_sub(s2));
m_egraph.merge(s1, s2, encode_dep(dep));
// m_egraph.propagate();
return !m_egraph.inconsistent();
}
bool slicing::merge(enode_vector& xs, enode_vector& ys, dep_t dep) { bool slicing::merge(enode_vector& xs, enode_vector& ys, dep_t dep) {
while (!xs.empty()) { while (!xs.empty()) {
SASSERT(!ys.empty()); SASSERT(!ys.empty());