| Age | Commit message (Collapse) | Author |
|---|
|
|
|
As it turns out, self-registering types are problematic with static
linkage [0]. Instead of fixing the issue with linker flags, which seems
possible but also brittle (e.g. the flags may be different for different
linkers), this commit adds an explicit registration of each
preprocessing pass.
[0] https://www.bfilipek.com/2018/02/static-vars-static-lib.html
|
|
This commit refactors how preprocessing pass registration works,
inspired by LLVM's approach [0]. The basic idea is that every
preprocessing pass declares a static variable of type `RegisterPass` in
its source file that registers the pass with the
`PreprocessingPassRegistry` when starting the program. The registry is a
singleton that keeps track of all the available passes and allows other
code to create instances of the passes (note: previously the registry
itself was owning the passes but this is no longer the case). One of the
advantages of this solution is that we have a list of available passes
directly at the beginning of the program, which is useful for example
when parsing options.
As a side effect, this commit also fixes the SortInference pass, which
was expecting arguments other than the preprocessing pass context in its
constructor.
This commit is required for fixing dumping pre/post preprocessing
passes. It is also the ground work for allowing the user to specify a
preprocessing pipeline using command-line arguments.
[0] https://llvm.org/docs/WritingAnLLVMPass.html
|
|
This fixes a few open issues with symmetry detection algorithm. It also extends the algorithm to do:
- Alpha equivalence to recognize symmetries between quantified formulas,
- A technique to recognize a subset of variables in two terms are symmetric, e.g. from x in A ^ x in B, we find A and B are interchangeable by treating x as a fixed symbol,
- Symmetry breaking for maximal subterms instead of variables.
|
|
variables (#1888)
|
|
|
|
|
|
|
