update doc

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Dec 11, 2022 · f7269bb · f7269bb
1 parent a9f52b0
commit f7269bb
Show file tree

Hide file tree

Showing 6 changed files with 13 additions and 13 deletions.
diff --git a/src/ast/simplifiers/propagate_values.cpp b/src/ast/simplifiers/propagate_values.cpp
@@ -115,5 +115,5 @@ void propagate_values::updt_params(params_ref const& p) {
 
 void propagate_values::collect_param_descrs(param_descrs& r) {
     th_rewriter::get_param_descrs(r);
-    r.insert("max_rounds", CPK_UINT, "(default: 4) maximum number of rounds.");
+    r.insert("max_rounds", CPK_UINT, "maximum number of rounds.", "4");
 }
diff --git a/src/ast/simplifiers/solve_eqs.cpp b/src/ast/simplifiers/solve_eqs.cpp
@@ -270,10 +270,10 @@ namespace euf {
     }
 
     void solve_eqs::collect_param_descrs(param_descrs& r) {
-        r.insert("solve_eqs_max_occs", CPK_UINT, "(default: infty) maximum number of occurrences for considering a variable for gaussian eliminations.");
-        r.insert("theory_solver", CPK_BOOL, "(default: true) use theory solvers.");
-        r.insert("ite_solver", CPK_BOOL, "(default: true) use if-then-else solver.");
-        r.insert("context_solve", CPK_BOOL, "(default: false) solve equalities under disjunctions.");
+        r.insert("solve_eqs_max_occs", CPK_UINT, "(default: infty) maximum number of occurrences for considering a variable for gaussian eliminations.", "4294967295");
+        r.insert("theory_solver", CPK_BOOL, "theory solvers.", "true");
+        r.insert("ite_solver", CPK_BOOL, "use if-then-else solver.", "true");
+        r.insert("context_solve", CPK_BOOL, "solve equalities under disjunctions.", "false");
     }
 
     void solve_eqs::collect_statistics(statistics& st) const {

diff --git a/src/tactic/core/blast_term_ite_tactic.cpp b/src/tactic/core/blast_term_ite_tactic.cpp
@@ -179,7 +179,7 @@ class blast_term_ite_tactic : public tactic {
     void collect_param_descrs(param_descrs & r) override {
         insert_max_memory(r);
         insert_max_steps(r);
-        r.insert("max_inflation", CPK_UINT, "(default: infinity) multiplicative factor of initial term size.");
+        r.insert("max_inflation", CPK_UINT, "(default: infinity) multiplicative factor of initial term size.", "4294967295");
     }
 
     void operator()(goal_ref const & in, goal_ref_buffer & result) override {

diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp
@@ -611,8 +611,8 @@ void ctx_simplify_tactic::updt_params(params_ref const & p) {
 void ctx_simplify_tactic::get_param_descrs(param_descrs & r) {
     insert_max_memory(r);
     insert_max_steps(r);
-    r.insert("max_depth", CPK_UINT, "(default: 1024) maximum term depth.");
-    r.insert("propagate_eq", CPK_BOOL, "(default: false) enable equality propagation from bounds.");
+    r.insert("max_depth", CPK_UINT, "maximum term depth.", "1024");
+    r.insert("propagate_eq", CPK_BOOL, "enable equality propagation from bounds.", "false");
 }
 
 void ctx_simplify_tactic::operator()(goal_ref const & in,

diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp
@@ -230,7 +230,7 @@ class propagate_values_tactic : public tactic {
 
     void collect_param_descrs(param_descrs & r) override {
         th_rewriter::get_param_descrs(r);
-        r.insert("max_rounds", CPK_UINT, "(default: 4) maximum number of rounds.");
+        r.insert("max_rounds", CPK_UINT, "maximum number of rounds.", "4");
     }
 
     void operator()(goal_ref const & in, goal_ref_buffer & result) override {

diff --git a/src/util/params.cpp b/src/util/params.cpp
@@ -314,19 +314,19 @@ void param_descrs::display_markdown(std::ostream & out, bool smt2_style, bool in
 }
 
 void insert_max_memory(param_descrs & r) {
-    r.insert("max_memory", CPK_UINT, "(default: infty) maximum amount of memory in megabytes.");
+    r.insert("max_memory", CPK_UINT, "(default: infty) maximum amount of memory in megabytes.", "4294967295");
 }
 
 void insert_max_steps(param_descrs & r) {
-    r.insert("max_steps", CPK_UINT, "(default: infty) maximum number of steps.");
+    r.insert("max_steps", CPK_UINT, "(default: infty) maximum number of steps.", "4294967295");
 }
 
 void insert_produce_models(param_descrs & r) {
-    r.insert("produce_models", CPK_BOOL, "(default: false) model generation.");
+    r.insert("produce_models", CPK_BOOL, "model generation.", "false");
 }
 
 void insert_produce_proofs(param_descrs & r) {
-    r.insert("produce_proofs", CPK_BOOL, "(default: false) proof generation.");
+    r.insert("produce_proofs", CPK_BOOL, "proof generation.", "false");
 }
 
 void insert_timeout(param_descrs & r) {