From 9e2ec9d0181d35267ec35a559d49f3f1d59fce03 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 25 Jan 2023 13:32:51 -0800
Subject: [PATCH] add stubs for proof production in elim_unconstrained

---
 src/ast/simplifiers/elim_unconstrained.cpp | 30 ++++++++++++++++++++--
 src/ast/simplifiers/elim_unconstrained.h   |  2 ++
 2 files changed, 30 insertions(+), 2 deletions(-)

diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp
index 9c4badd01..41877202a 100644
--- a/src/ast/simplifiers/elim_unconstrained.cpp
+++ b/src/ast/simplifiers/elim_unconstrained.cpp
@@ -36,6 +36,12 @@ Author:
 
     Nikolaj Bjorner (nbjorner) 2022-11-11.
 
+Notes:
+
+proof production is work in progress.
+reconstruct_term should assign proof objects with nodes by applying
+monotonicity or reflexivity rules. 
+
 --*/
 
 
@@ -85,6 +91,14 @@ void elim_unconstrained::eliminate() {
         for (expr* arg : *to_app(t))
             m_args.push_back(reconstruct_term(get_node(arg)));
         bool inverted = m_inverter(t->get_decl(), to_app(t)->get_num_args(), m_args.data() + sz, r);
+        proof_ref pr(m);
+        if (inverted && m_enable_proofs) {
+            expr * s    = m.mk_app(t->get_decl(), to_app(t)->get_num_args(), m_args.data() + sz);
+            expr * eq   = m.mk_eq(s, r);
+            proof * pr1 = m.mk_def_intro(eq);
+            proof * pr  = m.mk_apply_def(s, r, pr1);
+            m_trail.push_back(pr);
+        }
         n.m_refcount = 0;
         m_args.shrink(sz);
         if (!inverted) {
@@ -103,6 +117,7 @@ void elim_unconstrained::eliminate() {
 
         m_root.setx(r->get_id(), e->get_id(), UINT_MAX);
         get_node(e).m_term = r;
+        get_node(e).m_proof = pr;
         get_node(e).m_refcount++;
         IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(e, m) << "\n");
         SASSERT(!m_heap.contains(root(e)));
@@ -147,11 +162,18 @@ void elim_unconstrained::invalidate_parents(expr* e) {
  */
 void elim_unconstrained::init_nodes() {
 
+    m_enable_proofs = false;
+    m_trail.reset();
     m_fmls.freeze_suffix();
 
     expr_ref_vector terms(m);
-    for (unsigned i : indices())
-        terms.push_back(m_fmls[i].fml());
+    for (unsigned i : indices()) {
+        auto [f, p, d] = m_fmls[i]();
+        terms.push_back(f);
+        if (p)
+            m_enable_proofs = true;
+    }
+
     m_trail.append(terms);
     m_heap.reset();
     m_root.reset();
@@ -163,6 +185,9 @@ void elim_unconstrained::init_nodes() {
     // top-level terms have reference count > 0
     for (expr* e : terms)
         inc_ref(e);
+
+    m_inverter.set_produce_proofs(m_enable_proofs);
+        
 }
 
 /**
@@ -253,6 +278,7 @@ void elim_unconstrained::gc(expr* t) {
     }
 }
 
+
 expr_ref elim_unconstrained::reconstruct_term(node& n0) {
     expr* t = n0.m_term;
     if (!n0.m_dirty)
diff --git a/src/ast/simplifiers/elim_unconstrained.h b/src/ast/simplifiers/elim_unconstrained.h
index aae14bdcb..19af099d0 100644
--- a/src/ast/simplifiers/elim_unconstrained.h
+++ b/src/ast/simplifiers/elim_unconstrained.h
@@ -26,6 +26,7 @@ class elim_unconstrained : public dependent_expr_simplifier {
         unsigned         m_refcount = 0;
         expr*            m_term = nullptr;
         expr*            m_orig = nullptr;
+        proof*           m_proof = nullptr;
         bool             m_dirty = false;
         ptr_vector<expr> m_parents;
     };
@@ -49,6 +50,7 @@ class elim_unconstrained : public dependent_expr_simplifier {
     stats                    m_stats;
     unsigned_vector          m_root;
     bool                     m_created_compound = false;
+    bool                     m_enable_proofs = false;
 
     bool is_var_lt(int v1, int v2) const;
     node& get_node(unsigned n) { return m_nodes[n]; }