Merge pull request #678 from diffblue/not_s_eventually

Simplify ¬ sva_s_eventually φ --> sva_always ¬φ

Author: tautschnig

src/temporal-logic/normalize_property.cpp

@@ -53,6 +53,16 @@ exprt normalize_pre_not(not_exprt expr)
     // ¬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_eventually_expr(op).op()}};
+  }
 
   return std::move(expr);
 }

src/temporal-logic/normalize_property.h

@@ -33,6 +33,8 @@ Author: Daniel Kroening, [email protected]
 /// a sva_reject_on b --> ¬a ∧ b
 /// a sva_sync_accept_on b --> a ∨ b
 /// a sva_sync_reject_on b --> ¬a ∧ b
+/// ¬ sva_s_eventually φ --> sva_always ¬φ
+/// ¬ sva_always φ --> sva_s_eventually ¬φ
 /// ¬Xφ --> X¬φ
 /// ¬¬φ --> φ
 /// ¬Gφ --> F¬φ