From e1417597688c8cd5057971316977db4841489b7d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 2 Nov 2022 15:59:08 -0700 Subject: [PATCH] init solve_eqs --- src/ast/simplifiers/CMakeLists.txt | 1 + src/ast/simplifiers/solve_eqs.cpp | 116 +++++++++++++++++++++++++++++ src/ast/simplifiers/solve_eqs.h | 75 +++++++++++++++++++ 3 files changed, 192 insertions(+) create mode 100644 src/ast/simplifiers/solve_eqs.cpp create mode 100644 src/ast/simplifiers/solve_eqs.h diff --git a/src/ast/simplifiers/CMakeLists.txt b/src/ast/simplifiers/CMakeLists.txt index 650410415..d07220fb5 100644 --- a/src/ast/simplifiers/CMakeLists.txt +++ b/src/ast/simplifiers/CMakeLists.txt @@ -2,6 +2,7 @@ z3_add_component(simplifiers SOURCES euf_completion.cpp bv_slice.cpp + solve_eqs.cpp COMPONENT_DEPENDENCIES euf rewriter diff --git a/src/ast/simplifiers/solve_eqs.cpp b/src/ast/simplifiers/solve_eqs.cpp new file mode 100644 index 000000000..77808c142 --- /dev/null +++ b/src/ast/simplifiers/solve_eqs.cpp @@ -0,0 +1,116 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + solve_eqs.cpp + +Abstract: + + simplifier for solving equations + +Author: + + Nikolaj Bjorner (nbjorner) 2022-11-2. + +--*/ + + + +#include "ast/simplifiers/solve_eqs.h" + + +namespace euf { + + + void solve_eqs::init() { + + } + + // initialize graph that maps variable ids to next ids + void solve_eqs::extract_dep_graph(dep_eq_vector& eqs) { + m_var2id.reset(); + m_id2var.reset(); + m_next.reset(); + unsigned sz = 0; + for (auto const& [v, t, d] : eqs) + 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)) + continue; + m_var2id[v->get_id()] = m_id2var.size(); + m_id2var.push_back(v); + } + m_next.resize(m_id2var.size()); + + for (auto const& [v, t, d] : eqs) + m_next[var2id(v)].push_back(t); + } + + void solve_eqs::add_subst(app* v, expr* term) { + + } + + /** + * Build a substitution while assigning levels to terms. + * The substitution is well-formed when variables are replaced with terms whose + * Free variables have higher levels. + */ + void solve_eqs::extract_subst() { + m_var2level.reset(); + m_var2level.resize(m_id2var.size(), UINT_MAX); + auto is_explored = [&](unsigned id) { + return m_var2level[id] != UINT_MAX; + }; + auto is_safe = [&](unsigned lvl, expr* t) { + for (auto* e : subterms::all(expr_ref(t, m))) + if (is_var(e) && m_var2level[var2id(e)] < lvl) + return false; + }; + + unsigned init_level = UINT_MAX; + for (unsigned id = 0; id < m_id2var.size(); ++id) { + if (is_explored(id)) + continue; + // initialize current level to have enough room to assign different levels to all variables. + init_level -= m_id2var.size() + 1; + unsigned curr_level = init_level; + todo.push_back(id); + while (!todo.empty()) { + unsigned j = todo.back(); + todo.pop_back(); + if (is_explored(j)) + continue; + m_var2level[id] = curr_level++; + for (expr* t : m_next[j]) { + if (!is_safe(curr_level, t)) + continue; + add_subst(m_id2var[j], t); + for (auto* e : subterms::all(expr_ref(t, m))) + if (is_var(e) && !is_explored(var2id(e))) + todo.push_back(var2id(e)); + break; + } + } + } + } + + void solve_eqs::extract_subst(dep_eq_vector& eqs, dep_eq_vector& subst) { + + } + + void solve_eqs::apply_subst() { + + } + + void solve_eqs::reduce() { + init(); + dep_eq_vector eqs, subst; + get_eqs(eqs); + extract_subst(eqs, subst); + apply_subst(); + advance_qhead(m_fmls.size()); + } + +} diff --git a/src/ast/simplifiers/solve_eqs.h b/src/ast/simplifiers/solve_eqs.h new file mode 100644 index 000000000..936816bc4 --- /dev/null +++ b/src/ast/simplifiers/solve_eqs.h @@ -0,0 +1,75 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + solve_eqs.h + +Abstract: + + simplifier for solving equations + +Author: + + Nikolaj Bjorner (nbjorner) 2022-11-2. + +--*/ + + +#pragma once + +#include "ast/simplifiers/dependent_expr_state.h" +#include "ast/rewriter/th_rewriter.h" + + +namespace euf { + + struct dependent_eq { + app* var; + expr_ref term; + expr_dependency* dep; + dependent_eq(app* var, expr_ref& term, expr_dependency* d) : var(var), term(term), dep(d) {} + }; + + typedef vector dep_eq_vector; + + class extract_eq { + pulic: + virtual ~extract_eq() {} + virtual void get_eqs(depdendent_expr const& e, dep_eq_vector& eqs) = 0; + }; + + class solve_eqs : public dependent_expr_simplifier { + th_rewriter m_rewriter; + scoped_ptr_vector m_extract_plugins; + unsigned_vector m_var2id; + ptr_vector m_id2var; + vector m_next; + + void init(); + + bool is_var(expr* v) const; + unsigned var2id(expr* v) const { return m_var2id[v->get_id()]; } + + void get_eqs(dep_eq_vector& eqs) { + for (unsigned i = m_qhead; i < m_fmls.size(); ++i) + get_eqs(m_fmls[i](), eqs); + } + + void get_eqs(dependent_expr const& f, dep_eq_vector& eqs) { + for (auto* ex : m_extract_plugins) + ex->get_eqs(f, eqs); + } + + void extract_subst(dep_eq_vector& eqs, dep_eq_vector& subst); + void apply_subst(); + + public: + + solve_eqs(ast_manager& m, dependent_expr_state& fmls) : dependent_expr_simplifier(m, fmls), m_rewriter(m) {} + + void push() override { dependent_expr_simplifier::push(); } + void pop(unsigned n) override { dependent_expr_simplifier::pop(n); } + void reduce() override; + }; +}