watform / fortress Goto Github PK

let's refactor the code so that the options are pulled into top-level "packages" and the model finders if parameterized by 1) the solver and 2) the compiler. These packages will be complete choices (matching CLI choices) for model finding algorithm (iterative or not), package of compilers, and solver. Try to avoid mixing class extensions and options, and "names" for packages of compilers, etc.

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