| Age | Commit message (Collapse) | Author |
|---|
|
This PR does a major refactoring on how we organize our builds to allow both shared and static builds. We now build the libraries using object libraries to allow building the libraries both dynamically and statically in the same build folder, though the static library is optional (ENABLE_STATIC_LIBRARY). The binary is linked either dynamically or statically (depending on ENABLE_STATIC_BINARY).
|
|
This commit identifies a couple of scenarios where an operation required
2 searches into a map/hashmap and replaces them with a single search.
This also makes the code shorter.
Signed-off-by: Mikolas Janota <mikolas.janota@gmail.com>
|
|
backtrackable.h was defining a datastructure Backtracker, which was
a member in ArrayInfo and Info but it was not doing anything.
|
|
Fixes #6453. This commit replaces all calls to std::allocator with calls to
std::allocator_traits. Strictly speaking, allocate() and deallocate() are
not deprecated but the commit replaces them for uniformity.
|
|
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
|
|
This commit adds CDList::emplace_back(), which allows users to create
elements in CDList in-place (as opposed to copying the items using
CDList::push_back(). This allows CDList to be used with
std::unique_ptrs, which do not allow copying. Using
CDList::emplace_back() could also be more efficient in certain cases.
|
|
This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
|
|
cmake complains that the static base and context libraries are not
exported as install targets. Since we do not want to install these
libraries we'll build object libraries instead.
|
|
This PR creates a support library from the utilities in base and context, which will be required in the parser as soon as we move the symbol table/manager to the parser.
Note: I decided to always build static libraries from base and context (and optionally enable -fPIC for shared builds) since I'm not sure if we want to have these libraries installed separately. Right now these are considered as cvc5 internal utilities that can be used in all cvc5 libraries, but not outside.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
We do not allow that a context object is invalid on destruction.
This guards against invalid use as described in #2607. Note that #2607
proposed to skip invalid objects on destruction. We now rather do not
allow for such a case to occur at all.
|
|
This PR does some more cleanup of the includes.
|
|
|
|
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 further removes obsolete explicit includes of stdint.h.
|
|
|
|
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.
|
|
|
|
|
|
Our `CDMapBlack` test failed to compile with newer versions of libstdc++
because they require the `value_type` to be defined for the iterator
(accessed via `std::iterator_traits`). Due to the implementation of
`std::iterator_traits`, we also need to define `iterator_category`,
`difference_type`, `pointer`, and `reference`.
|
|
Fix syntax error when --language-bindings is java
Replace __attribute__((__unused__)) with CVC4_UNUSED macro
Signed-off-by: matken11235 <26405363+matken11235@users.noreply.github.com>
|
|
Fixes 2887.
|
|
|
|
TODO: cvc4autoconfig.h
|
|
|
|
(#2355)
There do not appear to be any instances these can be positive.
|
|
* Proposal for adding map utility functions to CVC4.
|
|
C++11 supports explicitly deleting functions that should not be used
(explictly or implictly), e.g. copy or assignment constructors. We were
previously using the CVC4_UNDEFINED macro that used a compiler-specific
attribute. The C++11 feature should be more portable.
|
|
Changing the return type of CDHashMap::iterator* to return a reference. Requires performance testing.
|
|
|
|
preparation for adding map utility functions. (#2209)
|
|
|
|
|
|
|
|
Adds missing override keywords.
|
|
Previously, we had -DCVC4_CONTEXT_MEMORY_MANAGER that needed to be added as a compile flag
to use the context memory manager (which we want by default). This makes compiling with
other build systems cumbersome because you have to know about the flag.
This commit replaces the -DCVC4_CONTEXT_MEMORY_MANAGER flag with a -DCVC4_DEBUG_CONTEXT_MEMORY_MANAGER
flag that does the opposite (in absence of the flag, we use the context memory manager).
Additionally, the commit fixes a memory leak in the debug context memory manager (the
destructor did not clean up the allocations).
|
|
|
|
|
|
|
|
My last commit for the Valgrind instrumentation contained a typo that
made the nightlies fail. This commit fixes the issue.
|
|
This commit adds two configuration options that help debugging memory
issues with allocations in the ContextMemoryManager:
--enable/disable-valgrind: This flag enables/disables Valgrind
instrumentation of the ContextMemoryManager. Enabled by default for
debug builds if the Valgrind headers are available.
--enable/disable-context-memory-manager: This flag enables/disables the
use of the ContextMemoryManager. If the flag is disableda dummy
ContextMemoryManager is used that does single allocations instead of
chunks. The flag is enabled by default.
|
|
|
|
This is a patch, originally from mdeters/cdhashmap-default-constructibility that allows CDHashMaps to be declared for objects that don't have default constructors.
|
|
|
|
|
