mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-08 07:15:07 +00:00
Code Activity

adding the learned clauses from the internalizer

Browse source
This commit is contained in:
Ilana Shapiro 2025-10-29 16:06:26 -07:00
parent f315cac0cd
commit cea52f493a
3 changed files with 20 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/smt_context.cpp
View file

@ -82,7 +82,8 @@ namespace smt {
m_mk_bool_var_trail(*this), m_mk_bool_var_trail(*this),
m_mk_enode_trail(*this), m_mk_enode_trail(*this),
m_mk_lambda_trail(*this), m_mk_lambda_trail(*this),
m_lemma_visitor(m) { m_lemma_visitor(m),
m_recorded_clauses(m) {
SASSERT(m_scope_lvl == 0); SASSERT(m_scope_lvl == 0);
SASSERT(m_base_lvl == 0); SASSERT(m_base_lvl == 0);

3
src/smt/smt_context.h
View file

@ -137,6 +137,7 @@ namespace smt {
scoped_ptr<base_dependent_expr_state> m_fmls; scoped_ptr<base_dependent_expr_state> m_fmls;
svector<double> m_lit_scores[2]; svector<double> m_lit_scores[2];
expr_ref_vector m_recorded_clauses;
// ----------------------------------- // -----------------------------------
@ -1301,6 +1302,8 @@ namespace smt {
void add_scores(unsigned n, literal const *lits); void add_scores(unsigned n, literal const *lits);
void record_clause(clause const* cls);
// ----------------------------------- // -----------------------------------
// //

15
src/smt/smt_internalizer.cpp
View file

@ -936,6 +936,7 @@ namespace smt {
m_lit_scores[0].reserve(v + 1); m_lit_scores[0].reserve(v + 1);
m_lit_scores[1].reserve(v + 1); m_lit_scores[1].reserve(v + 1);
m_lit_scores[0][v] = m_lit_scores[1][v] = 0.0; m_lit_scores[0][v] = m_lit_scores[1][v] = 0.0;
m_recorded_clauses.reserve(v + 1);
literal l(v, false); literal l(v, false);
literal not_l(v, true); literal not_l(v, true);
@ -965,6 +966,19 @@ namespace smt {
return v; return v;
} }
// following the pattern of solver::persist_clause in src/sat/smt/user_solver.cpp
void context::record_clause(clause const* cls) {
expr_ref_vector clause(m);
for (unsigned i = 0; i < cls->get_num_literals(); ++i) {
literal lit = cls->get_literal(i);
clause.push_back(literal2expr(~lit));
}
if (!clause.empty() && m.is_false(clause.back()))
clause.pop_back();
expr_ref disj(m.mk_or(clause.size(), clause.data()), m);
m_recorded_clauses.push_back(disj);
}
void context::add_scores(unsigned n, literal const *lits) { void context::add_scores(unsigned n, literal const *lits) {
for (unsigned i = 0; i < n; ++i) { for (unsigned i = 0; i < n; ++i) {
auto lit = lits[i]; auto lit = lits[i];
@ -1492,6 +1506,7 @@ namespace smt {
if (k == CLS_LEARNED) { if (k == CLS_LEARNED) {
int w2_idx = select_learned_watch_lit(cls); int w2_idx = select_learned_watch_lit(cls);
cls->swap_lits(1, w2_idx); cls->swap_lits(1, w2_idx);
record_clause(cls);
} }
else { else {
SASSERT(k == CLS_TH_LEMMA); SASSERT(k == CLS_TH_LEMMA);