From 1e06c7414acf11bd4ad85f777d4ed1f6d49e1c3e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 6 Dec 2022 15:44:21 -0800
Subject: [PATCH] add doc

---
 doc/mk_tactic_doc.py                 | 23 ++++++++++
 src/tactic/core/nnf_tactic.h         | 42 ++++++++++++++++-
 src/tactic/core/reduce_args_tactic.h | 67 +++++++++++++++++++++++++++-
 3 files changed, 130 insertions(+), 2 deletions(-)

diff --git a/doc/mk_tactic_doc.py b/doc/mk_tactic_doc.py
index 49d2a177a37..b49811fb9ea 100644
--- a/doc/mk_tactic_doc.py
+++ b/doc/mk_tactic_doc.py
@@ -5,7 +5,10 @@
 
 import os
 import re
+import sys
+import subprocess
 
+BUILD_DIR='../build'
 SCRIPT_DIR = os.path.abspath(os.path.dirname(__file__))
 OUTPUT_DIRECTORY = os.path.join(os.getcwd(), 'api')
 
@@ -14,10 +17,30 @@ def doc_path(path):
 
 is_doc = re.compile("Tactic Documentation")
 is_doc_end = re.compile("\-\-\*\/")
+is_tac_name = re.compile("## Tactic (.*)")
 
+def extract_params(ous, tac):
+    z3_exe = BUILD_DIR + "/z3"
+    out = subprocess.Popen([z3_exe, f"-tactics:{tac}"], stdout=subprocess.PIPE).communicate()[0]
+    if not out:
+        return
+    out = out.decode(sys.stdout.encoding)
+    ous.write("#### Parameters\n")
+    ous.write("```\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
     for line in ins:
+        m = is_tac_name.search(line)
+        if m:
+            tac_name = m.group(1)
         if is_doc_end.search(line):
+            if tac_name:
+                extract_params(ous, tac_name)
             break
         ous.write(line)
 
diff --git a/src/tactic/core/nnf_tactic.h b/src/tactic/core/nnf_tactic.h
index a821f56d0ec..fa724f2b877 100644
--- a/src/tactic/core/nnf_tactic.h
+++ b/src/tactic/core/nnf_tactic.h
@@ -13,7 +13,47 @@ Module Name:
 
     Leonardo de Moura (leonardo) 2011-12-28.
 
-Revision History:
+Note:
+
+   tactic documentation below co-created using gptchat (with some corrections) :-)
+
+Tactic Documentation:
+
+## Tactic nnf
+
+### Short Description:
+
+The tactic converts formulas to negation normal form (NNF)
+
+### Long Description
+
+In NNF, negations only appear in front of atomic formulas. 
+
+Standard rules for conversion into negation normal form are:
+- `(not (and p q))` is converted to `(or (not p) (not q))`
+- `(not (or p q))` is converted to `(and (not p) (not q))`
+- `(not (not p))` is converted to `p`
+- `(not (exists x. p))` is converted to `(forall x. (not p))`
+- `(not (forall x. p))` is converted to `(exists x. (not p))`
+
+
+Once all negations are pushed inside, the resulting formula is in NNF.
+
+### Example
+
+```z3
+  (declare-const x Int)
+  (assert (not (or (> x 0) (< x 0))))
+  (apply nnf)
+```
+
+This would convert the formula (not (or (> x 0) (< x 0))) to (and (<= x 0) (>= x 0)), which is in NNF.
+
+### Notes
+
+* supports unsat cores, proof terms
+
+
 
 --*/
 #pragma once
diff --git a/src/tactic/core/reduce_args_tactic.h b/src/tactic/core/reduce_args_tactic.h
index ed4dc3fb3f6..5fa1f74cda8 100644
--- a/src/tactic/core/reduce_args_tactic.h
+++ b/src/tactic/core/reduce_args_tactic.h
@@ -13,7 +13,72 @@ Module Name:
 
     Leonardo (leonardo) 2012-02-19
 
-Notes:
+Tactic Documentation:
+
+## Tactic reduce-args
+
+### Short Description:
+
+Reduce the number of arguments of function applications, when for all occurrences of a function f the i-th is a value.
+
+### 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 
+
+*      `f_a(t2)`   if   `t1 = a`
+*      `f_b(t2)`   if   `t2 = b`
+*      `f_c(t2)`   if   `t2 = c`
+
+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. 
+
+This transformation should work in the following way:
+
+```
+   1- Create a mapping decl2arg_map from declarations to tuples of booleans, an entry [f -> (true, false, true)]
+       means that f is a declaration with 3 arguments where the first and third arguments are always values.
+   2- Traverse the formula and populate the mapping. 
+        For each function application f(t1, ..., tn) do
+          a) Create a boolean tuple (is_value(t1), ..., is_value(tn)) and do
+             the logical-and with the tuple that is already in the mapping. If there is no such tuple
+             in the mapping, we just add a new entry.
+
+   If all entries are false-tuples, then there is nothing to be done. The transformation is not applicable.
+
+   Now, we create a mapping decl2new_decl from (decl, val_1, ..., val_n) to decls. Note that, n may be different for each entry,
+   but it is the same for the same declaration.
+   For example, suppose we have [f -> (true, false, true)] in decl2arg_map, 
+  and applications f(1, a, 2), f(1, b, 2), f(1, b, 3), f(2, b, 3), f(2, c, 3) in the formula.
+   Then, decl2arg_map would contain
+        (f, 1, 2) -> f_1_2
+        (f, 1, 3) -> f_1_3
+        (f, 2, 3) -> f_2_3
+   where f_1_2, f_1_3 and f_2_3 are new function symbols.
+   Using the new map, we can replace the occurrences of f.
+```
+
+### Example
+ 
+```z3
+(declare-fun f (Int Int) Bool)
+(declare-const x Int)
+(assert (f 1 2))
+(assert (f 1 3))
+(assert (f 2 4))
+(assert (f 2 5))
+(assert (f 1 6))
+(assert (f 1 7))
+(assert (f 1 x))
+(apply reduce-args)
+```
+
+### Notes
+
+* supports unsat cores
+* does not support proof terms
 
 --*/
 #pragma once