From 249575beedb41c0ce37d982c0e4abfc508e19775 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sun, 22 Sep 2024 14:13:24 -0700
Subject: [PATCH] SVA: until_with

This adds SVA's until_with to the word-level BMC backend.
---
 src/trans-word-level/property.cpp | 37 +++++++++++++++----------------
 1 file changed, 18 insertions(+), 19 deletions(-)

diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp
index 0614eb4c..f57892f4 100644
--- a/src/trans-word-level/property.cpp
+++ b/src/trans-word-level/property.cpp
@@ -407,10 +407,12 @@ static obligationst property_obligations_rec(
     DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
     return obligationst{no_timeframes - 1, or_exprt{tmp_q, expansion}};
   }
-  else if(property_expr.id() == ID_R)
+  else if(
+    property_expr.id() == ID_R || property_expr.id() == ID_sva_until_with ||
+    property_expr.id() == ID_sva_s_until_with)
   {
     // we expand: p R q <=> q ∧ (p ∨ X(p R q))
-    auto &R_expr = to_R_expr(property_expr);
+    auto &R_expr = to_binary_expr(property_expr);
     auto tmp_q =
       property_obligations_rec(R_expr.rhs(), solver, current, no_timeframes, ns)
         .conjunction()
@@ -436,23 +438,6 @@ static obligationst property_obligations_rec(
     DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
     return obligationst{no_timeframes - 1, and_exprt{tmp_q, expansion}};
   }
-  else if(
-    property_expr.id() == ID_sva_until_with ||
-    property_expr.id() == ID_sva_s_until_with)
-  {
-    // overlapping until
-
-    // we rewrite using 'next'
-    binary_exprt tmp = to_binary_expr(property_expr);
-    if(property_expr.id() == ID_sva_until_with)
-      tmp.id(ID_sva_until);
-    else
-      tmp.id(ID_sva_s_until);
-
-    tmp.op1() = X_exprt{tmp.op1()};
-
-    return property_obligations_rec(tmp, solver, current, no_timeframes, ns);
-  }
   else if(property_expr.id() == ID_and)
   {
     // Generate seperate sets of obligations for each conjunct,
@@ -602,6 +587,20 @@ static obligationst property_obligations_rec(
       return property_obligations_rec(
         to_not_expr(op).op(), solver, current, no_timeframes, ns);
     }
+    else if(op.id() == ID_sva_until || op.id() == ID_sva_s_until)
+    {
+      // ¬(φ U ψ) ≡ (¬φ R ¬ψ)
+      auto &U = to_binary_expr(op);
+      auto R = sva_until_with_exprt{not_exprt{U.lhs()}, not_exprt{U.rhs()}};
+      return property_obligations_rec(R, solver, current, no_timeframes, ns);
+    }
+    else if(op.id() == ID_sva_until_with || op.id() == ID_sva_s_until_with)
+    {
+      // ¬(φ R ψ) ≡ (¬φ U ¬ψ)
+      auto &R = to_binary_expr(op);
+      auto U = sva_until_exprt{not_exprt{R.lhs()}, not_exprt{R.rhs()}};
+      return property_obligations_rec(U, solver, current, no_timeframes, ns);
+    }
     else
       return obligationst{
         instantiate_property(property_expr, current, no_timeframes, ns)};