| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
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.
|
|
Fixes debug regressions, introduced by a combination of the addition of sequence update and the change to pointers.
|
|
This adds basic support for string/sequence updating, which has a semantics that is length preserving.
|
|
Now that we can break the old API, we don't need an ExprSequence
anymore. This commit removes ExprSequence and replaces all of its uses
with Sequence. Note that I had to temporarily make sequence.h public
because we currently include it in a "public" header because we still
generate the code for Expr::mkConst<Sequence>().
|
|
|
|
This adds the expr-level sequence datatypes. This is required for further progress on sequences. However, note that this class may be deleted in the further when the Expr level is replaced.
|
|
This class is the Node-level representation of a sequence. It is analogous to CVC4::String.
|
