python-nnf icon indicating copy to clipboard operation
python-nnf copied to clipboard

Fix up comparisons with disperate variable sets

Open haz opened this issue 5 years ago • 3 comments

When a theory doesn't mention all of the variables, then counting, comparing, etc all become incorrect. Ultimately, a fix will need to come in the form of an NNF potentially storing a superset of the variables currently mentioned in descendants via the walk functionality.

haz avatar Jul 30 '20 18:07 haz

This assumption should go away once this issue is resolved.

haz avatar Jul 30 '20 18:07 haz

I gave this some thought during initial development but didn't come up with anything that really felt right.

One fix could be to add an optional keyword argument names for passing an explicit set of variables.

Comparing using the current behavior of .equivalent() is resistant to this problem, at least.

blyxxyz avatar Jul 30 '20 19:07 blyxxyz

Ya, I considered the names argument too. Problem there is that it proliferates -- many places might need it (or have sub-procedures that need it). The make_smooth operation is certainly one that would require it...

haz avatar Jul 30 '20 19:07 haz