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

optimization of sls-arith and fix build warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-01-12 09:49:48 -08:00
parent 49dba337f7
commit b780b54574
3 changed files with 22 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/rewriter.h
View file

@ -189,7 +189,7 @@ public:
*/ */
class inv_var_shifter : public var_shifter_core { class inv_var_shifter : public var_shifter_core {
protected: protected:
unsigned m_shift; unsigned m_shift = 0;
void process_var(var * v) override; void process_var(var * v) override;
public: public:
inv_var_shifter(ast_manager & m):var_shifter_core(m) {} inv_var_shifter(ast_manager & m):var_shifter_core(m) {}

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

@ -2372,8 +2372,10 @@ namespace sls {
template<typename num_t> template<typename num_t>
typename arith_base<num_t>::bool_info& arith_base<num_t>::get_bool_info(expr* e) { typename arith_base<num_t>::bool_info& arith_base<num_t>::get_bool_info(expr* e) {
m_bool_info.reserve(e->get_id() + 1, bool_info(m_config.paws_init)); unsigned id = e->get_id();
return m_bool_info[e->get_id()]; if (id >= m_bool_info.size())
m_bool_info.reserve(id + 1, bool_info(m_config.paws_init));
return m_bool_info[id];
} }
template<typename num_t> template<typename num_t>
@ -2648,10 +2650,6 @@ namespace sls {
void arith_base<num_t>::lookahead_num(var_t v, num_t const& delta) { void arith_base<num_t>::lookahead_num(var_t v, num_t const& delta) {
num_t old_value = value(v); num_t old_value = value(v);
if (!update_num(v, delta))
return;
num_t new_value = old_value + delta;
expr* e = m_vars[v].m_expr; expr* e = m_vars[v].m_expr;
if (m_last_expr != e) { if (m_last_expr != e) {
if (m_last_expr) if (m_last_expr)
@ -2660,6 +2658,14 @@ namespace sls {
insert_update_stack_rec(e); insert_update_stack_rec(e);
m_last_expr = e; m_last_expr = e;
} }
else if (m_last_delta == delta)
return;
m_last_delta = delta;
num_t new_value = old_value + delta;
if (!update_num(v, delta))
return;
auto score = lookahead(e, false); auto score = lookahead(e, false);
TRACE("arith_verbose", tout << "lookahead " << v << " " << mk_bounded_pp(e, m) << " := " << delta + old_value << " " << score << " (" << m_best_score << ")\n";); TRACE("arith_verbose", tout << "lookahead " << v << " " << mk_bounded_pp(e, m) << " := " << delta + old_value << " " << score << " (" << m_best_score << ")\n";);
if (score > m_best_score) { if (score > m_best_score) {
@ -2844,7 +2850,7 @@ namespace sls {
add_lookahead(info, vars[(start + i) % sz]); add_lookahead(info, vars[(start + i) % sz]);
if (m_updates.empty()) if (m_updates.empty())
return false; return false;
std::stable_sort(m_updates.begin(), m_updates.end(), [](auto const& a, auto const& b) { return a.m_var < b.m_var; }); std::stable_sort(m_updates.begin(), m_updates.end(), [](auto const& a, auto const& b) { return a.m_var < b.m_var || (a.m_var == b.m_var && a.m_delta < b.m_delta); });
m_last_expr = nullptr; m_last_expr = nullptr;
sz = m_updates.size(); sz = m_updates.size();
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {

9
src/ast/sls/sls_seq_plugin.cpp
View file

@ -380,6 +380,7 @@ namespace sls {
return ev.val0.svalue; return ev.val0.svalue;
} }
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
return ev.val0.svalue;
} }
case OP_SEQ_EMPTY: { case OP_SEQ_EMPTY: {
ev.val0.svalue = zstring(); ev.val0.svalue = zstring();
@ -626,8 +627,8 @@ namespace sls {
IF_VERBOSE(3, verbose_stream() << is_true << ": " << mk_bounded_pp(e, m, 3) << "\n"); IF_VERBOSE(3, verbose_stream() << is_true << ": " << mk_bounded_pp(e, m, 3) << "\n");
if (ctx.is_true(e)) { if (ctx.is_true(e)) {
// equality // equality
if (false && ctx.rand(2) != 0 && repair_down_str_eq_edit_distance_incremental(e)) //if (false && ctx.rand(2) != 0 && repair_down_str_eq_edit_distance_incremental(e))
return true; // return true;
if (ctx.rand(2) != 0 && repair_down_str_eq_edit_distance(e)) if (ctx.rand(2) != 0 && repair_down_str_eq_edit_distance(e))
return true; return true;
if (ctx.rand(2) != 0 && repair_down_str_eq_unify(e)) if (ctx.rand(2) != 0 && repair_down_str_eq_unify(e))
@ -693,7 +694,7 @@ namespace sls {
hashtable<zstring, zstring_hash_proc, default_eq<zstring>> set; hashtable<zstring, zstring_hash_proc, default_eq<zstring>> set;
set.insert(zstring("")); set.insert(zstring(""));
for (unsigned i = 0; i < val_other.length(); ++i) { for (unsigned i = 0; i < val_other.length(); ++i) {
for (unsigned j = val_other.length(); j > 0; ++j) { for (unsigned j = val_other.length(); j-- > 0; ) {
zstring sub = val_other.extract(i, j); zstring sub = val_other.extract(i, j);
if (set.contains(sub)) if (set.contains(sub))
break; break;
@ -1890,6 +1891,8 @@ namespace sls {
if (min_length < UINT_MAX && s.length() < str.length()) { if (min_length < UINT_MAX && s.length() < str.length()) {
// reward small lengths // reward small lengths
// penalize size differences (unless min_length decreases) // penalize size differences (unless min_length decreases)
// TODO: fix this. this is pow(2.0, min_length - current_min_length) for double precision
// but heuristic could be reconsidered
score = 1 << (current_min_length - min_length); score = 1 << (current_min_length - min_length);
score /= ((double)abs((int)s.length() - (int)str.length()) + 1); score /= ((double)abs((int)s.length() - (int)str.length()) + 1);
} }