mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

Make it compile again

Browse source
This commit is contained in:
Clemens Eisenhofer 2022-11-20 17:34:37 +01:00
parent 4f4d56eb91
commit 5240a8382a
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -132,9 +132,9 @@ namespace polysat {
if (new_var) {
s.add_clause(s.eq(s.var(pv2), s.shl(m.one(), s.var(pv))), false);
}
#elif 1
#elif 0
// computing the complete function by hamming-distance
get_hamming_distance();
//get_hamming_distance();
#else
// Naive approach with bit-and
// (pv = k && pv2 = 2^k) <==> ((v & (2^(k + 1) - 1)) = 2^k)
@ -165,7 +165,7 @@ namespace polysat {
if (p.is_val()) {
rational pv(p.val().trailing_zeros());
rational pv2 = rational::power_of_two(p.val().trailing_zeros());
return { m.mk_val(pv), m.mk_val(pv2) };
return { p.manager().mk_val(pv), p.manager().mk_val(pv2) };
}
pvar v = p.var();