init solve_eqs

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

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());
+    }
+
+}

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<dependent_eq> 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<extract_eq> m_extract_plugins;
+        unsigned_vector               m_var2id;
+        ptr_vector<app>               m_id2var;
+        vector<uint_set>              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;
+    };
+}