Merge pull request #744 from diffblue/property-nnf

extract per-node NNF computation for temporal logic from word-level BMC

Author: tautschnig

src/temporal-logic/Makefile

@@ -1,4 +1,5 @@
 SRC = negate_property.cpp \
+      nnf.cpp \
       normalize_property.cpp \
       temporal_logic.cpp \
       #empty line

src/temporal-logic/nnf.cpp

@@ -0,0 +1,101 @@
+/*******************************************************************\
+
+Module: Negation Normal Form for temporal logic
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "nnf.h"
+
+#include <verilog/sva_expr.h>
+
+#include "temporal_expr.h"
+
+std::optional<exprt> negate_property_node(const exprt &expr)
+{
+  if(expr.id() == ID_U)
+  {
+    // ¬(φ U ψ) ≡ (¬φ R ¬ψ)
+    auto &U = to_U_expr(expr);
+    return R_exprt{not_exprt{U.lhs()}, not_exprt{U.rhs()}};
+  }
+  else if(expr.id() == ID_R)
+  {
+    // ¬(φ R ψ) ≡ (¬φ U ¬ψ)
+    auto &R = to_R_expr(expr);
+    return U_exprt{not_exprt{R.lhs()}, not_exprt{R.rhs()}};
+  }
+  else if(expr.id() == ID_G)
+  {
+    // ¬G φ ≡ F ¬φ
+    auto &G = to_G_expr(expr);
+    return F_exprt{not_exprt{G.op()}};
+  }
+  else if(expr.id() == ID_F)
+  {
+    // ¬F φ ≡ G ¬φ
+    auto &F = to_F_expr(expr);
+    return G_exprt{not_exprt{F.op()}};
+  }
+  else if(expr.id() == ID_X)
+  {
+    // ¬X φ ≡ X ¬φ
+    auto &X = to_X_expr(expr);
+    return X_exprt{not_exprt{X.op()}};
+  }
+  else if(expr.id() == ID_implies)
+  {
+    // ¬(a->b) ≡ a && ¬b
+    auto &implies_expr = to_implies_expr(expr);
+    return and_exprt{implies_expr.lhs(), not_exprt{implies_expr.rhs()}};
+  }
+  else if(expr.id() == ID_and)
+  {
+    auto operands = expr.operands();
+    for(auto &op : operands)
+      op = not_exprt{op};
+    return or_exprt{std::move(operands)};
+  }
+  else if(expr.id() == ID_or)
+  {
+    auto operands = expr.operands();
+    for(auto &op : operands)
+      op = not_exprt{op};
+    return and_exprt{std::move(operands)};
+  }
+  else if(expr.id() == ID_not)
+  {
+    return to_not_expr(expr).op();
+  }
+  else if(expr.id() == ID_sva_until)
+  {
+    // ¬(φ W ψ) ≡ (¬φ strongR ¬ψ)
+    auto &W = to_sva_until_expr(expr);
+    return strong_R_exprt{not_exprt{W.lhs()}, not_exprt{W.rhs()}};
+  }
+  else if(expr.id() == ID_sva_s_until)
+  {
+    // ¬(φ U ψ) ≡ (¬φ R ¬ψ)
+    auto &U = to_sva_s_until_expr(expr);
+    return R_exprt{not_exprt{U.lhs()}, not_exprt{U.rhs()}};
+  }
+  else if(expr.id() == ID_sva_until_with)
+  {
+    // ¬(φ R ψ) ≡ (¬φ U ¬ψ)
+    // Note LHS and RHS are swapped.
+    auto &until_with = to_sva_until_with_expr(expr);
+    auto R = R_exprt{until_with.rhs(), until_with.lhs()};
+    return sva_until_exprt{not_exprt{R.lhs()}, not_exprt{R.rhs()}};
+  }
+  else if(expr.id() == ID_sva_s_until_with)
+  {
+    // ¬(φ strongR ψ) ≡ (¬φ W ¬ψ)
+    // Note LHS and RHS are swapped.
+    auto &s_until_with = to_sva_s_until_with_expr(expr);
+    auto strong_R = strong_R_exprt{s_until_with.rhs(), s_until_with.lhs()};
+    return weak_U_exprt{not_exprt{strong_R.lhs()}, not_exprt{strong_R.rhs()}};
+  }
+  else
+    return {};
+}

src/temporal-logic/nnf.h

@@ -0,0 +1,18 @@
+/*******************************************************************\
+
+Module: Negation Normal Form for temporal logic
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_TEMPORAL_LOGIC_NNF_H
+#define CPROVER_TEMPORAL_LOGIC_NNF_H
+
+#include <util/expr.h>
+
+/// Negates a single node (i.e., not recursively) of a temporal logic formula.
+/// Returns {} if no negation is known.
+std::optional<exprt> negate_property_node(const exprt &);
+
+#endif

src/trans-word-level/property.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/symbol_table.h>
 
 #include <ebmc/ebmc_error.h>
+#include <temporal-logic/nnf.h>
 #include <temporal-logic/temporal_expr.h>
 #include <temporal-logic/temporal_logic.h>
 #include <verilog/sva_expr.h>
@@ -511,106 +512,23 @@ static obligationst property_obligations_rec(
     // We need NNF, try to eliminate the negation.
     auto &op = to_not_expr(property_expr).op();
 
-    if(op.id() == ID_U)
-    {
-      // ¬(φ U ψ) ≡ (¬φ R ¬ψ)
-      auto &U = to_U_expr(op);
-      auto R = R_exprt{not_exprt{U.lhs()}, not_exprt{U.rhs()}};
-      return property_obligations_rec(R, current, no_timeframes);
-    }
-    else if(op.id() == ID_R)
-    {
-      // ¬(φ R ψ) ≡ (¬φ U ¬ψ)
-      auto &R = to_R_expr(op);
-      auto U = U_exprt{not_exprt{R.lhs()}, not_exprt{R.rhs()}};
-      return property_obligations_rec(U, current, no_timeframes);
-    }
-    else if(op.id() == ID_G)
-    {
-      // ¬G φ ≡ F ¬φ
-      auto &G = to_G_expr(op);
-      auto F = F_exprt{not_exprt{G.op()}};
-      return property_obligations_rec(F, current, no_timeframes);
-    }
-    else if(op.id() == ID_F)
-    {
-      // ¬F φ ≡ G ¬φ
-      auto &F = to_F_expr(op);
-      auto G = G_exprt{not_exprt{F.op()}};
-      return property_obligations_rec(G, current, no_timeframes);
-    }
-    else if(op.id() == ID_X)
-    {
-      // ¬X φ ≡ X ¬φ
-      auto &X = to_X_expr(op);
-      auto negX = X_exprt{not_exprt{X.op()}};
-      return property_obligations_rec(negX, current, no_timeframes);
-    }
-    else if(op.id() == ID_implies)
-    {
-      // ¬(a->b) --> a && ¬b
-      auto &implies_expr = to_implies_expr(op);
-      auto and_expr =
-        and_exprt{implies_expr.lhs(), not_exprt{implies_expr.rhs()}};
-      return property_obligations_rec(and_expr, current, no_timeframes);
-    }
-    else if(op.id() == ID_and)
-    {
-      auto operands = op.operands();
-      for(auto &op : operands)
-        op = not_exprt{op};
-      auto or_expr = or_exprt{std::move(operands)};
-      return property_obligations_rec(or_expr, current, no_timeframes);
-    }
-    else if(op.id() == ID_or)
-    {
-      auto operands = op.operands();
-      for(auto &op : operands)
-        op = not_exprt{op};
-      auto and_expr = and_exprt{std::move(operands)};
-      return property_obligations_rec(and_expr, current, no_timeframes);
-    }
-    else if(op.id() == ID_not)
+    auto op_negated_opt = negate_property_node(op);
+
+    if(op_negated_opt.has_value())
     {
       return property_obligations_rec(
-        to_not_expr(op).op(), current, no_timeframes);
-    }
-    else if(op.id() == ID_sva_until)
-    {
-      // ¬(φ W ψ) ≡ (¬φ strongR ¬ψ)
-      auto &W = to_sva_until_expr(op);
-      auto strong_R = strong_R_exprt{not_exprt{W.lhs()}, not_exprt{W.rhs()}};
-      return property_obligations_rec(strong_R, current, no_timeframes);
+        op_negated_opt.value(), current, no_timeframes);
     }
-    else if(op.id() == ID_sva_s_until)
+    else if(is_temporal_operator(op))
     {
-      // ¬(φ U ψ) ≡ (¬φ R ¬ψ)
-      auto &U = to_sva_s_until_expr(op);
-      auto R = R_exprt{not_exprt{U.lhs()}, not_exprt{U.rhs()}};
-      return property_obligations_rec(R, current, no_timeframes);
-    }
-    else if(op.id() == ID_sva_until_with)
-    {
-      // ¬(φ R ψ) ≡ (¬φ U ¬ψ)
-      // Note LHS and RHS are swapped.
-      auto &until_with = to_sva_until_with_expr(op);
-      auto R = R_exprt{until_with.rhs(), until_with.lhs()};
-      auto U = sva_until_exprt{not_exprt{R.lhs()}, not_exprt{R.rhs()}};
-      return property_obligations_rec(U, current, no_timeframes);
-    }
-    else if(op.id() == ID_sva_s_until_with)
-    {
-      // ¬(φ strongR ψ) ≡ (¬φ W ¬ψ)
-      // Note LHS and RHS are swapped.
-      auto &s_until_with = to_sva_s_until_with_expr(op);
-      auto strong_R = strong_R_exprt{s_until_with.rhs(), s_until_with.lhs()};
-      auto W =
-        weak_U_exprt{not_exprt{strong_R.lhs()}, not_exprt{strong_R.rhs()}};
-      return property_obligations_rec(W, current, no_timeframes);
+      throw ebmc_errort() << "failed to make NNF for " << op.id();
     }
     else
+    {
+      // state formula
       return obligationst{
         instantiate_property(property_expr, current, no_timeframes)};
+    }
   }
   else
   {