summaryrefslogtreecommitdiff
path: root/src/expr/node_manager.cpp
AgeCommit message (Collapse)Author
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}.
2016-01-08Adding a new Listener utility class. Changing the ResourceManager to use ↵Tim King
Listeners for reporting hard and soft resource out() events.
2016-01-08Removing StatisticsRegistry's static functions current() and registerStat().Tim King
- The functionality the get the StatisticsRegistry attached to the SmtEngine was previously through StatisticsRegistry::current(). This is the dominant StatisticsRegistry in the code. (There is another StatisticsRegistry attached to the NodeManager.) Having this be a static function on StatisticsRegistry requires the use of an SmtEngine in the wrong compilation unit. - Usages of StatisticsRegistry::current() that were visible in prop/{bvminisat,minisat} has been removed. A pointer to the relevant StatisticsRegistry should be passed instead into the constructor. - The function StatisticsRegistry::current() has been replaced by SmtScope::currentStatisticsRegistry(). SmtScope is in the libcvc4 package, where SmtEngine is available in the compilation unit. - The function smtStatisticsRegistry() is a synonym for SmtScope::currentStatisticsRegistry() in smt/smt_statistics_registry.h. This header has fewer include dependencies than the one for SmtScope. - Correspondingly, the static functions StatisticsRegistry::{registerStat, unregisterStat} have been removed. One should instead use smtStatisticsRegistry()->{registerStat,unregisterStat} instead. - The KEEP_STATISTIC macro has been moved into smt/smt_statistics_registry.h. - Documents the reason StatisticsRegistry is CVC4_PUBLIC. This lets me remove the warning I added. - Removing most operators for timespec from statistics_registry.h file. These a bit error prone in clang. - Most of the really confusing ifdef's in util/statistics_registry.h are gone.
2015-12-24Miscellaneous fixesTim King
- Splitting the two instances of CheckArgument. The template version is now always defined in base/exception.h and is available in a cvc4_public header. This version has lost its variadic version (due to swig not supporting va_list's). The CPP macro version has been renamed PrettyCheckArgument. (Taking suggestions for a better name.) This is now only defined in base/cvc4_assert.h. Only use this in cvc4_private headers and in .cpp files that can use cvc4_private headers. To use a variadic version of CheckArguments, outside of this scope, you need to duplicate this macro locally. See cvc3_compat.cpp for an example. - Making fitsSignedInt() and fitsUnsignedInt() work more robustly for CLN on 32 bit systems. - Refactoring ArrayStoreAll to avoid potential problems with circular header inclusions. - Changing some headers to use iosfwd when possible.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback