From 53cb389398f9492137fd00f198eba1e004872d5b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Dec 2012 13:05:14 -0800 Subject: [PATCH] fixing unit tests Signed-off-by: Nikolaj Bjorner --- src/smt/params/smt_params.cpp | 49 +++++++++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) create mode 100644 src/smt/params/smt_params.cpp diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp new file mode 100644 index 000000000..70f0ad811 --- /dev/null +++ b/src/smt/params/smt_params.cpp @@ -0,0 +1,49 @@ +/*++ +Copyright (c) 2006 Microsoft Corporation + +Module Name: + + smt_params.cpp + +Abstract: + + + +Author: + + Leonardo de Moura (leonardo) 2008-02-20. + +Revision History: + +--*/ +#include"smt_params.h" +#include"smt_params_helper.hpp" + +void smt_params::updt_local_params(params_ref const & _p) { + smt_params_helper p(_p); + m_auto_config = p.auto_config(); + m_ematching = p.ematching(); + m_phase_selection = static_cast(p.phase_selection()); + m_restart_strategy = static_cast(p.restart_strategy()); + m_restart_factor = p.restart_factor(); + m_case_split_strategy = static_cast(p.case_split()); + m_delay_units = p.delay_units(); + m_delay_units_threshold = p.delay_units_threshold(); +} + +void smt_params::updt_params(params_ref const & p) { + preprocessor_params::updt_params(p); + qi_params::updt_params(p); + theory_arith_params::updt_params(p); + theory_bv_params::updt_params(p); + updt_local_params(p); +} + +void smt_params::updt_params(context_params const & p) { + m_auto_config = p.m_auto_config; + m_soft_timeout = p.m_timeout; + m_model = p.m_model; + m_model_validate = p.m_validate_model; + m_proof_mode = p.m_proof ? PGM_FINE : PGM_DISABLED; +} +