Support for str.< and str.<=
#109
Conversation
| if(!this->m_conversion_todo.empty()) { | ||
| return false; | ||
| } |
There was a problem hiding this comment.
It means that underapproximation will not turn on if we have any to_code/from_code/to_int/from_int. Is there any reason we want to turn it off? If yes, add a comment.
There was a problem hiding this comment.
Ok, when I thought about it, it seems to me that it should work for the conversions.
| * x < y & x != eps -> x = u.v1.w1 | ||
| * x < y & x != eps -> v1 in re.allchar | ||
| * x < y & x != eps -> v2 in re.allchar | ||
| * x < y & x != eps -> to_code(v1) + k = to_code(v2) & k >= 1 |
There was a problem hiding this comment.
This is overly convoluted, you can just do to_code(v1) < to_code(v2).
There was a problem hiding this comment.
Not really. There is some sad story inside the function.
There was a problem hiding this comment.
Well, that is weird. Maybe it becomes nonlinear because to_code is a function? But still, does not make sense if your hack works.
There was a problem hiding this comment.
Yes, thats strange.
| if(!this->m_conversion_todo.empty()) { | ||
| return false; | ||
| } |
There was a problem hiding this comment.
It means that underapproximation will not turn on if we have any to_code/from_code/to_int/from_int. Is there any reason we want to turn it off? If yes, add a comment.
Co-authored-by: David Chocholatý <chocholaty.david@protonmail.com>
Basic support for predicates
str.<andstr.<=. Implemented usingto_codefunction.