From f7269bb60a3165d6a670f22aaa45b164b23906a7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 11 Dec 2022 10:16:17 -0800 Subject: [PATCH] update doc Signed-off-by: Nikolaj Bjorner --- src/ast/simplifiers/propagate_values.cpp | 2 +- src/ast/simplifiers/solve_eqs.cpp | 8 ++++---- src/tactic/core/blast_term_ite_tactic.cpp | 2 +- src/tactic/core/ctx_simplify_tactic.cpp | 4 ++-- src/tactic/core/propagate_values_tactic.cpp | 2 +- src/util/params.cpp | 8 ++++---- 6 files changed, 13 insertions(+), 13 deletions(-) diff --git a/src/ast/simplifiers/propagate_values.cpp b/src/ast/simplifiers/propagate_values.cpp index 1083cc36d73..efaf7f244ac 100644 --- 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 index e481dad8dee..1117ad0bcc5 100644 --- 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 index 987ab9f9075..b38f08e5496 100644 --- 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 index 9ef1cf224b9..aa4358e9cb1 100644 --- 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 index 6b8395fd860..5d5bc09454b 100644 --- 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 index c801b342146..d8902615245 100644 --- 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) {