Open
Description
Works for intervals. We can avoid this check when we encounter octagonal constraints (two-variable meet irreducible). For example, consider the following scenario.
val = {x+y<=5, y+z<=10, ...}, m_ir = x+z<=3, then is_subsumed(m_ir, val)=true
The current is_subsumed check implementation cannot infer true
for the above scenario. This may be due to the fact that the val is not guaranteed to be closed always. Or the logic of checking (!m_ir && val)
is SAT does not work for two-variable meet irreducible.