1. All changes to be merged should reside on a branch of your fork of cvc5.

   • GitHub Actions workers on the main cvc5 repository are shared by everyone and should primarily be used for testing pull requests and main. You get separate GitHub Actions workers for testing branches on your fork, so it is highly encouraged that you use this to not congenst the queue of the main repository.

   • If you made major changes, break down your changes into small chunks and submit a pull request for each chunk in order to make reviewing less painful.

   • Do not commit work in progress. You should always create pull requests for self-contained finished chunks. New features that are too big for one pull request should be split into smaller (self-contained) pull requests.

   • If your pull request implements a new feature or major change, it should also update the NEWS file.

2. Create a pull request via GitHub.

3. If you are a member of the cvc5 organization select at least one reviewer and label your pull request.
   If you are an external contributor, a team member will assign reviewers and labels for you.
   Label pull requests with respect to their complexity (simple, moderate, complex) and priority (normal, minor, major).
   

   • The level of complexity indicates the complexity of the code changes (and as a consequence, the reviewing task), and based on the complexity, one or two approving code reviews are required:

     • simple and moderate: Require one approving code review.

     • complex: Require two approving code reviews.

   • The level of priority indicates how urgently the changes of a pull request need to get into main:

     • major: Urgent changes/fixes that take precedence over pull requests marked as normal.

     • minor: Not urgent, normal pull requests take precedence over minor.

4. You need approval for your pull request from one (simple, moderate) or two (complex) reviewers before you can merge your pull request.

5. Commits pushed to the pull request should only contain fixes and changes related to reviewer comments.

   • We require that pull requests are up-to-date with main before they can be merged. You can either update your branch on the GitHub page of your pull request or you can (while you are on the branch of your pull request) merge the current main using git pull origin main (this creates a merge commit that can be squashed when merging the pull request) and then git push to update the pull request.

6. If reviewers make non-trivial code suggestions, you might want to consider to acknowledge them for that by adding a Co-authored-by: REVIEWER_NAME <REVIEWER EMAIL> to the description of the PR. This line will then be included in the description of the commit when it is merged back to main.

