- changed status to on hold
Symmetrybreaking should work for sorts over (subsets of) builtins
Issue #126
resolved
No description provided.
Comments (6)
-
-
reporter
- changed status to new
We want this to be checked instead of assumed. The bug was filed because of a graphcolouring problem modelled over integers and we were surprised symmetry breaking did nothing.
-
- changed status to open
Pushed a rudimentary symmetry detection scheme over (subsets) of builtins. There is ample room for improvement by analysing a given theory + vocabulary + structure.
-
reporter
- changed milestone to Later
-
reporter
- removed milestone
Removing milestone: Later (automated comment)
-
- changed status to resolved
- Log in to comment
Are we sure we want this? I can see no reason why anyone would make a (sub)sort of the nat, int or float type, if not to use it in conjunction with <, +, MIN, sum{}, #{}... symbols. In all these cases, symmetry is broken. I think it will be easier for both the IDP user as well as the IDP developer to simply not perform symmetry detection over nat, int or float.