From 097ca91c7ecda726e78c3357c43fc129db706767 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sun, 8 Sep 2024 11:39:30 +0100
Subject: [PATCH] =?UTF-8?q?Simplify=20=C2=AC=20sva=5Fs=5Feventually=20?=
 =?UTF-8?q?=CF=86=20-->=20sva=5Falways=20=C2=AC=CF=86?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This adds two rules to the property normalizer for the negation of SVA
s_eventually and SVA always.
---
 src/temporal-logic/normalize_property.cpp | 10 ++++++++++
 src/temporal-logic/normalize_property.h   |  2 ++
 2 files changed, 12 insertions(+)

diff --git a/src/temporal-logic/normalize_property.cpp b/src/temporal-logic/normalize_property.cpp
index 9286a3ecc..5cab13d8d 100644
--- a/src/temporal-logic/normalize_property.cpp
+++ b/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);
 }
diff --git a/src/temporal-logic/normalize_property.h b/src/temporal-logic/normalize_property.h
index 8c7a75e71..31bf4af45 100644
--- a/src/temporal-logic/normalize_property.h
+++ b/src/temporal-logic/normalize_property.h
@@ -31,6 +31,8 @@ Author: Daniel Kroening, dkr@amazon.com
 /// 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¬φ