diff --git a/clintest/quantifier.py b/clintest/quantifier.py index d846020..01dbed6 100644 --- a/clintest/quantifier.py +++ b/clintest/quantifier.py @@ -119,6 +119,122 @@ def consume(self, value: bool) -> Outcome: return self.outcome() +class Less(Quantifier): + """ + A quantifier demanding that an assertion holds for a number of models less than a given supremum. + + Parameters + ---------- + supremum + The supremum + """ + + def __init__(self, supremum: int) -> None: + self.__supremum = supremum + self.__state = 0 + + def __repr__(self): + name = self.__class__.__name__ + return f"{name}({self.__supremum}, __state={self.__state})" + + def __str__(self): + return f"{self.__class__.__name__} {self.__state}/{self.__supremum}" + + def outcome(self) -> Outcome: + return Outcome(self.__state < self.__supremum, self.__state >= self.__supremum) + + def consume(self, value: bool) -> Outcome: + self.__state += value + return self.outcome() + + +class LessEqual(Quantifier): + """ + A quantifier demanding that an assertion holds for a number of models less than or equal to a given maximum. + + Parameters + ---------- + maximum + The maximum + """ + + def __init__(self, maximum: int) -> None: + self.__maximum = maximum + self.__state = 0 + + def __repr__(self): + name = self.__class__.__name__ + return f"{name}({self.__maximum}, __state={self.__state})" + + def __str__(self): + return f"{self.__class__.__name__} {self.__state}/{self.__maximum}" + + def outcome(self) -> Outcome: + return Outcome(self.__state <= self.__maximum, self.__state > self.__maximum) + + def consume(self, value: bool) -> Outcome: + self.__state += value + return self.outcome() + + +class Greater(Quantifier): + """ + A quantifier demanding that an assertion holds for a number of models greater than a given infimum. + + Parameters + ---------- + supremum + The infimum + """ + + def __init__(self, infimum: int) -> None: + self.__infimum = infimum + self.__state = 0 + + def __repr__(self): + name = self.__class__.__name__ + return f"{name}({self.__infimum}, __state={self.__state})" + + def __str__(self): + return f"{self.__class__.__name__} {self.__state}/{self.__infimum}" + + def outcome(self) -> Outcome: + return Outcome(self.__state > self.__infimum, self.__state > self.__infimum) + + def consume(self, value: bool) -> Outcome: + self.__state += value + return self.outcome() + + +class GreaterEqual(Quantifier): + """ + A quantifier demanding that an assertion holds for a number of models than or equal to a given minimum. + + Parameters + ---------- + supremum + The minimum + """ + + def __init__(self, minimum: int) -> None: + self.__minimum = minimum + self.__state = 0 + + def __repr__(self): + name = self.__class__.__name__ + return f"{name}({self.__minimum}, __state={self.__state})" + + def __str__(self): + return f"{self.__class__.__name__} {self.__state}/{self.__minimum}" + + def outcome(self) -> Outcome: + return Outcome(self.__state >= self.__minimum, self.__state >= self.__minimum) + + def consume(self, value: bool) -> Outcome: + self.__state += value + return self.outcome() + + class Finished(Quantifier): """ A wrapper around an `inner` quantifier indicating that computation has finished.