| Age | Commit message (Collapse) | Author |
|---|
|
This renames everything but GitHub links and build system related
macros. Switching the build system to cvc5 will be the last step in the
renaming process.
|
|
This PR refactors how we collect statistics.
It splits the current statistic values into the values and a proxy object. The actual values now live inside the registry (making the ownership model way easier) while the proxy object are handed to whoever wants to collect a new statistic.
It also extends the C++ API to obtain and inspect the statistics.
To change the ownership, this PR needs to touch every single statistic in the whole codebase and change how it is registered.
|
|
|
|
|
|
This is in preparation for refactoring skolem creation throughout the code base to improve proofs and migrate Theory::expandDefinitions to Rewriter::expandDefinitions.
This PR also eliminates some unused code in TheoryArithPrivate.
Followup PRs will start formalizing/eliminating calls to mkDummySkolem.
|
|
Currently, NodeBuilder takes a single template argument: An integer
that determines the expected number of arguments. This argument is used
to determine the size of the d_inlineNvChildSpace array. This array is
used to construct nodes inline. The advantage of this is that we don't
have to allocate a NodeValue on the heap for the node under
construction until we are sure that the node is new. While templating
the array size may save some stack space (or avoid a heap allocation if
we statically know that we a fixed number of children and that number is
greater than 10), it complicates the code and leads to longer compile
times. Thus, this commit removes the template argument and moves some of
the NodeBuilder code to a source file for faster compilation.
CPU build time before change (debug build): 2429.68s
CPU build time after change (debug build): 2228.44s
Signed-off-by: Andres Noetzli noetzli@amazon.com
|
|
|
|
|
|
Creating BitVectors (and deleting them) is in general expensive because
of the underlying multi-precision Integer. If possible, unnecessary
constructions and desctructions of BitVectors should be avoided.
The most common use case for `setBit` is that for an existing BitVector,
a given bit should be set to a certain value. Not doing this in place
generates unnecessary constructions and destructions of BitVectors.
|
|
This PR uses IntegralHistogramStat instead of HistogramStat when appropriate, that is everywhere.
|
|
This PR does a first round of refactoring on the statistics, in particular the Stat class and derived classes.
It significantly shrinks the class hierarchy, modernizes some code (e.g. use std::chrono instead of clock_gettime), removes unused features (e.g. nesting of statistics) and does some general cleanup and consolidation.
Subsequent PRs are planned to change the ownership model (right now every module owns the Stat object) which makes the whole register / unregister mechanism obsolete.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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 cleans up a ton of includes, based on the suggestions of iwyu.
Mostly, it removes includes from header files in favor of forward declarations and adds includes to source files.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This PR adds a new statistics class that improves on HistogramStat if we know that the type is integral (also supporting enums).
Instead of using a comparably slow std::map like HistogramStat, IntegralHistogramStat uses a std::vector that is resized appropriately.
The integral values are simply cast to std::int64_t and used as indices into the vector.
|
|
This deletes variable flags from NodeManager::mkVar and moves ExprManager sort flags to NodeManager.
These flags are used for determining when a variable or sort should be printed via the old dump infrastructure. The old dump infrastructure is simplified in this PR accordingly.
This PR should preserve behavior of the previous dumping with a minor exception that the internal trace "declarations" will also included symbols introduced from define-fun. This will be further refactored later. This is in preparation for removing the includes expr.h/expr_manager.h from node_manager.h.
|
|
|
|
|
|
This sets up the infrastructure for migrating unit tests from CxxTest to
Google Test. It further migrates api/datatype_api_black to the new
infrastructure.
|
|
The following tests fail (locally) when compiling with debug and without symfpu:
unit/api/sort_black (Failed)
unit/theory/logic_info_white (Failed)
unit/util/floatingpoint_black (Child aborted)
This PR conditions the relevant parts of these tests to the availability of symfpu.
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
|
|
|
|
Previously, BitVector::setBit only allowed to set the bit at the given
index to 1. This changes its behavior to be also able to set it to 0.
|
|
|
|
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.
|
|
This updates remaining uses of the Expr-level Datatype that are not related to their creation / memory management in ExprManager.
This required updating a unit test from Expr -> Node.
|
|
This replaces the old options listener infrastructure with the OptionsManager introduced in cb8d041.
It eliminates a "beforeSearchListener", which was a custom way of some options throwing a modal exception if they were set after initialization. Now all options are consistent: no option can be set after initialization.
It also moves managed ostream objects to the OptionsManager.
@mpreiner The next step will be to remove the "notifies" field from the Options build system and then proceed with cleaning src/options/.
|
