Merge pull request #765 from diffblue/property_nnf

extract NNF from `normalize_property_rec`

Author: tautschnig

src/temporal-logic/nnf.cpp

@@ -139,3 +139,35 @@ std::optional<exprt> negate_property_node(const exprt &expr)
   else
     return {};
 }
+
+exprt property_nnf(exprt expr)
+{
+  // Do the node
+  if(expr.id() == ID_not)
+  {
+    auto node_opt = negate_property_node(to_not_expr(expr).op());
+    if(!node_opt.has_value())
+      return expr; // give up
+
+    expr = node_opt.value();
+  }
+  else if(expr.id() == ID_implies)
+  {
+    auto &implies = to_implies_expr(expr);
+    expr = or_exprt{not_exprt{implies.lhs()}, implies.rhs()};
+  }
+  else if(
+    expr.id() == ID_equal && to_equal_expr(expr).lhs().type().id() == ID_bool)
+  {
+    auto &equal = to_equal_expr(expr);
+    expr = and_exprt{
+      implies_exprt{equal.lhs(), equal.rhs()},
+      implies_exprt{equal.rhs(), equal.lhs()}};
+  }
+
+  // Do the operands, recursively
+  for(auto &op : expr.operands())
+    op = property_nnf(op);
+
+  return expr;
+}

src/temporal-logic/nnf.h

@@ -15,4 +15,7 @@ Author: Daniel Kroening, [email protected]
 /// Returns {} if no negation is known.
 std::optional<exprt> negate_property_node(const exprt &);
 
+/// Turn a full property into NNF
+exprt property_nnf(exprt);
+
 #endif

src/temporal-logic/normalize_property.cpp

@@ -14,66 +14,11 @@ Author: Daniel Kroening, [email protected]
 
 #include <verilog/sva_expr.h>
 
+#include "nnf.h"
 #include "temporal_expr.h"
 #include "temporal_logic.h"
 #include "trivial_sva.h"
 
-exprt normalize_pre_not(not_exprt expr)
-{
-  const auto &op = expr.op();
-
-  if(op.id() == ID_and)
-  {
-    auto operands = op.operands();
-    for(auto &op : operands)
-      op = not_exprt{op};
-    return or_exprt{std::move(operands)};
-  }
-  else if(op.id() == ID_or)
-  {
-    auto operands = op.operands();
-    for(auto &op : operands)
-      op = not_exprt{op};
-    return and_exprt{std::move(operands)};
-  }
-  else if(op.id() == ID_not)
-  {
-    return to_not_expr(op).op();
-  }
-  else if(op.id() == ID_G)
-  {
-    // ¬Gφ --> F¬φ
-    return F_exprt{not_exprt{to_G_expr(op).op()}};
-  }
-  else if(op.id() == ID_F)
-  {
-    // ¬Fφ --> G¬φ
-    return G_exprt{not_exprt{to_F_expr(op).op()}};
-  }
-  else if(op.id() == ID_X)
-  {
-    // ¬Xφ --> X¬φ
-    return X_exprt{not_exprt{to_X_expr(op).op()}};
-  }
-  else if(op.id() == ID_sva_always)
-  {
-    // ¬ sva_always φ --> sva_s_eventually ¬φ
-    return sva_s_eventually_exprt{not_exprt{to_sva_always_expr(op).op()}};
-  }
-  else if(op.id() == ID_sva_s_eventually)
-  {
-    // ¬ sva_s_eventually φ --> sva_always ¬φ
-    return sva_always_exprt{not_exprt{to_sva_s_eventually_expr(op).op()}};
-  }
-
-  return std::move(expr);
-}
-
-exprt normalize_pre_implies(implies_exprt expr)
-{
-  return or_exprt{not_exprt{expr.lhs()}, expr.rhs()};
-}
-
 exprt normalize_pre_sva_non_overlapped_implication(
   sva_non_overlapped_implication_exprt expr)
 {
@@ -113,13 +58,11 @@ exprt normalize_pre_sva_cycle_delay(sva_cycle_delay_exprt expr)
 exprt normalize_property_rec(exprt expr)
 {
   // pre-traversal
-  if(expr.id() == ID_not)
-    expr = normalize_pre_not(to_not_expr(expr));
-  else if(expr.id() == ID_implies)
-    expr = normalize_pre_implies(to_implies_expr(expr));
-  else if(expr.id() == ID_sva_non_overlapped_implication)
+  if(expr.id() == ID_sva_non_overlapped_implication)
+  {
     expr = normalize_pre_sva_non_overlapped_implication(
       to_sva_non_overlapped_implication_expr(expr));
+  }
   else if(expr.id() == ID_sva_nexttime)
   {
     auto one = natural_typet{}.one_expr();
@@ -184,5 +127,8 @@ exprt normalize_property(exprt expr)
   // now do recursion
   expr = normalize_property_rec(expr);
 
+  // NNF
+  expr = property_nnf(expr);
+
   return expr;
 }