mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

restore nyi trace

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-01-06 08:37:14 -08:00
parent a8b88b1850
commit 67827bfe56
2 changed files with 15 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/ast/sls/sls_bv_lookahead.cpp
View file

@ -344,7 +344,13 @@ namespace sls {
//verbose_stream() << "compute score " << mk_bounded_pp(a, m) << " is-true " << is_true << " is-true-new " << is_true_new << "\n";
if (is_true == is_true_new)
return 1;
expr* x, * y;
if (is_uninterp(a))
return 0;
if (m.is_true(a))
return is_true ? 1 : 0;
if (m.is_false(a))
return is_true ? 0 : 1;
expr* x, * y, * z;
if (m.is_not(a, x))
return new_score(x, !is_true);
if ((m.is_and(a) && is_true) || (m.is_or(a) && !is_true)) {
@ -364,6 +370,10 @@ namespace sls {
auto v1 = m_ev.get_bool_value(y);
return (is_true == (v0 == v1)) ? 1 : 0;
}
if (m.is_ite(a, x, y, z)) {
auto v0 = m_ev.get_bool_value(x);
return v0 ? new_score(y, is_true) : new_score(z, is_true);
}
if (is_true && m.is_eq(a, x, y) && bv.is_bv(x)) {
auto const& vx = wval(x);
@ -377,6 +387,9 @@ namespace sls {
//verbose_stream() << "hamming distance " << mk_bounded_pp(a, m) << " " << d << "\n";
return d;
}
else if (!is_true && m.is_eq(a, x, y) && bv.is_bv(x)) {
return 0;
}
else if (bv.is_ule(a, x, y)) {
auto const& vx = wval(x);
auto const& vy = wval(y);
@ -430,7 +443,6 @@ namespace sls {
rational n = m_ev.m_tmp3.get_value(vx.nw);
n /= rational(rational::power_of_two(vx.bw));
double dbl = n.get_double();
verbose_stream() << mk_bounded_pp(a, m) << " x:" <<vx << " y:" << vy << " " << dbl << "\n";
return (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl;
}
else if (is_true && m.is_distinct(a) && bv.is_bv(to_app(a)->get_arg(0))) {
@ -446,10 +458,6 @@ namespace sls {
}
return nd / np;
}
else {
verbose_stream() << "new score not implemented for " << mk_bounded_pp(a, m) << "\n";
NOT_IMPLEMENTED_YET();
}
return 0;
}

2
src/params/sls_params.pyg
View file

@ -25,7 +25,7 @@ def_module_params('sls',
('dt_axiomatic', BOOL, True, 'use axiomatic mode or model reduction for datatype solver'),
('track_unsat', BOOL, 0, 'keep a list of unsat assertions as done in SAT - currently disabled internally'),
('random_seed', UINT, 0, 'random seed'),
('bv_use_top_level_assertions', BOOL, False, 'use top-level assertions for BV lookahead solver'),
('bv_use_top_level_assertions', BOOL, True, 'use top-level assertions for BV lookahead solver'),
('bv_use_lookahead', BOOL, True, 'use lookahead solver for BV'),
('bv_allow_rotation', BOOL, True, 'allow model rotation when repairing literal assignment'),
('str_update_strategy', UINT, 1, 'string update candidate selection: 0 - single character based update, 1 - subsequence based update')