None of the urestrict function implementations handle the error condition when the uniqid of a variable appears in both the off-set and the on-set.
Even though the regular point { var : int } mapping seems sufficient, the original reason I added it was because a dict is not hashable, which makes it cumbersome to save restrict values in a table. This is a very important property for BDDs, and is potentially interesting for cache-related performance improvement of other function representations. Also, it is occasionally useful to use the set intersection capabilities which are not available for dictionaries without doing a conversion.
This came up while thinking about #70, because adding additional assumptions outside of a restrict operations always opens up the possibility of a contradiction:
with a:
f.restrict({a: 0})
This basically says, "with a=1, set a=0".
So one way or the other, we need a consistent way of dealing with this situation.
None of the
urestrictfunction implementations handle the error condition when the uniqid of a variable appears in both the off-set and the on-set.Even though the regular point
{ var : int }mapping seems sufficient, the original reason I added it was because adictis not hashable, which makes it cumbersome to saverestrictvalues in a table. This is a very important property for BDDs, and is potentially interesting for cache-related performance improvement of other function representations. Also, it is occasionally useful to use thesetintersection capabilities which are not available for dictionaries without doing a conversion.This came up while thinking about #70, because adding additional assumptions outside of a
restrictoperations always opens up the possibility of a contradiction:This basically says, "with a=1, set a=0".
So one way or the other, we need a consistent way of dealing with this situation.