add doc for card2bv

src/ast/rewriter/pb2bv_rewriter.cpp

@@ -200,7 +200,7 @@ struct pb2bv_rewriter::imp {
             }
 
             if (m_pb_solver == "segmented") {
-				throw default_exception("segmented encoding is disabled, use a different value for pb.solver");
+                throw default_exception("segmented encoding is disabled, use a different value for pb.solver");
                 switch (is_le) {
                 case l_true:  return mk_seg_le(k);
                 case l_false: return mk_seg_ge(k);
@@ -1077,9 +1077,9 @@ struct pb2bv_rewriter::imp {
     }
 
     void collect_param_descrs(param_descrs& r) const {
-        r.insert("keep_cardinality_constraints", CPK_BOOL, "(default: false) retain cardinality constraints (don't bit-blast them) and use built-in cardinality solver");
+        r.insert("keep_cardinality_constraints", CPK_BOOL, "retain cardinality constraints (don't bit-blast them) and use built-in cardinality solver", "false");
-        r.insert("pb.solver", CPK_SYMBOL, "(default: solver) retain pb constraints (don't bit-blast them) and use built-in pb solver");
+        r.insert("pb.solver", CPK_SYMBOL, "encoding used for Pseudo-Boolean constraints: totalizer, sorting, binary_merge, bv, solver. PB constraints are retained if set to 'solver'", "solver");
-        r.insert("cardinality.encoding", CPK_SYMBOL, "(default: none) grouped, bimander, ordered, unate, circuit");
+        r.insert("cardinality.encoding", CPK_SYMBOL, "encoding used for cardinality constraints: grouped, bimander, ordered, unate, circuit", "none");
     }
 
     unsigned get_num_steps() const { return m_rw.get_num_steps(); }

src/tactic/arith/arith_bounds_tactic.cpp

@@ -61,7 +61,7 @@ struct arith_bounds_tactic : public tactic {
             return true;
         }
         if ((!is_negated && (a.is_lt(e, e1, e2) || a.is_gt(e, e2, e1))) ||
-                 (is_negated && (a.is_le(e, e2, e1) || a.is_ge(e, e1, e2)))) {
+            (is_negated && (a.is_le(e, e2, e1) || a.is_ge(e, e1, e2)))) {
             is_strict = true;
             return true;
         }

src/tactic/arith/bound_manager.cpp

@@ -262,13 +262,12 @@ void bound_manager::reset() {
 }
 
 bool bound_manager::inconsistent() const {
-    for (auto const& kv : m_lowers) {
+    for (auto const& [k,v] : m_lowers) {
-        limit const& lim1 = kv.m_value;
+        limit const& lim1 = v;
         limit lim2;        
-        if (m_uppers.find(kv.m_key, lim2)) {
+        if (m_uppers.find(k, lim2)) {
-            if (lim1.first > lim2.first) {
+            if (lim1.first > lim2.first)
-                return true;
+                return true;            
-            }
             if (lim1.first == lim2.first &&
                 !lim1.second && lim2.second) {
                 return true;

src/tactic/arith/card2bv_tactic.h

@@ -5,14 +5,55 @@ Module Name:
 
     card2bv_tactic.cpp
 
-Abstract:
-
-    Tactic for converting Pseudo-Boolean constraints to BV
-
 Author:
 
     Nikolaj Bjorner (nbjorner) 2014-03-20
 
+Tactic Documentation:
+
+## Tactic car2bv
+
+### Short Description
+
+Tactic for converting Pseudo-Boolean constraints to bit-vectors.
+
+### Long Description 
+
+The tactic implements a set of standard methods for converting cardinality and Pseudo-Boolean constraints into bit-vector or propositional formulas
+(using basic logical connectives, conjunction, disjunction, negation). The conversions from cardinality constraints are controlled
+separately from the conversions from Pseudo-Boolean constraints using different parameters.
+
+### Example
+
+```z3
+(declare-const a1 Bool)
+(declare-const a2 Bool)
+(declare-const a3 Bool)
+(declare-const a4 Bool)
+(declare-const a5 Bool)
+(declare-const a6 Bool)
+(push)
+(assert ((_ at-most 1) a1 a2 a3 a4 a5 a6))
+(assert ((_ at-most 2) a1 a2 a3 a4 a5 a6))
+(apply (with card2bv :cardinality.encoding unate))
+(apply (with card2bv :cardinality.encoding circuit))
+(apply (with card2bv :cardinality.encoding ordered))
+(apply (with card2bv :cardinality.encoding grouped))
+(apply (with card2bv :cardinality.encoding bimander))
+(pop)
+(assert ((_ pbge 5 2 3 4 4 3 5) a1 a2 a3 a4 a5 a6))
+(apply (with card2bv :pb.solver totalizer))
+(apply (with card2bv :pb.solver sorting))
+(apply (with card2bv :pb.solver binary_merge))
+(apply (with card2bv :pb.solver bv))
+(apply (with card2bv :pb.solver solver))
+```
+
+### Notes
+
+* supports cores
+* does not support proofs
+
 --*/
 #pragma once