SMV: avoid ambiguity when generating binary expression strings

Author: kroening

src/smvlang/expr2smv.cpp

@@ -90,7 +90,8 @@ Function: expr2smvt::convert_binary
 expr2smvt::resultt expr2smvt::convert_binary(
   const exprt &src,
   const std::string &symbol,
-  precedencet precedence)
+  precedencet precedence,
+  bool is_associative)
 {
   if(src.operands().size()<2)
     return convert_norep(src);
@@ -112,10 +113,18 @@ expr2smvt::resultt expr2smvt::convert_binary(
 
     auto op_rec = convert_rec(*it);
 
-    if(precedence > op_rec.p)
+    // clang-format off
+    bool use_parentheses =
+        src.id() == it->id() && is_associative ? false
+      : precedence >= op_rec.p;
+    // clang-format on
+
+    if(use_parentheses)
       dest += '(';
+
     dest += op_rec.s;
-    if(precedence > op_rec.p)
+
+    if(use_parentheses)
       dest += ')';
   }
 
@@ -434,14 +443,14 @@ Function: expr2smvt::convert_rec
 expr2smvt::resultt expr2smvt::convert_rec(const exprt &src)
 {
   if(src.id()==ID_plus)
-    return convert_binary(src, "+", precedencet::PLUS);
+    return convert_binary(src, "+", precedencet::PLUS, true);
 
   else if(src.id()==ID_minus)
   {
     if(src.operands().size()<2)
       return convert_norep(src);
     else
-      return convert_binary(src, "-", precedencet::PLUS);
+      return convert_binary(src, "-", precedencet::PLUS, true);
   }
 
   else if(src.id()==ID_unary_minus)
@@ -455,57 +464,60 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src)
   else if(src.id()==ID_index)
     return convert_index(to_index_expr(src), precedencet::INDEX);
 
-  else if(src.id()==ID_mult || src.id()==ID_div)
-    return convert_binary(src, src.id_string(), precedencet::MULT);
+  else if(src.id() == ID_mult)
+    return convert_binary(src, src.id_string(), precedencet::MULT, true);
+
+  else if(src.id() == ID_div)
+    return convert_binary(src, src.id_string(), precedencet::MULT, false);
 
   else if(src.id() == ID_mod)
-    return convert_binary(src, src.id_string(), precedencet::MULT);
+    return convert_binary(src, src.id_string(), precedencet::MULT, false);
 
   else if(src.id() == ID_smv_setin)
-    return convert_binary(src, "in", precedencet::IN);
+    return convert_binary(src, "in", precedencet::IN, false);
 
   else if(src.id() == ID_smv_setnotin)
-    return convert_binary(src, "notin", precedencet::IN);
+    return convert_binary(src, "notin", precedencet::IN, false);
 
   else if(src.id() == ID_smv_union)
-    return convert_binary(src, "union", precedencet::UNION);
+    return convert_binary(src, "union", precedencet::UNION, false);
 
   else if(src.id()==ID_lt || src.id()==ID_gt ||
           src.id()==ID_le || src.id()==ID_ge)
-    return convert_binary(src, src.id_string(), precedencet::REL);
+    return convert_binary(src, src.id_string(), precedencet::REL, false);
 
   else if(src.id()==ID_equal)
   {
     if(src.get_bool(ID_C_smv_iff))
-      return convert_binary(src, "<->", precedencet::IFF);
+      return convert_binary(src, "<->", precedencet::IFF, false);
     else
-      return convert_binary(src, "=", precedencet::REL);
+      return convert_binary(src, "=", precedencet::REL, false);
   }
 
   else if(src.id()==ID_notequal)
-    return convert_binary(src, "!=", precedencet::REL);
+    return convert_binary(src, "!=", precedencet::REL, false);
 
   else if(src.id()==ID_not)
     return convert_unary(to_not_expr(src), "!", precedencet::NOT);
 
   else if(src.id() == ID_and || src.id() == ID_bitand)
-    return convert_binary(src, "&", precedencet::AND);
+    return convert_binary(src, "&", precedencet::AND, true);
 
   else if(src.id() == ID_or || src.id() == ID_bitor)
-    return convert_binary(src, "|", precedencet::OR);
+    return convert_binary(src, "|", precedencet::OR, true);
 
   else if(src.id() == ID_implies || src.id() == ID_smv_bitimplies)
-    return convert_binary(src, "->", precedencet::IMPLIES);
+    return convert_binary(src, "->", precedencet::IMPLIES, false);
 
   else if(src.id() == ID_xor || src.id() == ID_bitxor)
-    return convert_binary(src, "xor", precedencet::OR);
+    return convert_binary(src, "xor", precedencet::OR, true);
 
   else if(src.id() == ID_xnor || src.id() == ID_bitxnor)
   {
     if(src.get_bool(ID_C_smv_iff))
-      return convert_binary(src, "<->", precedencet::IFF);
+      return convert_binary(src, "<->", precedencet::IFF, false);
     else
-      return convert_binary(src, "xnor", precedencet::OR);
+      return convert_binary(src, "xnor", precedencet::OR, false);
   }
 
   else if(
@@ -540,7 +552,7 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src)
     src.id() == ID_ER || src.id() == ID_U)
   {
     return convert_binary(
-      to_binary_expr(src), src.id_string(), precedencet::TEMPORAL);
+      to_binary_expr(src), src.id_string(), precedencet::TEMPORAL, false);
   }
 
   else if(
@@ -565,15 +577,17 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src)
   else if(src.id() == ID_R)
   {
     // LTL release is "V" in NuSMV
-    return convert_binary(to_binary_expr(src), "V", precedencet::TEMPORAL);
+    return convert_binary(
+      to_binary_expr(src), "V", precedencet::TEMPORAL, false);
   }
 
   else if(src.id() == ID_smv_S || src.id() == ID_smv_T)
   {
     return convert_binary(
       to_binary_expr(src),
       std::string(src.id_string(), 4, std::string::npos),
-      precedencet::TEMPORAL);
+      precedencet::TEMPORAL,
+      false);
   }
 
   else if(src.id() == ID_if)
@@ -608,17 +622,17 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src)
 
   else if(src.id() == ID_concatenation)
   {
-    return convert_binary(to_binary_expr(src), "::", precedencet::CONCAT);
+    return convert_binary(to_binary_expr(src), "::", precedencet::CONCAT, true);
   }
 
   else if(src.id() == ID_shl)
   {
-    return convert_binary(to_binary_expr(src), "<<", precedencet::SHIFT);
+    return convert_binary(to_binary_expr(src), "<<", precedencet::SHIFT, false);
   }
 
   else if(src.id() == ID_lshr || src.id() == ID_ashr)
   {
-    return convert_binary(to_binary_expr(src), ">>", precedencet::SHIFT);
+    return convert_binary(to_binary_expr(src), ">>", precedencet::SHIFT, false);
   }
 
   else if(src.id() == ID_smv_extend)

src/smvlang/expr2smv_class.h

@@ -87,8 +87,11 @@ class expr2smvt
 
   resultt convert_nondet_choice(const exprt &);
 
-  resultt
-  convert_binary(const exprt &src, const std::string &symbol, precedencet);
+  resultt convert_binary(
+    const exprt &src,
+    const std::string &symbol,
+    precedencet,
+    bool is_associative);
 
   resultt convert_rtctl(
     const ternary_exprt &src,