From e8112a6564fa5891b8459ae477971282e5e7d5f4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 3 Nov 2022 21:35:07 -0700
Subject: [PATCH] add initial stubs for model reconstruction trail

---
 src/ast/simplifiers/CMakeLists.txt            |  1 +
 src/ast/simplifiers/dependent_expr_state.h    |  3 +-
 .../model_reconstruction_trail.cpp            | 43 ++++++++++
 .../simplifiers/model_reconstruction_trail.h  | 80 +++++++++++++++++++
 4 files changed, 126 insertions(+), 1 deletion(-)
 create mode 100644 src/ast/simplifiers/model_reconstruction_trail.cpp
 create mode 100644 src/ast/simplifiers/model_reconstruction_trail.h

diff --git a/src/ast/simplifiers/CMakeLists.txt b/src/ast/simplifiers/CMakeLists.txt
index a260dd3b7..dc7aa6fb6 100644
--- a/src/ast/simplifiers/CMakeLists.txt
+++ b/src/ast/simplifiers/CMakeLists.txt
@@ -3,6 +3,7 @@ z3_add_component(simplifiers
     bv_slice.cpp
     euf_completion.cpp
     extract_eqs.cpp
+    model_reconstruction_trail.cpp
     solve_eqs.cpp
   COMPONENT_DEPENDENCIES
     euf
diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h
index 34517525f..32ad59681 100644
--- a/src/ast/simplifiers/dependent_expr_state.h
+++ b/src/ast/simplifiers/dependent_expr_state.h
@@ -32,8 +32,9 @@ Author:
 #include "util/trail.h"
 #include "util/statistics.h"
 #include "util/params.h"
-#include "ast/simplifiers/dependent_expr.h"
 #include "ast/converters/model_converter.h"
+#include "ast/simplifiers/dependent_expr.h"
+
 
 /**
    abstract interface to state updated by simplifiers.
diff --git a/src/ast/simplifiers/model_reconstruction_trail.cpp b/src/ast/simplifiers/model_reconstruction_trail.cpp
new file mode 100644
index 000000000..f99685854
--- /dev/null
+++ b/src/ast/simplifiers/model_reconstruction_trail.cpp
@@ -0,0 +1,43 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    model_reconstruction_trail.cpp
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-3.
+    
+--*/
+
+
+#include "ast/simplifiers/model_reconstruction_trail.h"
+#include "ast/converters/generic_model_converter.h"
+
+
+void model_reconstruction_trail::replay(dependent_expr const& d, vector<dependent_expr>& added) {
+    // accumulate a set of dependent exprs, updating m_trail to exclude loose 
+    // substitutions that use variables from the dependent expressions.
+    ast_mark free_vars;
+    auto [f, dep] = d;
+    for (expr* t : subterms::all(expr_ref(f, m))) 
+        free_vars.mark(t);
+    
+    NOT_IMPLEMENTED_YET();
+}
+
+/**
+ * retrieve the current model converter corresponding to chaining substitutions from the trail.
+ */
+model_converter_ref model_reconstruction_trail::get_model_converter() {
+    model_converter_ref mc = alloc(generic_model_converter, m, "dependent-expr-model");
+    // walk the trail from the back.
+    // add substitutions from the back to the generic model converter
+    // after they have been normalized using a global replace that replaces 
+    // substituted variables by their terms.
+    NOT_IMPLEMENTED_YET();
+    return mc;
+
+}
+
diff --git a/src/ast/simplifiers/model_reconstruction_trail.h b/src/ast/simplifiers/model_reconstruction_trail.h
new file mode 100644
index 000000000..eeaf786d9
--- /dev/null
+++ b/src/ast/simplifiers/model_reconstruction_trail.h
@@ -0,0 +1,80 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    model_reconstruction_trail.h
+
+Abstract:
+
+   Model reconstruction trail
+   A model reconstruction trail comprises of a sequence of assignments 
+   together with assertions that were removed in favor of the assignments. 
+   The assignments satisfy the removed assertions but are not (necessarily) 
+   equivalent to the removed assertions. For the case where assignments 
+   are equivalent to removed assertions, we squash the removed assertions 
+   and don't track them.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-3.
+    
+--*/
+
+#pragma once
+
+#include "util/scoped_ptr_vector.h"
+#include "ast/rewriter/expr_replacer.h"
+#include "ast/simplifiers/dependent_expr.h"
+#include "ast/converters/model_converter.h"
+
+class model_reconstruction_trail {
+
+    ast_manager& m;
+
+    struct model_reconstruction_trail_entry {
+        scoped_ptr<expr_replacer> m_replace;
+        vector<dependent_expr>    m_removed;
+        model_reconstruction_trail_entry(expr_replacer* r, vector<dependent_expr> const& rem) :
+            m_replace(r), m_removed(rem) {}
+    };
+
+    scoped_ptr_vector<model_reconstruction_trail_entry> m_trail;
+    unsigned_vector m_limit;
+
+public:
+
+    model_reconstruction_trail(ast_manager& m) : m(m) {}
+
+    /**
+    * add a new substitution to the stack
+    */
+    void push(expr_replacer* r, vector<dependent_expr> const& removed) {
+        m_trail.push_back(alloc(model_reconstruction_trail_entry, r, removed));
+    }
+
+    /**
+    * register a new depedent expression, update the trail 
+    * by removing substitutions that are not equivalence preserving.
+    */
+    void replay(dependent_expr const& d, vector<dependent_expr>& added);
+
+    /**
+    * retrieve the current model converter corresponding to chaining substitutions from the trail.
+    */
+    model_converter_ref get_model_converter();
+
+    /**
+    * push a context. Portions of the trail added within a context are removed after a context pop.
+    */
+    void push() {
+        m_limit.push_back(m_trail.size());
+    }
+
+    void pop(unsigned n) {
+        unsigned old_sz = m_limit[m_limit.size() - n];
+        m_trail.resize(old_sz);
+        m_limit.shrink(m_limit.size() - n);
+    }
+};
+