more tactic descriptions

doc/mk_tactic_doc.py

@@ -59,6 +59,7 @@ def find_tactic_name(path):
             m = is_tac_name.search(line)
             if m:
                 return m.group(1)
+    print(f"no tactic in {path}")
     return ""
 
 def presort_files():

src/tactic/bv/bv_bound_chk_tactic.h

@@ -9,6 +9,14 @@ Module Name:
 
   Mikolas Janota
 
+Tactic Documentation
+
+## Tactic bv_bound_chk
+
+### Short Description
+
+Attempts to detect inconsistencies of bounds on bv expressions.
+
 ### Notes 
 
 * does not support proofs, does not support cores

src/tactic/bv/bv_slice_tactic.h

@@ -13,6 +13,34 @@ Module Name:
 
     Nikolaj Bjorner (nbjorner) 2022-10-30
 
+Tactic Documentation
+
+## Tactic bv-slice
+
+### Short Description
+
+Slices bit-vectors into sub-ranges to allow simplifying sub-ranges.
+
+### Long Description
+
+It rewrites a state using bit-vector slices. 
+Slices are extracted from bit-vector equality assertions.
+An equality assertion may equate a sub-range of a bit-vector
+with a constant. The tactic ensures that all occurrences of the
+subrange are replaced by the constants to allow additional 
+simplification
+
+### Example
+
+```z3 ignore-errors
+(declare-const x (_ BitVec 32))
+(declare-const y (_ BitVec 32))
+        (assert (= ((_ extract 31 16) x) (_ bv123 16)))
+(assert (= ((_ extract 15 0) x) ((_ extract 16 1) y)))
+(assert (= (bvadd x x) y))
+(apply bv-slice)
+```
+
 --*/
 #pragma once
 

src/tactic/core/dom_simplify_tactic.h

@@ -14,7 +14,29 @@ Module Name:
 
     Nikolaj and Nuno 
 
-Notes:
+Tactic Documentation:
+
+## Tactic dom-simplify
+
+### Short Description
+
+Apply dominator simplification rules
+
+### Long Description
+
+Dominator-based simplification is a context dependent simplification function that uses a dominator tree to control the number of paths it 
+visits during simplification. The expression DAG may have an exponential number of paths, but only paths corresponding to a dominator
+tree are visited. Since the paths selected by the dominator trees are limited, the simplifier may easily fail to simplify within a context. 
+
+### Example
+
+```z3
+(declare-const a Bool)
+(declare-const b Bool)
+(assert (and a (or a b)))
+(apply dom-simplify)
+```
+
 
 --*/
 

src/tactic/core/occf_tactic.h

@@ -5,20 +5,42 @@ Module Name:
 
     occf_tactic.h
 
-Abstract:
-
-    Put clauses in the assertion set in
-    OOC (one constraint per clause) form.
-    Constraints occurring in formulas that
-    are not clauses are ignored.
-    The formula can be put into CNF by
-    using mk_sat_preprocessor strategy.
-
 Author:
 
     Leonardo de Moura (leonardo) 2011-12-28.
 
-Revision History:
+Tactic Documentation:
+
+## Tactic occf
+
+### Short Description
+
+Put goal in one constraint per clause normal form 
+
+### Long Description
+
+Put clauses in the assertion set in
+OOC (one constraint per clause) form.
+Constraints occurring in formulas that
+are not clauses are ignored.
+The formula can be put into CNF by
+using `mk_sat_preprocessor` strategy.
+
+### Example
+
+```z3
+(declare-const x Int)
+(declare-const y Int)
+
+(assert (or (= x y) (> x (- y))))
+(assert (or (= x y) (< x (- y))))
+(apply occf)
+```
+
+### Notes
+
+* Does not support proofs
+* only clauses are considered
 
 --*/
 #pragma once

src/tactic/core/symmetry_reduce_tactic.h

@@ -13,7 +13,20 @@ Module Name:
 
     Nikolaj (nbjorner) 2011-05-31
 
-Notes:
+
+Tactic Documentation:
+
+## Tactic symmetry-reduce
+
+### Short Description
+
+Apply symmetry reduction
+
+### Long Description
+
+The tactic applies symmetry reduction for uninterpreted functions and equalities.
+It applies a straight-forward adaption of an algorithm proposed for veriT.
+
 
 --*/
 #pragma once

src/tactic/core/tseitin_cnf_tactic.h

@@ -7,42 +7,62 @@ Module Name:
 
 Abstract:
 
-    Puts an assertion set in CNF.
-    Auxiliary variables are used to avoid blowup.
 
