Skip to content

Commit 627f38b

Browse files
committed
Enable Wallace Tree multiplier for CaDiCaL
1 parent 36a3616 commit 627f38b

File tree

1 file changed

+3
-4
lines changed

1 file changed

+3
-4
lines changed

src/solvers/flattening/bv_utils.cpp

+3-4
Original file line numberDiff line numberDiff line change
@@ -798,7 +798,7 @@ bvt bv_utilst::wallace_tree(const std::vector<bvt> &pps)
798798

799799
bvt bv_utilst::unsigned_multiplier(const bvt &_op0, const bvt &_op1)
800800
{
801-
#if 1
801+
#ifndef SATCHECK_CADICAL
802802
bvt op0=_op0, op1=_op1;
803803

804804
if(is_constant(op1))
@@ -827,7 +827,7 @@ bvt bv_utilst::unsigned_multiplier(const bvt &_op0, const bvt &_op1)
827827
}
828828

829829
return product;
830-
#else
830+
#else
831831
// Wallace tree multiplier. This is disabled, as runtimes have
832832
// been observed to go up by 5%-10%, and on some models even by 20%.
833833

@@ -862,8 +862,7 @@ bvt bv_utilst::unsigned_multiplier(const bvt &_op0, const bvt &_op1)
862862
return zeros(op0.size());
863863
else
864864
return wallace_tree(pps);
865-
866-
#endif
865+
#endif
867866
}
868867

869868
bvt bv_utilst::unsigned_multiplier_no_overflow(

0 commit comments

Comments
 (0)