From 80033e874499d18f9b650235dbd4e75c568aa447 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 6 Dec 2022 17:02:04 -0800
Subject: [PATCH] cave in to supporting proofs (partially) in simplifiers,
 updated doc

---
 doc/mk_tactic_doc.py                          |  6 ++--
 src/ast/simplifiers/bit2int.h                 |  4 ++-
 src/ast/simplifiers/bit_blaster.cpp           |  4 +--
 src/ast/simplifiers/bv_elim.h                 |  2 +-
 src/ast/simplifiers/bv_slice.cpp              |  6 ++--
 src/ast/simplifiers/card2bv.cpp               |  6 ++--
 src/ast/simplifiers/cnf_nnf.h                 |  5 ++--
 .../simplifiers/demodulator_simplifier.cpp    |  2 +-
 src/ast/simplifiers/dependent_expr.h          | 24 ++++++++++++++--
 src/ast/simplifiers/dependent_expr_state.h    |  3 ++
 src/ast/simplifiers/distribute_forall.h       |  2 +-
 src/ast/simplifiers/elim_bounds.h             |  2 +-
 src/ast/simplifiers/elim_term_ite.h           |  8 ++++--
 src/ast/simplifiers/elim_unconstrained.cpp    |  4 +--
 src/ast/simplifiers/eliminate_predicates.cpp  | 10 +++----
 src/ast/simplifiers/euf_completion.cpp        |  8 +++---
 src/ast/simplifiers/extract_eqs.cpp           |  4 +--
 src/ast/simplifiers/flatten_clauses.h         | 20 ++++++-------
 src/ast/simplifiers/max_bv_sharing.cpp        |  5 ++--
 .../model_reconstruction_trail.cpp            | 11 ++++----
 src/ast/simplifiers/propagate_values.cpp      |  6 ++--
 src/ast/simplifiers/pull_nested_quantifiers.h |  4 ++-
 src/ast/simplifiers/push_ite.h                |  5 ++--
 src/ast/simplifiers/refine_inj_axiom.h        |  2 +-
 src/ast/simplifiers/rewriter_simplifier.h     |  3 +-
 src/ast/simplifiers/solve_context_eqs.cpp     |  2 +-
 src/ast/simplifiers/solve_eqs.cpp             |  7 +++--
 src/qe/lite/qe_lite.cpp                       |  5 ++--
 src/sat/sat_solver/sat_smt_solver.cpp         |  8 +++---
 src/shell/main.cpp                            |  7 +++--
 src/shell/smtlib_frontend.cpp                 |  7 +++--
 src/shell/smtlib_frontend.h                   |  2 +-
 src/tactic/core/injectivity_tactic.cpp        | 15 +---------
 src/tactic/core/injectivity_tactic.h          | 28 ++++++++++++++++++-
 src/tactic/core/reduce_args_tactic.h          | 14 +++++-----
 src/tactic/dependent_expr_state_tactic.h      | 14 +++++-----
 36 files changed, 157 insertions(+), 108 deletions(-)

diff --git a/doc/mk_tactic_doc.py b/doc/mk_tactic_doc.py
index b49811fb9ea..85dfcb4c35d 100644
--- a/doc/mk_tactic_doc.py
+++ b/doc/mk_tactic_doc.py
@@ -21,16 +21,14 @@ def doc_path(path):
 
 def extract_params(ous, tac):
     z3_exe = BUILD_DIR + "/z3"
-    out = subprocess.Popen([z3_exe, f"-tactics:{tac}"], stdout=subprocess.PIPE).communicate()[0]
+    out = subprocess.Popen([z3_exe, f"-tacticsmd:{tac}"], stdout=subprocess.PIPE).communicate()[0]
     if not out:
         return
     out = out.decode(sys.stdout.encoding)
-    ous.write("#### Parameters\n")
-    ous.write("```\n")
+    ous.write("### Parameters\n\n")
     for line in out:
         ous.write(line.replace("\r",""))
     ous.write("\n")
-    ous.write("```\n")
     
 def generate_tactic_doc(ous, f, ins):
     tac_name = None
diff --git a/src/ast/simplifiers/bit2int.h b/src/ast/simplifiers/bit2int.h
index 6605c2e7ef4..64c7f3ecf6d 100644
--- a/src/ast/simplifiers/bit2int.h
+++ b/src/ast/simplifiers/bit2int.h
@@ -35,8 +35,10 @@ class bit2int_simplifier : public dependent_expr_simplifier {
         for (unsigned idx : indices()) {
             auto const& d = m_fmls[idx];
             m_rewriter(d.fml(), r, pr);
-            m_fmls.update(idx, dependent_expr(m, r, d.dep()));
+            m_fmls.update(idx, dependent_expr(m, r, mp(d.pr(), pr), d.dep()));
         }
     }
+
+    bool supports_proofs() const override { return true; }
 };
 
diff --git a/src/ast/simplifiers/bit_blaster.cpp b/src/ast/simplifiers/bit_blaster.cpp
index a1988a9306e..c66cef826da 100644
--- a/src/ast/simplifiers/bit_blaster.cpp
+++ b/src/ast/simplifiers/bit_blaster.cpp
@@ -38,13 +38,13 @@ void bit_blaster::reduce() {
     proof_ref  new_pr(m);
     bool change = false;
     for (unsigned idx : indices()) {
-        auto [curr, d] = m_fmls[idx]();
+        auto [curr, p, d] = m_fmls[idx]();
         m_rewriter(curr, new_curr, new_pr);        
         if (curr != new_curr) {
             m_num_steps += m_rewriter.get_num_steps();
             change = true;                    
             TRACE("bit_blaster", tout << mk_pp(curr, m) << " -> " << new_curr << "\n";);
-            m_fmls.update(idx, dependent_expr(m, new_curr, d));
+            m_fmls.update(idx, dependent_expr(m, new_curr, mp(p, new_pr), d));
         }
     }
     
diff --git a/src/ast/simplifiers/bv_elim.h b/src/ast/simplifiers/bv_elim.h
index 6f045fc5420..344a9df82e7 100644
--- a/src/ast/simplifiers/bv_elim.h
+++ b/src/ast/simplifiers/bv_elim.h
@@ -36,7 +36,7 @@ class elim_simplifier : public dependent_expr_simplifier {
             if (!has_quantifiers(d.fml()))
                 continue;
             m_rewriter(d.fml(), r);
-            m_fmls.update(idx, dependent_expr(m, r, d.dep()));
+            m_fmls.update(idx, dependent_expr(m, r, nullptr, d.dep()));
         }
     }
 };