7. Merging pull requests to main.
   This step can be done on the GitHub page of your pull request.

   • Merging is only possible after GitHub Actions has succeeded.

   • Authors of a pull request are expected to perform the merge if they have write access to the repository (reviewers should not merge pull requests of developers that have privileges to do that themselves).

   • Creating merge commits for pull requests is not allowed (we prefer a linear history) and therefore disabled via the GitHub interface.

   • Squash commits are preferred over rebase commits. If the intermediate commits are not of general interest, do a squash commit

   • In most cases, GitHub should automatically add the pull request number (#<number>) to the title of the commit. Do not remove the number and add it if it is missing (useful for debugging/documentation purposes).

• Use the pull request description as commit message if the description is more detailed than the commit message. Do not use the automatically generated commit message for squashed commits that contain all commit titles (this is not descriptive at all).

• External Contributors: Make sure that the signed-off line is part of the commit message. We require external contributors to squash all commits and sign-off the commit. These PRs should be usually ready to merge without modifying any commit message.

• GitHub automatically adds a Co-authored by: …​ line to the commit message as soon as anyone other than the original author committed to the PR. This also includes branch updates from main. Only include the Co-authored by: …​ lines if the co-author contributed to the PR via suggestions or commits, but not via updating the branch.

• Make sure to include Co-authored by: …​ lines that have been included in the description of the PR by the PR author to acknowledge contributions from reviewers.

• When clearing the queue of approved PRs

  • Do not merge PRs labeled as do not merge, even if they are approved. Typically, this label is added when there’s minor fixes that need to be applied by the author before the PR is ready to merge. The author is responsible for indicating that everything has been addressed by removing this label.

  • Merge in order of submission, oldest first.

  • PRs labeled as major take precedence over ones labeled as normal and minor.

There are some good ideas on internet posts, like these:
https://alexgaynor.net/2015/dec/29/shrinking-code-review/
https://www.thedroidsonroids.com/blog/splitting-pull-request

It is the developer’s responsibility to make a PR easy to review.

To quote from the second article above:

First things first. It’s the author’s responsibility to make the code
review easy. The reviewers can’t spend as much time as you did digging
into the context of the problem. Therefore, you need to present the
code changes in a friendly form. Delivering your PR in small portions
is one of the ways to do it, but doesn’t exhaust the list.

1. PRs labeled as major should be reviewed ASAP (= within 2 days, ideally).

2. PRs should not sit around unattended for months — start working on it incrementally and submit review chunks.

3. PRs that are huge and can not be split up easily can be reviewed file by file. GitHub supports this quite well already, you can mark files as viewed and such.

4. Try to split up huge PRs if possible — it will speed up the reviewing process.

5. Feel free to bug people regularly if you’re waiting for reviews, but don’t forget that all of us only have so much time to dedicate to reviews per day (this also relates to item 4, the smaller the PRs, the faster the turnaround).

6. Review as thoroughly as possible and reasonable — it is not required that you understand every piece of code you review (semantically, not syntactically). it is great if you do, but if it takes you weeks to achieve that it might be not worth it.

This approach allows to run iwyu on a single source file, and iwyu will print suggestions for this source file and the header file of the same name. First figure out the location of the C++ standard library shipped with clang, for example /usr/lib/llvm-10/lib/clang/10.0.0/include (this is probably not necessary on MacOS) and select a source file to analyze, for example src/expr/node.cpp. Then use iwyu_tool as follows:

iwyu_tool -p <build-dir> <source-file> -- -Xiwyu --cxx17ns -I<stdlib-dir>

iwyu_tool -p . ../src/expr/node.cpp -- -Xiwyu --cxx17ns -I/usr/lib/llvm-10/lib/clang/10.0.0/include/

Note that iwyu is not perfect: it may suggest to remove headers that can not be removed; it may suggest to forward declare types where this is not possible; it may suggest to replace includes by others where it does not make sense. You should thus check every change manually!

Configure cvc5 with

Before using cvc5, first reset the code coverage counters to zero with

After using cvc5 you can generate a coverage report for all cvc5 executions since the last coverage-reset with

You will find the coverage report in build/coverage.

For testing C++ tests only, configure cvc5 with

Nightly coverage reports are available on our website.

Configure cvc5 with

and execute with

perf generates a perf.data file in the current working directory. You can generate the report with

1. Use Node to store nodes in containers or member variables.

2. Make functions take TNode and return Node.

Expressions (or nodes) in cvc5 are generally represented by Node or TNode objects. They both reference NodeValue that is actually stored in a NodeManager, but differ in that Node maintains a reference count while TNode does not. In standard C++ terms, we conceptually have Node = std::shared_ptr<NodeValue> and TNode = std::weak_ptr<NodeValue>.

The NodeValue type is not to be used by anyone except Node, TNode and NodeManager. While nodes are conceptually immutable (and Node and TNode enforce this), NodeValue is mutable and thus not suited to be used directly, even internally within the cvc5 library. Furthermore, Node and TNode both implement a minimum of sanity checking (at least in assertions-enabled builds) to ensure that they are used correctly: never referencing a NodeValue with zero reference count, for example.

Under the hood, one template type (the NodeTemplate<>) implements both Node and TNode (Node and TNode are typedefs to instantiations of the NodeTemplate<> template with reference-counting turned on and off). Thus, Node and TNode provide the same interface and can be exchanged easily without compiler troubles (if it is safe to do so, of course).

The Node type maintains reference counts, and thus ensures proper lifetimes for all nodes. When a Node object is created pointing to a NodeValue, it increases the reference count on that NodeValue. When the Node is destructed (or points away), it decrements the reference count. As soon as the reference count is zero, the respective NodeValue is eligible for reclamation by the NodeManager: it will soon be deallocated and can no longer be used.

The TNode does not maintain reference counts, which avoid some overhead which can be significant in certain scenarios. However, it is also prone to issues when the underlying NodeValue is deallocated while a TNode is still being used.

Most importantly: If in doubt, use Node. Using Node is always safe, using TNode instead can provide some performance benefits. Hence, the question actually is: When is it safe to use TNode?

Whether a TNode can be used depends on some Node keeping the underlying NodeValue alive. As long as this is ensured, using TNode is safe. Some typical examples for safe and unsafe usage of TNode are listed below.

Several properties, in particular relative ordering as per standard comparison operators, of nodes depend on their id, which is dynamically chosen upon node construction. Hence, if a node is deallocated and then reconstructed, it is not necessarily the same. Similarly, TNode objects do not become "safe again" when a node is re-constructed. Note that in reality, a re-created node oftentimes does have the same underlying NodeValue, since zero-reference-count nodes are not immediately reclaimed (they are in the so-called zombie state, and they are reclaimed in bulk when there are enough zombies). But because they are immediately eligible for reclamation, you cannot rely on this. This also implies that it is not sufficient that "a corresponding Node exists every time a TNode is used", but we need to ensure that "a corresponding Node exists continuously as long as a TNode is used".

A common practice is to take function arguments as const& to avoid (oftentimes expensive copy operations). Albeit not being trivially copyable (in the strict standard C++ sense of std::is_trivially_copyable), copying a TNode is almost certainly simplified to a single register assignment when compiler optimization is enabled. Using a reference (which copies a pointer to the referenced node internally) can thus not be expected to be any faster, but may instead pose problems for caching: while accessing a function argument TNode tn only accesses the current stack frame (where tn lives) and the NodeValue in the NodeManager, when using references we may need to additionally access the place where the referenced TNode lives.

While move semantics (&&, std::move) can be greatly beneficial, their benefit depends on the possibility to make a move more efficient than a copy. Given that the special "null value" (Node()) is reference counted as well, every new Node requires increasing some reference count. Using Node(Node&& n) instead of Node(const Node& n) could merely change which reference counts are changed when, but not change their overall number. We thus do not offer move semantics and thereby keep the interface (slightly) simpler.

Regression tests consist of input files and expected outcomes, so they perform end-to-end testing of the cvc5 binary. All the regression tests are located in test/regression/. See the README in the corresponding directory for details on the format, the organization, and how to add new regressions.

Unit tests a small portion (a unit) of the code base. We use CxxTest to implement the unit tests. To run the unit tests, CxxTest needs to be installed on the machine.

All the unit tests are located in test/unit/. For instructions on how to run the unit tests, refer to the INSTALL guide.

System, or API, testing is a form of regression testing on cvc5 libraries rather than the driver. Rather than .cvc and .smt2 instances as input, a system test is a source file that is built and linked against the cvc5 libraries and uses its API, bypassing the usual cvc5 driver. These tests are located under test/system/.

Every non-exceptional line of code should be covered by our tests. To generate code coverage information using gcov, configure cvc5 with --coverage. For more detailed instructions about coverage testing, seehttps://github.com/cvc5/cvc5/wiki/Developer-Guide#code-coverage-reports[how to generate code coverage reports]. , compile the project, then run make coverage. This generates an HTML report of the coverage information in <build_dir>/coverage. For more details on how to generate coverage reports and test for uncovered functions, see profiling code.

You can configure multiple cvc5 builds to be built in separate build directories. By default ./configure.sh creates a directory build, with ./configure.sh --name=<build-directory> you can create a build directory with name <build-directory>.

You can determine the build type of a cvc5 binary with the --show-config command-line option. For example, the following command shows the config of a production build.

To see if the binary is statically linked, or not, use the ldd command:

The above output is from a dynamically linked cvc5 binary, which is dynamically linked against the cvc5 libraries libcvc5parser.so.1 and libcvc5.so.1. This is the default behavior of the build system.

If the cvc5 libraries are missing from the list, the binary was statically linked against the cvc5 libraries and dynamically linked against system libraries. This can be achieved by configuring with ./configure.sh --static --no-static-binary.

If you want a fully static binary, which is also statically link against system libraries use: ./configure.sh --static.

Note that on some platforms compiling a fully static binary may be difficult or not possible. In these cases use the --no-static-binary configure option.

When you create new source and header files make sure to add them via git add …​ and add them to the corresponding CMakeLists.txt file. If the file you create is in a directory with a CMakeLists.txt add it to this file, otherwise in most of the cases you want to add it to src/CMakeLists.txt.

Here are some important gotchas to keep in mind:

1. Your ContextObj subclass must call destroy() from its destructor. This ensures that, if prematurely destructed (that is, before the Context goes away), your object is properly unregistered from the Context.

2. Be careful if you allocate in an alternative memory manager (see below).

3. FIXME add more gotchas

You need to be careful; even at a high scope level, all objects registered for backtracking with a Context are inserted at scope zero. This means your program will crash if you delete the associated memory too soon. Now re-read that sentence. If you create a CDO<int> (with new) at scope level 10, and delete it upon backtracking to scope level 9, the CDO<int> destructor properly unregisters itself from the Context. However, if you allocate it in a memory manager (such as the ContextMemoryManager) that doesn’t guarantee that the destructor is called, your program will crash (perhaps much later), because the object is still registered at scope level 0 (and thus a bad pointer appears on a list). You may prefer to create a CDO<int*> rather than a CDO<int>*, which solves the issue (you can prematurely delete the int* without incident). But that may leak memory, so there are additional constructors in ContextObj and CDO<> (those starting with a bool argument) that specifically "register" the object at the current scope level. They aren’t registered at scope level 0, so the problem doesn’t occur. However, you have to be careful.

But why allocate ContextObj instances with the ContextMemoryManager if it’s so complicated? There’s a big advantage: you don’t have to track the lifetime of the ContextObj. The object simply ceases to exist when the Context is popped. Thus you can create an object in context memory, and if you stow pointers to it only in context memory as well, all is cleaned up for you when the scope pops. Here’s a list of gotchas:

1. For data structures intended solely to be allocated in context memory, privately declare (but don’t define) an operator new(size_t) and destructor (as currently in the Link class).

2. For data structures that may or may not be allocated in context memory, and are designed to be that way (especially if they contain ContextObj instances), they should be heavily documented---especially the destructor, since it may or may not be called.

3. There’s also an issue for generic code---some class Foo<T> might be allocated in context memory, and that might normally be fine, but if T is a ContextObj this requires certain care.

4. Note that certain care is required for ContextObj inside of data structures. If the (enclosing) data structure can be allocated in ContextMemoryManager ("CMM"), that means the (enclosed) ContextObj can be, even if it was not designed to be allocated in that way. In many instances, it may be required that data structures enclosing ContextObj be parameterized with a similar bool allocatedInCMM argument as the special constructor in this class (and pass it on to all ContextObj instances).

All documentation that lives in the docs folder is written in *.rst files in the reStructuredText format and directly processed by Sphinx. See https://www.sphinx-doc.org/en/master/ for general information. The different APIs are made available via language-specific toolchains and can be linked via "domains", e.g. :cpp:class: for a C++ class. We have a few custom Sphinx extensions:

• examples is used for the examples. For a particular example, it renders one tab per language the example is available in and provides syntax highlighting. It heavily relies on the sphinx_tabs extension.

• include_build_file allows to include rst files from the build folder, i.e., documentation sources that has been automatically generated by the build system, e.g., for command line options. This is necessary as Sphinx does not support multiple source folders.

The C++ API sources are parsed with doxygen, which is configured to only produce xml output. This xml output is then used by the Sphinx extension breathe. Typically, we have one rst file for an API class (and associated helper classes) that uses .. doxygenclass:: to render the class documentation.

When writing documentation in the C++ API, be aware that these comments are processed by doxygen, not by Sphinx!

Sphinx supports python natively (via the autodoc extension). autodoc requires the python library to be built and then generates the documentation from the docstrings exposed by the library.