mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

minor

Browse source
This commit is contained in:
Jakob Rath 2023-02-22 16:30:57 +01:00
parent c76379c0cf
commit a8bfd01190
2 changed files with 10 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -34,23 +34,25 @@ namespace polysat {
void saturation::log_lemma(pvar v, conflict& core) {
IF_VERBOSE(2, {
auto const& cl = core.lemmas().back();
clause* cl = core.lemmas().back();
verbose_stream() << m_rule << " v" << v << " ";
for (auto lit : *cl)
verbose_stream() << s.lit2cnstr(lit) << " ";
verbose_stream() << " " << *cl << "\n";
IF_VERBOSE(15, {
for (auto lit : *cl)
verbose_stream() << " " << lit_pp(s, lit) << "\n";
});
});
}
void saturation::perform(pvar v, conflict& core) {
IF_VERBOSE(2, verbose_stream() << "v" << v << " " << core << "\n");
for (auto c : core)
//if (perform(v, c, core)) Why stop eagerly?
// return;
for (signed_constraint c : core)
perform(v, c, core);
}
bool saturation::perform(pvar v, signed_constraint const& c, conflict& core) {
bool saturation::perform(pvar v, signed_constraint c, conflict& core) {
if (c.is_currently_true(s))
return false;
@ -58,10 +60,10 @@ namespace polysat {
if (c->is_ule()) {
auto i = inequality::from_ule(c);
return try_inequality(v, i, core) | prop;
return try_inequality(v, i, core) || prop;
}
if (c->is_umul_ovfl())
return try_umul_ovfl(v, c, core) | prop;
return try_umul_ovfl(v, c, core) || prop;
return false;
}

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

@ -173,7 +173,7 @@ namespace polysat {
public:
saturation(solver& s);
void perform(pvar v, conflict& core);
bool perform(pvar v, signed_constraint const& sc, conflict& core);
bool perform(pvar v, signed_constraint sc, conflict& core);
};
/*