From 940fadb7018c355c3c7d0dd9f8d82922307854f1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 7 Dec 2022 08:51:18 -0800
Subject: [PATCH] doc

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/core/blast_term_ite_tactic.cpp |  2 -
 src/tactic/core/blast_term_ite_tactic.h   | 38 +++++++++++++++----
 src/tactic/core/ctx_simplify_tactic.h     | 25 +++++++++++-
 src/tactic/core/elim_term_ite_tactic.h    | 35 ++++++++++++++---
 src/tactic/core/pb_preprocess_tactic.cpp  | 32 ++++------------
 src/tactic/core/pb_preprocess_tactic.h    | 46 ++++++++++++++++++++++-
 src/tactic/core/tseitin_cnf_tactic.cpp    | 39 +------------------
 src/tactic/core/tseitin_cnf_tactic.h      | 32 +++++++++++++++-
 8 files changed, 167 insertions(+), 82 deletions(-)

diff --git a/src/tactic/core/blast_term_ite_tactic.cpp b/src/tactic/core/blast_term_ite_tactic.cpp
index 49e43e6335d..987ab9f9075 100644
--- a/src/tactic/core/blast_term_ite_tactic.cpp
+++ b/src/tactic/core/blast_term_ite_tactic.cpp
@@ -13,8 +13,6 @@ Module Name:
  
     Nikolaj Bjorner (nbjorner) 2013-11-4
 
-Notes:
-
 --*/
 #include "ast/normal_forms/defined_names.h"
 #include "ast/rewriter/rewriter_def.h"
diff --git a/src/tactic/core/blast_term_ite_tactic.h b/src/tactic/core/blast_term_ite_tactic.h
index b5f643a1eca..a322b8e11df 100644
--- a/src/tactic/core/blast_term_ite_tactic.h
+++ b/src/tactic/core/blast_term_ite_tactic.h
@@ -4,20 +4,42 @@ Copyright (c) 2013 Microsoft Corporation
 Module Name:
 
     blast_term_ite_tactic.h
-
-Abstract:
-
-    Blast term if-then-else by hoisting them up.
-    This is expensive but useful in some cases, such as
-    for enforcing constraints being in difference logic.
-    Use elim-term-ite elsewhere when possible.
    
 
 Author:
 
     Nikolaj Bjorner (nbjorner) 2013-11-4
 
-Notes:
+Tactic Documentation:
+
+## Tactic blast-term-ite
+
+### Short Description:
+
+Blast term if-then-else by hoisting them up.
+This is expensive but useful in some cases, such as
+for enforcing constraints being in difference logic.
+Use `elim-term-ite` elsewhere when possible.
+
+### Example
+ 
+```z3
+(declare-fun f (Int) Int)
+(declare-fun p (Int) Bool)
+(declare-const c1 Bool)
+(declare-const c2 Bool)
+(declare-const c3 Bool)
+(declare-const e1 Int) 
+(declare-const e2 Int) 
+(declare-const e3 Int)
+(declare-const e4 Int)
+(assert (p (f (if c1 (if c2 e1 (if c3 e2 e3)) e4))))
+(apply blast-term-ite) 
+```
+
+### Notes
+
+
 
 --*/
 #pragma once
diff --git a/src/tactic/core/ctx_simplify_tactic.h b/src/tactic/core/ctx_simplify_tactic.h
index c8e34f33d08..213f01f6234 100644
--- a/src/tactic/core/ctx_simplify_tactic.h
+++ b/src/tactic/core/ctx_simplify_tactic.h
@@ -13,7 +13,30 @@ Module Name:
 
     Leonardo (leonardo) 2011-10-26
 
-Notes:
+Tactic Documentation:
+
+## Tactic ctx-simplify
+
+### Short Description:
+
+The tactic performs simplifies sub-formulas using context built up by walking assertions and sub-formulas.
+
+### Example
+ 
+```z3
+  (declare-const p Bool)
+  (declare-const q Bool)
+  (declare-const r Bool)
+  (declare-fun f (Bool) Bool)
+  (assert p)
+  (assert (or (f p) (and r (or (not r) q))))
+  (apply ctx-simplify)
+```
+
+### Notes
+
+* supports proof terms with limited features
+
 
 --*/
 #pragma once
