From 28668c6efc5c6d6fa5cdfe630b56d7c370b13f53 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 4 Nov 2022 11:25:05 -0700 Subject: [PATCH] set up model reconstruction trail --- src/ast/expr_substitution.h | 4 +- src/ast/rewriter/expr_replacer.cpp | 5 ++ src/ast/rewriter/expr_replacer.h | 7 +- src/ast/simplifiers/dependent_expr.h | 4 + .../model_reconstruction_trail.cpp | 76 +++++++++++++++++-- .../simplifiers/model_reconstruction_trail.h | 62 +++++++++------ src/ast/simplifiers/solve_eqs.cpp | 10 +-- src/muz/spacer/spacer_iuc_solver.cpp | 6 +- 8 files changed, 130 insertions(+), 44 deletions(-) diff --git a/src/ast/expr_substitution.h b/src/ast/expr_substitution.h index 6d4b1b618..0e285ff7d 100644 --- a/src/ast/expr_substitution.h +++ b/src/ast/expr_substitution.h @@ -44,8 +44,10 @@ public: bool empty() const { return m_subst.empty(); } unsigned size() const { return m_subst.size(); } void insert(expr * s, expr * def, proof * def_pr = nullptr, expr_dependency * def_dep = nullptr); + void insert(expr* s, expr* def, expr_dependency* def_dep) { insert(s, def, nullptr, def_dep); } void erase(expr * s); - expr* find(expr* s) { proof* pr; expr* def; VERIFY(find(s, def, pr)); SASSERT(def); return def; } + expr* find(expr* s) { return m_subst[s]; } + expr_dependency* dep(expr* s) { return (*m_subst_dep)[s]; } bool find(expr * s, expr * & def, proof * & def_pr); bool find(expr * s, expr * & def, proof * & def_pr, expr_dependency * & def_dep); bool contains(expr * s); diff --git a/src/ast/rewriter/expr_replacer.cpp b/src/ast/rewriter/expr_replacer.cpp index 4fa83bed0..1007261ae 100644 --- a/src/ast/rewriter/expr_replacer.cpp +++ b/src/ast/rewriter/expr_replacer.cpp @@ -25,6 +25,11 @@ void expr_replacer::operator()(expr * t, expr_ref & result, proof_ref & result_p operator()(t, result, result_pr, result_dep); } +void expr_replacer::operator()(expr* t, expr_ref& result, expr_dependency_ref& result_dep) { + proof_ref result_pr(m()); + operator()(t, result, result_pr, result_dep); +} + void expr_replacer::operator()(expr * t, expr_ref & result) { proof_ref pr(m()); operator()(t, result, pr); diff --git a/src/ast/rewriter/expr_replacer.h b/src/ast/rewriter/expr_replacer.h index 82982adff..50831073b 100644 --- a/src/ast/rewriter/expr_replacer.h +++ b/src/ast/rewriter/expr_replacer.h @@ -34,9 +34,10 @@ public: virtual void set_substitution(expr_substitution * s) = 0; virtual void operator()(expr * t, expr_ref & result, proof_ref & result_pr, expr_dependency_ref & deps) = 0; - virtual void operator()(expr * t, expr_ref & result, proof_ref & result_pr); - virtual void operator()(expr * t, expr_ref & result); - virtual void operator()(expr_ref & t) { expr_ref s(t, m()); (*this)(s, t); } + void operator()(expr* t, expr_ref& result, expr_dependency_ref& deps); + void operator()(expr * t, expr_ref & result, proof_ref & result_pr); + void operator()(expr * t, expr_ref & result); + void operator()(expr_ref & t) { expr_ref s(t, m()); (*this)(s, t); } virtual unsigned get_num_steps() const { return 0; } virtual void reset() = 0; diff --git a/src/ast/simplifiers/dependent_expr.h b/src/ast/simplifiers/dependent_expr.h index 9d6d8625e..53f9cb9d8 100644 --- a/src/ast/simplifiers/dependent_expr.h +++ b/src/ast/simplifiers/dependent_expr.h @@ -68,6 +68,10 @@ public: m_fml = nullptr; m_dep = nullptr; } + + ast_manager& get_manager() const { return m; } + + expr* fml() const { return m_fml; } std::tuple operator()() const { return { m_fml, m_dep }; diff --git a/src/ast/simplifiers/model_reconstruction_trail.cpp b/src/ast/simplifiers/model_reconstruction_trail.cpp index 2e8eab0e6..077443e7e 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.cpp +++ b/src/ast/simplifiers/model_reconstruction_trail.cpp @@ -21,24 +21,86 @@ void model_reconstruction_trail::replay(dependent_expr const& d, vectorm_active) + continue; + + // updates that have no intersections with current variables are skipped + if (!t->intersects(free_vars)) + continue; + + // loose entries that intersect with free vars are deleted from the trail + // and their removed formulas are added to the resulting constraints. + if (t->is_loose()) { + added.append(t->m_removed); + for (auto r : t->m_removed) + add_vars(r, free_vars); + m_trail_stack.push(value_trail(t->m_active)); + t->m_active = false; + continue; + } + + // rigid entries: + // apply substitution to added in case of rigid model convertions + for (auto& d : added) { + auto [f, dep1] = d(); + expr_ref g(m); + expr_dependency_ref dep2(m); + (*t->m_replace)(f, g, dep2); + d = dependent_expr(m, g, m.mk_join(dep1, dep2)); + } + } } /** * retrieve the current model converter corresponding to chaining substitutions from the trail. */ model_converter_ref model_reconstruction_trail::get_model_converter() { - model_converter_ref mc = alloc(generic_model_converter, m, "dependent-expr-model"); + + // // walk the trail from the back // add substitutions from the back to the generic model converter // after they have been normalized using a global replace that replaces // substituted variables by their terms. - NOT_IMPLEMENTED_YET(); - return mc; + // + + scoped_ptr rp = mk_default_expr_replacer(m, true); + scoped_ptr subst = alloc(expr_substitution, m, true, false); + rp->set_substitution(subst.get()); + generic_model_converter_ref mc = alloc(generic_model_converter, m, "dependent-expr-model"); + bool first = true; + for (unsigned i = m_trail.size(); i-- > 0; ) { + auto* t = m_trail[i]; + if (!t->m_active) + continue; + + if (first) { + first = false; + for (auto const& [v, def] : t->m_subst->sub()) { + expr_dependency* dep = t->m_subst->dep(v); + subst->insert(v, def, dep); + mc->add(v, def); + } + continue; + } + expr_dependency_ref new_dep(m); + expr_ref new_def(m); + + for (auto const& [v, def] : t->m_subst->sub()) { + rp->operator()(def, new_def, new_dep); + expr_dependency* dep = t->m_subst->dep(v); + new_dep = m.mk_join(dep, new_dep); + subst->insert(v, new_def, new_dep); + mc->add(v, new_def); + } + + } + return model_converter_ref(mc.get()); } diff --git a/src/ast/simplifiers/model_reconstruction_trail.h b/src/ast/simplifiers/model_reconstruction_trail.h index eeaf786d9..8f1ba4381 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.h +++ b/src/ast/simplifiers/model_reconstruction_trail.h @@ -24,33 +24,62 @@ Author: #pragma once #include "util/scoped_ptr_vector.h" +#include "util/trail.h" +#include "ast/for_each_expr.h" #include "ast/rewriter/expr_replacer.h" #include "ast/simplifiers/dependent_expr.h" #include "ast/converters/model_converter.h" class model_reconstruction_trail { - ast_manager& m; + struct entry { + scoped_ptr m_replace; + scoped_ptr m_subst; + vector m_removed; + bool m_active = true; + + entry(expr_replacer* r, expr_substitution* s, vector const& rem) : + m_replace(r), m_subst(s), m_removed(rem) {} + + bool is_loose() const { return !m_removed.empty(); } + + bool intersects(ast_mark const& free_vars) const { + return std::any_of(m_subst->sub().begin(), m_subst->sub().end(), [&](auto const& kv) { return free_vars.is_marked(kv.m_key); }); + } + - struct model_reconstruction_trail_entry { - scoped_ptr m_replace; - vector m_removed; - model_reconstruction_trail_entry(expr_replacer* r, vector const& rem) : - m_replace(r), m_removed(rem) {} }; - scoped_ptr_vector m_trail; - unsigned_vector m_limit; + ast_manager& m; + trail_stack& m_trail_stack; + scoped_ptr_vector m_trail; + + void add_vars(dependent_expr const& d, ast_mark& free_vars) { + for (expr* t : subterms::all(expr_ref(d.fml(), d.get_manager()))) + free_vars.mark(t, true); + } + + bool intersects(ast_mark const& free_vars, dependent_expr const& d) { + expr_ref term(d.fml(), d.get_manager()); + auto iter = subterms::all(term); + return std::any_of(iter.begin(), iter.end(), [&](expr* t) { return free_vars.is_marked(t); }); + } + + bool intersects(ast_mark const& free_vars, vector const& added) { + return std::any_of(added.begin(), added.end(), [&](dependent_expr const& d) { return intersects(free_vars, d); }); + } public: - model_reconstruction_trail(ast_manager& m) : m(m) {} + model_reconstruction_trail(ast_manager& m, trail_stack& tr): + m(m), m_trail_stack(tr) {} /** * add a new substitution to the stack */ void push(expr_replacer* r, vector const& removed) { - m_trail.push_back(alloc(model_reconstruction_trail_entry, r, removed)); + m_trail.push_back(alloc(entry, r, nullptr, removed)); + m_trail_stack.push(push_back_vector(m_trail)); } /** @@ -63,18 +92,5 @@ public: * retrieve the current model converter corresponding to chaining substitutions from the trail. */ model_converter_ref get_model_converter(); - - /** - * push a context. Portions of the trail added within a context are removed after a context pop. - */ - void push() { - m_limit.push_back(m_trail.size()); - } - - void pop(unsigned n) { - unsigned old_sz = m_limit[m_limit.size() - n]; - m_trail.resize(old_sz); - m_limit.shrink(m_limit.size() - n); - } }; diff --git a/src/ast/simplifiers/solve_eqs.cpp b/src/ast/simplifiers/solve_eqs.cpp index 6b2a27d2d..e4361ad97 100644 --- a/src/ast/simplifiers/solve_eqs.cpp +++ b/src/ast/simplifiers/solve_eqs.cpp @@ -60,7 +60,7 @@ namespace euf { m_id2level.reset(); m_id2level.resize(m_id2var.size(), UINT_MAX); m_subst_ids.reset(); - m_subst = alloc(expr_substitution, m, false, false); + m_subst = alloc(expr_substitution, m, true, false); auto is_explored = [&](unsigned id) { return m_id2level[id] != UINT_MAX; @@ -120,16 +120,15 @@ namespace euf { expr_dependency_ref new_dep(m); expr_ref new_def(m); - proof_ref new_pr(m); for (unsigned id : m_subst_ids) { if (!m.inc()) break; auto const& [v, def, dep] = m_next[id][0]; - rp->operator()(def, new_def, new_pr, new_dep); + rp->operator()(def, new_def, new_dep); m_stats.m_num_steps += rp->get_num_steps() + 1; new_dep = m.mk_join(dep, new_dep); - m_subst->insert(v, new_def, new_pr, new_dep); + m_subst->insert(v, new_def, nullptr, new_dep); // we updated the substitution, but we don't need to reset rp // because all cached values there do not depend on v. } @@ -149,11 +148,10 @@ namespace euf { scoped_ptr rp = mk_default_expr_replacer(m, true); rp->set_substitution(m_subst.get()); expr_ref new_f(m); - proof_ref new_pr(m); expr_dependency_ref new_dep(m); for (unsigned i = m_qhead; i < m_fmls.size() && !m_fmls.inconsistent(); ++i) { auto [f, d] = m_fmls[i](); - rp->operator()(f, new_f, new_pr, new_dep); + rp->operator()(f, new_f, new_dep); if (new_f == f) continue; new_dep = m.mk_join(d, new_dep); diff --git a/src/muz/spacer/spacer_iuc_solver.cpp b/src/muz/spacer/spacer_iuc_solver.cpp index 4f7342590..b8b51c0c6 100644 --- a/src/muz/spacer/spacer_iuc_solver.cpp +++ b/src/muz/spacer/spacer_iuc_solver.cpp @@ -244,12 +244,10 @@ namespace spacer { } void iuc_solver::elim_proxies (expr_ref_vector &v) { - expr_ref f = mk_and (v); scoped_ptr rep = mk_expr_simp_replacer (m); rep->set_substitution (&m_elim_proxies_sub); - (*rep)(f); - v.reset(); - flatten_and(f, v); + (*rep)(v); + flatten_and(v); } void iuc_solver::get_iuc(expr_ref_vector &core) {