From 7b12a5c5a8b2ace6551fe084c0b766bab52e40b7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 3 Nov 2022 04:49:20 -0700 Subject: [PATCH] build fix --- src/ast/expr_substitution.h | 1 + src/ast/simplifiers/extract_eqs.h | 2 +- src/ast/simplifiers/solve_eqs.cpp | 35 ++++++++++++++++++++++++---- src/ast/simplifiers/solve_eqs.h | 13 +++++++++++ src/tactic/core/solve_eqs_tactic.cpp | 10 ++------ 5 files changed, 48 insertions(+), 13 deletions(-) diff --git a/src/ast/expr_substitution.h b/src/ast/expr_substitution.h index bbd1c0e8e..6d4b1b618 100644 --- a/src/ast/expr_substitution.h +++ b/src/ast/expr_substitution.h @@ -45,6 +45,7 @@ public: unsigned size() const { return m_subst.size(); } void insert(expr * s, expr * def, proof * def_pr = nullptr, expr_dependency * def_dep = nullptr); void erase(expr * s); + expr* find(expr* s) { proof* pr; expr* def; VERIFY(find(s, def, pr)); SASSERT(def); return def; } 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/simplifiers/extract_eqs.h b/src/ast/simplifiers/extract_eqs.h index e6c81bb20..29c136028 100644 --- a/src/ast/simplifiers/extract_eqs.h +++ b/src/ast/simplifiers/extract_eqs.h @@ -30,7 +30,7 @@ namespace euf { app* var; expr_ref term; expr_dependency* dep; - dependent_eq(app* var, expr_ref& term, expr_dependency* d) : var(var), term(term), dep(d) {} + dependent_eq(app* var, expr_ref const& term, expr_dependency* d) : var(var), term(term), dep(d) {} }; typedef vector dep_eq_vector; diff --git a/src/ast/simplifiers/solve_eqs.cpp b/src/ast/simplifiers/solve_eqs.cpp index d9fbf9664..38100fcdc 100644 --- a/src/ast/simplifiers/solve_eqs.cpp +++ b/src/ast/simplifiers/solve_eqs.cpp @@ -20,7 +20,7 @@ Author: #include "ast/ast_util.h" #include "ast/for_each_expr.h" #include "ast/ast_pp.h" -#include "ast/arith_decl_plugin.h" +#include "ast/recfun_decl_plugin.h" #include "ast/rewriter/expr_replacer.h" #include "ast/simplifiers/solve_eqs.h" @@ -37,7 +37,7 @@ namespace euf { sz = std::max(sz, v->get_id()); m_var2id.resize(sz + 1, UINT_MAX); for (auto const& [v, t, d] : eqs) { - if (is_var(v)) + if (is_var(v) || !can_be_var(v)) continue; m_var2id[v->get_id()] = m_id2var.size(); m_id2var.push_back(v); @@ -103,7 +103,9 @@ namespace euf { } void solve_eqs::add_subst(dependent_eq const& eq) { + SASSERT(can_be_var(eq.var)); m_subst->insert(eq.var, eq.term, nullptr, eq.dep); + ++m_stats.m_num_elim_vars; } void solve_eqs::normalize() { @@ -118,10 +120,11 @@ namespace euf { proof_ref new_pr(m); for (unsigned id : m_subst_ids) { - // checkpoint(); + if (!m.inc()) + break; auto const& [v, def, dep] = m_next[id][0]; rp->operator()(def, new_def, new_pr, new_dep); - // m_num_steps += rp->get_num_steps() + 1; + 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); // we updated the substitution, but we don't need to reset rp @@ -141,6 +144,8 @@ namespace euf { } void solve_eqs::apply_subst() { + if (!m.inc()) + return; scoped_ptr rp = mk_default_expr_replacer(m, true); rp->set_substitution(m_subst.get()); expr_ref new_f(m); @@ -170,6 +175,23 @@ namespace euf { advance_qhead(m_fmls.size()); } + void solve_eqs::filter_unsafe_vars() { + m_unsafe_vars.reset(); + recfun::util rec(m); + for (func_decl* f : rec.get_rec_funs()) + for (expr* term : subterms::all(expr_ref(rec.get_def(f).get_rhs(), m))) + m_unsafe_vars.mark(term); + } + +#if 0 + model_converter_ref solve_eqs::get_model_converter() { + model_converter_ref mc = alloc(gmc, m, "solve-eqs"); + for (unsigned id : m_subst_ids) + static_cast(mc.get())->add(id2var(id), m_subst->find(v)); + return mc; + } +#endif + solve_eqs::solve_eqs(ast_manager& m, dependent_expr_state& fmls) : dependent_expr_simplifier(m, fmls), m_rewriter(m) { register_extract_eqs(m, m_extract_plugins); @@ -186,4 +208,9 @@ namespace euf { #endif } + void solve_eqs::collect_statistics(statistics& st) const { + st.update("solve-eqs-steps", m_stats.m_num_steps); + st.update("solve-eqs-elim-vars", m_stats.m_num_elim_vars); + } + } diff --git a/src/ast/simplifiers/solve_eqs.h b/src/ast/simplifiers/solve_eqs.h index 942498a52..62f24413a 100644 --- a/src/ast/simplifiers/solve_eqs.h +++ b/src/ast/simplifiers/solve_eqs.h @@ -26,6 +26,11 @@ Author: namespace euf { class solve_eqs : public dependent_expr_simplifier { + struct stats { + unsigned m_num_steps = 0; + unsigned m_num_elim_vars = 0; + }; + th_rewriter m_rewriter; scoped_ptr_vector m_extract_plugins; unsigned_vector m_var2id, m_id2level, m_subst_ids; @@ -33,6 +38,9 @@ namespace euf { vector m_next; scoped_ptr m_subst; + expr_mark m_unsafe_vars; // expressions that cannot be replaced + stats m_stats; + void add_subst(dependent_eq const& eq); bool is_var(expr* e) const { return e->get_id() < m_var2id.size() && m_var2id[e->get_id()] != UINT_MAX; } @@ -48,6 +56,8 @@ namespace euf { ex->get_eqs(f, eqs); } + void filter_unsafe_vars(); + bool can_be_var(expr* e) const { return is_uninterp_const(e) && !m_unsafe_vars.is_marked(e); } void extract_subst(); void extract_dep_graph(dep_eq_vector& eqs); void normalize(); @@ -62,5 +72,8 @@ namespace euf { void reduce() override; void updt_params(params_ref const& p) override; + void collect_statistics(statistics& st) const override; + + // model_converter_ref get_model_converter(); }; } diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index 5a076aa0f..0a0525e70 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -977,14 +977,8 @@ class solve_eqs_tactic : public tactic { if (m_produce_models) { if (!mc.get()) mc = alloc(gmc, m(), "solve-eqs"); - for (app* v : m_ordered_vars) { - expr * def = nullptr; - proof * pr; - expr_dependency * dep = nullptr; - m_norm_subst->find(v, def, pr, dep); - SASSERT(def); - static_cast(mc.get())->add(v, def); - } + for (app* v : m_ordered_vars) + static_cast(mc.get())->add(v, m_norm_subst->find(v)); } }