Symmetry breaking code refactoring

[nancyday]

The symmetry breaking code is currently factored as follows:

compiler/fortressCompilers

• contains many compilers with various symmetry breaking transformers
• this code is repetitive and can be shortened by using the Configurable Compiler

transformers/ SymmetryBreakingTransformer SymmetryBreakingTransformerSI (adds sort inference) SymmetryBreakingTransformer_MostUsed (use selection heuristic of breaking on most used elements) SymmetryBreakingTransformer_NoSkolem (do not symmetry break on skolem constants/functions) These are all parameterized by 1) the selection heuristic (which order to choose constants/functions/predicates) 2) the symmetry breaking factory (the functions that take an element and do the symmetry breaking on it)

• These could be folded into one file by:
  • SI could be made a parameter
  • MostUsed is a selection heuristic (which is already a parameter) - it requires some preprocessing, which could be abstracted into the selection heuristic as a preprocessing step where functions/predicates are put in a certain order - this preprocessing step can also be used to cover the "weirdness" part of SymmetryBreakingTransformer, where the functions/predicates are put in a certain order to that the symmetry breaking schemes can be clearly incremental (used in Joe's paper)
  • NoSkolem can be part of the selection heuristic preprocessing step, which creates the lists in order but removes skolem functions from the list
  • Additionally, right now all symmetry breaking schemes do constants first - that could be part of the selection heuristic

symmetry/ SymmetryBreaker, Symmetry SymmetryBreakerDL, SymmetryDL (DL = disjunctive limit)

• the above can be combined where SymmetryBreaker is the interface (given a function create the constraints for it) and Symmetry and SymmetryDL are two implementations, one of which creates as many disjunctions as possible and the other puts limits on the number of disjunctions used

symmetry/StalenessState, StalenessTracker, RemainingIdentifiersTracker

• monitor which symbols have been used as domain elements somewhere (including in symmetry breaking) and therefore cannot have more symmetry breaking done on them

symmetry/SelectionHeuristic, SelectionHeuristicWithConstants a

• are selection heuristics - may be some overlap between them

symmetry/HyperGraph, Microstructure, ExperimentalSymmetryBreakers are probably no longer used

[jporemba]

A few comments (partially following up on my Slack discussion with Nancy):

1) I believe that SymmetryBreakingTransformerSI is intended to be used on problems where sort inference has not already been performed, and you explicitly do not want to keep the inferred sorts once symmetry breaking is done. SymmetryBreakingTransformerSI leaves the sorts unchanged when it is finished - the sort inference is temporary. We introduced this for evaluation purposes, but it is not clear that you would want this behaviour for standard uses.

2) HyperGraph and Microstructure were used during my undergrad thesis, but have no practical use in Fortress (they were a theoretical tool mainly), so can be removed if you wish.

[nancyday]

Additional info from Joe: Even through the FortressTWOCompiler_SI() does not seem to use the SymmetryBreakingTransformerSI, the compilation steps include the SortInferenceTransformer so it does do sort inference. "The reason does not take this approach, is that we wanted to use sort inference for the purposes of symmetry breaking only, but not actually change the sorts of the problem, so that we have as close to an apples-to-apples comparison as possible (maybe changing the sort names changes how Z3 behaves, for example). So the sort inference in v3 is used temporarily during the symmetry breaking process, then thrown away later "