update doc

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

src/tactic/arith/eq2bv_tactic.h

@@ -5,16 +5,32 @@ Module Name:
 
     eq2bv_tactic.h
 
-Abstract:
-
-    Extract integer variables that are used as finite domain indicators.
-    The integer variables can only occur in equalities.
-
 Author:
 
     Nikolaj Bjorner (nbjorner) 2015-8-19
 
-Notes:
+Tactic Documentation:
+
+## Tactic eq2bv
+
+### Short Description
+
+Extract integer variables that are used as finite domain indicators.
+The integer variables can only occur in equalities.
+
+### Example
+
+```z3
+(declare-const x Int)
+(declare-const y Int)
+(assert (or (= x 5) (> y 3)))
+(assert (or (= x 4) (= y 2)))
+(apply eq2bv)
+```
+
+### Notes
+
+* does not support proofs
 
 --*/
 #pragma once

src/tactic/arith/factor_tactic.cpp

@@ -303,7 +303,7 @@ class factor_tactic : public tactic {
 
     void collect_param_descrs(param_descrs & r) override {
         r.insert("split_factors", CPK_BOOL,
-                 "(default: true) apply simplifications such as (= (* p1 p2) 0) --> (or (= p1 0) (= p2 0)).");
+                 "apply simplifications such as (= (* p1 p2) 0) --> (or (= p1 0) (= p2 0)).", "true");
         polynomial::factor_params::get_param_descrs(r);
     }
 

src/tactic/arith/factor_tactic.h

@@ -13,7 +13,21 @@ Module Name:
 
     Leonardo de Moura (leonardo) 2012-02-03
 
-Revision History:
+Tactic Documentation:
+
+## Tactic factor
+
+### Short Description
+
+Factor polynomials in equalities and inequalities.
+
+### Example
+```z3
+(declare-const x Real)
+(declare-const y Real)
+(assert (> (* x x) (* x y)))
+(apply factor)
+```
 
 --*/
 #pragma once

src/tactic/arith/fix_dl_var_tactic.h

@@ -7,18 +7,35 @@ Module Name:
 
 Abstract:
 
-    Fix a difference logic variable to 0.
-    If the problem is in the difference logic fragment, that is, all arithmetic terms
-    are of the form (x + k), and the arithmetic atoms are of the 
-    form x - y <= k or x - y = k. Then, we can set one variable to 0.
 
-    This is useful because, many bounds can be exposed after this operation is performed.
 
 Author:
 
     Leonardo (leonardo) 2011-12-29
 
-Notes:
+Tactic Documentation:
+
+## Tactic fix-dl-var
+
+### Short Description
+
+Fix a difference logic variable to `0`.
+If the problem is in the difference logic fragment, that is, all arithmetic terms
+are of the form `(x + k)`, and the arithmetic atoms are of the
+form `x - y <= k` or `x - y = k`. Then, we can set one variable to `0`.
+
+This is useful because, many bounds can be exposed after this operation is performed.
+
+### Example
+
+```z3
+(declare-const x Real)
+(declare-const y Real)
+(declare-const z Real)
+(assert (<= (+ x (* -1.0 y)) 3.0))
+(assert (<= (+ x (* -1.0 z)) 5.0))
+(apply fix-dl-var)
+```
 
 --*/
 #pragma once

src/tactic/arith/fm_tactic.cpp

@@ -467,10 +467,8 @@ class fm_tactic : public tactic {
                 x = t;
                 return true;
             }
-            else if (m_util.is_to_real(t) && is_uninterp_const(to_app(t)->get_arg(0))) {
-                x = to_app(t)->get_arg(0);
-                return true;
-            }
+            else if (m_util.is_to_real(t, x) && is_uninterp_const(x)) 
+                return true;            
             return false;
         }
 
@@ -1675,12 +1673,12 @@ class fm_tactic : public tactic {
     void collect_param_descrs(param_descrs & r) override {
         insert_produce_models(r);
         insert_max_memory(r);
-        r.insert("fm_real_only", CPK_BOOL, "(default: true) consider only real variables for fourier-motzkin elimination.");
-        r.insert("fm_occ", CPK_BOOL, "(default: false) consider inequalities occurring in clauses for FM.");
-        r.insert("fm_limit", CPK_UINT, "(default: 5000000) maximum number of constraints, monomials, clauses visited during FM.");
-        r.insert("fm_cutoff1", CPK_UINT, "(default: 8) first cutoff for FM based on maximum number of lower/upper occurrences.");
-        r.insert("fm_cutoff2", CPK_UINT, "(default: 256) second cutoff for FM based on num_lower * num_upper occurrences.");
-        r.insert("fm_extra", CPK_UINT, "(default: 0) max. increase on the number of inequalities for each FM variable elimination step.");
+        r.insert("fm_real_only", CPK_BOOL, "consider only real variables for fourier-motzkin elimination.", "true");
+        r.insert("fm_occ",       CPK_BOOL, "consider inequalities occurring in clauses for FM.", "false");
+        r.insert("fm_limit",    CPK_UINT, "maximum number of constraints, monomials, clauses visited during FM.", "5000000");
+        r.insert("fm_cutoff1",  CPK_UINT, "first cutoff for FM based on maximum number of lower/upper occurrences.", "8");
+        r.insert("fm_cutoff2",  CPK_UINT, "second cutoff for FM based on num_lower * num_upper occurrences.", "256");
+        r.insert("fm_extra",    CPK_UINT, "max. increase on the number of inequalities for each FM variable elimination step.", "0");
     }
 
 

src/tactic/arith/fm_tactic.h

@@ -5,20 +5,43 @@ Module Name:
 
     fm_tactic.h
 
-Abstract:
-
-    Use Fourier-Motzkin to eliminate variables.
-    This strategy can handle conditional bounds 
-    (i.e., clauses with at most one constraint).
-    
-    The strategy mk_occf can be used to put the
-    formula in OCC form.
-
 Author:
 
     Leonardo de Moura (leonardo) 2012-02-04.
 
-Revision History:
+Tactic Documentation:
+
+## Tactic fm
+
+### Short Description
+
+Use Fourier-Motzkin to eliminate variables.
+This strategy can handle conditional bounds
+(i.e., clauses with at most one constraint).
+
+The strategy mk_occf can be used to put the
+formula in OCC form.
+
+### Example
+
+```z3
+(declare-const x Real)
+(declare-const y Real)
+(declare-const z Real)
+(declare-const u Real)
+(declare-const v Real)
+(declare-const w Real)
+(declare-fun P (Real) Bool)
+(assert (<= x (+ y (* 2.0 z))))
+(assert (>= x (- y z)))
+(assert (>= x (- y 3 (* 3 z))))
+(assert (>= x 5))
+(assert (<= x u))
+(assert (>= x v))
+(assert (P u))
+(assert (P v))
+(apply fm)
+```
 
 --*/
 #pragma once