add demodulator simplifier

refactor demodulator-rewriter a bit to separate reusable features.

scripts/mk_project.py

@@ -39,7 +39,7 @@ def init_project_def():
     add_lib('macros', ['rewriter'], 'ast/macros')
     add_lib('model',  ['macros'])
     add_lib('converters', ['model'], 'ast/converters')
-    add_lib('simplifiers', ['euf', 'normal_forms', 'bit_blaster', 'converters'], 'ast/simplifiers')
+    add_lib('simplifiers', ['euf', 'normal_forms', 'bit_blaster', 'converters', 'substitution'], 'ast/simplifiers')
     add_lib('tactic', ['simplifiers'])
     add_lib('solver', ['params', 'model', 'tactic', 'proofs'])
     add_lib('cmd_context', ['solver', 'rewriter', 'params'])

src/CMakeLists.txt

@@ -52,9 +52,9 @@ add_subdirectory(ast/macros)
 add_subdirectory(model)
 add_subdirectory(ast/euf)
 add_subdirectory(ast/converters)
+add_subdirectory(ast/substitution)
 add_subdirectory(ast/simplifiers)
 add_subdirectory(tactic)
-add_subdirectory(ast/substitution)
 add_subdirectory(smt/params)
 add_subdirectory(parsers/util)
 add_subdirectory(math/grobner)

src/ast/rewriter/th_rewriter.h

