mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

allow parameters to overwrite logic, fixes bug report by Nuno

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-03-07 10:44:06 -08:00
parent 8c4d791f01
commit 49d0e28621
3 changed files with 12 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/smt/tactic/smt_tactic.cpp
View file

@ -99,7 +99,7 @@ public:
m_ctx(0), m_ctx(0),
m_callback(0) { m_callback(0) {
updt_params_core(p); updt_params_core(p);
TRACE("smt_tactic", tout << this << "\np: " << p << "\n";); TRACE("smt_tactic", tout << "p: " << p << "\n";);
} }
virtual tactic * translate(ast_manager & m) { virtual tactic * translate(ast_manager & m) {
@ -120,13 +120,12 @@ public:
} }
virtual void updt_params(params_ref const & p) { virtual void updt_params(params_ref const & p) {
TRACE("smt_tactic", tout << this << "\nupdt_params: " << p << "\n";); TRACE("smt_tactic", tout << "updt_params: " << p << "\n";);
updt_params_core(p); updt_params_core(p);
fparams().updt_params(p); fparams().updt_params(p);
symbol logic = p.get_sym(symbol("logic"), symbol::null); m_logic = p.get_sym(symbol("logic"), m_logic);
if (logic != symbol::null) { if (m_logic != symbol::null && m_ctx) {
if (m_ctx) m_ctx->set_logic(logic); m_ctx->set_logic(m_logic);
m_logic = logic;
} }
SASSERT(p.get_bool("auto_config", fparams().m_auto_config) == fparams().m_auto_config); SASSERT(p.get_bool("auto_config", fparams().m_auto_config) == fparams().m_auto_config);
} }

2
src/solver/tactic2solver.cpp
View file

@ -128,8 +128,8 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
ast_manager & m = m_assertions.m(); ast_manager & m = m_assertions.m();
m_result = alloc(simple_check_sat_result, m); m_result = alloc(simple_check_sat_result, m);
m_tactic->cleanup(); m_tactic->cleanup();
m_tactic->updt_params(m_params);
m_tactic->set_logic(m_logic); m_tactic->set_logic(m_logic);
m_tactic->updt_params(m_params); // parameters are allowed to overwrite logic.
goal_ref g = alloc(goal, m, m_produce_proofs, m_produce_models, m_produce_unsat_cores); goal_ref g = alloc(goal, m, m_produce_proofs, m_produce_models, m_produce_unsat_cores);
unsigned sz = m_assertions.size(); unsigned sz = m_assertions.size();

8
src/util/mpn.cpp
View file

@ -226,7 +226,7 @@ size_t mpn_manager::div_normalize(mpn_digit const * numer, size_t const lnum,
mpn_sbuffer & n_denom) const mpn_sbuffer & n_denom) const
{ {
size_t d = 0; size_t d = 0;
while (((denom[lden-1] << d) & MASK_FIRST) == 0) d++; while (lden > 0 && ((denom[lden-1] << d) & MASK_FIRST) == 0) d++;
SASSERT(d < DIGIT_BITS); SASSERT(d < DIGIT_BITS);
n_numer.resize(lnum+1); n_numer.resize(lnum+1);
@ -239,7 +239,8 @@ size_t mpn_manager::div_normalize(mpn_digit const * numer, size_t const lnum,
for (size_t i = 0; i < lden; i++) for (size_t i = 0; i < lden; i++)
n_denom[i] = denom[i]; n_denom[i] = denom[i];
} }
else { else if (lnum != 0) {
SASSERT(lden > 0);
mpn_digit q = FIRST_BITS(d, numer[lnum-1]); mpn_digit q = FIRST_BITS(d, numer[lnum-1]);
n_numer[lnum] = q; n_numer[lnum] = q;
for (size_t i = lnum-1; i > 0; i--) for (size_t i = lnum-1; i > 0; i--)
@ -249,6 +250,9 @@ size_t mpn_manager::div_normalize(mpn_digit const * numer, size_t const lnum,
n_denom[i] = denom[i] << d | FIRST_BITS(d, denom[i-1]); n_denom[i] = denom[i] << d | FIRST_BITS(d, denom[i-1]);
n_denom[0] = denom[0] << d; n_denom[0] = denom[0] << d;
} }
else {
d = 0;
}
TRACE("mpn_norm", tout << "Normalized: n_numer="; display_raw(tout, n_numer.c_ptr(), n_numer.size()); TRACE("mpn_norm", tout << "Normalized: n_numer="; display_raw(tout, n_numer.c_ptr(), n_numer.size());
tout << " n_denom="; display_raw(tout, n_denom.c_ptr(), n_denom.size()); tout << std::endl; ); tout << " n_denom="; display_raw(tout, n_denom.c_ptr(), n_denom.size()); tout << std::endl; );