| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
|
|
|
|
|
|
Removes some hacks due to Swig 2's incomplete C++11 support and adds
checks for version 3 at configuration time as well as in swig.h
|
|
|
|
|
|
|
|
|
|
Add isConst check for lambda expressions by conversions to and from an Array representation where isConst is implemented. This enables check-model to succeed on higher-order benchmarks. Change the builtin rewriter for lambda to attempt to put lambdas into constant form. Update regression.
|
|
C++11 introduced the thread_local keyword, so we don't need to use
non-standard extensions or our custom pthread extension anymore.
The behavior was previously introduced as a workaround in commit
753a072c542c1c254d7c6adbf10e091ba585ede5. This commit
introduces the macro CVC4_THREAD_LOCAL that can be used to
declare variables as thread local. For Swig, this macro is defined to
be empty.
|
|
* Replacing __gnu_cxx::hash_map with std::unordered_map.
* Replacing __gnu_cxx::hash_set with std::unordered_set.
* Replacing __gnu_cxx::hash with std::hash.
* Adding missing includes.
|
|
Disable support for subrange and predicate subtypes (which were only partially supported previously).
|
|
|
|
regressions.
|
|
|
|
|
|
|
|
Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
|
|
|
|
|
|
declaration in cvc printer.
|
|
|
|
during call to mkMutualDatatypes.
|
|
|
|
|
