11import cpp
22
33/**
4- * Describes whether a relation is 'strict' (that is, a `<` or `>`
4+ * The strictness of a relation. Either 'strict' (that is, a `<` or `>`
55 * relation) or 'non-strict' (a `<=` or `>=` relation).
66 */
7- newtype RelationStrictness =
7+ newtype TRelationStrictness =
88 /**
99 * Represents that a relation is 'strict' (that is, a `<` or `>` relation).
1010 */
@@ -14,6 +14,19 @@ newtype RelationStrictness =
1414 */
1515 Nonstrict ( )
1616
17+ /**
18+ * The strictness of a relation. Either 'strict' (that is, a `<` or `>`
19+ * relation) or 'non-strict' (a `<=` or `>=` relation).
20+ */
21+ class RelationStrictness extends TRelationStrictness {
22+ /** Gets the string representation of this relation strictness. */
23+ string toString ( ) {
24+ this = Strict ( ) and result = "strict"
25+ or
26+ this = Nonstrict ( ) and result = "non-strict"
27+ }
28+ }
29+
1730/**
1831 * Describes whether a relation is 'greater' (that is, a `>` or `>=`
1932 * relation) or 'lesser' (a `<` or `<=` relation).
@@ -105,10 +118,10 @@ predicate relOpWithSwap(
105118 *
106119 * This allows for the relation to be either as written, or with its
107120 * arguments reversed; for example, if `rel` is `x < 5` then
108- * `relOpWithSwapAndNegate(rel, x, 5, Lesser(), Strict(), true)`,
109- * `relOpWithSwapAndNegate(rel, 5, x, Greater(), Strict(), true)`,
110- * `relOpWithSwapAndNegate(rel, x, 5, Greater(), Nonstrict(), false)` and
111- * `relOpWithSwapAndNegate(rel, 5, x, Lesser(), Nonstrict(), false)` hold.
121+ * - `relOpWithSwapAndNegate(rel, x, 5, Lesser(), Strict(), true)`,
122+ * - `relOpWithSwapAndNegate(rel, 5, x, Greater(), Strict(), true)`,
123+ * - `relOpWithSwapAndNegate(rel, x, 5, Greater(), Nonstrict(), false)` and
124+ * - `relOpWithSwapAndNegate(rel, 5, x, Lesser(), Nonstrict(), false)` hold.
112125 */
113126predicate relOpWithSwapAndNegate (
114127 RelationalOperation rel , Expr a , Expr b , RelationDirection dir , RelationStrictness strict ,
0 commit comments