diff --git a/src/tactic/core/elim_term_ite_tactic.h b/src/tactic/core/elim_term_ite_tactic.h
index 8fa9f90319c..ca8d3d43e38 100644
--- a/src/tactic/core/elim_term_ite_tactic.h
+++ b/src/tactic/core/elim_term_ite_tactic.h
@@ -5,16 +5,39 @@ Module Name:
 
     elim_term_ite_tactic.h
 
-Abstract:
-
-    Eliminate term if-then-else by adding 
-    new fresh auxiliary variables.
-
 Author:
 
     Leonardo (leonardo) 2011-12-29
 
-Notes:
+Tactic Documentation:
+
+## Tactic elim-term-ite
+
+### Short Description:
+
+Eliminate term if-then-else by adding 
+new fresh auxiliary variables.
+
+
+### Example
+ 
+```z3
+(declare-fun f (Int) Int)
+(declare-fun p (Int) Bool)
+(declare-const c1 Bool)
+(declare-const c2 Bool)
+(declare-const c3 Bool)
+(declare-const e1 Int) 
+(declare-const e2 Int) 
+(declare-const e3 Int)
+(declare-const e4 Int)
+(assert (p (f (if c1 (if c2 e1 (if c3 e2 e3)) e4))))
+(apply elim-term-ite) 
+```
+
+### Notes
+
+* supports proof terms and unsat cores
 
 --*/
 #pragma once
diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp
index 9f071713504..05ed6eee903 100644
--- a/src/tactic/core/pb_preprocess_tactic.cpp
+++ b/src/tactic/core/pb_preprocess_tactic.cpp
@@ -14,22 +14,6 @@ Module Name:
 
     Nikolaj Bjorner (nbjorner) 2013-12-23
 
-Notes:
-
-    Resolution for PB constraints require the implicit 
-    inequalities that each variable ranges over [0,1]
-    so not all resolvents produce smaller sets of clauses.
-
-    We here implement subsumption resolution.  
-
-    x + y >= 1
-    A~x + B~y + Cz >= k
-    ---------------------
-    Cz >= k - B    
-
-    where A <= B, x, y do not occur elsewhere.    
-
-
 --*/
 #include "tactic/core/pb_preprocess_tactic.h"
 #include "tactic/tactical.h"
@@ -106,22 +90,20 @@ class pb_preprocess_tactic : public tactic {
         return alloc(pb_preprocess_tactic, m);
     }
 
-    char const* name() const override { return "pb_preprocess"; }
+    char const* name() const override { return "pb-preprocess"; }
     
     void operator()(
         goal_ref const & g, 
         goal_ref_buffer & result) override {
         tactic_report report("pb-preprocess", *g);
-        if (g->proofs_enabled()) {
-            throw tactic_exception("pb-preprocess does not support proofs");
-        }
-
-        generic_model_converter* pp = alloc(generic_model_converter, m, "pb-preprocess");
-
         g->inc_depth();        
         result.push_back(g.get());       
-        while (simplify(g, *pp));
-        g->add(pp);
+
+        if (!g->proofs_enabled()) {
+            generic_model_converter* pp = alloc(generic_model_converter, m, "pb-preprocess");            
+            while (simplify(g, *pp));
+            g->add(pp);
+        }
 
         // decompose(g);
     }
diff --git a/src/tactic/core/pb_preprocess_tactic.h b/src/tactic/core/pb_preprocess_tactic.h
index ec387e6e0fa..83e8723f631 100644
--- a/src/tactic/core/pb_preprocess_tactic.h
+++ b/src/tactic/core/pb_preprocess_tactic.h
@@ -14,7 +14,51 @@ Module Name:
 
     Nikolaj Bjorner (nbjorner) 2013-12-23
 
