From 55ca6ce44b2f6963831209528a8b49728c7c58bf Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 4 Mar 2015 19:14:57 +0000 Subject: [PATCH] Resurrected the dack* options. Signed-off-by: Christoph M. Wintersteiger --- src/smt/params/dyn_ack_params.cpp | 22 ++++++++++------------ src/smt/params/dyn_ack_params.h | 6 +++++- src/smt/params/smt_params.cpp | 1 + src/smt/params/smt_params_helper.pyg | 8 +++++++- 4 files changed, 23 insertions(+), 14 deletions(-) diff --git a/src/smt/params/dyn_ack_params.cpp b/src/smt/params/dyn_ack_params.cpp index 2e94c376d..c559e2b9b 100644 --- a/src/smt/params/dyn_ack_params.cpp +++ b/src/smt/params/dyn_ack_params.cpp @@ -17,16 +17,14 @@ Revision History: --*/ #include"dyn_ack_params.h" +#include"smt_params_helper.hpp" -#if 0 -void dyn_ack_params::register_params(ini_params & p) { - p.register_int_param("dack", 0, 2, reinterpret_cast(m_dack), - "0 - disable dynamic ackermannization, 1 - expand Leibniz's axiom if a congruence is the root of a conflict, 2 - expand Leibniz's axiom if a congruence is used during conflict resolution."); - p.register_bool_param("dack_eq", m_dack_eq, "enable dynamic ackermannization for transtivity of equalities"); - p.register_unsigned_param("dack_threshold", m_dack_threshold, "number of times the congruence rule must be used before Leibniz's axiom is expanded"); - p.register_double_param("dack_factor", m_dack_factor, "number of instance per conflict"); - p.register_unsigned_param("dack_gc", m_dack_gc, "Dynamic ackermannization garbage collection frequency (per conflict)."); - p.register_double_param("dack_gc_inv_decay", m_dack_gc_inv_decay); -} -#endif - +void dyn_ack_params::updt_params(params_ref const & _p) { + smt_params_helper p(_p); + m_dack = static_cast(p.dack()); + m_dack_eq = p.dack_eq(); + m_dack_factor = p.dack_factor(); + m_dack_threshold = p.dack_threshold(); + m_dack_gc = p.dack_gc(); + m_dack_gc_inv_decay = p.dack_gc_inv_decay(); +} \ No newline at end of file diff --git a/src/smt/params/dyn_ack_params.h b/src/smt/params/dyn_ack_params.h index 9f7ce578c..95b5aff8a 100644 --- a/src/smt/params/dyn_ack_params.h +++ b/src/smt/params/dyn_ack_params.h @@ -19,6 +19,8 @@ Revision History: #ifndef _DYN_ACK_PARAMS_H_ #define _DYN_ACK_PARAMS_H_ +#include"params.h" + enum dyn_ack_strategy { DACK_DISABLED, DACK_ROOT, // congruence is the root of the conflict @@ -34,15 +36,17 @@ struct dyn_ack_params { double m_dack_gc_inv_decay; public: - dyn_ack_params(): + dyn_ack_params(params_ref const & p = params_ref()) : m_dack(DACK_ROOT), m_dack_eq(false), m_dack_factor(0.1), m_dack_threshold(10), m_dack_gc(2000), m_dack_gc_inv_decay(0.8) { + updt_params(p); } + void updt_params(params_ref const & _p); }; diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 18619c8ec..2f8d9c1ee 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -46,6 +46,7 @@ void smt_params::updt_local_params(params_ref const & _p) { void smt_params::updt_params(params_ref const & p) { preprocessor_params::updt_params(p); + dyn_ack_params::updt_params(p); qi_params::updt_params(p); theory_arith_params::updt_params(p); theory_bv_params::updt_params(p); diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 869b8cdc4..39818e621 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -45,5 +45,11 @@ def_module_params(module_name='smt', ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'), ('arith.ignore_int', BOOL, False, 'treat integer variables as real'), ('array.weak', BOOL, False, 'weak array theory'), - ('array.extensional', BOOL, True, 'extensional array theory') + ('array.extensional', BOOL, True, 'extensional array theory'), + ('dack', UINT, 1, '0 - disable dynamic ackermannization, 1 - expand Leibniz\'s axiom if a congruence is the root of a conflict, 2 - expand Leibniz\'s axiom if a congruence is used during conflict resolution'), + ('dack.eq', BOOL, False, 'enable dynamic ackermannization for transtivity of equalities'), + ('dack.factor', DOUBLE, 0.1, 'number of instance per conflict'), + ('dack.gc', UINT, 2000, 'Dynamic ackermannization garbage collection frequency (per conflict)'), + ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'), + ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded') ))