-
Notifications
You must be signed in to change notification settings - Fork 21
[DEV][Sanitizer]Implement max and min reduce operations in _to_z3 #208
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: main
Are you sure you want to change the base?
Changes from all commits
0f49b98
5209989
460a1a9
ca7d953
69d5161
99e5833
41da73a
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -2,7 +2,7 @@ | |
| from collections import namedtuple | ||
| from collections.abc import Callable | ||
| from dataclasses import dataclass, field | ||
| from functools import cached_property | ||
| from functools import cached_property, reduce | ||
| from typing import Any, Optional, Union | ||
| import re | ||
|
|
||
|
|
@@ -1182,10 +1182,16 @@ def _to_z3(self) -> tuple[ArithRef, list]: | |
| self._z3 = Sum(arr) | ||
|
|
||
| if self.op == "max": | ||
| raise NotImplementedError("_to_z3 of max is not implemented yet") | ||
| arr, self._constraints = self.input._to_z3() | ||
| if not arr: | ||
| raise ValueError("Cannot compute max of empty array") | ||
| self._z3 = reduce(lambda a, b: If(a >= b, a, b), arr) | ||
|
|
||
| if self.op == "min": | ||
| raise NotImplementedError("_to_z3 of min is not implemented yet") | ||
| arr, self._constraints = self.input._to_z3() | ||
| if not arr: | ||
| raise ValueError("Cannot compute min of empty array") | ||
| self._z3 = reduce(lambda a, b: If(a <= b, a, b), arr) | ||
|
Comment on lines
1184
to
+1194
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
The new implementation assumes Useful? React with 👍 / 👎. |
||
|
|
||
| if self.op == "load" or self.op == "store": | ||
| # Load and store operations | ||
|
|
||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think the tests are not as good as the previous tests. Should be refactored