From 4ad3324d2e54efec047244bd4067426b3f051766 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jul 2023 12:58:17 -0700 Subject: [PATCH 1/4] fixes to trim Signed-off-by: Nikolaj Bjorner --- src/sat/sat_proof_trim.cpp | 70 ++++++++++++++------------------------ src/sat/sat_proof_trim.h | 13 ++++--- 2 files changed, 35 insertions(+), 48 deletions(-) diff --git a/src/sat/sat_proof_trim.cpp b/src/sat/sat_proof_trim.cpp index b4171f51d..d47819921 100644 --- a/src/sat/sat_proof_trim.cpp +++ b/src/sat/sat_proof_trim.cpp @@ -7,15 +7,13 @@ Abstract: - proof replay and trim + The proof is trimmed by re-running the proof steps and collecting justified literals + at level 0. The proof is obtained by back-tracing the justificiations attached to literals. Author: Nikolaj Bjorner 2023-10-04 - Notes: - - --*/ #include "sat/sat_proof_trim.h" @@ -31,10 +29,7 @@ namespace sat { vector> proof_trim::trim() { m_result.reset(); - m_core_literals.reset(); - m_propagated.resize(num_vars(), false); - m_core_literals.insert(literal_vector()); - m_core_literals.insert(m_conflict); + m_propagated.resize(num_vars(), false); IF_VERBOSE(10, s.display(verbose_stream() << "trim\n")); @@ -58,7 +53,7 @@ namespace sat { del(cl, clp); if (!in_core(cl)) continue; - IF_VERBOSE(4, verbose_stream() << cl << " in-core " << in_core(cl) << ": "; for (auto const& c : m_core_literals) verbose_stream() << "{" << c << "} "; verbose_stream() << "\n"); + IF_VERBOSE(4, verbose_stream() << cl << " in-core " << in_core(cl) << ": "; for (auto const& [k,v] : m_clauses) verbose_stream() << "{" << v.m_clauses << "} "; verbose_stream() << "\n"); m_result.push_back({id, unsigned_vector()}); if (is_initial) @@ -122,7 +117,6 @@ namespace sat { auto js = s.get_justification(l); bool in_coi = false; - //verbose_stream() << l << " " << js << "\n"; if (js.is_clause()) for (literal lit : s.get_clause(js)) in_coi |= m_in_coi.contains(lit.index()); @@ -281,19 +275,18 @@ namespace sat { } std::sort(m_clause.begin(), m_clause.end()); IF_VERBOSE(3, verbose_stream() << "add core " << m_clause << "\n"); - unsigned id; - VERIFY(m_clause2id.find(m_clause, id)); + auto& [clauses, id, in_core] = m_clauses.find(m_clause); + in_core = true; m_result.back().second.push_back(id); - m_core_literals.insert(m_clause); if (l != null_literal && s.lvl(l) == 0) { m_clause.reset(); m_clause.push_back(l); - m_core_literals.insert(m_clause); + m_clauses.insert_if_not_there(m_clause, {{}, 0, true }).m_in_core = true; } } bool proof_trim::in_core(literal_vector const& cl) const { - return m_core_literals.contains(cl); + return m_clauses.find(cl).m_in_core; } void proof_trim::revive(literal_vector const& cl, clause* cp) { @@ -313,23 +306,15 @@ namespace sat { auto* e = m_clauses.find_core(cl); if (!e) return cp; - auto& v = e->get_data().m_value; - if (!v.empty()) { - cp = v.back(); + auto& [clauses, id, in_core] = e->get_data().m_value; + if (!clauses.empty()) { + cp = clauses.back(); TRACE("sat", tout << "del: " << *cp << "\n"); s.detach_clause(*cp); - v.pop_back(); + clauses.pop_back(); } return cp; - } - - void proof_trim::save(literal_vector const& lits, clause* cl) { - if (!cl) - return; - IF_VERBOSE(3, verbose_stream() << "add: " << *cl << "\n"); - auto& v = m_clauses.insert_if_not_there(lits, clause_vector()); - v.push_back(cl); - } + } proof_trim::proof_trim(params_ref const& p, reslimit& lim): s(p, lim) { @@ -337,24 +322,26 @@ namespace sat { } void proof_trim::assume(unsigned id, bool is_initial) { - std::sort(m_clause.begin(), m_clause.end()); + std::sort(m_clause.begin(), m_clause.end()); if (unit_or_binary_occurs()) - return; - if (!m_conflict.empty() && m_clause.empty()) - m_trail.push_back({id , m_clause, nullptr, true, is_initial}); + return; + if (!m_conflict.empty() && m_clause.empty()) { + m_clauses.insert(m_clause, { {}, id, m_clause.empty() }); + m_trail.push_back({ id , m_clause, nullptr, true, is_initial }); + } if (!m_conflict.empty()) return; IF_VERBOSE(3, verbose_stream() << (is_initial?"assume ":"rup ") << m_clause << "\n"); - std::sort(m_clause.begin(), m_clause.end()); - m_clause2id.insert(m_clause, id); auto* cl = s.mk_clause(m_clause, status::redundant()); + auto& [clauses, id2, in_core] = m_clauses.insert_if_not_there(m_clause, { {}, id, m_clause.empty() }); + if (cl) + clauses.push_back(cl); + m_trail.push_back({ id, m_clause, cl, true, is_initial }); auto is_unit2 = [&]() { - if (s.value(m_clause[0]) == l_false) { - std::swap(m_clause[0], m_clause[1]); - return true; - } + if (s.value(m_clause[0]) == l_false) + std::swap(m_clause[0], m_clause[1]); return s.value(m_clause[1]) == l_false; }; @@ -375,16 +362,13 @@ namespace sat { return false; }; - m_trail.push_back({ id, m_clause, cl, true, is_initial }); if (m_clause.size() == 2 && is_unit2()) s.propagate_bin_clause(m_clause[0], m_clause[1]); else if (m_clause.size() > 2 && is_unit()) s.propagate_clause(*cl, true, 0, s.cls_allocator().get_offset(cl)); s.propagate(false); if (s.inconsistent() || all_of(m_clause, [&](sat::literal lit) { return s.value(lit) == l_false; })) - set_conflict(m_clause, cl); - - save(m_clause, cl); + set_conflict(m_clause, cl); } /** @@ -411,6 +395,4 @@ namespace sat { void proof_trim::infer(unsigned id) { assume(id, false); } - - } diff --git a/src/sat/sat_proof_trim.h b/src/sat/sat_proof_trim.h index 9a43315f3..24091e69c 100644 --- a/src/sat/sat_proof_trim.h +++ b/src/sat/sat_proof_trim.h @@ -47,10 +47,16 @@ namespace sat { return a == b; } }; - map m_clauses; - map m_clause2id; - hashtable m_core_literals; + + struct clause_info { + clause_vector m_clauses; + unsigned m_id = 0; + bool m_in_core = false; + }; + + + map m_clauses; bool_vector m_propagated; void del(literal_vector const& cl, clause* cp); @@ -65,7 +71,6 @@ namespace sat { bool in_core(literal_vector const& cl) const; void revive(literal_vector const& cl, clause* cp); clause* del(literal_vector const& cl); - void save(literal_vector const& lits, clause* cl); uint_set m_units; bool unit_or_binary_occurs(); From f4b87b37638cf48f91830f46861aeb53d2597d9f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jul 2023 13:04:49 -0700 Subject: [PATCH 2/4] fix memory smash in euf completion Signed-off-by: Nikolaj Bjorner --- src/ast/simplifiers/euf_completion.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp index 3ede7024e..280b5e6bf 100644 --- a/src/ast/simplifiers/euf_completion.cpp +++ b/src/ast/simplifiers/euf_completion.cpp @@ -307,7 +307,7 @@ namespace euf { } }; SASSERT(e); - if (num_scopes() > 0) + if (num_scopes() > 0 && m_canonical.size() > n->get_id()) m_trail.push(vtrail(m_canonical, n->get_id())); m_canonical.setx(n->get_id(), e); m_epochs.setx(n->get_id(), m_epoch, 0); From 3782eb1be4a5bd228d144b1885db364f75818533 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Jul 2023 19:50:07 -0700 Subject: [PATCH 3/4] fix #6785 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 32c7a5763..e6e52dd79 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -11286,6 +11286,8 @@ def Plus(re): >>> print(simplify(InRe("", re))) False """ + if z3_debug(): + _z3_assert(is_expr(re), "expression expected") return ReRef(Z3_mk_re_plus(re.ctx_ref(), re.as_ast()), re.ctx) @@ -11299,6 +11301,8 @@ def Option(re): >>> print(simplify(InRe("aa", re))) False """ + if z3_debug(): + _z3_assert(is_expr(re), "expression expected") return ReRef(Z3_mk_re_option(re.ctx_ref(), re.as_ast()), re.ctx) @@ -11317,6 +11321,8 @@ def Star(re): >>> print(simplify(InRe("", re))) True """ + if z3_debug(): + _z3_assert(is_expr(re), "expression expected") return ReRef(Z3_mk_re_star(re.ctx_ref(), re.as_ast()), re.ctx) @@ -11330,6 +11336,8 @@ def Loop(re, lo, hi=0): >>> print(simplify(InRe("", re))) False """ + if z3_debug(): + _z3_assert(is_expr(re), "expression expected") return ReRef(Z3_mk_re_loop(re.ctx_ref(), re.as_ast(), lo, hi), re.ctx) @@ -11343,11 +11351,17 @@ def Range(lo, hi, ctx=None): """ lo = _coerce_seq(lo, ctx) hi = _coerce_seq(hi, ctx) + if z3_debug(): + _z3_assert(is_expr(lo), "expression expected") + _z3_assert(is_expr(hi), "expression expected") return ReRef(Z3_mk_re_range(lo.ctx_ref(), lo.ast, hi.ast), lo.ctx) def Diff(a, b, ctx=None): """Create the difference regular expression """ + if z3_debug(): + _z3_assert(is_expr(a), "expression expected") + _z3_assert(is_expr(b), "expression expected") return ReRef(Z3_mk_re_diff(a.ctx_ref(), a.ast, b.ast), a.ctx) def AllChar(regex_sort, ctx=None): From 68663fd97a9bda48155de1bf087e303be256f1eb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 6 Jul 2023 09:02:58 -0700 Subject: [PATCH 4/4] fix indentation for python file Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index e6e52dd79..20871d36e 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -11351,7 +11351,7 @@ def Range(lo, hi, ctx=None): """ lo = _coerce_seq(lo, ctx) hi = _coerce_seq(hi, ctx) - if z3_debug(): + if z3_debug(): _z3_assert(is_expr(lo), "expression expected") _z3_assert(is_expr(hi), "expression expected") return ReRef(Z3_mk_re_range(lo.ctx_ref(), lo.ast, hi.ast), lo.ctx) @@ -11359,7 +11359,7 @@ def Range(lo, hi, ctx=None): def Diff(a, b, ctx=None): """Create the difference regular expression """ - if z3_debug(): + if z3_debug(): _z3_assert(is_expr(a), "expression expected") _z3_assert(is_expr(b), "expression expected") return ReRef(Z3_mk_re_diff(a.ctx_ref(), a.ast, b.ast), a.ctx)