From ea9421bb381eadb9fe3d4192f3ed34ae170d258a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 12 Jan 2013 16:40:45 -0800 Subject: [PATCH] Expose rcf module parameters Signed-off-by: Leonardo de Moura --- src/math/realclosure/rcf.pyg | 7 +++++++ src/math/realclosure/realclosure.cpp | 14 ++++++++------ 2 files changed, 15 insertions(+), 6 deletions(-) create mode 100644 src/math/realclosure/rcf.pyg diff --git a/src/math/realclosure/rcf.pyg b/src/math/realclosure/rcf.pyg new file mode 100644 index 000000000..ad24ad530 --- /dev/null +++ b/src/math/realclosure/rcf.pyg @@ -0,0 +1,7 @@ +def_module_params('rcf', + description='real closed fields', + export=True, + params=(('use_prem', BOOL, True, "use pseudo-remainder instead of remainder when computing GCDs and Sturm-Tarski sequences"), + ('initial_precision', UINT, 24, "a value k that is the initial interval size (as 1/2^k) when creating transcendentals and approximated division"), + ('inf_precision', UINT, 24, "a value k that is the initial interval size (i.e., (0, 1/2^l)) used as an approximation for infinitesimal values"), + ('max_precision', UINT, 64, "during sign determination we switch from interval arithmetic to complete methods when the interval size is less than 1/2^k, where k is the max_precision"))) diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp index 9de57b387..ee4a4cc22 100644 --- a/src/math/realclosure/realclosure.cpp +++ b/src/math/realclosure/realclosure.cpp @@ -20,6 +20,7 @@ Notes: --*/ #include"realclosure.h" +#include"rcf_params.hpp" #include"array.h" #include"mpbq.h" #include"mpz_matrix.h" @@ -676,11 +677,12 @@ namespace realclosure { m_cancel = f; } - void updt_params(params_ref const & p) { - m_use_prem = p.get_bool("use_prem", true); - m_ini_precision = p.get_uint("initial_precision", 24); - m_inf_precision = p.get_uint("inf_precision", 24); - m_max_precision = p.get_uint("max_precision", 64); // == 1/2^64 for interval arithmetic methods, it switches to complete methods after that. + void updt_params(params_ref const & _p) { + rcf_params p(_p); + m_use_prem = p.use_prem(); + m_ini_precision = p.initial_precision(); + m_inf_precision = p.inf_precision(); + m_max_precision = p.max_precision(); bqm().power(mpbq(2), m_inf_precision, m_plus_inf_approx); bqm().set(m_minus_inf_approx, m_plus_inf_approx); bqm().neg(m_minus_inf_approx); @@ -5316,7 +5318,7 @@ namespace realclosure { } void manager::get_param_descrs(param_descrs & r) { - // TODO + rcf_params::collect_param_descrs(r); } void manager::set_cancel(bool f) {