| Age | Commit message (Collapse) | Author |
|---|
|
We store constants, e.g., BitVector and Rational, in our node infrastructure. As a result, we were indirectly including some headers in almost all files, e.g., the GMP headers. This commit changes that by forward-declaring the classes for the constants. As a result, we have to include headers like util/rational.h explicitly when we use Rational but it saves about 3 minutes in compile time (CPU time).
The commit changes RoundingMode from an enum to an enum class such that it can be forward declared.
|
|
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Similar to #6031, this PR implements suggestions from iwyu to reduce the number of includes in header files by introducing forward declarations and moving includes to source files.
|
|
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
|
|
|
|
Until now, the `Rewriter` was responsible for creating `TheoryRewriter`
instances. This commit adds a method `mkTheoryRewriter()` that theories
override to create an instance of their corresponding theory rewriter.
The advantage is that the theories can pass additional information to
their theory rewriter (e.g. a statistics object).
|
|
pass_bv_gauss_white.h included bv_gauss.cpp to test the functions in the
anonymous namespace, which resulted in ODR (one definition rule)
violations reported by ASAN.
This commit exposes the functionality required in the unit tests as
private static members of the BVGauss class. Since this is a white unit
test, we can access private members in the tests.
|
|
Fixes 2887.
|
|
|
|
|
|
|
