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

Add overload for conflict::add_lemma

Browse source
This commit is contained in:
Jakob Rath 2022-10-31 15:19:36 +01:00
parent 6a03df9017
commit 4cdd3bf77d
2 changed files with 12 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/math/polysat/conflict.cpp
View file

@ -329,14 +329,24 @@ namespace polysat {
m_vars.insert(v); m_vars.insert(v);
} }
void conflict::add_lemma(std::initializer_list<signed_constraint> cs) {
add_lemma(std::data(cs), cs.size());
}
void conflict::add_lemma(signed_constraint const* cs, size_t cs_len) { void conflict::add_lemma(signed_constraint const* cs, size_t cs_len) {
clause_builder cb(s); clause_builder cb(s);
for (size_t i = 0; i < cs_len; ++i) for (size_t i = 0; i < cs_len; ++i)
cb.push(cs[i]); cb.push(cs[i]);
clause_ref lemma = cb.build(); add_lemma(cb.build());
}
void conflict::add_lemma(clause_ref lemma) {
SASSERT(lemma); SASSERT(lemma);
lemma->set_redundant(true); lemma->set_redundant(true);
LOG("Side lemma: " << *lemma); LOG("Side lemma: " << *lemma);
for (sat::literal lit : *lemma) {
LOG(" " << lit_pp(s, lit));
}
m_lemmas.push_back(std::move(lemma)); m_lemmas.push_back(std::move(lemma));
// If possible, we should set the new constraint to l_true; // If possible, we should set the new constraint to l_true;
// and re-enable the assertions marked with "tag:true_by_side_lemma". // and re-enable the assertions marked with "tag:true_by_side_lemma".
@ -348,10 +358,6 @@ namespace polysat {
// - l_false constraints are disallowed in the conflict (as before). // - l_false constraints are disallowed in the conflict (as before).
} }
void conflict::add_lemma(std::initializer_list<signed_constraint> cs) {
add_lemma(std::data(cs), cs.size());
}
#if 0 #if 0
void conflict::bool_propagate(signed_constraint c, signed_constraint const* premises, unsigned premises_len) { void conflict::bool_propagate(signed_constraint c, signed_constraint const* premises, unsigned premises_len) {
if (c.is_always_false()) { if (c.is_always_false()) {

1
src/math/polysat/conflict.h
View file

@ -202,6 +202,7 @@ namespace polysat {
/** Add a side lemma to the conflict; to be learned in addition to the main lemma after conflict resolution finishes. */ /** Add a side lemma to the conflict; to be learned in addition to the main lemma after conflict resolution finishes. */
void add_lemma(std::initializer_list<signed_constraint> cs); void add_lemma(std::initializer_list<signed_constraint> cs);
void add_lemma(signed_constraint const* cs, size_t cs_len); void add_lemma(signed_constraint const* cs, size_t cs_len);
void add_lemma(clause_ref lemma);
#if 0 #if 0
/** /**