| Age | Commit message (Collapse) | Author |
|---|
|
This changes cvc5 to use a single `NodeManager` per thread (using
`thread_local`). We have decided that this is more convenient because
nodes between solvers in the same thread could be exchanged and that
there isn't really an advantage of having multiple `NodeManager`s per
thread.
One wrinkle of this change is that `NodeManager::init()` must be called
explicitly before the `NodeManager` can be used. This code can currently
not be moved to the constructor of `NodeManager` because the code
indirectly calls `NodeManager::currentNM()`, which leads to a loop
because the `NodeManager` is created in `NodeManager::currentNM()`.
Further refactoring is required to get rid of this restriction.
|
|
This PR combines the two enums InputLanguage and OutputLanguage into a single Language type. It makes sure that AST is not used as input language using a predicate whenever the option is set.
|
|
This feature is useful for example for succinctly inserting children of
a node in the reverse order. To make this work, the commit fixes the
declaration of `reference` in the `NodeValue::iterator`. The
`std::reverse_iterator` adapter expects the `reference` type to match
the return type of `operator*` in the corresponding iterator (as
mandated by the standard). Despite its name, `reference` does not have
to be a C++ reference. Note that we cannot actually make it a C++
reference because `NodeValue::iterator` wraps the `NodeValue*` in a
`Node`/`TNode` in `operator*`.
|
|
|
|
This commit adds support for braced-init-lists in calls to `mkNode()`,
e.g., `mkNode(REGEXP_EMPTY, {})`. Previously, such a call would result
in a node of kind `REGEXP_EMPTY` with a single null node as a child
because the compiler chose the `mkNode(Kind kind, TNode child1)` variant
and converted `{}` to a node using the default constructor. This commit
adds an overload of `mkNode()` that takes an `initializer_list<TNode>`
to allow this use case. It also adds a `mkNode()` overload with zero children
for convenience and removes the 4- and 5-children variants because they
saw little use. Finally, it makes the default constructor of `NodeTemplate`
explicit to avoid accidental conversions.
|
|
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
|
|
This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
|
|
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.
|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
This PR replaces the old algorithm for reconstructing sygus terms with a new "proper" implementation.
|
|
|
|
|
|
|
|
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.
|
|
Co-authored-by: Gereon Kremer <nafur42@gmail.com>
|
|
This further removes obsolete explicit includes of stdint.h.
|
|
This removes infrastructure for stream property related to printing type annotations on all variables.
This is towards refactoring the printers.
|
|
This PR adds three instantiation modes to the SyGuS instantiation module.
|
|
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.
|
|
|
|
Renamed operator CHOICE to WITNESS, and removed it from the front end
|
|
Fixes #4273 and fixes #4274 .
This also removes a spurious assertion from the Node::substitute method that the result node is not equal to the domain. This is violated for f(f(x)) { f(x) -> x }.
|
|
|
|
|
|
|
|
|
|
+ use explicit types in NodeValue
+ add unit test for Term::isParameterized()
Co-Authored-By: makaimann <makaim@stanford.edu>
|
|
|
|
|
|
|
|
Fixes 2887.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
