SMV: precedence of !

NuSMV uses a different precedence of the not operator ! than CMU SMV.  This
commit special-cases this operator, and adds parentheses to avoid this
ambiguity.

Author: kroening

regression/smv/range-type/range_type4.desc

@@ -3,6 +3,6 @@ range_type4.smv
 --bound 10
 ^EXIT=0$
 ^SIGNAL=0$
-^\[spec1\] AG \(!x = 6\): PROVED up to bound 10$
+^\[spec1\] AG !\(x = 6\): PROVED up to bound 10$
 --
 ^warning: ignoring

regression/smv/word/bitwise1.desc

@@ -1,8 +1,8 @@
 CORE
 bitwise1.smv
 
-^\[.*\] !0ud8_123 = 0ud8_132: PROVED$
-^\[.*\] !0sd8_123 = -0sd8_124: PROVED$
+^\[.*\] !\(0ud8_123 = 0ud8_132\): PROVED$
+^\[.*\] !\(0sd8_123 = -0sd8_124\): PROVED$
 ^\[.*\] \(0ud8_123 \& 0ud8_7\) = 0ud8_3: PROVED$
 ^\[.*\] \(0ud8_123 \| 0ud8_7\) = 0ud8_127: PROVED$
 ^\[.*\] \(0ud8_123 xor 0ud8_7\) = 0ud8_124: PROVED$

src/smvlang/expr2smv.cpp

@@ -227,13 +227,28 @@ expr2smvt::resultt expr2smvt::convert_unary(
   const std::string &symbol,
   precedencet precedence)
 {
-  auto op_rec = convert_rec(src.op());
+  auto &op = src.op();
+
+  auto op_rec = convert_rec(op);
+
+  // We special-case negation (!), since the precedence
+  // of this operator changed between CMU SMV and NuSMV.
+
+  // clang-format off
+  bool parentheses =
+      op.operands().size() == 1 ? false
+    : src.id() == ID_not        ? true
+    : precedence >= op_rec.p;
+  // clang-format on
 
   std::string dest = symbol;
-  if(precedence > op_rec.p)
+
+  if(parentheses)
     dest += '(';
+
   dest += op_rec.s;
-  if(precedence > op_rec.p)
+
+  if(parentheses)
     dest += ')';
 
   return {precedence, std::move(dest)};