Added 'min' and 'max' to front-end language (#844)

ChangeLog.md

@@ -1,5 +1,9 @@
 # Changelog for Vehicle
 
+## Version 0.15
+
+* Added functions `min` and `max` over rationals.
+
 ## Version 0.14.1
 
 * Removed `Explicit` as a command line compilation target option as it never worked.

docs/language/tips-and-tricks.rst

@@ -72,19 +72,16 @@ calculate the maximum score and then require it to be less than 0.2:
 
 .. code-block:: agda
 
-   max : Rat -> Rat -> Rat
-   max x y = if x <= y then x else y
-
    largestScore : Tensor Rat [10] -> Rat
    largestScore xs = fold max 0 xs
 
    isUncertainAbout : Tensor Rat [24, 24] -> Bool
    isUncertainAbout x = largestScore (classify x) <= 0.2
 
 However, this definition would experience an exponential blow-up when
-compiled down to low-level verification queries, as each branch of the
-10 :code:`if` statements would need to be explored. In total 1024 queries
-would be generated.
+compiled down to low-level verification queries, as :code:`max` is compiled down
+to an :code:`if` statement and each branch of the 10 :code:`if` statements would
+need to be explored. In total 1024 queries would be generated.
 
 This blow-up can be avoided by instead using a "relational" approach to
 encoding the constraint, instead stating that all classes scores must be less

vehicle/lib/std.vcl

@@ -13,6 +13,16 @@ typeAnn t a = a
 notBoolOp2 : (A -> B -> Bool) -> (A -> B -> Bool)
 notBoolOp2 f x y = not (f x y)
 
+--------------------------------------------------------------------------------
+-- Orderings
+--------------------------------------------------------------------------------
+
+min : {{HasLeq a a}} -> a -> a -> a
+min x y = if x <= y then x else y
+
+max : {{HasLeq a a}} -> a -> a -> a
+max x y = if y <= x then x else y
+
 --------------------------------------------------------------------------------
 -- List
 --------------------------------------------------------------------------------

vehicle/tests/golden/compile/simple-minmax/Marabou.err.golden

@@ -0,0 +1,12 @@
+
+Warning: In property 'p', at least one of the generated queries were found to contain a strict inequality (i.e. constraints of the form 'x < y'). Unfortunately the Marabou query format only supports non-strict inequalities (i.e. constraints of the form 'x <= y').
+
+In order to provide support, Vehicle has automatically converted the strict inequalities to non-strict inequalites. This is not sound, but errors will be at most the floating point epsilon used by the verifier, which is usually very small (e.g. 1e-9). However, this may lead to unexpected behaviour (e.g. loss of the law of excluded middle).
+
+See https://github.com/vehicle-lang/vehicle/issues/74 for further details.
+
+
+Warning: In property 'p', the following network input variables do not always have both a lower and a upper bound. This is not currently supported by the Marabou query format.
+  In queries 1, 2, 3 and 4:
+    f₀[input]!0 - no lower or upper bound
+

vehicle/tests/golden/compile/simple-minmax/Marabou.queries/p-query1.txt.golden

@@ -0,0 +1,7 @@
+// WARNING: This file was generated automatically by Vehicle
+// and should not be modified manually!
+// Metadata:
+//  - Marabou query format version: unknown
+//  - Vehicle version: 0.14.1+dev
++y0 -y1 <= 0.0
+y0 <= 0.0

vehicle/tests/golden/compile/simple-minmax/Marabou.queries/p-query2.txt.golden

@@ -0,0 +1,7 @@
+// WARNING: This file was generated automatically by Vehicle
+// and should not be modified manually!
+// Metadata:
+//  - Marabou query format version: unknown
+//  - Vehicle version: 0.14.1+dev
+-y0 +y1 <= 0.0
+y1 <= 0.0

vehicle/tests/golden/compile/simple-minmax/Marabou.queries/p-query3.txt.golden

@@ -0,0 +1,7 @@
+// WARNING: This file was generated automatically by Vehicle
+// and should not be modified manually!
+// Metadata:
+//  - Marabou query format version: unknown
+//  - Vehicle version: 0.14.1+dev
+-y0 +y1 <= 0.0
+y0 >= 1.0

vehicle/tests/golden/compile/simple-minmax/Marabou.queries/p-query4.txt.golden

@@ -0,0 +1,7 @@
+// WARNING: This file was generated automatically by Vehicle
+// and should not be modified manually!
+// Metadata:
+//  - Marabou query format version: unknown
+//  - Vehicle version: 0.14.1+dev
++y0 -y1 <= 0.0
+y1 >= 1.0