Merge pull request #704 from diffblue/smv-iff

SMV: use `ID_smv_iff` for `<->`

Author: tautschnig

regression/ebmc/smv/smv_iff1.desc

@@ -0,0 +1,7 @@
+CORE
+smv_iff1.smv
+
+^file .* line 9: Expected expression of type `boolean', but got expression `x', which is of type `0..10'$
+^EXIT=2$
+^SIGNAL=0$
+--

regression/ebmc/smv/smv_iff1.smv

@@ -0,0 +1,9 @@
+MODULE main
+
+VAR x : 0..10;
+
+ASSIGN init(x) := 1;
+       next(x) := x;
+
+-- type error: lhs is not Boolean
+SPEC x <-> (x != 0)

regression/ebmc/smv/smv_iff2.desc

@@ -0,0 +1,7 @@
+CORE
+smv_iff2.smv
+--bdd
+^\[.*\] \(AG x != 5\) <-> \(x != 5 & AX AG x != 5\): PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/smv/smv_iff2.smv

@@ -0,0 +1,14 @@
+MODULE main
+
+VAR x : 0..10;
+
+ASSIGN
+  init(x) := 1;
+
+  next(x) :=
+    case
+      x>=3 : 3;
+      TRUE: x+1;
+    esac;
+
+SPEC AG x != 5 <-> (x != 5 & AX AG x != 5)

src/ebmc/bdd_engine.cpp

@@ -673,6 +673,12 @@ bdd_enginet::BDD bdd_enginet::CTL(const exprt &expr)
       result = result | CTL(op);
     return result;
   }
+  else if(
+    expr.id() == ID_equal && to_equal_expr(expr).lhs().type().id() == ID_bool)
+  {
+    return (
+      !(CTL(to_binary_expr(expr).lhs())) ^ CTL(to_binary_expr(expr).rhs()));
+  }
   else if(expr.id() == ID_EX)
   {
     return EX(CTL(to_EX_expr(expr).op()));
@@ -891,7 +897,10 @@ void bdd_enginet::get_atomic_propositions(const exprt &expr)
 {
   if(
     expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_not ||
-    expr.id() == ID_implies || is_temporal_operator(expr))
+    expr.id() == ID_implies ||
+    (expr.id() == ID_equal &&
+     to_equal_expr(expr).lhs().type().id() == ID_bool) ||
+    is_temporal_operator(expr))
   {
     for(const auto & op : expr.operands())
       if(op.type().id() == ID_bool)

src/hw_cbmc_irep_ids.h

@@ -15,6 +15,8 @@ IREP_ID_ONE(F)
 IREP_ID_ONE(E)
 IREP_ID_ONE(G)
 IREP_ID_ONE(X)
+IREP_ID_ONE(smv_iff)
+IREP_ID_TWO(C_smv_iff, "#smv_iff")
 IREP_ID_ONE(sva_accept_on)
 IREP_ID_ONE(sva_reject_on)
 IREP_ID_ONE(sva_sync_accept_on)
@@ -215,7 +217,7 @@ IREP_ID_ONE(verilog_ref)
 IREP_ID_ONE(verilog_reg)
 IREP_ID_ONE(verilog_integer)
 IREP_ID_ONE(verilog_time)
-IREP_ID_ONE(iff)
+IREP_ID_ONE(verilog_iff)
 IREP_ID_ONE(offset)
 IREP_ID_ONE(xnor)
 IREP_ID_ONE(specify)

src/smvlang/expr2smv.cpp

@@ -449,7 +449,12 @@ bool expr2smvt::convert(
     return convert_binary(src, dest, src.id_string(), precedence=11);
 
   else if(src.id()==ID_equal)
-    return convert_binary(src, dest, "=", precedence=11);
+  {
+    if(src.get_bool(ID_C_smv_iff))
+      return convert_binary(src, dest, "<->", precedence = 16);
+    else
+      return convert_binary(src, dest, "=", precedence = 11);
+  }
 
   else if(src.id()==ID_notequal)
     return convert_binary(src, dest, "!=", precedence=11);
@@ -466,9 +471,6 @@ bool expr2smvt::convert(
   else if(src.id()==ID_implies)
     return convert_binary(src, dest, "->", precedence=2);
 
-  else if(src.id()==ID_iff)
-    return convert_binary(src, dest, "<->", precedence=3);
-
   else if(
     src.id() == ID_AG || src.id() == ID_EG || src.id() == ID_AF ||
     src.id() == ID_EF || src.id() == ID_AX || src.id() == ID_EX ||

src/smvlang/parser.y

@@ -455,7 +455,7 @@ term       : variable_name
            | term DIVIDE_Token term   { binary_arith($$, $1, ID_div, $3); }
            | term PLUS_Token term     { binary_arith($$, $1, ID_plus, $3); }
            | term MINUS_Token term    { binary_arith($$, $1, ID_minus, $3); }
-           | term EQUIV_Token term    { binary($$, $1, ID_equal, $3, bool_typet{}); }
+           | term EQUIV_Token term    { binary($$, $1, ID_smv_iff, $3, bool_typet{}); }
            | term IMPLIES_Token term  { binary($$, $1, ID_implies, $3, bool_typet{}); }
            | term XOR_Token term      { j_binary($$, $1, ID_xor, $3, bool_typet{}); }
            | term OR_Token term       { j_binary($$, $1, ID_or, $3, bool_typet{}); }

src/smvlang/smv_typecheck.cpp

@@ -681,12 +681,17 @@ void smv_typecheckt::typecheck(
       }
     }
   }
-  else if(expr.id()==ID_and ||
-          expr.id()==ID_or ||
-          expr.id()==ID_xor ||
-          expr.id()==ID_not)
+  else if(
+    expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_xor ||
+    expr.id() == ID_not)
+  {
+    typecheck_op(expr, bool_typet(), mode);
+  }
+  else if(expr.id() == ID_smv_iff)
   {
     typecheck_op(expr, bool_typet(), mode);
+    expr.set(ID_C_smv_iff, true);
+    expr.id(ID_equal);
   }
   else if(expr.id()==ID_nondet_symbol)
   {

src/verilog/expr2verilog.cpp

@@ -1337,7 +1337,7 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
     return convert_binary(
       to_multi_ary_expr(src), "->", precedence = verilog_precedencet::IMPLIES);
 
-  else if(src.id()==ID_iff)
+  else if(src.id() == ID_verilog_iff)
     return convert_binary(
       to_multi_ary_expr(src), "<->", precedence = verilog_precedencet::IMPLIES);
 

src/verilog/parser.y

@@ -3534,7 +3534,7 @@ expression:
 	| expression "->" expression
 		{ init($$, ID_implies); mto($$, $1); mto($$, $3); }
 	| expression "<->" expression
-		{ init($$, ID_iff); mto($$, $1); mto($$, $3); }
+		{ init($$, ID_verilog_iff); mto($$, $1); mto($$, $3); }
 	| expression TOK_PLUS expression
 		{ init($$, ID_plus); mto($$, $1); mto($$, $3); }
 	| expression TOK_MINUS expression

src/verilog/verilog_typecheck_expr.cpp

@@ -2644,7 +2644,7 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
   else if(expr.id()==ID_replication)
     return convert_replication_expr(to_replication_expr(expr));
   else if(
-    expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_iff ||
+    expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_verilog_iff ||
     expr.id() == ID_implies)
   {
     Forall_operands(it, expr)