Merge pull request #1191 from diffblue/normalize-no-nnf

`normalize_property` no longer generates NNF

Author: tautschnig

regression/ebmc/smv-netlist/always_with_range1.desc

@@ -4,7 +4,7 @@ always_with_range1.sv
 ^LTLSPEC node275 & X node275 & X X node275 .*
 ^LTLSPEC G node275$
 ^LTLSPEC node275 & X node275 & X X node275 .*
-^LTLSPEC G \(\!node306 \| X node337\)$
+^LTLSPEC G \(node306 -> X node337\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --

src/temporal-logic/ltl_sva_to_string.cpp

@@ -91,6 +91,11 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
   {
     return infix(" xor ", expr, mode);
   }
+  else if(
+    expr.id() == ID_equal && to_equal_expr(expr).lhs().type().id() == ID_bool)
+  {
+    return infix("<->", expr, mode);
+  }
   else if(expr.id() == ID_implies)
   {
     return infix("->", expr, mode);

src/temporal-logic/normalize_property.cpp

@@ -15,7 +15,6 @@ Author: Daniel Kroening, [email protected]
 #include <verilog/sva_expr.h>
 
 #include "ltl.h"
-#include "nnf.h"
 #include "temporal_expr.h"
 #include "temporal_logic.h"
 #include "trivial_sva.h"
@@ -112,8 +111,5 @@ exprt normalize_property(exprt expr)
   // now do recursion
   expr = normalize_property_rec(expr);
 
-  // NNF
-  expr = property_nnf(expr);
-
   return expr;
 }