mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 01:18:45 +00:00
Code Activity

use learned vs relevant distinction for theory lemmas

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-02-03 13:40:06 -08:00
parent a513488c54
commit ef7893cdca
11 changed files with 26 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/dyn_ack.cpp
View file

@ -431,7 +431,7 @@ namespace smt {
justification * js = nullptr; justification * js = nullptr;
if (m.proofs_enabled()) if (m.proofs_enabled())
js = alloc(dyn_ack_cc_justification, n1, n2); js = alloc(dyn_ack_cc_justification, n1, n2);
clause * cls = m_context.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA, del_eh); clause * cls = m_context.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA_RELEVANT, del_eh);
if (!cls) { if (!cls) {
dealloc(del_eh); dealloc(del_eh);
return; return;
@ -490,7 +490,7 @@ namespace smt {
ctx.mark_as_relevant(eq1); ctx.mark_as_relevant(eq1);
ctx.mark_as_relevant(eq2); ctx.mark_as_relevant(eq2);
ctx.mark_as_relevant(eq3); ctx.mark_as_relevant(eq3);
clause* cls = ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA, del_eh); clause* cls = ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA_RELEVANT, del_eh);
if (!cls) { if (!cls) {
dealloc(del_eh); dealloc(del_eh);
return; return;

12
src/smt/smt_clause.h
View file

@ -41,11 +41,13 @@ namespace smt {
CLS_AUX, // an input assumption CLS_AUX, // an input assumption
CLS_TH_AXIOM, // a theory axiom CLS_TH_AXIOM, // a theory axiom
CLS_LEARNED, // learned through conflict resolution CLS_LEARNED, // learned through conflict resolution
CLS_TH_LEMMA // a theory lemma CLS_TH_LEMMA_RELEVANT, // a theory lemma, atoms are reinitialzed as relevant for theory propagation
CLS_TH_LEMMA_LEARNED // a theory lemma, lemma is replayed for Boolean propagation.
}; };
inline bool is_axiom(clause_kind k) { return k == CLS_AUX || k == CLS_TH_AXIOM; } inline bool is_axiom(clause_kind k) { return k == CLS_AUX || k == CLS_TH_AXIOM; }
inline bool is_lemma(clause_kind k) { return k == CLS_LEARNED || k == CLS_TH_LEMMA; } inline bool is_lemma(clause_kind k) { return k == CLS_LEARNED || k == CLS_TH_LEMMA_RELEVANT || k == CLS_TH_LEMMA_LEARNED; }
inline bool is_th_lemma(clause_kind k) { return k == CLS_TH_LEMMA_RELEVANT || k == CLS_TH_LEMMA_LEARNED; }
/** /**
\brief A SMT clause. \brief A SMT clause.
@ -54,8 +56,8 @@ namespace smt {
*/ */
class clause { class clause {
unsigned m_num_literals; unsigned m_num_literals;
unsigned m_capacity:24; //!< some of the clause literals can be simplified and removed, this field contains the original number of literals (used for GC). unsigned m_capacity:23; //!< some of the clause literals can be simplified and removed, this field contains the original number of literals (used for GC).
unsigned m_kind:2; //!< kind unsigned m_kind:3; //!< kind
unsigned m_reinit:1; //!< true if the clause is in the reinit stack (only for learned clauses and aux_lemmas) unsigned m_reinit:1; //!< true if the clause is in the reinit stack (only for learned clauses and aux_lemmas)
unsigned m_reinternalize_atoms:1; //!< true if atoms must be reinitialized during reinitialization unsigned m_reinternalize_atoms:1; //!< true if atoms must be reinitialized during reinitialization
unsigned m_has_atoms:1; //!< true if the clause has memory space for storing atoms. unsigned m_has_atoms:1; //!< true if the clause has memory space for storing atoms.
@ -169,7 +171,7 @@ namespace smt {
} }
bool is_th_lemma() const { bool is_th_lemma() const {
return get_kind() == CLS_TH_LEMMA; return smt::is_th_lemma(get_kind());
} }

3
src/smt/smt_clause_proof.cpp
View file

@ -51,7 +51,8 @@ namespace smt {
return status::th_assumption; return status::th_assumption;
case CLS_LEARNED: case CLS_LEARNED:
return status::lemma; return status::lemma;
case CLS_TH_LEMMA: case CLS_TH_LEMMA_LEARNED:
case CLS_TH_LEMMA_RELEVANT:
return status::th_lemma; return status::th_lemma;
default: default:
UNREACHABLE(); UNREACHABLE();

4
src/smt/smt_context.cpp
View file

@ -2321,7 +2321,7 @@ namespace smt {
}); });
literal l(v, sign); literal l(v, sign);
cls->set_literal(j, l); cls->set_literal(j, l);
if (cls->get_kind() == CLS_TH_LEMMA) if (cls->get_kind() == CLS_TH_LEMMA_RELEVANT)
mark_as_relevant(l); mark_as_relevant(l);
} }
SASSERT(ilvl <= m_scope_lvl); SASSERT(ilvl <= m_scope_lvl);
@ -2351,7 +2351,7 @@ namespace smt {
SASSERT(!cls->reinternalize_atoms()); SASSERT(!cls->reinternalize_atoms());
literal l1 = cls->get_literal(0); literal l1 = cls->get_literal(0);
literal l2 = cls->get_literal(1); literal l2 = cls->get_literal(1);
if (cls->get_kind() == CLS_TH_LEMMA) { if (cls->get_kind() == CLS_TH_LEMMA_RELEVANT) {
mark_as_relevant(l1); mark_as_relevant(l1);
mark_as_relevant(l2); mark_as_relevant(l2);
} }

2
src/smt/smt_context.h
View file

@ -971,7 +971,7 @@ namespace smt {
} }
void mk_th_lemma(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params = 0, parameter * params = nullptr) { void mk_th_lemma(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params = 0, parameter * params = nullptr) {
mk_th_clause(tid, num_lits, lits, num_params, params, CLS_TH_LEMMA); mk_th_clause(tid, num_lits, lits, num_params, params, CLS_TH_LEMMA_RELEVANT);
} }
void mk_th_lemma(theory_id tid, literal_vector const& ls, unsigned num_params = 0, parameter * params = nullptr) { void mk_th_lemma(theory_id tid, literal_vector const& ls, unsigned num_params = 0, parameter * params = nullptr) {

9
src/smt/smt_internalizer.cpp
View file

@ -1399,7 +1399,8 @@ namespace smt {
} }
break; break;
} }
case CLS_TH_LEMMA: case CLS_TH_LEMMA_RELEVANT:
case CLS_TH_LEMMA_LEARNED:
dump_lemma(num_lits, lits); dump_lemma(num_lits, lits);
if (!simplify_aux_lemma_literals(num_lits, lits)) { if (!simplify_aux_lemma_literals(num_lits, lits)) {
if (j && !j->in_region()) { if (j && !j->in_region()) {
@ -1474,7 +1475,7 @@ namespace smt {
cls->swap_lits(1, w2_idx); cls->swap_lits(1, w2_idx);
} }
else { else {
SASSERT(k == CLS_TH_LEMMA); SASSERT(is_th_lemma(k));
int w1_idx = select_watch_lit(cls, 0); int w1_idx = select_watch_lit(cls, 0);
cls->swap_lits(0, w1_idx); cls->swap_lits(0, w1_idx);
int w2_idx = select_watch_lit(cls, 1); int w2_idx = select_watch_lit(cls, 1);
@ -1487,14 +1488,14 @@ namespace smt {
add_watch_literal(cls, 1); add_watch_literal(cls, 1);
if (get_assignment(cls->get_literal(0)) == l_false) { if (get_assignment(cls->get_literal(0)) == l_false) {
set_conflict(b_justification(cls)); set_conflict(b_justification(cls));
if (k == CLS_TH_LEMMA && m_scope_lvl > m_base_lvl) { if (is_th_lemma(k) && m_scope_lvl > m_base_lvl) {
reinit = true; reinit = true;
iscope_lvl = m_scope_lvl; iscope_lvl = m_scope_lvl;
} }
} }
else if (get_assignment(cls->get_literal(1)) == l_false) { else if (get_assignment(cls->get_literal(1)) == l_false) {
assign(cls->get_literal(0), b_justification(cls)); assign(cls->get_literal(0), b_justification(cls));
if (k == CLS_TH_LEMMA && m_scope_lvl > m_base_lvl) { if (is_th_lemma(k) && m_scope_lvl > m_base_lvl) {
reinit = true; reinit = true;
iscope_lvl = m_scope_lvl; iscope_lvl = m_scope_lvl;
} }

2
src/smt/theory_arith_core.h
View file

@ -3008,7 +3008,7 @@ namespace smt {
if (proofs_enabled()) if (proofs_enabled())
js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.data(), js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.data(),
ante.num_params(), ante.params("assign-bounds")); ante.num_params(), ante.params("assign-bounds"));
ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA, nullptr); ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA_LEARNED, nullptr);
} }
else { else {
ctx.assign(l, ctx.mk_justification( ctx.assign(l, ctx.mk_justification(

2
src/smt/theory_arith_int.h
View file

@ -677,7 +677,7 @@ namespace smt {
ante.eqs().size(), ante.eqs().data(), ante, l)); ante.eqs().size(), ante.eqs().data(), ante, l));
if (l == false_literal) if (l == false_literal)
ctx.mk_clause(0, nullptr, js, CLS_TH_LEMMA, nullptr); ctx.mk_clause(0, nullptr, js, CLS_TH_LEMMA_LEARNED, nullptr);
else else
ctx.assign(l, js); ctx.assign(l, js);
return true; return true;

2
src/smt/theory_diff_logic_def.h
View file

@ -664,7 +664,7 @@ void theory_diff_logic<Ext>::new_edge(dl_var src, dl_var dst, unsigned num_edges
lits.size(), lits.data(), lits.size(), lits.data(),
params.size(), params.data()); params.size(), params.data());
} }
ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA, nullptr); ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA_LEARNED, nullptr);
#if 0 #if 0
TRACE("arith", TRACE("arith",

4
src/smt/theory_lra.cpp
View file

@ -2399,7 +2399,7 @@ public:
VERIFY(validate_assign(lit)); VERIFY(validate_assign(lit));
if (params().m_arith_dump_lemmas) if (params().m_arith_dump_lemmas)
dump_assign_lemma(lit); dump_assign_lemma(lit);
if (false && core.size() < small_lemma_size() && eqs.empty()) { if (core.size() < small_lemma_size() && eqs.empty()) {
m_core2.reset(); m_core2.reset();
for (auto const& c : core) { for (auto const& c : core) {
m_core2.push_back(~c); m_core2.push_back(~c);
@ -2410,7 +2410,7 @@ public:
js = alloc(theory_lemma_justification, get_id(), ctx(), m_core2.size(), m_core2.data(), js = alloc(theory_lemma_justification, get_id(), ctx(), m_core2.size(), m_core2.data(),
ps.size(), ps.data()); ps.size(), ps.data());
} }
ctx().mk_clause(m_core2.size(), m_core2.data(), js, CLS_TH_LEMMA, nullptr); ctx().mk_clause(m_core2.size(), m_core2.data(), js, CLS_TH_LEMMA_LEARNED, nullptr);
} }
else { else {
ctx().assign( ctx().assign(

4
src/smt/theory_pb.cpp
View file

@ -936,7 +936,7 @@ namespace smt {
if (proofs_enabled()) { if (proofs_enabled()) {
js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.data()); js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.data());
} }
ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA, nullptr); ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA_LEARNED, nullptr);
} }
SASSERT(ctx.inconsistent()); SASSERT(ctx.inconsistent());
} }
@ -1518,7 +1518,7 @@ namespace smt {
if (proofs_enabled()) { if (proofs_enabled()) {
js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.data()); js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.data());
} }
ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA, nullptr); ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA_LEARNED, nullptr);
} }