more tactic descriptions

src/tactic/ufbv/macro_finder_tactic.h

@@ -13,7 +13,45 @@ Author:
 
     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 @@ Notes:
 #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 @@ Author:
 
     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