mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

Lemma names

Browse source
This commit is contained in:
Jakob Rath 2022-11-28 19:13:38 +01:00
parent 0c44391b9e
commit 4aa04fa475
6 changed files with 16 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -298,26 +298,27 @@ namespace polysat {
m_vars.insert(v); m_vars.insert(v);
} }
void conflict::add_lemma(std::initializer_list<signed_constraint> cs) { void conflict::add_lemma(char const* name, std::initializer_list<signed_constraint> cs) {
add_lemma(std::data(cs), cs.size()); add_lemma(name, std::data(cs), cs.size());
} }
void conflict::add_lemma(signed_constraint const* cs, size_t cs_len) { void conflict::add_lemma(char const* name, 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.insert_eval(cs[i]); cb.insert_eval(cs[i]);
add_lemma(cb.build()); add_lemma(name, cb.build());
} }
void conflict::add_lemma(clause_ref lemma) { void conflict::add_lemma(char const* name, clause_ref lemma) {
LOG_H3("Lemma " << (name ? name : "<unknown>") << ": " << show_deref(lemma));
SASSERT(lemma); SASSERT(lemma);
lemma->set_redundant(true); lemma->set_redundant(true);
LOG_H3("Lemma: " << *lemma);
for (sat::literal lit : *lemma) { for (sat::literal lit : *lemma) {
LOG(lit_pp(s, lit)); LOG(lit_pp(s, lit));
SASSERT(s.m_bvars.value(lit) != l_true); SASSERT(s.m_bvars.value(lit) != l_true);
} }
m_lemmas.push_back(std::move(lemma)); m_lemmas.push_back(std::move(lemma));
// TODO: pass to inference_logger (with name)
} }
void conflict::remove(signed_constraint c) { void conflict::remove(signed_constraint c) {

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

@ -160,9 +160,9 @@ namespace polysat {
void insert_eval(signed_constraint c); void insert_eval(signed_constraint c);
/** 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(char const* name, std::initializer_list<signed_constraint> cs);
void add_lemma(signed_constraint const* cs, size_t cs_len); void add_lemma(char const* name, signed_constraint const* cs, size_t cs_len);
void add_lemma(clause_ref lemma); void add_lemma(char const* name, clause_ref lemma);
/** Remove c from core */ /** Remove c from core */
void remove(signed_constraint c); void remove(signed_constraint c);

2
src/math/polysat/saturation.cpp
View file

@ -81,7 +81,7 @@ namespace polysat {
SASSERT(c.bvalue(s) != l_true); SASSERT(c.bvalue(s) != l_true);
m_lemma.insert(c); m_lemma.insert(c);
core.add_lemma(m_lemma.build()); // TODO: log with name m_rule core.add_lemma(m_rule, m_lemma.build());
return true; return true;
} }

10
src/math/polysat/superposition.cpp
View file

@ -72,23 +72,19 @@ namespace polysat {
SASSERT(c1.is_currently_true(s)); SASSERT(c1.is_currently_true(s));
SASSERT(c2.is_currently_false(s)); SASSERT(c2.is_currently_false(s));
SASSERT_EQ(c1.bvalue(s), l_true); SASSERT_EQ(c1.bvalue(s), l_true);
SASSERT(c2.bvalue(s) != l_false); SASSERT_EQ(c2.bvalue(s), l_true);
signed_constraint c = resolve1(v, c1, c2); signed_constraint c = resolve1(v, c1, c2);
if (!c) if (!c)
continue; continue;
SASSERT(c.is_currently_false(s)); SASSERT(c.is_currently_false(s));
// char const* inf_name = "?";
switch (c.bvalue(s)) { switch (c.bvalue(s)) {
case l_false: case l_false:
core.add_lemma({c, ~c1, ~c2}); core.add_lemma("superposition l_false", {c, ~c1, ~c2});
// core.log_inference(inference_sup("l_false", v, c2, c1));
return l_true; return l_true;
case l_undef: case l_undef:
// inf_name = "l_undef"; core.add_lemma("superposition l_undef", {c, ~c1, ~c2});
core.add_lemma({c, ~c1, ~c2});
// core.log_inference(inference_sup("l_undef lemma", v, c2, c1));
break; break;
case l_true: case l_true:
break; break;

2
src/math/polysat/variable_elimination.cpp
View file

@ -107,7 +107,7 @@ namespace polysat {
cb.insert(~c); cb.insert(~c);
cb.insert(~c_target); cb.insert(~c_target);
cb.insert(c_new); cb.insert(c_new);
core.add_lemma(cb.build()); core.add_lemma("variable elimination", cb.build());
} }
} }

2
src/math/polysat/viable.cpp
View file

@ -726,7 +726,7 @@ namespace polysat {
while (e != first); while (e != first);
SASSERT(all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) == l_false; })); SASSERT(all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) == l_false; }));
core.add_lemma(lemma.build()); core.add_lemma("viable", lemma.build());
core.logger().log(inf_fi(*this, v)); core.logger().log(inf_fi(*this, v));
return true; return true;
} }