From 49d18496fd7ada9f8b622ed1c74ca2ce762c2993 Mon Sep 17 00:00:00 2001
From: Tobias Stolzmann <tobias.stolzmann@potassco.com>
Date: Thu, 22 Feb 2024 11:57:33 +0100
Subject: [PATCH] Add an assertion for implication

---
 clintest/assertion.py   | 28 ++++++++++++++++++++++++++++
 tests/test_assertion.py | 10 ++++++++++
 2 files changed, 38 insertions(+)

diff --git a/clintest/assertion.py b/clintest/assertion.py
index f915307..882c991 100644
--- a/clintest/assertion.py
+++ b/clintest/assertion.py
@@ -228,3 +228,31 @@ def __repr__(self):
 
     def holds_for(self, model: Model) -> bool:
         return any((operand.holds_for(model) for operand in self.__operands))
+
+
+class Implies(Assertion):
+    """
+    The implication of two given assertions.
+    This assertion holds if `antecedent` holds implies that `consequent` holds.
+    In other words, this assertion holds if `antecedent` does not hold or `consequent` holds.
+
+    Parameters
+    ----------
+    antecedent
+        The `Assertion` to be the antecedent of the implication
+    consequent
+        The `Assertion` to be the consequent of the implication
+    """
+
+    def __init__(self, antecedent: Assertion, consequent: Assertion) -> None:
+        self.__antecedent = antecedent
+        self.__consequent = consequent
+
+    def __repr__(self):
+        name = self.__class__.__name__
+        antecedent = repr(self.__antecedent)
+        consequent = repr(self.__consequent)
+        return f"{name}({antecedent}, {consequent})"
+
+    def holds_for(self, model: Model) -> None:
+        return not self.__antecedent.holds_for(model) or self.__consequent.holds_for(model)
diff --git a/tests/test_assertion.py b/tests/test_assertion.py
index 4925809..8ad10cf 100644
--- a/tests/test_assertion.py
+++ b/tests/test_assertion.py
@@ -102,3 +102,13 @@ def test_or(frame):
         Or(),
         Or(False_(), False_()),
     ])
+
+def test_implies(frame):
+    from clintest.assertion import Implies, True_, False_
+    frame([
+        Implies(False_(), False_()),
+        Implies(False_(), True_()),
+        Implies(True_(), True_()),
+    ], [
+        Implies(True_(), False_()),
+    ])