summaryrefslogtreecommitdiff
path: root/src/expr/node_manager.cpp
AgeCommit message (Collapse)Author
2020-08-01Add methods for constructing datatype types from NodeManager (#4823)Andrew Reynolds
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.
2020-07-17Add NodeManagerScopes to fix use-after-free issues (#4768)Andres Noetzli
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.
2020-07-07Transfer ownership of internal Options from NodeManager to SmtEngine (#4682)Andrew Reynolds
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.
2020-06-16Update copyright headers.Aina Niemetz
2020-06-06Fix destruction order in NodeManager (#4578)Andres Noetzli
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.
2020-06-05(proof-new) Rename ProofSkolemCache to SkolemManager (#4556)Andrew Reynolds
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.
2020-06-03(proof-new) Adding rules and proof checker for EUF (#4559)Haniel Barbosa
2020-05-30Add the sequence type (#4539)Andrew Reynolds
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.
2020-04-14Remove early type check option (#4234)Andrew Reynolds
Required to decouple options from NodeManager. This option is now always enabled in debug, and disabled in production.
2020-04-08Eliminate call to currentNM within NodeManager (#4227)Andrew Reynolds
Eliminates 2 unintentional calls to the global access function.
2020-03-27Do not require that function sorts are first class internally (#4128)Andrew Reynolds
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 .
2020-03-05Enable -Wshadow and fix warnings. (#3909)Mathias Preiner
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>
2020-02-19resource manager: Add statistic for every resource. (#3772)Mathias Preiner
This commit adds statistics for all resource steps. A resource statistic is incremented by 1 if the resource is spent (via `spendResource`). Fixes #3751.
2019-12-16Move Datatype management to ExprManager (#3568)Andrew Reynolds
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.
2019-12-11Activate node-level datatype API (#3540)Andrew Reynolds
2019-12-06Add ExprManager as argument to Datatype (#3535)Andrew Reynolds
2019-12-05Introduce the Node-level Datatypes API (#3462)Andrew Reynolds
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.
2019-11-11Add missing utilities for Node-level Datatype API (#3451)Andrew Reynolds
2019-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
2019-03-28Fix freeing nodes with maxed refcounts (#2903)Andres Noetzli
2019-03-26Update copyright headers.Aina Niemetz
2018-08-07Require Swig 3 (#2283)Andres Noetzli
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
2018-08-01Fix issues with printing parametric datatypes in smt2 (#2213)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2018-03-02Fixed typo.Aina Niemetz
2018-01-17Removes yet more throw specifiers. Updating the documentation as needed. (#1518)Tim King
2017-09-13Add isConst check for lambda expressions. (#1084)Andrew Reynolds
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.
2017-08-30Use thread_local instead of compiler extensions (#210)Andres Noetzli
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.
2017-07-20Moving from the gnu extensions for hash maps to the c++11 hash mapsTim King
* 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.
2017-07-12Make type rules more strict for operators whose type rules involve subtypes. ↵ajreynol
Disable support for subrange and predicate subtypes (which were only partially supported previously).
2017-07-07Update copyright headers.Mathias Preiner
2017-04-14Actively split for upwards closusure intersection. Minor clean up, add ↵ajreynol
regressions.
2017-04-14Fix bug related to portfolio with nullary operators.ajreynol
2017-04-14Fix nullary operator printers, minor.ajreynol
2017-04-12Add nullary operator metakind.ajreynol
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove ↵ajreynol
Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
2016-12-29Eliminating a signed vs. unsigned comparison.Tim King
2016-11-10Adding garbage collection of nodes with maxed out reference counts.Tim King
2016-11-01Make tuple and record names unique. Do not print internal datatype ↵ajreynol
declaration in cvc printer.
2016-11-01Fix memory leak in TheorySetsRels. Minor cleanup.ajreynol
2016-11-01Revert change to datatypes API for passing pointers, instead make deep copy ↵ajreynol
during call to mkMutualDatatypes.
2016-11-01Working memory leak free version, changes interface to pointers.ajreynol
2016-10-31Minor refactoring in preparation for datatypes node cycle breaking.ajreynol
2016-09-14Support for unique variable generation in node manager.ajreynol
2016-09-12Ensure sep.nil is unique per type at NodeManager level. Add simple symmetry ↵ajreynol
breaking in theory sep.
2016-06-17Cleanup from last commit, treat sep.nil as variable kind.ajreynol
2016-04-03Updating the copyright headers and scripts.Tim King
2016-02-15More simplification to internal implementation of tuples and records.ajreynol
2016-02-15Eliminate most of the internal representation infrastructure for tuples and ↵ajreynol
records, replace with datatypes throughout, update cvc printer for tuples/records. Minor changes to API for records and tuples.
2016-01-28Adding listeners to Options.Tim King
- Options -- Added the new option attribute :notify. One can get a notify() call on the Listener after a the option's value is updated. This is the new preferred way to achieve dynamic dispatch for options. -- Removed SmtOptionsHandler and pushed its functionality into OptionsHandler and Listeners. -- Added functions to Options for registering listeners of the notify calls. -- Changed a number of options to use the new listener infrastructure. -- Fixed a number of warnings in options. -- Added the ArgumentExtender class to better capture how arguments are inserted while parsing options and ease memory management. Previously this was the "preemptGetopt" procedure. -- Moved options/options_handler_interface.{cpp,h} to options/options_handler.{cpp,h}. - Theories -- Reimplemented alternative theories to use a datastructure stored on TheoryEngine instead of on Options. - Ostream Handling: -- Added new functionality that generalized how ostreams are opened, options/open_stream.h. -- Simplified the memory management for different ostreams, smt/managed_ostreams.h. -- Had the SmtEnginePrivate manage the memory for the ostreams set by options. -- Simplified how the setting of ostreams are updated, smt/update_ostream.h. - Configuration and Tags: -- Configuration can now be used during predicates and handlers for options. -- Moved configuration.{cpp,h,i} and configuration_private.h from util/ into base/. -- Moved {Debug,Trace}_tags.* from being generated in options/ into base/. - cvc4_private.h -- Upgraded #warning's in cvc4_private.h and cvc4_private_library.h to #error's. -- Added public first-order (non-templatized) member functions for options get and set the value of options outside of libcvc4. Fixed all of the use locations. -- Made lib/lib/clock_gettime.h a cvc4_private_library.h header. - Antlr -- Fixed antlr and cvc4 macro definition conflicts that caused warnings. - SmtGlobals -- Refactored replayStream and replayLog out of SmtGlobals. -- Renamed SmtGlobals to LemmaChannels and moved the implementation into smt_util/lemma_channels.{h,cpp}.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback