mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

insert_eval?

Browse source
This commit is contained in:
Jakob Rath 2023-01-05 17:41:08 +01:00
parent aeb6138c25
commit 1002538565
2 changed files with 7 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/solver.cpp
View file

@ -904,6 +904,10 @@ namespace polysat {
if (m_bvars.is_true(lit)) // may happen if we only use the clause to justify a new constraint; it is not a real lemma
return std::nullopt;
if (!m_bvars.is_assigned(lit)) {
DEBUG_CODE({
if (lit2cnstr(lit).eval(*this) != l_undef)
LOG("WARNING: missed evaluation of literal: " << lit_pp(*this, lit));
});
SASSERT(!is_propagation);
is_propagation = true;
continue;

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

@ -697,15 +697,15 @@ namespace polysat {
pdd a_pi = get_pseudo_inverse(a, a_parity);
#else
pdd a_pi = s.pseudo_inv(a);
//precondition.insert(~s.eq(a_pi * a, rational::power_of_two(a_parity))); // TODO: This is unfortunately not a justification as the inverse might not be set yet (Can we make it to one?)
precondition.insert(~s.parity_at_most(a, a_parity));
//precondition.insert_eval(~s.eq(a_pi * a, rational::power_of_two(a_parity))); // TODO: This is unfortunately not a justification as the inverse might not be set yet (Can we make it to one?)
precondition.insert_eval(~s.parity_at_most(a, a_parity));
#endif
pdd shift = a;
if (a_parity > 0) {
shift = s.lshr(a1, a1.manager().mk_val(a_parity));
precondition.insert(~s.eq(rational::power_of_two(a_parity) * shift, a1)); // TODO: Or s.parity_at_least(a1, a_parity) but we want to reuse the variable introduced by the shift
precondition.insert_eval(~s.eq(rational::power_of_two(a_parity) * shift, a1)); // TODO: Or s.parity_at_least(a1, a_parity) but we want to reuse the variable introduced by the shift
}
LOG("Forced elimination: " << a_pi * (-b) * shift + b1);
LOG("a: " << a);