Skip to content

Commit 7a8bc91

Browse files
Add hyper-rectangle test and update docs for min/max
1 parent dad64ba commit 7a8bc91

File tree

8 files changed

+1402
-4
lines changed

8 files changed

+1402
-4
lines changed

Diff for: docs/language/arithmetic.rst

+16
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,14 @@ The available operations over naturals are:
4949
- :code:`>`
5050
- :code:`Nat -> Nat -> Bool`
5151
- :code:`x >= y`
52+
* - Min
53+
- :code:`min`
54+
- :code:`Nat -> Nat -> Bool`
55+
- :code:`min x y`
56+
* - Max
57+
- :code:`max`
58+
- :code:`Nat -> Nat -> Bool`
59+
- :code:`max x y`
5260

5361
Note that inequalities can be chained, so that ``x < y <= z`` will be
5462
expanded to ``x < y and y <= z``.
@@ -105,6 +113,14 @@ The available operations over rationals are:
105113
- :code:`>`
106114
- :code:`Rat -> Rat -> Bool`
107115
- :code:`x >= y`
116+
* - Min
117+
- :code:`min`
118+
- :code:`Rat -> Rat -> Bool`
119+
- :code:`min x y`
120+
* - Max
121+
- :code:`max`
122+
- :code:`Rat -> Rat -> Bool`
123+
- :code:`max x y`
108124

109125

110126
.. note::

Diff for: docs/language/vectors.rst

+12-4
Original file line numberDiff line numberDiff line change
@@ -170,20 +170,28 @@ the set of operations supported by ``Index`` types is extremely limited:
170170
- Example
171171
* - Less than or equal
172172
- :code:`<=`
173-
- :code:`Index d -> Index d -> Bool`
173+
- :code:`Index d1 -> Index d2 -> Bool`
174174
- :code:`x <= y`
175175
* - Less than
176176
- :code:`<`
177-
- :code:`Index d -> Index d -> Bool`
177+
- :code:`Index d1 -> Index d2 -> Bool`
178178
- :code:`x < y`
179179
* - Greater than or equal
180180
- :code:`>=`
181-
- :code:`Index d -> Index d -> Bool`
181+
- :code:`Index d1 -> Index d2 -> Bool`
182182
- :code:`x >= y`
183183
* - Greater than
184184
- :code:`>`
185-
- :code:`Index d -> Index d -> Bool`
185+
- :code:`Index d1 -> Index d2 -> Bool`
186186
- :code:`x >= y`
187+
* - Min
188+
- :code:`min`
189+
- :code:`Index d1 -> Index d2 -> Bool`
190+
- :code:`min x y`
191+
* - Max
192+
- :code:`max`
193+
- :code:`Index d1 -> Index d2 -> Bool`
194+
- :code:`max x y`
187195

188196
Non-constant sizes
189197
------------------
1.18 KB
Binary file not shown.
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
// WARNING: This file was generated automatically by Vehicle
2+
// and should not be modified manually!
3+
// Metadata:
4+
// - Marabou query format version: unknown
5+
// - Vehicle version: 0.14.1+dev
6+
+y0 -y1 <= 0.0
7+
x0 <= 1.0
8+
x0 >= 0.0
9+
x1 <= 1.0
10+
x1 >= 0.0
11+
x2 <= 1.0
12+
x2 >= -0.23146467466735562
13+
x3 <= 1.0
14+
x3 >= -0.17030859913804158
15+
x4 <= 1.0
16+
x4 >= -0.15181423637665412
17+
x5 <= 1.0
18+
x5 >= -0.09376206565379208
19+
x6 <= 1.0
20+
x6 >= -0.12252536033731846
21+
x7 <= 1.0
22+
x7 >= -0.07527999060969304
23+
x8 <= 1.0
24+
x8 >= -0.16953891559897394
25+
x9 <= 1.0
26+
x9 >= -0.2587957298637119
27+
x10 <= 1.0
28+
x10 >= -0.18418175113682422
29+
x11 <= 1.0
30+
x11 >= -0.15278713734873317
31+
x12 <= 1.0
32+
x12 >= -0.0736900786611618
33+
x13 <= 1.0
34+
x13 >= -0.07213913784800313
35+
x14 <= 1.0
36+
x14 >= -0.06726546917623602
37+
x15 <= 1.0
38+
x15 >= -0.06668490077590639
39+
x16 <= 1.0
40+
x16 >= -0.10018156123016132
41+
x17 <= 1.0
42+
x17 >= -0.17078887483783187
43+
x18 <= 1.0
44+
x18 >= -0.09815711812407239
45+
x19 <= 1.0
46+
x19 >= -0.07486999880282023
47+
x20 <= 1.0
48+
x20 >= -0.030188310612655818
49+
x21 <= 1.0
50+
x21 >= -0.07905960941677105
51+
x22 <= 1.0
52+
x22 >= -0.03748206502179757
53+
x23 <= 1.0
54+
x23 >= -0.05442083785306469
55+
x24 <= 1.0
56+
x24 >= -0.062439538467816115
57+
x25 <= 1.0
58+
x25 >= -0.1447197088302923
59+
x26 <= 1.0
60+
x26 >= -0.03415181550241956
61+
x27 <= 1.0
62+
x27 >= -0.05484392698265897
63+
x28 <= 1.0
64+
x28 >= -0.059158504620057895
65+
x29 <= 1.0
66+
x29 >= -0.09836248531326969

0 commit comments

Comments
 (0)