Merge pull request #1032 from diffblue/SVA-antecedent-consequent

SVA: antecedent/consequent methods

Author: tautschnig

src/temporal-logic/nnf.cpp

@@ -130,16 +130,17 @@ std::optional<exprt> negate_property_node(const exprt &expr)
     // 1800 2017 16.12.9
     // !(a #-# b)   --->   a |-> !b
     auto &followed_by = to_sva_followed_by_expr(expr);
-    auto not_b = not_exprt{followed_by.property()};
-    return sva_overlapped_implication_exprt{followed_by.lhs(), not_b};
+    auto not_b = not_exprt{followed_by.consequent()};
+    return sva_overlapped_implication_exprt{followed_by.antecedent(), not_b};
   }
   else if(expr.id() == ID_sva_nonoverlapped_followed_by)
   {
     // 1800 2017 16.12.9
     // !(a #=# b)   --->   a |=> !b
     auto &followed_by = to_sva_followed_by_expr(expr);
-    auto not_b = not_exprt{followed_by.property()};
-    return sva_non_overlapped_implication_exprt{followed_by.lhs(), not_b};
+    auto not_b = not_exprt{followed_by.consequent()};
+    return sva_non_overlapped_implication_exprt{
+      followed_by.antecedent(), not_b};
   }
   else
     return {};

src/trans-word-level/property.cpp

@@ -586,7 +586,7 @@ static obligationst property_obligations_rec(
 
     // get match points for LHS sequence
     auto match_points =
-      instantiate_sequence(followed_by.sequence(), current, no_timeframes);
+      instantiate_sequence(followed_by.antecedent(), current, no_timeframes);
 
     exprt::operandst disjuncts;
     mp_integer t = current;
@@ -610,7 +610,7 @@ static obligationst property_obligations_rec(
       {
         auto obligations_rec =
           property_obligations_rec(
-            followed_by.property(), property_start, no_timeframes)
+            followed_by.consequent(), property_start, no_timeframes)
             .conjunction();
 
         disjuncts.push_back(

src/verilog/sva_expr.h

@@ -635,14 +635,55 @@ static inline sva_s_until_with_exprt &to_sva_s_until_with_expr(exprt &expr)
   return static_cast<sva_s_until_with_exprt &>(expr);
 }
 
-class sva_overlapped_implication_exprt : public binary_predicate_exprt
+/// base class for |->, |=>, #-#, #=#
+class sva_implication_base_exprt : public binary_predicate_exprt
 {
 public:
-  explicit sva_overlapped_implication_exprt(exprt op0, exprt op1)
+  explicit sva_implication_base_exprt(
+    exprt __antecedent,
+    irep_idt __id,
+    exprt __consequent)
     : binary_predicate_exprt(
-        std::move(op0),
+        std::move(__antecedent),
+        __id,
+        std::move(__consequent))
+  {
+  }
+
+  // a sequence
+  const exprt &antecedent() const
+  {
+    return lhs();
+  }
+
+  exprt &antecedent()
+  {
+    return lhs();
+  }
+
+  // a property
+  const exprt &consequent() const
+  {
+    return rhs();
+  }
+
+  exprt &consequent()
+  {
+    return rhs();
+  }
+};
+
+/// |->
+class sva_overlapped_implication_exprt : public sva_implication_base_exprt
+{
+public:
+  explicit sva_overlapped_implication_exprt(
+    exprt __antecedent,
+    exprt __consequent)
+    : sva_implication_base_exprt(
+        std::move(__antecedent),
         ID_sva_overlapped_implication,
-        std::move(op1))
+        std::move(__consequent))
   {
   }
 };
@@ -663,14 +704,17 @@ to_sva_overlapped_implication_expr(exprt &expr)
   return static_cast<sva_overlapped_implication_exprt &>(expr);
 }
 
-class sva_non_overlapped_implication_exprt : public binary_predicate_exprt
+/// |=>
+class sva_non_overlapped_implication_exprt : public sva_implication_base_exprt
 {
 public:
-  explicit sva_non_overlapped_implication_exprt(exprt op0, exprt op1)
-    : binary_predicate_exprt(
-        std::move(op0),
+  explicit sva_non_overlapped_implication_exprt(
+    exprt __antecedent,
+    exprt __consequent)
+    : sva_implication_base_exprt(
+        std::move(__antecedent),
         ID_sva_non_overlapped_implication,
-        std::move(op1))
+        std::move(__consequent))
   {
   }
 };
@@ -834,27 +878,19 @@ static inline sva_or_exprt &to_sva_or_expr(exprt &expr)
   return static_cast<sva_or_exprt &>(expr);
 }
 
-class sva_followed_by_exprt : public binary_predicate_exprt
+// #-#, #=#
+class sva_followed_by_exprt : public sva_implication_base_exprt
 {
 public:
-  const exprt &sequence() const
-  {
-    return op0();
-  }
-
-  exprt &sequence()
-  {
-    return op0();
-  }
-
-  const exprt &property() const
-  {
-    return op1();
-  }
-
-  exprt &property()
+  explicit sva_followed_by_exprt(
+    exprt __antecedent,
+    irep_idt __id,
+    exprt __consequent)
+    : sva_implication_base_exprt(
+        std::move(__antecedent),
+        __id,
+        std::move(__consequent))
   {
-    return op1();
   }
 };