@@ -52,6 +52,7 @@ class th_rewriter {
 
     expr_ref mk_app(func_decl* f, unsigned num_args, expr* const* args);
     expr_ref mk_app(func_decl* f, ptr_vector<expr> const& args) { return mk_app(f, args.size(), args.data()); }
+    expr_ref mk_app(func_decl* f, expr_ref_vector const& args) { return mk_app(f, args.size(), args.data()); }
     expr_ref mk_eq(expr* a, expr* b);
 
     bool reduce_quantifier(quantifier * old_q, 

src/ast/simplifiers/CMakeLists.txt

@@ -3,6 +3,7 @@ z3_add_component(simplifiers
     bit_blaster.cpp
     bv_slice.cpp
     card2bv.cpp
+    demodulator_simplifier.cpp
     dependent_expr_state.cpp
     elim_unconstrained.cpp
     eliminate_predicates.cpp
@@ -18,4 +19,5 @@ z3_add_component(simplifiers
     rewriter
     bit_blaster
     normal_forms
+    substitution
 )

src/ast/simplifiers/demodulator_simplifier.cpp

@@ -0,0 +1,199 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    demodulator_simplifier.cpp
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-12-4
+
+--*/
+
+#include "ast/simplifiers/demodulator_simplifier.h"
+
+demodulator_index::~demodulator_index() {
+    reset();
+}
+
+void demodulator_index::reset() {
+    for (auto& [k, v] : m_fwd_index)
+        dealloc(v);
+    for (auto& [k, v] : m_bwd_index)
+        dealloc(v);
+    m_fwd_index.reset();
+    m_bwd_index.reset();
+}
+
+void demodulator_index::add(func_decl* f, unsigned i, obj_map<func_decl, uint_set*>& map) {
+    uint_set* s;
+    if (!map.find(f, s)) {
+        s = alloc(uint_set);
+        map.insert(f, s);
+    }
+    s->insert(i);
+}
+
+void demodulator_index::del(func_decl* f, unsigned i, obj_map<func_decl, uint_set*>& map) {
+    uint_set* s;
+    if (map.find(f, s))
+        s->remove(i);
+}
+
+void demodulator_index::insert_bwd(expr* e, unsigned i) {
+    struct proc {
+        unsigned i;
+        demodulator_index& idx;
+        proc(unsigned i, demodulator_index& idx) :i(i), idx(idx) {}
+        void operator()(app* a) {
+            if (a->get_num_args() > 0 && is_uninterp(a))
+                idx.add(a->get_decl(), i, idx.m_bwd_index);
+        }
+        void operator()(expr* e) {}
+    };
+    proc p(i, *this);
+    for_each_expr(p, e);
+}
+
+void demodulator_index::remove_bwd(expr* e, unsigned i) {
+    struct proc {
+        unsigned i;
+        demodulator_index& idx;
+        proc(unsigned i, demodulator_index& idx) :i(i), idx(idx) {}
+        void operator()(app* a) {
+            if (a->get_num_args() > 0 && is_uninterp(a))
+                idx.del(a->get_decl(), i, idx.m_bwd_index);
+        }
+        void operator()(expr* e) {}
+    };
+    proc p(i, *this);
+    for_each_expr(p, e);
+}
+
+demodulator_simplifier::demodulator_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& st):
+    dependent_expr_simplifier(m, st),
+    m_util(m),
+    m_match_subst(m),
+    m_rewriter(m),
+    m_pinned(m)
+{
+    std::function<bool(func_decl* f, expr_ref_vector const& args, expr_ref& r)> rw = [&](func_decl* f, expr_ref_vector const& args, expr_ref& r) {
+        return rewrite1(f, args, r);
+    };
+    m_rewriter.set_rewrite1(rw);
+}
+
+void demodulator_simplifier::rewrite(unsigned i) {
+    if (m_index.empty())
+        return;
+
+    m_dependencies.reset();
+    expr* f = fml(i);
+    expr_ref r = m_rewriter.rewrite(f);
+    if (r == f)
+        return;
+    expr_dependency_ref d(dep(i), m);
+    for (unsigned j : m_dependencies)
+        d = m.mk_join(d, dep(j));
+    m_fmls.update(i, dependent_expr(m, r, d));
+}
+
+bool demodulator_simplifier::rewrite1(func_decl* f, expr_ref_vector const& args, expr_ref& np) {
+    uint_set* set;
+    if (!m_index.find_fwd(f, set))
+        return false;
+
+    TRACE("demodulator", tout << "trying to rewrite: " << f->get_name() << " args:\n" << m_new_args << "\n";);
+
+    for (unsigned i : *set) {
+
+        auto const& [lhs, rhs] = m_rewrites[i];
+
+        if (lhs->get_num_args() != args.size())
+            continue;
+
+        SASSERT(lhs->get_decl() == f);
+
+        TRACE("demodulator", tout << "Matching with demodulator: " << mk_pp(d, m) << std::endl; );
+
+        if (m_match_subst(lhs, rhs, args.data(), np)) {
+            TRACE("demodulator_bug", tout << "succeeded...\n" << mk_pp(rhs, m) << "\n===>\n" << np << "\n";);
+            m_dependencies.insert(i);
+            return true;
+        }
+    }
+
+    return false;
+}
+
+void demodulator_simplifier::reschedule_processed(func_decl* f) {
+    uint_set* set = nullptr;
+    if (!m_index.find_bwd(f, set))
+        return;
+    uint_set tmp;
+    for (auto i : *set)
+        if (m_processed.contains(i))
+            tmp.insert(i);
+    for (auto i : tmp) {
+        m_processed.remove(i);
+        m_index.remove_fwd(f, i);
+        m_index.remove_bwd(fml(i), i);
+        m_todo.push_back(i);
+    }
+}
+
+void demodulator_simplifier::reschedule_demodulators(func_decl* f, expr* lhs) {
+    uint_set* set;
+    if (!m_index.find_bwd(f, set))
+        return;
+    uint_set all_occurrences(*set);
+    for (unsigned i : all_occurrences) {
+        app_expr_pair p;
+        if (!m_rewrites.find(i, p))
+            continue;        
+        if (!m_match_subst.can_rewrite(fml(i), lhs))
+            continue;
+        func_decl* f = p.first->get_decl();
+        m_index.remove_fwd(f, i);
+        m_index.remove_bwd(fml(i), i);
+        m_todo.push_back(i);
+    }
+}
+
+void demodulator_simplifier::reset() {
+    m_pinned.reset();
+    m_index.reset();
+    m_processed.reset();
+    m_todo.reset();
+    unsigned max_vid = 1;
+    for (unsigned i : indices())
+        max_vid = std::max(max_vid, m_util.max_var_id(fml(i)));
+    m_match_subst.reserve(max_vid);
+}
+
+void demodulator_simplifier::reduce() {
+    reset();
+    for (unsigned i : indices())
+        m_todo.push_back(i);
+
+    app_ref large(m);
+    expr_ref small(m);
+    while (!m_todo.empty()) {
+        unsigned i = m_todo.back();
+        m_todo.pop_back();
+        rewrite(i);
+        if (m_util.is_demodulator(fml(i), large, small)) {
+            func_decl* f = large->get_decl();
+            reschedule_processed(f);
+            reschedule_demodulators(f, large);
+            m_index.insert_fwd(f, i);
+            m_rewrites.insert(i, app_expr_pair(large, small));
+            m_pinned.push_back(large);
+            m_pinned.push_back(small);
+        }
+        else
+            m_processed.insert(i);
+        m_index.insert_bwd(fml(i), i);
+    }
+}

src/ast/simplifiers/demodulator_simplifier.h

@@ -0,0 +1,60 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    demodulator_simplifier.h
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-12-4
+
+--*/
+
+#pragma once
+
+#include "ast/substitution/demodulator_rewriter.h"
+#include "ast/simplifiers/dependent_expr_state.h"
+#include "util/uint_set.h"
+
+class demodulator_index {
+    obj_map<func_decl, uint_set*> m_fwd_index, m_bwd_index; 
+    void add(func_decl* f, unsigned i, obj_map<func_decl, uint_set*>& map);
+    void del(func_decl* f, unsigned i, obj_map<func_decl, uint_set*>& map);
+ public:
+    ~demodulator_index();
+    void reset();
+    void insert_fwd(func_decl* f, unsigned i) { add(f, i, m_fwd_index); }
+    void remove_fwd(func_decl* f, unsigned i) { del(f, i, m_fwd_index); }
+    void insert_bwd(expr* e, unsigned i);
+    void remove_bwd(expr* e, unsigned i);
+    bool find_fwd(func_decl* f, uint_set*& s) { return m_bwd_index.find(f, s); }
+    bool find_bwd(func_decl* f, uint_set*& s) { return m_fwd_index.find(f, s); }
+    bool empty() const { return m_fwd_index.empty(); }
+};
+
+class demodulator_simplifier : public dependent_expr_simplifier {
+    typedef std::pair<app*, expr*> app_expr_pair;
+    demodulator_index         m_index;
+    demodulator_util          m_util;
+    demodulator_match_subst   m_match_subst;
+    demodulator_rewriter_util m_rewriter;
+    u_map<app_expr_pair>      m_rewrites;
+    uint_set                  m_processed, m_dependencies;
+    unsigned_vector           m_todo;
+    expr_ref_vector           m_pinned;
+
+    void rewrite(unsigned i);
+    bool rewrite1(func_decl* f, expr_ref_vector const& args, expr_ref& np);
+    expr* fml(unsigned i) { return m_fmls[i].fml(); }
+    expr_dependency* dep(unsigned i) { return m_fmls[i].dep(); }
+    void reschedule_processed(func_decl* f);
+    void reschedule_demodulators(func_decl* f, expr* lhs);
+    void reset();
+
+ public:
+     demodulator_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& st);
+     void reduce() override;
+
+
+};