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

hm

Browse source
This commit is contained in:
Jakob Rath 2022-10-31 15:54:56 +01:00
parent 29695391de
commit e33f728128
1 changed files with 6 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -95,6 +95,12 @@ namespace polysat {
LOG("c_target: " << lit_pp(s, c_target)); LOG("c_target: " << lit_pp(s, c_target));
LOG("c_new: " << lit_pp(s, c_new)); LOG("c_new: " << lit_pp(s, c_new));
// New constraint is already true (maybe we already derived it previously?)
// TODO: It might make sense to keep different derivations of the same constraint.
// E.g., if the new clause could derive c_new at a lower decision level.
if (c_new.bvalue(s) == l_true)
continue;
clause_builder cb(s); clause_builder cb(s);
for (auto [w, wv] : a) for (auto [w, wv] : a)
cb.push(~s.eq(s.var(w), wv)); cb.push(~s.eq(s.var(w), wv));