not-contains: implement not-contains > LIA reduction

VeriFIT / z3-noodler

The Z3-Noodler String Solver

Other

6 stars 5 forks source link

not-contains: implement not-contains > LIA reduction #168

Open MichalHe opened 1 month ago

MichalHe commented 1 month ago

This PR implements a reduction of a single not-contains predicate into a LIA formula when the languages of the underlying variables are flat, building on #150.