mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

avoid repeated clauses during scoring function

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-23 10:51:12 -08:00
parent b149d1f803
commit ce615ee116
2 changed files with 13 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/ast/sls/sls_arith_clausal.cpp
View file

@ -222,7 +222,7 @@ namespace sls {
for (auto const& u : a.m_updates)
lookahead(u.m_var, u.m_delta);
// verbose_stream() << a.m_updates.size() << " " << m_num_lookaheads << " lookaheads\n";
// verbose_stream() << a.m_updates.size() << " " << m_num_lookaheads << " lookaheads\n";
ctx.rlimit().inc(1 + m_num_lookaheads);
critical_move(m_best_var, m_best_delta, mt);
return m_best_var;
@ -300,9 +300,16 @@ namespace sls {
if (!a.update_num(v, delta))
return -1;
double score = 0;
m_tmp_nat_set.reset();
m_tmp_nat_set.assure_domain(ctx.clauses().size() + 1);
for (auto bv : vi.m_bool_vars_of) {
for (auto lit : { sat::literal(bv, false), sat::literal(bv, true) }) {
for (auto ci : ctx.get_use_list(lit)) {
for (auto ci : ctx.get_use_list(lit)) {
if (m_tmp_nat_set.contains(ci)) {
continue;
}
m_tmp_nat_set.insert(ci);
auto const& c = ctx.get_clause(ci);
unsigned num_true = 0;
for (auto lit : c) {

4
src/ast/sls/sls_arith_clausal.h
View file

@ -19,10 +19,12 @@ Author:
#include "util/checked_int64.h"
#include "util/optional.h"
#include "util/nat_set.h"
#include "ast/ast_trail.h"
#include "ast/arith_decl_plugin.h"
#include "ast/sls/sls_context.h"
namespace sls {
template<typename num_t>
@ -78,6 +80,8 @@ namespace sls {
unsigned m_best_last_step = 0;
unsigned m_num_lookaheads = 0;
nat_set m_tmp_nat_set;
// avoid checking the same updates twice
var_t m_last_var = UINT_MAX;
num_t m_last_delta;