-    Features:
+Author:
+
+    Leonardo (leonardo) 2011-12-29
+
+Tactic Documentation:
+
+## Tactic tseitin-cnf
+
+### Short Description
+
+Convert goal into CNF using tseitin-like encoding (note: quantifiers are ignored).
+
+### Long Description
+
+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 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 
+- Efficient encoding is used for chains of if-then-elses 
 
-    - Distributivity is applied to non-shared nodes if the blowup is acceptable.
+- Distributivity is applied to non-shared nodes if the blowup is acceptable.
     
-    - The features above can be disabled/enabled using parameters.
+- The features above can be disabled/enabled using parameters.
 
-    - The assertion-set is only modified if the resultant set of clauses
-    is "acceptable".
+- The assertion-set is only modified if the resultant set of clauses is "acceptable".
 
-    Notes: 
+Notes: 
     
-    - Term-if-then-else expressions are not handled by this strategy.
-    This kind of expression should be processed by other strategies.
+- 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.
+- Quantifiers are treated as "theory" atoms. They are viewed
+as propositional variables by this strategy.
     
-    - The assertion set may contain free variables. 
+- 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.
+- This strategy assumes the assertion_set_rewriter was used before invoking it.
+In particular, it is more effective when "and" operators
+were eliminated.
 
-Author:
+### Example
 
-    Leonardo (leonardo) 2011-12-29
+```z3
+(declare-const a Bool)
+(declare-const b Bool)
+(declare-const c Bool)
+
+(assert (= a (= b c)))
+(apply tseitin-cnf)
+```
 
 --*/
 #pragma once

src/tactic/ufbv/macro_finder_tactic.h

@@ -13,7 +13,45 @@ Module Name:
 
     Christoph (cwinter) 2012-10-26
 
-Notes:
+Tactic Description
+
+## Tactic macro-finder
+
+### Short Description 
+
+Identifies and applies macros.
+
+### Long Description
+
+It finds implicit macro definitions in quantifiers. 
+A main instance of a macro an equality that defines a function `f` using some term `t` that does not contain `f`.
+Other instances of macros are also recognized by the macro finder.
+
+* `(forall (x) (= (f x) t))`
+
+* `not (= (p x) t)` is recognized as `(p x) = (not t)`
+
+* `(iff (= (f x) t) cond)`  rewrites to `(f x) = (if cond t else (k x))`
+   * add clause `(not (= (k x) t))`
+
+* `(= (+ (f x) s) t)` becomes `(= (f x) (- t s))`
+
+* `(= (+ (* -1 (f x)) x) t)`  becomes `(= (f x) (- (- t s)))`
+
+### Example
+
+```z3
+(declare-fun f (Int) Int)
+(declare-fun p (Int) Bool)
+
+(assert (forall ((x Int)) (= (+ (f x) x) 3)))
+(assert (p (f 8)))
+(apply macro-finder)
+```
+
+### Notes
+
+* Supports proofs, unsat cores, but not goals with recursive function definitions.
 
 --*/
 #pragma once

src/tactic/ufbv/quasi_macros_tactic.cpp

@@ -21,8 +21,10 @@ Module Name:
 #include "ast/macros/macro_manager.h"
 #include "ast/macros/macro_finder.h"
 #include "ast/macros/quasi_macros.h"
+#include "ast/recfun_decl_plugin.h"
 #include "tactic/ufbv/quasi_macros_tactic.h"
 
+
 class quasi_macros_tactic : public tactic {
 
     struct imp {
@@ -41,6 +43,12 @@ class quasi_macros_tactic : public tactic {
 
             bool produce_proofs = g->proofs_enabled();
             bool produce_unsat_cores = g->unsat_core_enabled();
+
+            recfun::util rec(m());
+            if (!rec.get_rec_funs().empty()) {
+                result.push_back(g.get());
+                return;
+            }
 
             macro_manager mm(m_manager);
             quasi_macros qm(m_manager, mm);

src/tactic/ufbv/quasi_macros_tactic.h

@@ -13,7 +13,34 @@ Module Name:
 
     Christoph (cwinter) 2012-10-26
 
-Notes:
+Tactic Description
+
+## Tactic quasi-macro-finder
+
+### Short Description
+dentifies and applies quasi-macros.
+
+### Long Description
+
+A quasi macro defines a function symbol that contains more arguments than the number of bound variables it defines.
+The additional arguments are functions of the bound variables.
+ 
+### Example
+
+```z3
+(declare-fun f (Int Int Int) Int)
+(declare-fun p (Int) Bool)
+(declare-const a Int)
+
+(assert (forall ((x Int) (y Int)) (= (f x y 1) (* 2 x y))))
+(assert (p (f 8 a (+ a 8))))
+(apply quasi-macros)
+```
+
+### Notes
+
+* Supports proofs and cores
+
 
 --*/
 #pragma once