| Age | Commit message (Collapse) | Author |
|---|
|
This removes the special case of TUPLE_UPDATE and RECORD_UPDATE in favor of the more general datatype update.
Datatype update is handled analogously to APPLY_SELECTOR / APPLY_TESTER.
|
|
|
|
Previously, we were conditionally checking whether a function was "flat" e.g. did not have a function type as the range type.
The original motivation for this was to catch cases where the user made a declare-fun that had function return type, which is not permitted. All these checks are already done at the API level https://github.com/CVC4/CVC4/blob/master/src/api/cpp/cvc5_checks.h#L441.
However, internally we should have no such restriction. This is required for simplifying the LFSC term processor.
|
|
This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
|
|
|
|
|
|
Fixes #5150.
|
|
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
|
|
|
|
|
|
Currently, SEXPR applications are given a parametric type SEXPR_TYPE applied to the types of its arguments. This means that SEXPR that are type checked consume roughly double the memory. This issue arises in practice when printing proofs in the internal calculus.
There is no need to have SEXPR_TYPE as a parametric type, this PR makes SEXPR simply typed.
Also moves some implementation of TypeNode methods to type_node.cpp.
|
|
This PR does some refactoring on how we handle statistics in the driver, and some minor cleanup along the way.
The SmtEngine now has dedicated statistics for the data collected within the driver and provides utility functions to set them.
The driver pushes the collected statistics to the SmtEngine instead of adding them itself to the statistics registry.
The node manager no longer holds a statistics registry (that nobody used anymore anyway)
The command executor no longer holds a pointer to the SmtEngine itself. The pointer is not necessary and seems to become stale after we call reset on the command executor (which, luckily, we don't seem to do usually)
The main motivation for this change is to make the whole statistics infrastructure private to the library and not exporting it to the outside world.
|
|
This eliminates one of the dependencies of TypeNode on options. In particular, this makes it so that function types are always considered first-class.
This change makes it so that higher-order types can always be constructed; logic exceptions should occur if they are used in constraints.
|
|
|
|
This is in preparation for deleting the Expr layer.
This further fixes incorrect handling of ownership for the datatypes
owned by the NodeManager.
|
|
This also renames metakind::getLowerBoundForKind and
metakind::getUpperBoundForKind for consistency.
Note that the NodeManager class needs to be reordered to comply to our
style guidelines. This PR does not reorder but introduces a public block
at the top (where the rest of the public interface of the class should
go eventually).
|
|
|
|
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 is required for creating the representation of closues in LFSC, which are of the form ((forall x T) P) where notice that forall has non-flat function type (-> Int Sort (-> Bool Bool)).
|
|
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 uses BoundVarManager for several key places where bound variables are introduced, including for array extensionality witness terms, string preprocessing, quantifiers rewriting, and skolemization.
This is motivated by making certain steps in solving deterministic for the sake of proofs, and gives a more consistent pattern in general for constructing bound variables.
|
|
|
|
Required for detangling NodeManager from the Expr layer.
|
|
Required for updating the new API to use Node utilites as backend.
These utilities are copied directly from ExprManager and converted Expr -> Node.
|
|
This addresses the nightly failures. It ensures a node manager is in scope when constructing type nodes.
It also simplifies the construction of atomic type nodes to avoid an extra TypeNode(...) constructor.
|
|
This PR removes subtyping rules for bags and add operator MakeBagOp similar to SingletonOp
|
|
This PR removes subtyping for sets theory due to issues like #4502, #4507 and #4631.
Changes:
Add SingletonOp for singletons to specify the type of the single element in the set.
Add mkSingleton to the solver to enable the user to pass the sort of the single element.
Update smt and cvc parsers to use mkSingleton when the kind is SINGLETON
|
|
This PR adds initial headers and mostly empty source files for the theory of bags (multisets).
It acts as a basis for future commits.
It includes straightforward implementation for typing rules an enumerator for bags.
|
|
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 PR makes two simultaneous changes:
The new API uses Node-level DType instead of Expr-level Datatype. This required converting 2 of the last remaining calls in the parser that used Expr to use the new API.
Internally constructed datatypes (e.g. for sygus) use Node-level DType instead of Expr-level Datatype. Note this required moving a block of code for handling a corner case of sygus from Datatype -> DType.
This PR removes :
ExprManger::mkDatatypeType.
The Expr-level datatype itself. This PR removes all references to its include file.
It also updates one remaining unit test from Expr -> Node.
This PR will enable further removal of other datatype-specific things in the Expr layer.
|
|
This includes all fixes encountered while fixing unit tests with the Term -> Node version of Datatypes in the API.
After all pending PRs are merged, the next step will be to convert the new API to use e.g. CVC4::DType instead of CVC4::Datatype everywhere.
|
|
This is work towards eliminating the Expr-level datatype.
This PR implements the required methods for constructing datatype types from NodeManager.
In particular, this PR copies the "mkMutualDatatypeTypes" methods and converts them to Node-level.
The next PRs will be in preparation for using these methods instead of the Expr-level ones.
It also adds a flag d_isRecord to DType, which is required for supporting record printing in the cvc printer, which will be updated in another PR.
It also eliminates an interface for constructing constructor types via Expr-level DatatypeConstructor objects, which was unused.
|
|
This commit fixes our current ASan issues. Some methods in `NodeManager`
were not creating a `NodeManagerScope` for `this` but were indirectly
calling methods that get the `NodeManager` from the current scope, so we
ended up calling methods on a `NodeManager` that had already been
destroyed.
|
|
This PR decouples Options from NodeManager. Instead, options now live in SmtEngine.
The changes that were required for this PR include:
The main internal options object is now owned by SmtEngine instead of ExprManager.
The ownership resource manager is moved from NodeManager to SmtEngine.
Node manager listeners are deleted, timeouts and resource limits are set during SmtEngine::finishInit.
A temporary hack was added to make the last constructed SmtEngine to be the one in scope. This ensures that options are in scope whenever an SmtEngine is created.
The methods for invoking "subsolvers" (theory/smt_engine_subsolver.h,cpp) was simplified, as versions of these calls that change options do not have to clone a new copy of the ExprManager anymore.
Resource manager was removed from the smt2 parser.
Minor refactoring was done in SmtEngine to copy "original options" so that options are restored to their state after parsing command line options on reset.
Updates to unit tests to ensure conformance to new options scoping.
|
|
|
|
Fixes #4576. ASan was reporting memory leaks because the skolem manager
was being destroyed after the attributes and zombies were already
cleaned up in the destructor of NodeManager. This commit changes the
destruction order to ensure that the skolem manager is destroyed before
the rest of the cleanup.
Note: this issue did not only make the benchmark in #4576 fail but
several tests in our regressions.
|
|
This PR changes the design of ProofSkolemCache so that it has facilities for tracking proofs. This is required so that the term formula removal pass can be made proof-producing.
This makes it so that ProofSkolemCache is renamed to SkolemManager, which lives in NodeManager. Creating (most) skolems must be accompanied by a corresponding ProofGenerator that can provide the proof for the existential corresponding to their witness form.
Further updates will include refactoring the mkSkolemExists method of SkolemManager so that its contract wrt proofs is simpler.
Once all calls to mkSkolem go through the standard interface, then NodeManager::mkSkolem will be moved to SkolemManager::mkSkolemInternal.
|
|
|
|
This adds basic infrastructure for the sequence type, including its type rules, type enumerator and extensions to type functions.
The next step will be to finalize the support in TheoryStrings for sequences and then add front end support for sequences in the API/parsers.
|
|
Required to decouple options from NodeManager.
This option is now always enabled in debug, and disabled in production.
|
|
Eliminates 2 unintentional calls to the global access function.
|
|
This PR removes the requirement in the NodeManager that argument types to the function sort are first class.
Notice that the new API does this check (as it should): https://github.com/CVC4/CVC4/blob/master/src/api/cvc4cpp.cpp#L2633
Moreover, SyGuS v2 internally requires constructing function types having arguments that are not first class (e.g. regular expression type). This is required to update the regression https://github.com/CVC4/CVC4/blob/master/test/regress/regress1/sygus/re-concat.sy to SyGuS v2.
FYI @abdoo8080 .
|
|
Fixes all -Wshadow warnings and enables the -Wshadow compile flag globally.
Co-authored-by: Clark Barrett <barrett@cs.stanford.edu>
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
Co-authored-by: makaimann <makaim@stanford.edu>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Co-authored-by: AleksandarZeljic <zeljic@stanford.edu>
Co-authored-by: Caleb Donovick <cdonovick@users.noreply.github.com>
Co-authored-by: Amalee <amaleewilson@gmail.com>
Co-authored-by: Scott Kovach <dskovach@gmail.com>
Co-authored-by: ntsis <nekuna@gmail.com>
|
|
This commit adds statistics for all resource steps. A resource statistic is incremented by 1 if the resource is spent (via `spendResource`).
Fixes #3751.
|
|
This is further work towards decoupling the Expr layer from the Node layer.
This commit makes it so that ExprManager does memory management for Datatype while NodeManager maintains a list of DType.
As a reminder, the ownership policy (and level of indirection through DatatypeIndex) is necessary due to not being able to store Datatype within Node since this leads to circular dependencies in the Node AST.
|
|
|
|
|
|
This adds classes corresponding to the Node-level Datatype API "DType", which is a specification for a datatype type. It does not enable the use of this layer yet. A followup PR will update the Expr-level Datatype to use the Node-level code, which is currently verified to be functional on this branch: https://github.com/ajreynol/CVC4/tree/dtype-integrate. Futher PRs will make the internal (Node-level) code forgo the use of the Expr-layer datatype, which will then enable the Expr-layer to be replaced by the Term-layer datatype.
Most of the documentation for the methods in DType/DTypeConstructor/DTypeSelector was copied from Datatype/DatatypeConstructor/DatatypeConstructorArg.
|
|
|
|
|
