@@ -813,10 +813,9 @@ std::string expr2ct::convert_trinary(
813
813
if (src.operands ().size ()!=3 )
814
814
return convert_norep (src, precedence);
815
815
816
- const exprt::operandst &operands=src.operands ();
817
- const exprt &op0=operands.front ();
818
- const exprt &op1=*(++operands.begin ());
819
- const exprt &op2=operands.back ();
816
+ const exprt &op0=src.op0 ();
817
+ const exprt &op1=src.op1 ();
818
+ const exprt &op2=src.op2 ();
820
819
821
820
unsigned p0, p1, p2;
822
821
@@ -1028,6 +1027,61 @@ std::string expr2ct::convert_binary(
1028
1027
const std::string &symbol,
1029
1028
unsigned precedence,
1030
1029
bool full_parentheses)
1030
+ {
1031
+ if (src.operands ().size ()!=2 )
1032
+ return convert_norep (src, precedence);
1033
+
1034
+ const exprt &op0=src.op0 ();
1035
+ const exprt &op1=src.op1 ();
1036
+
1037
+ unsigned p0, p1;
1038
+
1039
+ std::string s_op0=convert_with_precedence (op0, p0);
1040
+ std::string s_op1=convert_with_precedence (op1, p1);
1041
+
1042
+ std::string dest;
1043
+
1044
+ // In pointer arithmetic, x+(y-z) is unfortunately
1045
+ // not the same as (x+y)-z, even though + and -
1046
+ // have the same precedence. We thus add parentheses
1047
+ // for the case x+(y-z). Similarly, (x*y)/z is not
1048
+ // the same as x*(y/z), but * and / have the same
1049
+ // precedence.
1050
+
1051
+ bool use_parentheses0=
1052
+ precedence>p0 ||
1053
+ (precedence==p0 && full_parentheses) ||
1054
+ (precedence==p0 && src.id ()!=op0.id ());
1055
+
1056
+ if (use_parentheses0)
1057
+ dest+=' (' ;
1058
+ dest+=s_op0;
1059
+ if (use_parentheses0)
1060
+ dest+=' )' ;
1061
+
1062
+ dest+=' ' ;
1063
+ dest+=symbol;
1064
+ dest+=' ' ;
1065
+
1066
+ bool use_parentheses1=
1067
+ precedence>p1 ||
1068
+ (precedence==p1 && full_parentheses) ||
1069
+ (precedence==p1 && src.id ()!=op1.id ());
1070
+
1071
+ if (use_parentheses1)
1072
+ dest+=' (' ;
1073
+ dest+=s_op1;
1074
+ if (use_parentheses1)
1075
+ dest+=' )' ;
1076
+
1077
+ return dest;
1078
+ }
1079
+
1080
+ std::string expr2ct::convert_multi_ary (
1081
+ const exprt &src,
1082
+ const std::string &symbol,
1083
+ unsigned precedence,
1084
+ bool full_parentheses)
1031
1085
{
1032
1086
if (src.operands ().size ()<2 )
1033
1087
return convert_norep (src, precedence);
@@ -3386,7 +3440,7 @@ std::string expr2ct::convert_with_precedence(
3386
3440
precedence=16 ;
3387
3441
3388
3442
if (src.id ()==ID_plus)
3389
- return convert_binary (src, " +" , precedence=12 , false );
3443
+ return convert_multi_ary (src, " +" , precedence=12 , false );
3390
3444
3391
3445
else if (src.id ()==ID_minus)
3392
3446
return convert_binary (src, " -" , precedence=12 , true );
@@ -3690,7 +3744,7 @@ std::string expr2ct::convert_with_precedence(
3690
3744
return convert_unary (src, " ~" , precedence=15 );
3691
3745
3692
3746
else if (src.id ()==ID_mult)
3693
- return convert_binary (src, " *" , precedence=13 , false );
3747
+ return convert_multi_ary (src, " *" , precedence=13 , false );
3694
3748
3695
3749
else if (src.id ()==ID_div)
3696
3750
return convert_binary (src, " /" , precedence=13 , true );
@@ -3739,22 +3793,22 @@ std::string expr2ct::convert_with_precedence(
3739
3793
return convert_complex (src, precedence=16 );
3740
3794
3741
3795
else if (src.id ()==ID_bitand)
3742
- return convert_binary (src, " &" , precedence=8 , false );
3796
+ return convert_multi_ary (src, " &" , precedence=8 , false );
3743
3797
3744
3798
else if (src.id ()==ID_bitxor)
3745
- return convert_binary (src, " ^" , precedence=7 , false );
3799
+ return convert_multi_ary (src, " ^" , precedence=7 , false );
3746
3800
3747
3801
else if (src.id ()==ID_bitor)
3748
- return convert_binary (src, " |" , precedence=6 , false );
3802
+ return convert_multi_ary (src, " |" , precedence=6 , false );
3749
3803
3750
3804
else if (src.id ()==ID_and)
3751
- return convert_binary (src, " &&" , precedence=5 , false );
3805
+ return convert_multi_ary (src, " &&" , precedence=5 , false );
3752
3806
3753
3807
else if (src.id ()==ID_or)
3754
- return convert_binary (src, " ||" , precedence=4 , false );
3808
+ return convert_multi_ary (src, " ||" , precedence=4 , false );
3755
3809
3756
3810
else if (src.id ()==ID_xor)
3757
- return convert_binary (src, " ^" , precedence=7 , false );
3811
+ return convert_multi_ary (src, " ^" , precedence=7 , false );
3758
3812
3759
3813
else if (src.id ()==ID_implies)
3760
3814
return convert_binary (src, " ==>" , precedence=3 , true );
0 commit comments