add missing tactic descriptions, add rewrite for tamagochi

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/rewriter/bool_rewriter.cpp

@@ -857,6 +857,7 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
         s = true;
     }
 
+
     // (ite c (ite c t1 t2) t3)       ==> (ite c t1 t3
     if (m().is_ite(t) && to_app(t)->get_arg(0) == c) {
         // Remark: (ite c (ite (not c) t1 t2) t3) ==> (ite c t2 t3) does not happen if applying rewrites bottom up
@@ -943,7 +944,6 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
     }
 
 #if 0
-    expr* t1, *t2;
     // (ite c (not (= t1 t2)) t1) ==> (not (= t1 (and c t2)))
     if (m().is_not(t, t1) && m().is_eq(t1, t1, t2) && e == t1) {
         expr_ref a(m());
@@ -960,6 +960,8 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
 #endif
 
 
+
+
     if (m().is_ite(t) && m_ite_extra_rules && m_elim_ite) {
         // (ite c1 (ite c2 t1 t2) t1) ==> (ite (and c1 (not c2)) t2 t1)
         if (e == to_app(t)->get_arg(1)) {

src/ast/rewriter/bv_rewriter.cpp

@@ -2807,6 +2807,28 @@ br_status bv_rewriter::mk_mkbv(unsigned num, expr * const * args, expr_ref & res
     return BR_FAILED;
 }
 
+bool bv_rewriter::is_bit(expr* t, unsigned& val) {
+    rational v;
+    unsigned sz;
+    return is_bv(t) && is_numeral(t, v, sz) && sz == 1 && (val = v.get_unsigned(), true);
+}
+
+bool bv_rewriter::is_eq_bit(expr * t, expr * & x, unsigned & val) {
+    expr* lhs, *rhs;
+    if (!m.is_eq(t, lhs, rhs))
+        return false;
+    if (is_bit(lhs, val)) {
+        x = rhs;
+        return true;
+    }
+    if (is_bit(rhs, val)) {
+        x = lhs;
+        return true;
+    }
+    return false;
+}
+
+
 br_status bv_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & result) {
     TRACE("bv_ite", tout << "mk_ite_core:\n" << mk_ismt2_pp(c, m) << "?\n"
             << mk_ismt2_pp(t, m) << "\n:" << mk_ismt2_pp(e, m) << "\n";);
@@ -2819,6 +2841,20 @@ br_status bv_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & resu
         return BR_REWRITE1;
     }
 
+    // if x = 0 then 0 else 1
+    expr* t1;
+    unsigned bit1, bit2, bit3;
+    if (is_bv(t) && is_eq_bit(c, t1, bit1) && is_bit(t, bit2) && is_bit(e, bit3)) {
+        if (bit1 == bit2 && bit3 != bit2) {
+            result = t1;
+            return BR_DONE;
+        }            
+        if (bit1 == bit3 && bit3 != bit2) {
+            result = m_util.mk_bv_not(t1);
+            return BR_REWRITE1;
+        }
+    }
+
     if (m_ite2id && m.is_eq(c) && is_bv(t) && is_bv(e)) {
         // detect when ite is actually some simple function based on the pattern (lhs=rhs) ? t : e
         expr * lhs = to_app(c)->get_arg(0);

src/ast/rewriter/bv_rewriter.h

@@ -193,6 +193,16 @@ public:
 
     bv_util & get_util() { return m_util; }
 
+    // Return true if t is of the form
+    //    (= t #b0)
+    //    (= t #b1)
+    //    (= #b0 t)
+    //    (= #b1 t)
+    bool is_eq_bit(expr* t, expr*& x, unsigned& val);
+
+    // return true if t is #b0 or #b1
+    bool is_bit(expr* t, unsigned& val);
+
 #define MK_BV_BINARY(OP)                         \
     expr_ref OP(expr* a, expr* b) {              \
         expr_ref result(m);                    \

src/ast/rewriter/th_rewriter.cpp

@@ -125,36 +125,6 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         return num_steps > m_max_steps;
     }
 
-    // Return true if t is of the form
-    //    (= t #b0)
-    //    (= t #b1)
-    //    (= #b0 t)
-    //    (= #b1 t)
-    bool is_eq_bit(expr * t, expr * & x, unsigned & val) {
-        if (!m().is_eq(t))
-            return false;
-        expr * lhs = to_app(t)->get_arg(0);
-        if (!m_bv_rw.is_bv(lhs))
-            return false;
-        if (m_bv_rw.get_bv_size(lhs) != 1)
-            return false;
-        expr * rhs = to_app(t)->get_arg(1);
-        rational v;
-        unsigned sz;
-        if (m_bv_rw.is_numeral(lhs, v, sz)) {
-            x    = rhs;
-            val  = v.get_unsigned();
-            SASSERT(val == 0 || val == 1);
-            return true;
-        }
-        if (m_bv_rw.is_numeral(rhs, v, sz)) {
-            x   = lhs;
-            val  = v.get_unsigned();
-            SASSERT(val == 0 || val == 1);
-            return true;
-        }
-        return false;
-    }
 
     // (iff (= x bit1) A)
     // --->
@@ -162,11 +132,11 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     br_status apply_tamagotchi(expr * lhs, expr * rhs, expr_ref & result) {
         expr * x;
         unsigned val;
-        if (is_eq_bit(lhs, x, val)) {
+        if (m_bv_rw.is_eq_bit(lhs, x, val)) {
             result = m().mk_eq(x, m().mk_ite(rhs, m_bv_rw.mk_numeral(val, 1), m_bv_rw.mk_numeral(1-val, 1)));
             return BR_REWRITE2;
         }
-        if (is_eq_bit(rhs, x, val)) {
+        if (m_bv_rw.is_eq_bit(rhs, x, val)) {
             result = m().mk_eq(x, m().mk_ite(lhs, m_bv_rw.mk_numeral(val, 1), m_bv_rw.mk_numeral(1-val, 1)));
             return BR_REWRITE2;
         }

src/cmd_context/echo_tactic.h

@@ -13,7 +13,7 @@ Author:
 
     Leonardo (leonardo) 2012-10-20
 
-Notes:
+## Tactic echo
 
 --*/
 #pragma once

src/math/subpaving/tactic/subpaving_tactic.h

@@ -15,6 +15,8 @@ Author:
 
 Revision History:
 
+## Tactic subpaving
+
 --*/
 #pragma once
 

src/muz/fp/horn_tactic.h

@@ -13,7 +13,29 @@ Author:
 
     Nikolaj Bjorner (nbjorner) 2012-11-16.
 
-Revision History:
+Tactic Documentation:
+
+## Tactic horn
+
+### Short Description
+
+Solve a set of Horn clauses using the SPACER engine.
+
+### Long Description
+
+The SPACER engine is specialized to solving Constrained Horn Clauses.
+This tactic instructs 
+
+## Tactic horn-simplify
+
+### Short Description
+
+Apply pre-processing simplification rules to a set of Horn clauses
+
+### Long Description
+This tactic exposes pre-processing simplification rules for Constrained Horn Clauses.
+They include a repertoire of simplification options that can be controlled by toggling
+the `fp` parameters.
 
 --*/
 #pragma once

src/sat/sat_solver/inc_sat_solver.cpp

@@ -26,7 +26,7 @@ Notes:
 #include "solver/solver.h"
 #include "solver/tactic2solver.h"
 #include "solver/parallel_params.hpp"
-#include "solver/parallel_tactic.h"
+#include "solver/parallel_tactical.h"
 #include "tactic/tactical.h"
 #include "tactic/aig/aig_tactic.h"
 #include "tactic/core/propagate_values_tactic.h"

src/sat/sat_solver/sat_smt_solver.cpp

@@ -33,8 +33,6 @@ Notes:
 #include "ast/ast_translation.h"
 #include "ast/ast_util.h"
 #include "solver/solver.h"
-#include "solver/parallel_params.hpp"
-#include "solver/parallel_tactic.h"
 #include "model/model_smt2_pp.h"
 #include "model/model_evaluator.h"
 #include "sat/sat_solver.h"

src/smt/tactic/smt_tactic_core.cpp

@@ -30,7 +30,7 @@ Notes:
 #include "solver/solver2tactic.h"
 #include "solver/solver.h"
 #include "solver/mus.h"
-#include "solver/parallel_tactic.h"
+#include "solver/parallel_tactical.h"
 #include "solver/parallel_params.hpp"
 
 typedef obj_map<expr, expr *> expr2expr_map;

src/solver/CMakeLists.txt

@@ -4,7 +4,7 @@ z3_add_component(solver
     check_logic.cpp
     combined_solver.cpp
     mus.cpp
-    parallel_tactic.cpp
+    parallel_tactical.cpp
     smt_logics.cpp
     solver.cpp
     solver_na2as.cpp

src/solver/parallel_tactical.cpp

@@ -3,7 +3,7 @@ Copyright (c) 2017 Microsoft Corporation
 
 Module Name:
 
-    parallel_tactic.cpp
+    parallel_tactical.cpp
 
 Abstract:
 
@@ -36,7 +36,7 @@ Notes:
 #include "solver/solver2tactic.h"
 #include "tactic/tactic.h"
 #include "tactic/tactical.h"
-#include "solver/parallel_tactic.h"
+#include "solver/parallel_tactical.h"
 #include "solver/parallel_params.hpp"
 
 

src/solver/parallel_tactical.h

@@ -12,8 +12,6 @@ Abstract:
 Author:
 
     Nikolaj Bjorner (nbjorner) 2017-10-9
-
-Notes:
    
 --*/
 #pragma once

src/tactic/aig/aig_tactic.h

@@ -13,7 +13,31 @@ Author:
 
     Leonardo (leonardo) 2011-10-24
 
-Notes:
+Tactic Documentation:
+
+## Tactic aig
+
+### Short Description
+
+Simplify Boolean structure using AIGs (And-inverter graphs).
+
+### Long Description
+
+And-inverter graphs (AIGs) uses just the Boolean connectives `and` and `not` to encode Boolean
+formulas. The circuit representation using AIGs first converts formulas using other connectives to this normal form, 
+then performs local simplification steps to minimize the circuit representation.
+Note that the simplification steps used by this tactic are heuristic, trading speed for power, 
+and do not represent a high-quality circuit minimization approach.
+
+### Example
+
+```z3
+(declare-const a Bool)
+(declare-const b Bool)
+(declare-const c Bool)
+(assert (or (and a b) (and b a c)))
+(apply aig)
+```
 
 --*/
 #pragma once

src/tactic/core/eliminate_predicates_tactic.h

@@ -13,6 +13,42 @@ Author:
 
     Nikolaj Bjorner (nbjorner) 2022-10-30
 
+Tactic Documentation:
+
+## Tactic elim-predicates
+
+### Short Description
+Eliminates predicates and macros from a formula.
+
+### Long Description
+The tactic subsumes the functionality of `macro-finder` and `quasi-macros`.
+Besides finding macros, it eliminates predicates using Davis-Putnam
+resolution.
+
+### Example
+
+the predicate `p` occurs once positively. All negative occurrences of `p` are resolved against this positive occurrence.
+The result of resolution is a set of equalities between arguments to `p`. The function `f` is replaced by a partial solution.
+
+```
+(declare-fun f (Int Int Int) Int)
+(declare-fun p (Int) Bool)
+(declare-const a Int)
+(declare-const b Int)
+
+(assert (forall ((x Int) (y Int)) (= (f x y (+ x y)) (* 2 x y))))
+(assert (p (f 8 a (+ a 8))))
+(assert (not (p (f 0 a (+ a 8)))))
+(assert (not (p (f 2 a (+ a 8)))))
+(assert (not (p (f 1 a (+ a b)))))
+(apply elim-predicates)
+```
+
+### Notes
+
+* support unsat cores
+* does not support proofs
+
 --*/
 #pragma once
 

src/tactic/fd_solver/fd_solver.cpp

@@ -24,7 +24,7 @@ Notes:
 #include "tactic/fd_solver/pb2bv_solver.h"
 #include "tactic/fd_solver/bounded_int2bv_solver.h"
 #include "solver/solver2tactic.h"
-#include "solver/parallel_tactic.h"
+#include "solver/parallel_tactical.h"
 #include "solver/parallel_params.hpp"
 
 solver * mk_fd_solver(ast_manager & m, params_ref const & p, bool incremental_mode) {

src/tactic/portfolio/smt_strategic_solver.cpp

@@ -43,7 +43,7 @@ Notes:
 #include "sat/sat_solver/sat_smt_solver.h"
 #include "ast/rewriter/bv_rewriter.h"
 #include "solver/solver2tactic.h"
-#include "solver/parallel_tactic.h"
+#include "solver/parallel_tactical.h"
 #include "solver/parallel_params.hpp"
 #include "params/tactic_params.hpp"
 #include "parsers/smt2/smt2parser.h"

src/tactic/ufbv/macro_finder_tactic.h

@@ -13,7 +13,7 @@ Author:
 
     Christoph (cwinter) 2012-10-26
 
-Tactic Description
+Tactic Documentation
 
 ## Tactic macro-finder
 

src/tactic/ufbv/quasi_macros_tactic.h

@@ -13,7 +13,7 @@ Author:
 
     Christoph (cwinter) 2012-10-26
 
-Tactic Description
+Tactic Documentation
 
 ## Tactic quasi-macro-finder