SMV: use ID_iff for <->

This changes the SMV front-end to use ID_iff for <->.  Support for ID_iff is
added to the BDD engine.

Author: kroening

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
+
+^\[.*\] 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

@@ -659,6 +659,11 @@ bdd_enginet::BDD bdd_enginet::CTL(const exprt &expr)
   {
     return (!CTL(to_binary_expr(expr).lhs())) | CTL(to_binary_expr(expr).rhs());
   }
+  else if(expr.id() == ID_iff)
+  {
+    return (
+      !(CTL(to_binary_expr(expr).lhs())) ^ CTL(to_binary_expr(expr).rhs()));
+  }
   else if(expr.id()==ID_and)
   {
     BDD result=mgr.True();
@@ -891,7 +896,8 @@ 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_iff ||
+    is_temporal_operator(expr))
   {
     for(const auto & op : expr.operands())
       if(op.type().id() == ID_bool)

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_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

@@ -674,10 +674,9 @@ 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 || expr.id() == ID_iff)
   {
     typecheck_op(expr, bool_typet(), mode);
   }