SMV: lowering for smv_bitimplies

SMV offers a bit-wise implication operator, which our backend lacks.  This
adds a lowering to bit-wise negation and bit-wise or.

Author: kroening

regression/smv/word/bitwise1.desc

@@ -7,6 +7,7 @@ bitwise1.smv
 ^\[.*\] \(0ud8_123 \| 0ud8_7\) = 0ud8_127: PROVED .*$
 ^\[.*\] \(0ud8_123 xor 0ud8_7\) = 0ud8_124: PROVED .*$
 ^\[.*\] \(0ud8_123 xnor 0ud8_7\) = 0ud8_131: PROVED .*$
+^\[.*\] \(0ud8_123 -> 0ud8_7\) = 0ud8_135: PROVED .*$
 ^\[.*\] \(0ud8_123 <-> 0ud8_7\) = 0ud8_131: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$

regression/smv/word/bitwise1.smv

@@ -17,7 +17,7 @@ SPEC (uwconst(123, 8) xor uwconst(7, 8)) = uwconst(124, 8)
 SPEC (uwconst(123, 8) xnor uwconst(7, 8)) = uwconst(131, 8)
 
 -- implication
---SPEC (uwconst(123, 8) -> uwconst(7, 8)) = uwconst(135, 8)
+SPEC (uwconst(123, 8) -> uwconst(7, 8)) = uwconst(135, 8)
 
 -- iff
 SPEC (uwconst(123, 8) <-> uwconst(7, 8)) = uwconst(131, 8)

src/smvlang/smv_expr.h

@@ -209,6 +209,30 @@ inline smv_min_exprt &to_smv_min_expr(exprt &expr)
   return static_cast<smv_min_exprt &>(expr);
 }
 
+// ->
+class smv_bitimplies_exprt : public binary_exprt
+{
+public:
+  smv_bitimplies_exprt(exprt __lhs, exprt __rhs)
+    : binary_exprt{std::move(__lhs), ID_smv_bitimplies, std::move(__rhs)}
+  {
+  }
+};
+
+inline const smv_bitimplies_exprt &to_smv_bitimplies_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_smv_bitimplies);
+  smv_bitimplies_exprt::check(expr);
+  return static_cast<const smv_bitimplies_exprt &>(expr);
+}
+
+inline smv_bitimplies_exprt &to_smv_bitimplies_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_smv_bitimplies);
+  smv_bitimplies_exprt::check(expr);
+  return static_cast<smv_bitimplies_exprt &>(expr);
+}
+
 class smv_unsigned_cast_exprt : public unary_exprt
 {
 public:

src/smvlang/smv_typecheck.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
 #include "smv_typecheck.h"
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
 #include <util/expr_util.h>
 #include <util/mathematical_expr.h>
@@ -1480,6 +1481,12 @@ void smv_typecheckt::lower_node(exprt &expr) const
     auto one = from_integer(1, expr.type());
     expr = if_exprt{op, std::move(one), std::move(zero)};
   }
+  else if(expr.id() == ID_smv_bitimplies)
+  {
+    // we'll lower a->b to !a|b
+    auto &implies = to_smv_bitimplies_expr(expr);
+    expr = bitor_exprt{bitnot_exprt{implies.op0()}, implies.op1()};
+  }
 
   // lower the type
   lower(expr.type());