From d552f917472d1d41d005e8bef89003dad38b823b Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 8 Feb 2026 20:14:45 -0800 Subject: [PATCH] use power_exprt in boolbvt This replaces the use of binary_exprt in boolbvt by the more specific power_exprt. --- src/solvers/flattening/boolbv.cpp | 3 ++- src/solvers/flattening/boolbv.h | 3 ++- src/solvers/flattening/boolbv_power.cpp | 13 +++++++------ 3 files changed, 11 insertions(+), 8 deletions(-) diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 3cbeca98a76..94813350942 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -233,7 +234,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr) else if(expr.id()==ID_not) return convert_not(to_not_expr(expr)); else if(expr.id()==ID_power) - return convert_power(to_binary_expr(expr)); + return convert_power(to_power_expr(expr)); else if(expr.id() == ID_popcount) return convert_popcount(to_popcount_expr(expr)); else if(expr.id() == ID_count_leading_zeros) diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 8a452fe9405..ccb080c38a7 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -38,6 +38,7 @@ class floatbv_typecast_exprt; class ieee_float_op_exprt; class overflow_result_exprt; class popcount_exprt; +class power_exprt; class replication_exprt; class unary_overflow_exprt; class union_typet; @@ -198,7 +199,7 @@ class boolbvt:public arrayst virtual bvt convert_symbol(const exprt &expr); virtual bvt convert_bv_reduction(const unary_exprt &expr); virtual bvt convert_not(const not_exprt &expr); - virtual bvt convert_power(const binary_exprt &expr); + virtual bvt convert_power(const power_exprt &expr); virtual bvt convert_function_application( const function_application_exprt &expr); virtual bvt convert_bitreverse(const bitreverse_exprt &expr); diff --git a/src/solvers/flattening/boolbv_power.cpp b/src/solvers/flattening/boolbv_power.cpp index c614e2773c0..1364f4ddf07 100644 --- a/src/solvers/flattening/boolbv_power.cpp +++ b/src/solvers/flattening/boolbv_power.cpp @@ -6,10 +6,11 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +#include #include "boolbv.h" -bvt boolbvt::convert_power(const binary_exprt &expr) +bvt boolbvt::convert_power(const power_exprt &expr) { const typet &type = expr.type(); @@ -19,14 +20,14 @@ bvt boolbvt::convert_power(const binary_exprt &expr) type.id()==ID_signedbv) { // Let's do the special case 2**x - bvt op0=convert_bv(expr.op0()); - bvt op1=convert_bv(expr.op1()); + bvt base = convert_bv(expr.base()); + bvt exponent = convert_bv(expr.exponent()); - literalt eq_2= - bv_utils.equal(op0, bv_utils.build_constant(2, op0.size())); + literalt eq_2 = + bv_utils.equal(base, bv_utils.build_constant(2, base.size())); bvt one=bv_utils.build_constant(1, width); - bvt shift=bv_utils.shift(one, bv_utilst::shiftt::SHIFT_LEFT, op1); + bvt shift = bv_utils.shift(one, bv_utilst::shiftt::SHIFT_LEFT, exponent); bvt nondet=prop.new_variables(width);