runtimeverification / haskell-backend

The symbolic execution engine powering the K Framework
BSD 3-Clause "New" or "Revised" License
204 stars 39 forks source link

Implement conjunction and negation over glob terms #3926

Closed goodlyrottenapple closed 3 weeks ago

goodlyrottenapple commented 3 weeks ago

This change allows us to write the following filter:

kore|booster>!(kore-term|detail).

i.e. log everything from kore and booster except for the innermost kore-term or detail contexts, which contain the pretty printed terms and extra details about e.g. rule locations which may be too noisy. This was previously not possible because we couldn't apply ! over a bracketed expression. I've added conjunction & for good measure, so we could also write the above filter as kore|booster>!kore-term&!detail.