From 7e69dab8f69747680d7af1d825bfc68a634afbd8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 6 Dec 2022 18:15:18 -0800
Subject: [PATCH] distribute forall cpp code

---
 doc/mk_tactic_doc.py                      |   5 ++
 src/ast/simplifiers/distribute_forall.cpp | 105 ++++++++++++++++++++++
 src/util/params.cpp                       |   2 +
 3 files changed, 112 insertions(+)
 create mode 100644 src/ast/simplifiers/distribute_forall.cpp

diff --git a/doc/mk_tactic_doc.py b/doc/mk_tactic_doc.py
index 85dfcb4c3..37b77ef52 100644
--- a/doc/mk_tactic_doc.py
+++ b/doc/mk_tactic_doc.py
@@ -19,12 +19,17 @@ is_doc = re.compile("Tactic Documentation")
 is_doc_end = re.compile("\-\-\*\/")
 is_tac_name = re.compile("## Tactic (.*)")
 
+def is_ws(s):
+    return all([0 for ch in s if ch != ' ' and ch != '\n'])
+
 def extract_params(ous, tac):
     z3_exe = BUILD_DIR + "/z3"
     out = subprocess.Popen([z3_exe, f"-tacticsmd:{tac}"], stdout=subprocess.PIPE).communicate()[0]
     if not out:
         return
     out = out.decode(sys.stdout.encoding)
+    if is_ws(out):
+        return
     ous.write("### Parameters\n\n")
     for line in out:
         ous.write(line.replace("\r",""))
diff --git a/src/ast/simplifiers/distribute_forall.cpp b/src/ast/simplifiers/distribute_forall.cpp
new file mode 100644
index 000000000..c7cc6659a
--- /dev/null
+++ b/src/ast/simplifiers/distribute_forall.cpp
@@ -0,0 +1,105 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    distribute_forall.cpp
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-02-18.
+    Nikolaj Bjorner (nbjorner) 2022-11-24
+
+--*/
+
+#include "ast/ast_util.h"
+#include "ast/rewriter/rewriter.h"
+#include "ast/rewriter/rewriter_def.h"
+#include "ast/rewriter/var_subst.h"
+#include "ast/simplifiers/dependent_expr_state.h"
+#include "ast/simplifiers/distribute_forall.h"
+
+struct distribute_forall_simplifier::rw_cfg : public default_rewriter_cfg {
+    ast_manager & m;
+
+    rw_cfg(ast_manager & m):m(m) {}
+
+    bool reduce_quantifier(quantifier * old_q,
+                           expr * new_body,
+                           expr * const * new_patterns,
+                           expr * const * new_no_patterns,
+                           expr_ref & result,
+                           proof_ref & result_pr) {
+
+        quantifier_ref tmp_q(m);
+        expr_ref_vector es(m);
+        expr* f;
+        if (is_forall(old_q)) {
+            // (forall X (and F1 ... Fn))
+            // -->
+            // (and (forall X F1)
+            //      ...
+            //      (forall X Fn)
+
+            if (!m.is_and(new_body) && !(m.is_not(new_body, f) && (m.is_implies(f) || m.is_or(f))))
+                return false;
+            flatten_and(new_body, es);
+            unsigned i = 0;
+            for (expr* arg : es) {
+                tmp_q = m.update_quantifier(old_q, arg);
+                es[i++] = elim_unused_vars(m, tmp_q, params_ref());
+            }
+            result = mk_and(es);
+            if (m.proofs_enabled()) 
+                result_pr = m.mk_push_quant(old_q, result);
+            return true;
+        }
+        if (is_exists(old_q)) {
+            // (exists X (or F1 ... Fn))
+            // -->
+            // (or (exists X F1)
+            //     ...
+            //     (exists X Fn)
+
+            if (!m.is_or(new_body) && !m.is_implies(new_body) && !(m.is_not(new_body, f) && m.is_and(f)))
+                return false;
+            flatten_or(new_body, es);
+            unsigned i = 0;
+            for (expr* arg : es) {
+                tmp_q = m.update_quantifier(old_q, arg);
+                es[i++] = elim_unused_vars(m, tmp_q, params_ref());
+            }
+            result = mk_or(es);
+            if (m.proofs_enabled()) 
+                result_pr = m.mk_push_quant(old_q, result);
+            return true;
+        }       
+        return false;
+    }
+};
+
+struct distribute_forall_simplifier::rw : public rewriter_tpl<rw_cfg> {
+    rw_cfg m_cfg;
+    
+    rw(ast_manager & m, bool proofs_enabled):
+        rewriter_tpl<rw_cfg>(m, proofs_enabled, m_cfg),
+        m_cfg(m) {
+    }
+};
+        
+void distribute_forall_simplifier::reduce() {
+    if (!m_fmls.has_quantifiers())
+        return;
+    rw rw(m, m.proofs_enabled());
+    expr_ref r(m);
+    proof_ref pr(m);
+    for (unsigned idx : indices()) {
+        auto const& d = m_fmls[idx];
+        if (!has_quantifiers(d.fml()))
+            continue;
+        rw(d.fml(), r, pr);
+        if (r != d.fml())
+            m_fmls.update(idx, dependent_expr(m, r, mp(d.pr(), pr), d.dep()));
+    }
+};
+
diff --git a/src/util/params.cpp b/src/util/params.cpp
index ee61bf47f..c801b3421 100644
--- a/src/util/params.cpp
+++ b/src/util/params.cpp
@@ -167,6 +167,8 @@ struct param_descrs::imp {
             names.push_back(kv.m_key);
         }
         std::sort(names.begin(), names.end(), symlt());
+        if (names.empty())
+            return;
         if (markdown) {
             out << " Parameter | Type | Description | Default\n";
             out << " ----------|------|-------------|--------\n";