diff --git a/src/ast/simplifiers/bv_slice.cpp b/src/ast/simplifiers/bv_slice.cpp
index 7ffa56a29f9..45db268b3e7 100644
--- a/src/ast/simplifiers/bv_slice.cpp
+++ b/src/ast/simplifiers/bv_slice.cpp
@@ -28,7 +28,7 @@ namespace bv {
 
     void slice::process_eqs() {
         for (unsigned i : indices()) {
-            auto const [f, d] = m_fmls[i]();
+            auto const [f, p, d] = m_fmls[i]();
             process_eq(f);
         }  
     }
@@ -137,7 +137,7 @@ namespace bv {
         ptr_vector<expr> todo, args;
         expr* c;
         for (unsigned i : indices()) {
-            auto const [f, d] = m_fmls[i]();
+            auto const [f, p, d] = m_fmls[i]();
             todo.push_back(f);
             pin.push_back(f);
             while (!todo.empty()) {
@@ -191,7 +191,7 @@ namespace bv {
             }
             c = cache.get(f->get_id());
             if (c != f)                 
-                m_fmls.update(i, dependent_expr(m, c, d));            
+                m_fmls.update(i, dependent_expr(m, c, nullptr, d));            
         }
     }
 
diff --git a/src/ast/simplifiers/card2bv.cpp b/src/ast/simplifiers/card2bv.cpp
index 58774e1c6bc..b2fece21e3f 100644
--- a/src/ast/simplifiers/card2bv.cpp
+++ b/src/ast/simplifiers/card2bv.cpp
@@ -30,12 +30,12 @@ void card2bv::reduce() {
     expr_ref new_f1(m), new_f2(m);
     proof_ref new_pr(m);
     for (unsigned idx : indices()) {
-        auto [f, d] = m_fmls[idx]();
+        auto [f, p, d] = m_fmls[idx]();
         rw1(f, new_f1);        
         rw2(false, new_f1, new_f2, new_pr);        
         if (new_f2 != f) {
             TRACE("card2bv", tout << "Rewriting " << new_f1 << "\n" << new_f2 << "\n");
-            m_fmls.update(idx, dependent_expr(m, new_f2, d));
+            m_fmls.update(idx, dependent_expr(m, new_f2, mp(p, new_pr), d));
             ++m_stats.m_num_rewrites;
         }
     }
@@ -43,7 +43,7 @@ void card2bv::reduce() {
     expr_ref_vector fmls(m);
     rw2.flush_side_constraints(fmls);
     for (expr* e : fmls)
-        m_fmls.add(dependent_expr(m, e, nullptr));
+        m_fmls.add(dependent_expr(m, e, nullptr, nullptr));
 
     func_decl_ref_vector const& fns = rw2.fresh_constants();
     for (func_decl* f : fns)
diff --git a/src/ast/simplifiers/cnf_nnf.h b/src/ast/simplifiers/cnf_nnf.h
index 56cdc1367e1..6cb1c346e78 100644
--- a/src/ast/simplifiers/cnf_nnf.h
+++ b/src/ast/simplifiers/cnf_nnf.h
@@ -48,12 +48,13 @@ class cnf_nnf_simplifier : public dependent_expr_simplifier {
             push_todo.reset();
             push_todo_prs.reset();
             apply_nnf(d.fml(), push_todo, push_todo_prs, r, pr);
-            m_fmls.update(i, dependent_expr(m, r, d.dep()));
+            m_fmls.update(i, dependent_expr(m, r, mp(d.pr(), pr), d.dep()));
             for (expr* f : push_todo) {
                 if (!m.inc())
                     break;
                 m_rewriter(f, r, pr);
-                m_fmls.add(dependent_expr(m, r, d.dep()));
+                if (f != r)
+                    m_fmls.add(dependent_expr(m, r, pr, d.dep()));
             }
         }
     }
diff --git a/src/ast/simplifiers/demodulator_simplifier.cpp b/src/ast/simplifiers/demodulator_simplifier.cpp
index afd57b425ef..0e42e34818b 100644
--- a/src/ast/simplifiers/demodulator_simplifier.cpp
+++ b/src/ast/simplifiers/demodulator_simplifier.cpp
@@ -108,7 +108,7 @@ void demodulator_simplifier::rewrite(unsigned i) {
     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));
+    m_fmls.update(i, dependent_expr(m, r, nullptr, d));
 }
 
 bool demodulator_simplifier::rewrite1(func_decl* f, expr_ref_vector const& args, expr_ref& np) {
diff --git a/src/ast/simplifiers/dependent_expr.h b/src/ast/simplifiers/dependent_expr.h
index ddf119070e0..55f8d8f4695 100644
--- a/src/ast/simplifiers/dependent_expr.h
+++ b/src/ast/simplifiers/dependent_expr.h
@@ -24,21 +24,26 @@ Module Name:
 class dependent_expr {
     ast_manager& m;
     expr*            m_fml;
+    proof*           m_proof;
     expr_dependency* m_dep;
 public:
-    dependent_expr(ast_manager& m, expr* fml, expr_dependency* d):
+    dependent_expr(ast_manager& m, expr* fml, proof* p, expr_dependency* d):
         m(m),
         m_fml(fml),
+        m_proof(p),
         m_dep(d) {
         SASSERT(fml);
         m.inc_ref(fml);
         m.inc_ref(d);
+        m.inc_ref(p);
     }
 
     dependent_expr(ast_translation& tr, dependent_expr const& src) :
         m(tr.to()) {
         m_fml = tr(src.fml());
         m.inc_ref(m_fml);
+        m_proof = tr(src.pr());
+        m.inc_ref(m_proof);
         expr_dependency_translation dtr(tr);
         m_dep = dtr(src.dep());
         m.inc_ref(m_dep);
@@ -49,10 +54,13 @@ class dependent_expr {
         if (this != &other) {
             m.inc_ref(other.m_fml);
             m.inc_ref(other.m_dep);
+            m.inc_ref(other.m_proof);
             m.dec_ref(m_fml);
             m.dec_ref(m_dep);
+            m.dec_ref(m_proof);
             m_fml = other.m_fml;
             m_dep = other.m_dep;
+            m_proof = other.m_proof;
         }
         return *this;
     }
@@ -60,24 +68,30 @@ class dependent_expr {
     dependent_expr(dependent_expr const& other):
         m(other.m),
         m_fml(other.m_fml),
+        m_proof(other.m_proof),
         m_dep(other.m_dep) {
         m.inc_ref(m_fml);
+        m.inc_ref(m_proof);
         m.inc_ref(m_dep);
     }
 
     dependent_expr(dependent_expr && other) noexcept :
         m(other.m),
         m_fml(nullptr),
+        m_proof(nullptr),
         m_dep(nullptr) {
         std::swap(m_fml, other.m_fml);
+        std::swap(m_proof, other.m_proof);
         std::swap(m_dep, other.m_dep);
     }
 
     ~dependent_expr() {
         m.dec_ref(m_fml);
         m.dec_ref(m_dep);
+        m.dec_ref(m_proof);
         m_fml = nullptr;
         m_dep = nullptr;
+        m_proof = nullptr;
     }
 
     ast_manager& get_manager() const { return m; }
@@ -85,9 +99,11 @@ class dependent_expr {
     expr* fml() const { return m_fml; }
 
     expr_dependency* dep() const { return m_dep; }
+
+    proof* pr() const { return m_proof; }
     
-    std::tuple<expr*, expr_dependency*> operator()() const { 
-        return { m_fml, m_dep }; 
+    std::tuple<expr*, proof*, expr_dependency*> operator()() const { 
+        return { m_fml, m_proof, m_dep }; 
     }
 
     std::ostream& display(std::ostream& out) const {
@@ -99,6 +115,8 @@ class dependent_expr {
             for (expr* arg : deps)
                 out << mk_pp(arg, m) << " ";
         }
+        if (m_proof)
+            out << "\n:- " << mk_pp(m_proof, m);
         return out;
     }
 };
diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h
index 212bc99a4a3..85b6352ad25 100644
--- a/src/ast/simplifiers/dependent_expr_state.h
+++ b/src/ast/simplifiers/dependent_expr_state.h
@@ -135,6 +135,8 @@ class dependent_expr_simplifier {
 
     index_set indices() { return index_set(*this); }
 
+    proof* mp(proof* a, proof* b) { return (a && b) ? m.mk_modus_ponens(a, b) : nullptr;  }
+
 public:
     dependent_expr_simplifier(ast_manager& m, dependent_expr_state& s) : m(m), m_fmls(s), m_trail(s.m_trail) {}
     virtual ~dependent_expr_simplifier() {}
@@ -146,6 +148,7 @@ class dependent_expr_simplifier {
     virtual void reset_statistics() {}
     virtual void updt_params(params_ref const& p) {}
     virtual void collect_param_descrs(param_descrs& r) {}
+    virtual bool supports_proofs() const { return false; }
     ast_manager& get_manager() { return m; }
     dependent_expr_state& get_fmls() { return m_fmls; }
 };
diff --git a/src/ast/simplifiers/distribute_forall.h b/src/ast/simplifiers/distribute_forall.h
index 82709d29f72..3127a4ec87a 100644
--- a/src/ast/simplifiers/distribute_forall.h
+++ b/src/ast/simplifiers/distribute_forall.h
@@ -38,7 +38,7 @@ class distribute_forall_simplifier : public dependent_expr_simplifier {
             if (!has_quantifiers(d.fml()))
                 continue;
             m_dist(d.fml(), r);
-            m_fmls.update(idx, dependent_expr(m, r, d.dep()));
+            m_fmls.update(idx, dependent_expr(m, r, nullptr, d.dep()));
         }
     }
 };
diff --git a/src/ast/simplifiers/elim_bounds.h b/src/ast/simplifiers/elim_bounds.h
index d6631adfdd4..ed93faeba26 100644
--- a/src/ast/simplifiers/elim_bounds.h
+++ b/src/ast/simplifiers/elim_bounds.h
@@ -38,7 +38,7 @@ class elim_bounds_simplifier : public dependent_expr_simplifier {
             if (!has_quantifiers(d.fml()))
                 continue;
             m_rewriter(d.fml(), r);
-            m_fmls.update(idx, dependent_expr(m, r, d.dep()));
+            m_fmls.update(idx, dependent_expr(m, r, nullptr, d.dep()));
         }
     }
 };
diff --git a/src/ast/simplifiers/elim_term_ite.h b/src/ast/simplifiers/elim_term_ite.h
index 5b6ef38fa49..1b8f58f9e5d 100644
--- a/src/ast/simplifiers/elim_term_ite.h
+++ b/src/ast/simplifiers/elim_term_ite.h
@@ -33,13 +33,17 @@ class elim_term_ite_simplifier : public dependent_expr_simplifier {
         
     void reduce() override {
         expr_ref r(m);
+        proof_ref pr(m);
         for (unsigned idx : indices()) {
             auto const& d = m_fmls[idx];
-            m_rewriter(d.fml(), r);
-            m_fmls.update(idx, dependent_expr(m, r, d.dep()));
+            m_rewriter(d.fml(), r, pr);
+            if (d.fml() != r)
+                m_fmls.update(idx, dependent_expr(m, r, mp(d.pr(), pr), d.dep()));
         }
     }
 
+    bool supports_proofs() const override { return true; }
+
     void push() override { dependent_expr_simplifier::push(); m_df.push(); m_rewriter.push(); }
     
     void pop(unsigned n) override { m_rewriter.pop(n); m_df.pop(n); dependent_expr_simplifier::pop(n); }
diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp
index 7404382a38c..032c46a92f3 100644
--- a/src/ast/simplifiers/elim_unconstrained.cpp
+++ b/src/ast/simplifiers/elim_unconstrained.cpp
@@ -258,13 +258,13 @@ void elim_unconstrained::reconstruct_terms() {
 void elim_unconstrained::assert_normalized(vector<dependent_expr>& old_fmls) {
 
     for (unsigned i : indices()) {
-        auto [f, d] = m_fmls[i]();
+        auto [f, p, d] = m_fmls[i]();
         node& n = get_node(f);
         expr* g = n.m_term;
         if (f == g)
             continue;
         old_fmls.push_back(m_fmls[i]);
-        m_fmls.update(i, dependent_expr(m, g, d));
+        m_fmls.update(i, dependent_expr(m, g, nullptr, d));
         IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(f, m, 3) << " -> " << mk_bounded_pp(g, m, 3) << "\n");
         TRACE("elim_unconstrained", tout << mk_bounded_pp(f, m) << " -> " << mk_bounded_pp(g, m) << "\n");
     }
diff --git a/src/ast/simplifiers/eliminate_predicates.cpp b/src/ast/simplifiers/eliminate_predicates.cpp
index 700f96ce3b7..118edf04d24 100644
--- a/src/ast/simplifiers/eliminate_predicates.cpp
+++ b/src/ast/simplifiers/eliminate_predicates.cpp
@@ -536,7 +536,7 @@ void eliminate_predicates::reduce_definitions() {
         macro_expander.insert(v->m_head, v->m_def, v->m_dep);
     
     for (unsigned i : indices()) {
-        auto [f, d] = m_fmls[i]();
+        auto [f, p, d] = m_fmls[i]();
         expr_ref fml(f, m), new_fml(m);
         expr_dependency_ref dep(d, m);
         while (true) {
@@ -546,7 +546,7 @@ void eliminate_predicates::reduce_definitions() {
             rewrite(new_fml);
             fml = new_fml;
         }
-        m_fmls.update(i, dependent_expr(m, fml, dep));
+        m_fmls.update(i, dependent_expr(m, fml, nullptr, dep));
     }
     reset();
     init_clauses();
@@ -770,7 +770,7 @@ void eliminate_predicates::process_to_exclude(ast_mark& exclude_set) {
 
 
 eliminate_predicates::clause* eliminate_predicates::init_clause(unsigned i) {
-    auto [f, d] = m_fmls[i]();
+    auto [f, p, d] = m_fmls[i]();
     return init_clause(f, d, i);
 }
 
@@ -821,12 +821,12 @@ void eliminate_predicates::decompile() {
         if (cl->m_fml_index != UINT_MAX) {
             if (cl->m_alive)
                 continue;
-            dependent_expr de(m, m.mk_true(), nullptr);
+            dependent_expr de(m, m.mk_true(), nullptr, nullptr);
             m_fmls.update(cl->m_fml_index, de);
         }
         else if (cl->m_alive) {
             expr_ref new_cl = cl->m_fml;
-            dependent_expr de(m, new_cl, cl->m_dep);
+            dependent_expr de(m, new_cl, nullptr, cl->m_dep);
             m_fmls.add(de);
         }        
     }
diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp
index 78be41c1adc..3ede7024ee3 100644
--- a/src/ast/simplifiers/euf_completion.cpp
+++ b/src/ast/simplifiers/euf_completion.cpp
@@ -82,7 +82,7 @@ namespace euf {
 
         for (unsigned i = qhead(); i < sz; ++i) {
             expr* x, * y;
-            auto [f, d] = m_fmls[i]();
+            auto [f, p, d] = m_fmls[i]();
             if (m.is_eq(f, x, y)) {
                 enode* a = mk_enode(x);
                 enode* b = mk_enode(y);
@@ -108,19 +108,19 @@ namespace euf {
 
         if (m_egraph.inconsistent()) {
             auto* d = explain_conflict();
-            dependent_expr de(m, m.mk_false(), d);
+            dependent_expr de(m, m.mk_false(), nullptr, d);
             m_fmls.update(0, de);
             return;
         }
 
         unsigned sz = qtail();
         for (unsigned i = qhead(); i < sz; ++i) {
-            auto [f, d] = m_fmls[i]();
+            auto [f, p, d] = m_fmls[i]();
             
             expr_dependency_ref dep(d, m);
             expr_ref g = canonize_fml(f, dep);
             if (g != f) {
-                m_fmls.update(i, dependent_expr(m, g, dep));
+                m_fmls.update(i, dependent_expr(m, g, nullptr, dep));
                 m_stats.m_num_rewrites++;
                 IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(f, m, 3) << " -> " << mk_bounded_pp(g, m, 3) << "\n");
                 update_has_new_eq(g);
diff --git a/src/ast/simplifiers/extract_eqs.cpp b/src/ast/simplifiers/extract_eqs.cpp
index fdb889ee3ac..b2e264b1fb4 100644
--- a/src/ast/simplifiers/extract_eqs.cpp
+++ b/src/ast/simplifiers/extract_eqs.cpp
@@ -39,7 +39,7 @@ namespace euf {
         }
 
         void get_eqs(dependent_expr const& e, dep_eq_vector& eqs) override {
-            auto [f, d] = e();
+            auto [f, p, d] = e();
             expr* x, * y;
             if (m.is_eq(f, x, y)) {
                 if (x == y)
@@ -246,7 +246,7 @@ namespace euf {
         void get_eqs(dependent_expr const& e, dep_eq_vector& eqs) override {
             if (!m_enabled)
                 return;
-            auto [f, d] = e();
+            auto [f, p, d] = e();
             expr* x, * y;
             if (m.is_eq(f, x, y) && a.is_int_real(x)) {
                 solve_eq(f, x, y, d, eqs);
diff --git a/src/ast/simplifiers/flatten_clauses.h b/src/ast/simplifiers/flatten_clauses.h
index aa81024effb..e2da2d182aa 100644
--- a/src/ast/simplifiers/flatten_clauses.h
+++ b/src/ast/simplifiers/flatten_clauses.h
@@ -67,8 +67,8 @@ class flatten_clauses : public dependent_expr_simplifier {
                     decomposed = true;
                 if (decomposed) {
                     for (expr* arg : *to_app(b)) 
-                        m_fmls.add(dependent_expr(m, m.mk_or(a, mk_not(m, arg)), de.dep()));
-                    m_fmls.update(idx, dependent_expr(m, m.mk_true(), nullptr));
+                        m_fmls.add(dependent_expr(m, nullptr, m.mk_or(a, mk_not(m, arg)), de.dep()));
+                    m_fmls.update(idx, dependent_expr(m, nullptr, m.mk_true(), nullptr));
                     ++m_num_flat;
                     continue;
                 }
@@ -79,8 +79,8 @@ class flatten_clauses : public dependent_expr_simplifier {
                     decomposed = true;
                 if (decomposed) {
                     for (expr * arg : *to_app(b))
-                        m_fmls.add(dependent_expr(m, m.mk_or(a, arg), de.dep()));
-                    m_fmls.update(idx, dependent_expr(m, m.mk_true(), nullptr));
+                        m_fmls.add(dependent_expr(m, nullptr, m.mk_or(a, arg), de.dep()));
+                    m_fmls.update(idx, dependent_expr(m, nullptr, m.mk_true(), nullptr));
                     ++m_num_flat;
                     continue;
                 }
@@ -92,20 +92,20 @@ class flatten_clauses : public dependent_expr_simplifier {
                 if (decomposed) {
                     expr* na = mk_not(m, a);
                     for (expr* arg : *to_app(b))
-                        m_fmls.add(dependent_expr(m, m.mk_or(na, arg), de.dep()));
-                    m_fmls.update(idx, dependent_expr(m, m.mk_true(), nullptr));
+                        m_fmls.add(dependent_expr(m, m.mk_or(na, arg), nullptr, de.dep()));
+                    m_fmls.update(idx, dependent_expr(m, m.mk_true(), nullptr, nullptr));
                     ++m_num_flat;
                     continue;
                 }
                 if (m.is_implies(f, a, b)) {
-                    m_fmls.update(idx, dependent_expr(m, m.mk_or(mk_not(m, a), b), de.dep()));
+                    m_fmls.update(idx, dependent_expr(m, m.mk_or(mk_not(m, a), b), nullptr, de.dep()));
                     ++m_num_flat;
                     continue;
                 }
                 if (m.is_ite(f, a, b, c)) {
-                    m_fmls.add(dependent_expr(m, m.mk_or(mk_not(m, a), b), de.dep()));
-                    m_fmls.add(dependent_expr(m, m.mk_or(a, c), de.dep()));
-                    m_fmls.update(idx, dependent_expr(m, m.mk_true(), nullptr));
+                    m_fmls.add(dependent_expr(m, m.mk_or(mk_not(m, a), b), nullptr, de.dep()));
+                    m_fmls.add(dependent_expr(m, m.mk_or(a, c), nullptr, de.dep()));
+                    m_fmls.update(idx, dependent_expr(m, m.mk_true(), nullptr, nullptr));
                     ++m_num_flat;
                     continue;
                 }
diff --git a/src/ast/simplifiers/max_bv_sharing.cpp b/src/ast/simplifiers/max_bv_sharing.cpp
index c12fa4410d4..f708f9dce75 100644
--- a/src/ast/simplifiers/max_bv_sharing.cpp
+++ b/src/ast/simplifiers/max_bv_sharing.cpp
@@ -48,12 +48,11 @@ class max_bv_sharing : public dependent_expr_simplifier {
         expr_ref   new_curr(m);
         proof_ref  new_pr(m);
         for (unsigned idx : indices()) {
-            auto [curr, d] = m_fmls[idx]();
+            auto [curr, p, d] = m_fmls[idx]();
             m_rewriter(curr, new_curr, new_pr);
-            // Proof reconstruction: new_pr = m.mk_modus_ponens(old_pr, new_pr);
             if (new_curr != curr) {
                 m_num_steps += m_rewriter.get_num_steps();
-                m_fmls.update(idx, dependent_expr(m, new_curr, d));
+                m_fmls.update(idx, dependent_expr(m, new_curr, mp(p, new_pr), d));
             }
         }
     }
diff --git a/src/ast/simplifiers/model_reconstruction_trail.cpp b/src/ast/simplifiers/model_reconstruction_trail.cpp
index 7e8d3e2f1c3..567546e67b1 100644
--- a/src/ast/simplifiers/model_reconstruction_trail.cpp
+++ b/src/ast/simplifiers/model_reconstruction_trail.cpp
@@ -61,16 +61,17 @@ void model_reconstruction_trail::replay(unsigned qhead, dependent_expr_state& st
                 args.push_back(m.mk_var(i, d->get_domain(i)));
             head = m.mk_app(d, args);
             mrp.insert(head, t->m_def, t->m_dep);
-            dependent_expr de(m, t->m_def, t->m_dep);
+            dependent_expr de(m, t->m_def, nullptr, t->m_dep);
             add_vars(de, free_vars);
 
             for (unsigned i = qhead; i < st.qtail(); ++i) {
-                auto [f, dep1] = st[i]();
+                auto [f, p, dep1] = st[i]();
                 expr_ref g(m);
                 expr_dependency_ref dep2(m);
                 mrp(f, dep1, g, dep2);
                 CTRACE("simplifier", f != g, tout << "updated " << mk_pp(g, m) << "\n");
-                st.update(i, dependent_expr(m, g, dep2));
+                if (f != g)
+                    st.update(i, dependent_expr(m, g, nullptr, dep2));
             }
             continue;
         }
@@ -81,7 +82,7 @@ void model_reconstruction_trail::replay(unsigned qhead, dependent_expr_state& st
         ptr_vector<expr> dep_exprs;
         expr_ref_vector trail(m);
         for (unsigned i = qhead; i < st.qtail(); ++i) {
-            auto [f, dep1] = st[i]();
+            auto [f, p, dep1] = st[i]();
             auto [g, dep2] = rp->replace_with_dep(f);
             if (dep1) {
                 dep_exprs.reset();
@@ -98,7 +99,7 @@ void model_reconstruction_trail::replay(unsigned qhead, dependent_expr_state& st
                 if (!trail.empty()) 
                     dep1 = m.mk_join(dep_exprs.size(), dep_exprs.data());                
             }
-            dependent_expr d(m, g, m.mk_join(dep1, dep2));
+            dependent_expr d(m, g, nullptr, m.mk_join(dep1, dep2));
             CTRACE("simplifier", f != g, tout << "updated " << mk_pp(g, m) << "\n");
             add_vars(d, free_vars);
             st.update(i, d);
diff --git a/src/ast/simplifiers/propagate_values.cpp b/src/ast/simplifiers/propagate_values.cpp
index 7d698faa310..1083cc36d73 100644
--- a/src/ast/simplifiers/propagate_values.cpp
+++ b/src/ast/simplifiers/propagate_values.cpp
@@ -35,13 +35,13 @@ propagate_values::propagate_values(ast_manager& m, params_ref const& p, dependen
 
 void propagate_values::process_fml(unsigned i) {
     if (!m_subst.empty()) {
-        auto [f, dep] = m_fmls[i]();
+        auto [f, p, dep] = m_fmls[i]();
         expr_ref fml(m);
         proof_ref pr(m);
         m_rewriter(f, fml, pr);
         if (fml != f) {
             dep = m.mk_join(dep, m_rewriter.get_used_dependencies());
-            m_fmls.update(i, dependent_expr(m, fml, dep));
+            m_fmls.update(i, dependent_expr(m, fml, mp(p, pr), dep));
             ++m_stats.m_num_rewrites;
         }
         m_rewriter.reset_used_dependencies();
@@ -51,7 +51,7 @@ void propagate_values::process_fml(unsigned i) {
 
 void propagate_values::add_sub(dependent_expr const& de) {
     expr* x, * y;
-    auto const& [f, dep] = de();
+    auto const& [f, p, dep] = de();
     if (m.is_not(f, x) && m_shared.is_shared(x))
         m_subst.insert(x, m.mk_false(), dep);
     if (m_shared.is_shared(f))
diff --git a/src/ast/simplifiers/pull_nested_quantifiers.h b/src/ast/simplifiers/pull_nested_quantifiers.h
index a113c36c2f4..fac605d4971 100644
--- a/src/ast/simplifiers/pull_nested_quantifiers.h
+++ b/src/ast/simplifiers/pull_nested_quantifiers.h
@@ -40,7 +40,9 @@ class pull_nested_quantifiers_simplifier : public dependent_expr_simplifier {
         for (unsigned idx : indices()) {
             auto d = m_fmls[idx];
             m_pull(d.fml(), new_curr, new_pr);
-            m_fmls.update(idx, dependent_expr(m, new_curr, d.dep()));
+            m_fmls.update(idx, dependent_expr(m, new_curr, mp(d.pr(), new_pr), d.dep()));
         }
     }
+
+    bool supports_proofs() const override { return true; }
 };
diff --git a/src/ast/simplifiers/push_ite.h b/src/ast/simplifiers/push_ite.h
index e26070a7eda..8e508bf5344 100644
--- a/src/ast/simplifiers/push_ite.h
+++ b/src/ast/simplifiers/push_ite.h
@@ -35,7 +35,8 @@ class push_ite_simplifier : public dependent_expr_simplifier {
         for (unsigned idx : indices()) {
             auto const& d = m_fmls[idx];
             m_push(d.fml(), r);
-            m_fmls.update(idx, dependent_expr(m, r, d.dep()));
+            if (r != d.fml())
+                m_fmls.update(idx, dependent_expr(m, r, nullptr, d.dep()));
         }
     }
 };
@@ -58,7 +59,7 @@ class ng_push_ite_simplifier : public dependent_expr_simplifier {
         for (unsigned idx : indices()) {
             auto const& d = m_fmls[idx];
             m_push(d.fml(), r);
-            m_fmls.update(idx, dependent_expr(m, r, d.dep()));
+            m_fmls.update(idx, dependent_expr(m, r, nullptr, d.dep()));
         }
     }
 };
diff --git a/src/ast/simplifiers/refine_inj_axiom.h b/src/ast/simplifiers/refine_inj_axiom.h
index 2333ba690df..53c96081270 100644
--- a/src/ast/simplifiers/refine_inj_axiom.h
+++ b/src/ast/simplifiers/refine_inj_axiom.h
@@ -38,7 +38,7 @@ class refine_inj_axiom_simplifier : public dependent_expr_simplifier {
         for (unsigned idx : indices()) {
             expr* f = m_fmls[idx].fml();
             if (is_quantifier(f) && simplify_inj_axiom(m, to_quantifier(f), r)) 
-                m_fmls.update(idx, dependent_expr(m, r, m_fmls[idx].dep()));            
+                m_fmls.update(idx, dependent_expr(m, r, nullptr, m_fmls[idx].dep()));            
         }
     }
 };
diff --git a/src/ast/simplifiers/rewriter_simplifier.h b/src/ast/simplifiers/rewriter_simplifier.h
index be54ca005e4..f3dc91a51f3 100644
--- a/src/ast/simplifiers/rewriter_simplifier.h
+++ b/src/ast/simplifiers/rewriter_simplifier.h
@@ -44,9 +44,10 @@ class rewriter_simplifier : public dependent_expr_simplifier {
             auto d = m_fmls[idx];
             m_rewriter(d.fml(), new_curr, new_pr);
             m_num_steps += m_rewriter.get_num_steps();
-            m_fmls.update(idx, dependent_expr(m, new_curr, d.dep()));            
+            m_fmls.update(idx, dependent_expr(m, new_curr, mp(d.pr(), new_pr), d.dep()));            
         }
     }
+    bool supports_proofs() const override { return true; }
     void collect_statistics(statistics& st) const override { st.update("simplifier-steps", m_num_steps); }
     void reset_statistics() override { m_num_steps = 0; }
     void updt_params(params_ref const& p) override { m_params.append(p); m_rewriter.updt_params(m_params); }
diff --git a/src/ast/simplifiers/solve_context_eqs.cpp b/src/ast/simplifiers/solve_context_eqs.cpp
index 6cb38e4a686..b56802caf8d 100644
--- a/src/ast/simplifiers/solve_context_eqs.cpp
+++ b/src/ast/simplifiers/solve_context_eqs.cpp
@@ -282,7 +282,7 @@ namespace euf {
             else if (!s && 1 <= depth) {
                 for (extract_eq* ex : m_solve_eqs.m_extract_plugins) {
                     ex->set_allow_booleans(false);
-                    ex->get_eqs(dependent_expr(m, f, df.dep()), eqs);
+                    ex->get_eqs(dependent_expr(m, f, nullptr, df.dep()), eqs);
                     ex->set_allow_booleans(true);
                 }
             }
diff --git a/src/ast/simplifiers/solve_eqs.cpp b/src/ast/simplifiers/solve_eqs.cpp
index 94b089c809f..e481dad8dee 100644
--- a/src/ast/simplifiers/solve_eqs.cpp
+++ b/src/ast/simplifiers/solve_eqs.cpp
@@ -191,14 +191,15 @@ namespace euf {
         rp->set_substitution(m_subst.get());
 
         for (unsigned i : indices()) {
-            auto [f, d] = m_fmls[i]();
+            auto [f, p, d] = m_fmls[i]();
             auto [new_f, new_dep] = rp->replace_with_dep(f);
-            m_rewriter(new_f);
+            proof_ref new_pr(m);
+            m_rewriter(new_f, new_f, new_pr);
             if (new_f == f)
                 continue;
             new_dep = m.mk_join(d, new_dep);
             old_fmls.push_back(m_fmls[i]);
-            m_fmls.update(i, dependent_expr(m, new_f, new_dep));
+            m_fmls.update(i, dependent_expr(m, new_f, mp(p, new_pr), new_dep));
         }
     }
     
diff --git a/src/qe/lite/qe_lite.cpp b/src/qe/lite/qe_lite.cpp
index d3d45bd4b1e..a052ae94435 100644
--- a/src/qe/lite/qe_lite.cpp
+++ b/src/qe/lite/qe_lite.cpp
@@ -2431,12 +2431,13 @@ namespace {
             proof_ref new_pr(m);
             expr_ref new_f(m);
             for (unsigned i : indices()) {
-                expr* f = m_fmls[i].fml();
+                auto [f, p, d] = m_fmls[i]();
                 if (!has_quantifiers(f))
                     continue;
                 new_f = f;
                 m_qe(new_f, new_pr);
-                m_fmls.update(i, dependent_expr(m, new_f, m_fmls[i].dep()));
+                if (f != new_f) 
+                    m_fmls.update(i, dependent_expr(m, new_f, mp(p, new_pr), d));
             }
         }
     };
diff --git a/src/sat/sat_solver/sat_smt_solver.cpp b/src/sat/sat_solver/sat_smt_solver.cpp
index 3fd3a008030..e37d513a02e 100644
--- a/src/sat/sat_solver/sat_smt_solver.cpp
+++ b/src/sat/sat_solver/sat_smt_solver.cpp
@@ -86,7 +86,7 @@ class sat_smt_solver : public solver {
                 if (s.m.is_and(f)) {
                     auto* d = s.m_fmls[i].dep();
                     for (expr* arg : *to_app(f))
-                        s.m_fmls.push_back(dependent_expr(s.m, arg, d));
+                        s.m_fmls.push_back(dependent_expr(s.m, arg, nullptr, d));
                     continue;
                 }
                 if (i != j)
@@ -349,18 +349,18 @@ class sat_smt_solver : public solver {
             return a;
         expr* new_dep = m.mk_fresh_const("dep", m.mk_bool_sort());
         expr* fml = m.mk_iff(new_dep, a);
-        m_fmls.push_back(dependent_expr(m, fml, nullptr));
+        m_fmls.push_back(dependent_expr(m, fml, nullptr, nullptr));
         m_dep.insert(a, new_dep);
         return new_dep;
     }
 
     void assert_expr_core2(expr * t, expr * a) override {
         a = ensure_literal(a);
-        m_fmls.push_back(dependent_expr(m, t, m.mk_leaf(a)));
+        m_fmls.push_back(dependent_expr(m, t, nullptr, m.mk_leaf(a)));
     }
 
     void assert_expr_core(expr * t) override {
-        m_fmls.push_back(dependent_expr(m, t, nullptr));
+        m_fmls.push_back(dependent_expr(m, t, nullptr, nullptr));
     }
 
     ast_manager& get_manager() const override { return m; }
diff --git a/src/shell/main.cpp b/src/shell/main.cpp
index af3b22db06e..2fdd95d79e8 100644
--- a/src/shell/main.cpp
+++ b/src/shell/main.cpp
@@ -293,11 +293,12 @@ static void parse_cmd_line_args(std::string& input_file, int argc, char ** argv)
                 if (!opt_arg)
                     help_tactics();
                 else
-                    help_tactic(opt_arg);
+                    help_tactic(opt_arg, false);
             }
-            else if (strcmp(opt_name, "probes") == 0) {
+            else if (strcmp(opt_name, "tacticsmd") == 0 && opt_arg) 
+                help_tactic(opt_arg, true);
+            else if (strcmp(opt_name, "probes") == 0) 
                 help_probes();
-            }
             else {
                 std::cerr << "Error: invalid command line option: " << arg << "\n";
                 std::cerr << "For usage information: z3 -h\n";
diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp
index 220001b4044..698f0f23962 100644
--- a/src/shell/smtlib_frontend.cpp
+++ b/src/shell/smtlib_frontend.cpp
@@ -88,14 +88,17 @@ void help_tactics() {
         std::cout << "- " << cmd->get_name() << " " << cmd->get_descr() << "\n";
 }
 
-void help_tactic(char const* name) {
+void help_tactic(char const* name, bool markdown) {
     cmd_context ctx;
     for (auto cmd : ctx.tactics()) {
         if (cmd->get_name() == name) {
             tactic_ref t = cmd->mk(ctx.m());
             param_descrs descrs;
             t->collect_param_descrs(descrs);
-            descrs.display(std::cout, 4);
+            if (markdown)
+                descrs.display_markdown(std::cout);
+            else
+                descrs.display(std::cout, 4);
         }
     }
 }
diff --git a/src/shell/smtlib_frontend.h b/src/shell/smtlib_frontend.h
index 04f35c5c847..9769472f263 100644
--- a/src/shell/smtlib_frontend.h
+++ b/src/shell/smtlib_frontend.h
@@ -22,6 +22,6 @@ unsigned read_smtlib_file(char const * benchmark_file);
 unsigned read_smtlib2_commands(char const * command_file);
 void help_tactics();
 void help_probes();
-void help_tactic(char const* name);
+void help_tactic(char const* name, bool markdown);
 
 
diff --git a/src/tactic/core/injectivity_tactic.cpp b/src/tactic/core/injectivity_tactic.cpp
index dfcb152a254..e4071628cdf 100644
--- a/src/tactic/core/injectivity_tactic.cpp
+++ b/src/tactic/core/injectivity_tactic.cpp
@@ -5,19 +5,11 @@ Module Name:
 
   injectivity_tactic.cpp
 
-Abstract:
-
-  Injectivity tactics
-  - Discover axioms of the form `forall x. (= (g (f x)) x`
-    Mark `f` as injective
-  - Rewrite (sub)terms of the form `(= (f x) (f y))` to `(= x y)` whenever `f` is injective.
 
 Author:
 
   Nicolas Braud-Santoni (t-nibrau) 2017-08-10
 
-Notes:
-
 --*/
 #include <algorithm>
 #include <utility>
@@ -164,8 +156,6 @@ class injectivity_tactic : public tactic {
     struct rewriter_eq_cfg : public default_rewriter_cfg {
         ast_manager              & m_manager;
         InjHelper                & inj_map;
-//        expr_ref_vector            m_out;
-//        sort_ref_vector            m_bindings;
 
         ast_manager & m() const { return m_manager; }
 
@@ -176,14 +166,13 @@ class injectivity_tactic : public tactic {
         }
 
         void cleanup_buffers() {
-//            m_out.finalize();
         }
 
         void reset() {
         }
 
         br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
-            if(num != 2)
+            if (num != 2)
                 return BR_FAILED;
 
             if (!m().is_eq(f))
@@ -230,8 +219,6 @@ class injectivity_tactic : public tactic {
     finder *           m_finder;
     rewriter_eq *      m_eq;
     InjHelper *        m_map;
-//    rewriter_inverse * m_inverse;
-
     params_ref         m_params;
     ast_manager &      m_manager;
 
diff --git a/src/tactic/core/injectivity_tactic.h b/src/tactic/core/injectivity_tactic.h
index e23f8216309..78310909a8b 100644
--- a/src/tactic/core/injectivity_tactic.h
+++ b/src/tactic/core/injectivity_tactic.h
@@ -13,7 +13,33 @@ Module Name:
 
     Nicolas Braud-Santoni (t-nibrau) 2017-08-10
 
-Notes:
+
+Tactic Documentation:
+
+## Tactic injectivity
+
+### Short Description:
+
+- Discover axioms of the form `forall x. (= (g (f x)) x`
+  Mark `f` as injective
+
+- Rewrite (sub)terms of the form `(= (f x) (f y))` to `(= x y)` whenever `f` is injective.
+
+### Example
+ 
+```z3
+  (declare-fun f (Int) Int)
+  (declare-fun g (Int) Int)
+  (declare-const x Int)
+  (declare-const y Int)
+  (assert (forall ((x Int)) (= (g (f x)) x)))
+  (assert (not (= (f x) (f (f y)))))
+  (apply injectivity)
+```
+
+### Notes
+
+* does not support cores nor proofs
 
 --*/
 #pragma once
diff --git a/src/tactic/core/reduce_args_tactic.h b/src/tactic/core/reduce_args_tactic.h
index 5fa1f74cda8..615b4d70fc8 100644
--- a/src/tactic/core/reduce_args_tactic.h
+++ b/src/tactic/core/reduce_args_tactic.h
@@ -23,15 +23,15 @@ Reduce the number of arguments of function applications, when for all occurrence
 
 ### Long Description
 
-Example, suppose we have a function `f` with `2` arguments. 
-There are 1000 applications of this function, but the first argument is always "a", "b" or "c".
-Thus, we replace the `f(t1, t2)` with 
+Example, suppose we have a function $f$ with 2 arguments. 
+There are 1000 applications of this function, but the first argument is always $a$, $b$ or $c$.
+Thus, we replace the $f(t_1, t_2)$ with 
 
-*      `f_a(t2)`   if   `t1 = a`
-*      `f_b(t2)`   if   `t2 = b`
-*      `f_c(t2)`   if   `t2 = c`
+* $f_a(t_2)$   if   $t_1 = a$
+* $f_b(t_2)$   if   $t_2 = b$
+* $f_c(t_2)$   if   $t_2 = c$
 
-Since `f_a`, `f_b`, `f_c` are new symbols, satisfiability is preserved.
+Since $f_a$, $f_b$, $f_c$ are new symbols, satisfiability is preserved.
    
 This transformation is very similar in spirit to the Ackermman's reduction. 
 
diff --git a/src/tactic/dependent_expr_state_tactic.h b/src/tactic/dependent_expr_state_tactic.h
index f2d53236840..9da9c1965e0 100644
--- a/src/tactic/dependent_expr_state_tactic.h
+++ b/src/tactic/dependent_expr_state_tactic.h
@@ -49,7 +49,7 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state {
         m(m),
         m_params(p),
         m_factory(f),
-        m_dep(m, m.mk_true(), nullptr)
+        m_dep(m, m.mk_true(), nullptr, nullptr)
     {}
 
     /**
@@ -58,22 +58,22 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state {
     unsigned qtail() const override { return m_goal->size(); }
 
     dependent_expr const& operator[](unsigned i) override {
-        m_dep = dependent_expr(m, m_goal->form(i), m_goal->dep(i));
+        m_dep = dependent_expr(m, m_goal->form(i), m_goal->pr(i), m_goal->dep(i));
         return m_dep;
     }
     
     void update(unsigned i, dependent_expr const& j) override {
         if (inconsistent())
             return;
-        auto [f, d] = j();
-        m_goal->update(i, f, nullptr, d);
+        auto [f, p, d] = j();
+        m_goal->update(i, f, p, d);
     }
     
     void add(dependent_expr const& j) override {
         if (inconsistent())
             return;
-        auto [f, d] = j();
-        m_goal->assert_expr(f, nullptr, d);
+        auto [f, p, d] = j();
+        m_goal->assert_expr(f, p, d);
     }
 
     bool inconsistent() override {
@@ -108,7 +108,7 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state {
         tactic_report report(name(), *in);
         m_goal = in.get();
         try {
-            if (!in->proofs_enabled())
+            if (!in->proofs_enabled() || m_simp->supports_proofs())
                 m_simp->reduce();
             if (m.inc())
                 advance_qhead();