mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-09 12:50:32 +00:00
Code Activity

remove redundant pre-condition

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-02-13 11:54:50 -08:00
parent 4f9b277c32
commit e07c77e072
1 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -749,7 +749,6 @@ namespace polysat {
if (a_parity != a_max_parity || (a_parity > 0 && saturation.min_parity(a1, explain_a_parity) < a_parity)) if (a_parity != a_max_parity || (a_parity > 0 && saturation.min_parity(a1, explain_a_parity) < a_parity))
return { p, false }; // We need the parity of a and this has to be for sure less than the parity of a1 return { p, false }; // We need the parity of a and this has to be for sure less than the parity of a1
pdd a_pi = s.pseudo_inv(a); pdd a_pi = s.pseudo_inv(a);
for (auto c : explain_a_parity) for (auto c : explain_a_parity)
precondition.insert_eval(~c); precondition.insert_eval(~c);
@ -758,6 +757,7 @@ namespace polysat {
return { b1, true }; return { b1, true };
pdd shift = a; // [nsb cr: should this be a1?] pdd shift = a; // [nsb cr: should this be a1?]
if (a_parity > 0) { if (a_parity > 0) {
@ -766,7 +766,8 @@ namespace polysat {
signed_constraint shift_right_left = s.eq(rational::power_of_two(a_parity) * shift, a1); signed_constraint shift_right_left = s.eq(rational::power_of_two(a_parity) * shift, a1);
s.add_clause(~least_parity, shift_right_left, true); s.add_clause(~least_parity, shift_right_left, true);
// s.add_clause(~shift_right_left, least_parity, true); Might be interesting as well [although not needed]; needs to consider special case 0 // s.add_clause(~shift_right_left, least_parity, true); Might be interesting as well [although not needed]; needs to consider special case 0
precondition.insert_eval(~shift_right_left); // [nsb cr: this pre-condition is already implied from the parity explanations]
// precondition.insert_eval(~shift_right_left);
} }
LOG("Forced elimination: " << a_pi * (-b) * shift + b1); LOG("Forced elimination: " << a_pi * (-b) * shift + b1);
LOG("a: " << a); LOG("a: " << a);