mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-29 07:27:57 +00:00
Code Activity

add score access and reset

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-07-23 15:32:49 -07:00
parent 20b9690b01
commit ac857aaf72
2 changed files with 19 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/smt_context.h
View file

@ -189,6 +189,7 @@ namespace smt {
unsigned_vector m_lit_occs; //!< occurrence count of literals
svector<bool_var_data> m_bdata; //!< mapping bool_var -> data
svector<double> m_activity;
svector<double[2]> m_scores;
clause_vector m_aux_clauses;
clause_vector m_lemmas;
vector<clause_vector> m_clauses_to_reinit;
@ -929,6 +930,13 @@ namespace smt {
ast_pp_util m_lemma_visitor;
void dump_lemma(unsigned n, literal const* lits);
void dump_axiom(unsigned n, literal const* lits);
void add_scores(unsigned n, literal const* lits);
void reset_scores() {
for (auto& s : m_scores) s[0] = s[1] = 0.0;
}
double get_score(literal l) const {
return m_scores[l.var()][l.sign()];
}
public:
void ensure_internalized(expr* e);

11
src/smt/smt_internalizer.cpp
View file

@ -928,6 +928,8 @@ namespace smt {
set_bool_var(id, v);
m_bdata.reserve(v+1);
m_activity.reserve(v+1);
m_scores.reserve(v + 1);
m_scores[v][0] = m_scores[v][1] = 0.0;
m_bool_var2expr.reserve(v+1);
m_bool_var2expr[v] = n;
literal l(v, false);
@ -1416,6 +1418,7 @@ namespace smt {
break;
case CLS_LEARNED:
dump_lemma(num_lits, lits);
add_scores(num_lits, lits);
break;
default:
break;
@ -1524,6 +1527,14 @@ namespace smt {
}}
}
void context::add_scores(unsigned n, literal const* lits) {
for (unsigned i = 0; i < n; ++i) {
auto lit = lits[i];
unsigned v = lit.var();
m_scores[v][lit.sign()] += 1.0 / n;
}
}
void context::dump_axiom(unsigned n, literal const* lits) {
if (m_fparams.m_axioms2files) {
literal_buffer tmp;