-Notes:
+Documentation:
+
+## Tactic pb-preprocess
+
+### Short Description:
+
+The tactic eliminates variables from pseudo-Boolean inequalities and performs algebraic simplifcations on formulas
+
+### Long Description
+
+Resolution for PB constraints require the implicit 
+inequalities that each variable ranges over [0,1]
+so not all resolvents produce smaller sets of clauses.
+
+We here implement subsumption resolution.  
+
+```
+    x + y >= 1
+    A~x + B~y + Cz >= k
+    ---------------------
+    Cz >= k - B    
+```
+
+where `A <= B` and `x, y` do not occur elsewhere.    
+
+
+### Example
+ 
+```z3
+  (declare-const x Bool)
+  (declare-const y Bool)
+  (declare-const z Bool)
+  (declare-const u Bool)
+  (declare-const v Bool)
+  (assert ((_ pbge 1 1 1 2) (not x) (not y) (not z)))
+  (assert ((_ pbge 1 1 1 2) x u v))
+  (assert (not (and y v)))
+  (assert (not (and z u)))
+  (apply pb-preprocess)
+```
+
+### Notes
+
+* supports unsat cores
+* does not support proof terms
 
 --*/
 #pragma once
diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp
index e4476548a0c..667d53626b9 100644
--- a/src/tactic/core/tseitin_cnf_tactic.cpp
+++ b/src/tactic/core/tseitin_cnf_tactic.cpp
@@ -5,49 +5,14 @@ Module Name:
 
     tseitin_cnf_tactic.cpp
 
-Abstract:
-
-    Puts an assertion set in CNF.
-    Auxiliary variables are used to avoid blowup.
-
-    Features:
-    
-    - Efficient encoding is used for commonly used patterns such as:
-       (iff a (iff b c))
-       (or (not (or a b)) (not (or a c)) (not (or b c)))
-
-    - Efficient encoding is used for chains of if-then-elses 
-
-    - Distributivity is applied to non-shared nodes if the blowup is acceptable.
-    
-    - The features above can be disabled/enabled using parameters.
-
-    - The assertion-set is only modified if the resultant set of clauses
-    is "acceptable".
-
-    Notes: 
-    
-    - Term-if-then-else expressions are not handled by this strategy.
-    This kind of expression should be processed by other strategies.
-
-    - Quantifiers are treated as "theory" atoms. They are viewed
-    as propositional variables by this strategy.
-    
-    - The assertion set may contain free variables. 
-
-    - This strategy assumes the assertion_set_rewriter was
-    used before invoking it.
-    In particular, it is more effective when "and" operators
-    were eliminated.
-
-    TODO: add proof production
-
 Author:
 
     Leonardo (leonardo) 2011-12-29
 
 Notes:
 
+    TODO: add proof production
+
 --*/
 #include "ast/ast_pp.h"
 #include "tactic/tactical.h"
diff --git a/src/tactic/core/tseitin_cnf_tactic.h b/src/tactic/core/tseitin_cnf_tactic.h
index 363a1fafc23..a5e116825d9 100644
--- a/src/tactic/core/tseitin_cnf_tactic.h
+++ b/src/tactic/core/tseitin_cnf_tactic.h
@@ -10,12 +10,40 @@ Module Name:
     Puts an assertion set in CNF.
     Auxiliary variables are used to avoid blowup.
 
+    Features:
+    
+    - Efficient encoding is used for commonly used patterns such as:
+       (iff a (iff b c))
+       (or (not (or a b)) (not (or a c)) (not (or b c)))
+
+    - Efficient encoding is used for chains of if-then-elses 
+
+    - Distributivity is applied to non-shared nodes if the blowup is acceptable.
+    
+    - The features above can be disabled/enabled using parameters.
+
+    - The assertion-set is only modified if the resultant set of clauses
+    is "acceptable".
+
+    Notes: 
+    
+    - Term-if-then-else expressions are not handled by this strategy.
+    This kind of expression should be processed by other strategies.
+
+    - Quantifiers are treated as "theory" atoms. They are viewed
+    as propositional variables by this strategy.
+    
+    - The assertion set may contain free variables. 
+
+    - This strategy assumes the assertion_set_rewriter was
+    used before invoking it.
+    In particular, it is more effective when "and" operators
+    were eliminated.
+
 Author:
 
     Leonardo (leonardo) 2011-12-29
 
-Notes:
-
 --*/
 #pragma once