Merge branch 'master' of https://github.com/z3prover/z3

doc/mk_tactic_doc.py

@@ -53,13 +53,21 @@ def extract_tactic_doc(ous, f):
             if is_doc.search(line):
                 generate_tactic_doc(ous, f, ins)
 
+def find_tactic_name(path):
+    with open(path) as ins:
+        for line in ins:
+            m = is_tac_name.search(line)
+            if m:
+                return m.group(1)
+    return ""
+
 def presort_files():
     tac_files = []
     for root, dirs, files in os.walk(doc_path("../src")):
         for f in files:
             if f.endswith("tactic.h"):
                 tac_files += [(f, os.path.join(root, f))]
-    tac_files = sorted(tac_files, key = lambda x: x[0])
+    tac_files = sorted(tac_files, key = lambda x: find_tactic_name(x[1]))
     return tac_files
 
 def help(ous):

src/muz/spacer/spacer_sym_mux.cpp

@@ -144,10 +144,12 @@ struct conv_rewriter_cfg : public default_rewriter_cfg {
 
     bool get_subst(expr * s, expr * & t, proof * & t_pr)
     {
-        if (!is_app(s)) { return false; }
+        if (!is_app(s)) 
+            return false; 
         app * a = to_app(s);
         func_decl * sym = a->get_decl();
         if (!m_parent.has_index(sym, m_from_idx)) {
+            CTRACE("spacer", m_homogenous && m_parent.is_muxed(sym), tout << "not found " << mk_pp(a, m) << "\n");
             SASSERT(!m_homogenous || !m_parent.is_muxed(sym));
             return false;
         }

src/tactic/arith/nla2bv_tactic.cpp

@@ -442,9 +442,9 @@ class nla2bv_tactic : public tactic {
 
     void collect_param_descrs(param_descrs & r) override {
         r.insert("nla2bv_max_bv_size", CPK_UINT, "(default: inf) maximum bit-vector size used by nla2bv tactic");
-        r.insert("nla2bv_bv_size", CPK_UINT, "(default: 4) default bit-vector size used by nla2bv tactic.");
-        r.insert("nla2bv_root", CPK_UINT, "(default: 2) nla2bv tactic encodes reals into bit-vectors using expressions of the form a+b*sqrt(c), this parameter sets the value of c used in the encoding.");
-        r.insert("nla2bv_divisor", CPK_UINT, "(default: 2) nla2bv tactic parameter.");
+        r.insert("nla2bv_bv_size", CPK_UINT, "default bit-vector size used by nla2bv tactic.", "4");
+        r.insert("nla2bv_root", CPK_UINT, "nla2bv tactic encodes reals into bit-vectors using expressions of the form a+b*sqrt(c), this parameter sets the value of c used in the encoding.", "2");
+        r.insert("nla2bv_divisor", CPK_UINT, "nla2bv tactic parameter.", "2");
     }
 
     /**

src/tactic/arith/normalize_bounds_tactic.cpp

@@ -161,7 +161,7 @@ class normalize_bounds_tactic : public tactic {
 
     void collect_param_descrs(param_descrs & r) override {
         insert_produce_models(r);
-        r.insert("norm_int_only", CPK_BOOL, "(default: true) normalize only the bounds of integer constants.");
+        r.insert("norm_int_only", CPK_BOOL, "normalize only the bounds of integer constants.", "true");
     }
 
     void operator()(goal_ref const & in, 

src/tactic/arith/pb2bv_tactic.h

@@ -13,7 +13,32 @@ Module Name:
 
     Christoph (cwinter) 2012-02-15
 
-Notes:
+Tactic Documentation:
+
+## Tactic pb2bv
+
+### Short Description
+
+Convert pseudo-boolean constraints to bit-vectors
+
+### Example
+
+```z3
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+(declare-const u Int)
+(assert (<= 0 x))
+(assert (<= 0 y))
+(assert (<= 0 z))
+(assert (<= 0 u))
+(assert (<= x 1))
+(assert (<= y 1))
+(assert (<= z 1))
+(assert (<= u 1))
+(assert (>= (+ (* 3 x) (* 2 y) (* 2 z) (* 2 u)) 4))
+(apply pb2bv)
+```
 
 --*/
 #pragma once

src/tactic/arith/propagate_ineqs_tactic.h

@@ -4,30 +4,49 @@ Copyright (c) 2012 Microsoft Corporation
 Module Name:
 
     propagate_ineqs_tactic.h
+     
+Author:
 
-Abstract:
+    Leonardo (leonardo) 2012-02-19
 
-    This tactic performs the following tasks:
+Tactic Documentation:
 
-     - Propagate bounds using the bound_propagator.
-     - Eliminate subsumed inequalities.  
-       For example:
-          x - y >= 3
-          can be replaced with true if we know that
-          x >= 3 and y <= 0
-            
-     - Convert inequalities of the form p <= k and p >= k into p = k,
-       where p is a polynomial and k is a constant.
+## Tactic propagate-ineqs
 
-    This strategy assumes the input is in arith LHS mode.
-    This can be achieved by using option :arith-lhs true in the
-    simplifier.
-     
-Author:
+### Short Description
 
-    Leonardo (leonardo) 2012-02-19
+Propagate ineqs/bounds, remove subsumed inequalities
+
+### Long Description
+
+This tactic performs the following tasks:
+
+- Propagate bounds using the bound_propagator.
+- Eliminate subsumed inequalities.
+  - For example:
+    `x - y >= 3` can be replaced with true if we know that `x >= 3` and `y <= 0`
+
+ - Convert inequalities of the form `p <= k` and `p >= k` into `p = k`,
+   where `p` is a polynomial and `k` is a constant.
+
+This strategy assumes the input is in arith LHS mode.
+This can be achieved by using option :arith-lhs true in the simplifier.
 
-Notes:
+### Example
+```z3
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+(declare-const u Int)
+(declare-const v Int)
+(declare-const w Int)
+(assert (>= x 3))
+(assert (<= y 0))
+(assert (>= (- x y) 3))
+(assert (>= (* u v w) 2))
+(assert (<= (* v u w) 2))
+(apply (and-then simplify propagate-ineqs))
+```
 
 --*/
 #pragma once

src/tactic/arith/purify_arith_tactic.cpp

@@ -911,11 +911,11 @@ class purify_arith_tactic : public tactic {
 
     void collect_param_descrs(param_descrs & r) override {
         r.insert("complete", CPK_BOOL, 
-                 "(default: true) add constraints to make sure that any interpretation of a underspecified arithmetic operators is a function. The result will include additional uninterpreted functions/constants: /0, div0, mod0, 0^0, neg-root");
+                 "add constraints to make sure that any interpretation of a underspecified arithmetic operators is a function. The result will include additional uninterpreted functions/constants: /0, div0, mod0, 0^0, neg-root", "true");
         r.insert("elim_root_objects", CPK_BOOL,
-                 "(default: true) eliminate root objects.");
+                 "eliminate root objects.", "true");
         r.insert("elim_inverses", CPK_BOOL,
-                 "(default: true) eliminate inverse trigonometric functions (asin, acos, atan).");
+                 "eliminate inverse trigonometric functions (asin, acos, atan).", "true");
         th_rewriter::get_param_descrs(r);
     }
 

src/tactic/arith/purify_arith_tactic.h

@@ -42,7 +42,28 @@ Module Name:
 
     Leonardo de Moura (leonardo) 2011-12-30.
 
-Revision History:
+Tactic Documentation:
+
+## Tactic purify-arith
+
+### Short Description
+
+Eliminate unnecessary operators: -, /, div, mod, rem, is-int, to-int, ^, root-objects.
+These operators can be replaced by introcing fresh variables and using multiplication and addition.
+
+### Example
+```z3
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+(declare-const u Int)
+(declare-const v Int)
+(declare-const w Int)
+(assert (= (div x 3) y))
+(assert (= (mod z 4) u))
+(assert (> (mod v w) u))
+(apply purify-arith)
+```
 
 --*/
 #pragma once

src/tactic/arith/recover_01_tactic.cpp

@@ -407,7 +407,7 @@ class recover_01_tactic : public tactic {
 
     void collect_param_descrs(param_descrs & r) override {
         th_rewriter::get_param_descrs(r);
-        r.insert("recover_01_max_bits", CPK_UINT, "(default: 10) maximum number of bits to consider in a clause.");
+        r.insert("recover_01_max_bits", CPK_UINT, "maximum number of bits to consider in a clause.", "10");
     }
 
     void operator()(goal_ref const & g, 

src/tactic/bv/bit_blaster_tactic.cpp

@@ -129,10 +129,10 @@ class bit_blaster_tactic : public tactic {
     void collect_param_descrs(param_descrs & r) override {
         insert_max_memory(r);
         insert_max_steps(r);
-        r.insert("blast_mul", CPK_BOOL, "(default: true) bit-blast multipliers (and dividers, remainders).");
-        r.insert("blast_add", CPK_BOOL, "(default: true) bit-blast adders.");
-        r.insert("blast_quant", CPK_BOOL, "(default: false) bit-blast quantified variables.");
-        r.insert("blast_full", CPK_BOOL, "(default: false) bit-blast any term with bit-vector sort, this option will make E-matching ineffective in any pattern containing bit-vector terms.");
+        r.insert("blast_mul", CPK_BOOL, "bit-blast multipliers (and dividers, remainders).", "true");
+        r.insert("blast_add", CPK_BOOL, "bit-blast adders.", "true");
+        r.insert("blast_quant", CPK_BOOL, "bit-blast quantified variables.", "false");
+        r.insert("blast_full", CPK_BOOL, "bit-blast any term with bit-vector sort, this option will make E-matching ineffective in any pattern containing bit-vector terms.", "false");
     }
 
     void operator()(goal_ref const & g, 

src/tactic/bv/bit_blaster_tactic.h

@@ -1,21 +1,33 @@
  /*++
 Copyright (c) 2011 Microsoft Corporation
  
- Module Name:
+Module Name:
  
     bit_blaster_tactic.h
  
- Abstract:
+Author:
  
-    Apply bit-blasting to a given goal.
- 
- Author:
- 
-    Leonardo (leonardo) 2011-10-25
- 
- Notes:
+   Leonardo (leonardo) 2011-10-25
  
+Tactic Documentation:
+
+## Tactic bit-blast
+
+### Short Description
+
+Apply bit-blasting to a given goal.
+
+### Example
+
+```z3
+(declare-const x (_ BitVec 8))
+(declare-const y (_ BitVec 8))
+(assert (bvule x y))
+(apply bit-blast)
+```
+
  --*/
+
 #pragma once
 
 #include "util/params.h"

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