updated doc

src/tactic/bv/bv1_blaster_tactic.h

@@ -5,21 +5,37 @@ Module Name:
 
     bv1_blaster_tactic.h
 
-Abstract:
+Author:
 
-    Rewriter for "blasting" bit-vectors of size n into bit-vectors of size 1.
-    This rewriter only supports concat and extract operators.
-    This transformation is useful for handling benchmarks that contain
-    many BV equalities. 
+    Leonardo (leonardo) 2011-10-25
 
-    Remark: other operators can be mapped into concat/extract by using
-    the simplifiers.
+Tactic Documentation:
 
-Author:
+## Tactic bv1-blast
 
-    Leonardo (leonardo) 2011-10-25
+### Short Description
+
+Reduce bit-vector expressions into bit-vectors of size 1 (notes: only equality, extract and concat are supported).
+
+### Long Description
+
+Rewriter for "blasting" bit-vectors of size n into bit-vectors of size 1.
+This rewriter only supports concat and extract operators.
+This transformation is useful for handling benchmarks that contain
+many BV equalities. 
+
+_Remark_: other operators can be mapped into concat/extract by using
+the simplifiers.
+
+### Example
 
-Notes:
+```z3
+(declare-const x (_ BitVec 8))
+(declare-const y (_ BitVec 4))
+(declare-const z (_ BitVec 4))
+(assert (= (concat y z) x))
+    (apply bv1-blast)
+```
 
 --*/
 #pragma once

src/tactic/bv/bv_bound_chk_tactic.cpp

@@ -48,7 +48,6 @@ struct bv_bound_chk_rewriter_cfg : public default_rewriter_cfg {
         m_bv_ineq_consistency_test_max = p.bv_ineq_consistency_test_max();        
         m_max_memory = p.max_memory();
         m_max_steps = p.max_steps();
-
     }
 
     ast_manager & m() const { return m_m; }

src/tactic/bv/bv_bound_chk_tactic.h

@@ -1,18 +1,18 @@
  /*++
- Copyright (c) 2016 Microsoft Corporation
+Copyright (c) 2016 Microsoft Corporation
 
- Module Name:
+Module Name:
 
-  bv_bound_chk_tactic.h
+   bv_bound_chk_tactic.h
 
- Abstract:
+Author:
 
+  Mikolas Janota
 
- Author:
+### Notes 
 
- Mikolas Janota
+* does not support proofs, does not support cores
 
- Revision History:
  --*/
 #pragma once
 

src/tactic/bv/bv_size_reduction_tactic.h

@@ -7,19 +7,48 @@ Module Name:
 
 Abstract:
 
-    Reduce the number of bits used to encode constants, by using signed bounds.
-    Example: suppose x is a bit-vector of size 8, and we have
-    signed bounds for x such that:
-        -2 <= x <= 2
-    Then, x can be replaced by  ((sign-extend 5) k)
-    where k is a fresh bit-vector constant of size 3.
 
 Author:
 
     Leonardo (leonardo) 2012-02-19
 
 Notes:
 
+Tactic Documentation:
+
+## Tactic reduce-bv-size
+
+### Short Description
+
+Rry to reduce bit-vector sizes using inequalities.
+
+### Long Description
+
+Reduce the number of bits used to encode constants, by using signed bounds.
+Example: suppose $x$ is a bit-vector of size 8, and we have
+signed bounds for $x$ such that:
+
+```
+        -2 <= x <= 2
+```
+
+Then, $x$ can be replaced by  `((sign-extend 5) k)`
+where `k` is a fresh bit-vector constant of size 3.
+
+### Example
+
+```z3
+(declare-const x (_ BitVec 32))
+(assert (bvsle (bvneg (_ bv2 32)) x))
+(assert (bvsle x (_ bv2 32)))
+(assert (= (bvmul x x) (_ bv9 32)))
+(apply (and-then simplify reduce-bv-size))
+```
+
+### Notes
+
+* does not support proofs, nor unsat cores
+
 --*/
 #pragma once