From aed3d76a886ea1ef0a7c2db9504df893e388e591 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 14 Dec 2022 16:45:58 -0800
Subject: [PATCH] add doc

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/arith/lia2card_tactic.h         | 34 +++++++++--
 src/tactic/arith/nla2bv_tactic.h           | 24 +++++++-
 src/tactic/arith/normalize_bounds_tactic.h | 31 ++++++++---
 src/tactic/arith/recover_01_tactic.h       | 65 +++++++++++++++-------
 4 files changed, 121 insertions(+), 33 deletions(-)

diff --git a/src/tactic/arith/lia2card_tactic.h b/src/tactic/arith/lia2card_tactic.h
index ff076aa42..5186b419b 100644
--- a/src/tactic/arith/lia2card_tactic.h
+++ b/src/tactic/arith/lia2card_tactic.h
@@ -5,16 +5,38 @@ Module Name:
 
     lia2card_tactic.h
 
-Abstract:
-
-    Extract 0-1 integer variables used in 
-    cardinality constraints and replace them by Booleans.
-
 Author:
 
     Nikolaj Bjorner (nbjorner) 2013-11-5
 
-Notes:
+Tactic Documentation:
+
+## Tactic lia2card
+
+### Short Description
+
+Extract 0-1 integer variables used in 
+cardinality and pseudo-Boolean constraints and replace them by Booleans.
+
+### Example
+
+```z3
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+(assert (<= 0 x))
+(assert (<= 0 y))
+(assert (<= 0 z))
+(assert (>= 1 x))
+(assert (>= 1 y))
+(assert (>= 1 z))
+(assert (>= (+ (* 5 x) (* -2 z) (* 3 y) 1) 4))
+(apply lia2card)
+```
+
+### Notes
+
+* The tactic does not (properly) support proofs or cores.
 
 --*/
 #pragma once
diff --git a/src/tactic/arith/nla2bv_tactic.h b/src/tactic/arith/nla2bv_tactic.h
index 80a60b30f..d1acc861a 100644
--- a/src/tactic/arith/nla2bv_tactic.h
+++ b/src/tactic/arith/nla2bv_tactic.h
@@ -7,7 +7,6 @@ Module Name:
 
 Abstract:
 
-    Convert quantified NIA problems to bounded bit-vector arithmetic problems.
 
 Author:
 
@@ -16,6 +15,29 @@ Author:
 Notes:
     Ported to tactic framework on 2012-02-28
 
+Tactic Documentation:
+
+## Tactic nla2bv
+
+### Short Description
+
+Convert quantified NIA problems to bounded bit-vector arithmetic problems.
+
+### Example
+
+```z3
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+(assert (= (* x x y) (*  2 z y y)))
+(apply nla2bv)
+```
+
+### Notes
+
+* The tactic creates an under-approximation (a stronger set of formulas)
+
+
 --*/
 #pragma once
 
diff --git a/src/tactic/arith/normalize_bounds_tactic.h b/src/tactic/arith/normalize_bounds_tactic.h
index dec4d486e..4d456c38a 100644
--- a/src/tactic/arith/normalize_bounds_tactic.h
+++ b/src/tactic/arith/normalize_bounds_tactic.h
@@ -5,17 +5,34 @@ Module Name:
 
     normalize_bounds_tactic.h
 
-Abstract:
-
-    Replace x with x' + l, when l <= x
-    where x' is a fresh variable.
-    Note that, after the transformation 0 <= x'.
-
 Author:
 
     Leonardo de Moura (leonardo) 2011-10-21.
 
-Revision History:
+Tactic Documentation:
+
+## Tactic normalize-bounds
+
+### Short Description
+
+Replace $x$ with $x' + l$, when $l \leq x$
+where $x'$ is a fresh variable.
+Note that, after the transformation $0 \leq x'$.
+
+### Example
+
+```z3
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+(assert (<= 3 x))
+(assert (<= (+ x y) z))
+(apply normalize-bounds)
+```
+
+### Notes
+
+* supports proofs and cores
 
 --*/
 #pragma once
diff --git a/src/tactic/arith/recover_01_tactic.h b/src/tactic/arith/recover_01_tactic.h
index 4e16dbf4a..cd7e47ea0 100644
--- a/src/tactic/arith/recover_01_tactic.h
+++ b/src/tactic/arith/recover_01_tactic.h
@@ -5,29 +5,56 @@ Module Name:
 
     recover_01_tactic.h
 
-Abstract:
-
-    Recover 01 variables
-
-    Search for clauses of the form
-    p  or q or  x = 0
-    ~p or q or  x = k1
-    p  or ~q or x = k2
-    ~p or ~q or x = k1+k2
-
-    Then, replaces 
-    x with k1*y1 + k2*y2
-    p with y1=1
-    q with y2=1
-    where y1 and y2 are fresh 01 variables
-
-    The clauses are also removed.
-
 Author:
 
     Leonardo de Moura (leonardo) 2012-02-17.
 
-Revision History:
+Tactic Documentation:
+
+## Tactic recover-01
+
+### Short Description
+
+Recover 01 variables from propositional constants.
+
+### Long Description
+
+Search for clauses of the form
+
+```
+    p  or q or  x = 0
+    ~p or q or  x = k1
+    p  or ~q or x = k2
+    ~p or ~q or x = k1+k2
+```
+
+Then, replaces 
+
+
+* `x` with `k1*y1 + k2*y2`
+* `p` with `y1 = 1`
+* `q` with `y2 = 1`
+
+where `y1` and `y2` are fresh 01 variables.
+
+The clauses are also removed.
+
+### Example
+
+```z3
+(declare-const p Bool)
+(declare-const q Bool)
+(declare-const x Int)
+(assert (or p q (= x 0)))
+(assert (or (not p) q (= x 3)))
+(assert (or p (not q) (= x 6)))
+(assert (or (not p) (not q) (= x 9)))
+(apply recover-01)
+```
+
+### Notes
+
+* does not support proofs, does not support cores
 
 --*/
 #pragma once