| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
CMake 3.10.2 (default on Ubuntu 18.04) does not allow target_link_libraries on object libraries.
|
|
This PR does some minor refactorings in preparation for the new statistics: some renamings, removal of now obsolete code and usage of references instead of pointers.
|
|
This PR migrates CLN to a new Find script and adds the possibility to install CLN if not found in the system.
Also, it does a bit of cleanup.
|
|
|
|
|
|
Refactors GMP and libpoly to also use external projects and be available within cmake as proper targets.
|
|
This PR refactors the contrib script to download SymFPU to a cmake external project.
|
|
Since one of the last changes to the total time collection in the driver, this collection fails when the solver terminates unexpectedly (either by a signal or an exception). This PR fixes this issue and does some cleanup along the way.
|
|
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 PR eliminates all remaining uses of SExpr outside of statistics.
|
|
The build system (cmake) will automatically generate an export header
cvc4_export.h, which makes sure that the correct export features are
defined depending on the compiler and target platform. The macro CVC4_EXPORT
replaces CVC4_PUBLIC and its usage is reduced by 2/3.
Co-authored-by: Gereon Kremer <nafur42@gmail.com>
|
|
This PR does a first round of refactoring on the statistics, in particular the Stat class and derived classes.
It significantly shrinks the class hierarchy, modernizes some code (e.g. use std::chrono instead of clock_gettime), removes unused features (e.g. nesting of statistics) and does some general cleanup and consolidation.
Subsequent PRs are planned to change the ownership model (right now every module owns the Stat object) which makes the whole register / unregister mechanism obsolete.
|
|
This commit replaces all uses of assert with Assert from base/check.h to ensure that all assertions get checked in production builds with enabled assertions.
|
|
|
|
As noted in #5034, --tlimit is not working properly on windows. It turns out that the timer mechanism provided by the windows API are not suitable for our use case. Thus, this PR implements a generic std::thread-based timer mechanism which is used whenever the POSIX timers (setitimer) are not available. It also adds some documentation on the timer options and the reasons we ended up with this.
Fixes #5034.
|
|
This disables the temporarily available internals of Result.
It further changes the interface for getUnknownExplanation, which now
returns an enum value instead of a string.
|
|
Co-authored-by: Gereon Kremer <nafur42@gmail.com>
|
|
Previously we were not printing unsat cores when passing the option to dump them if we used the check-sat-assuming command or the QUERY command. This commit fixes this.
It also kills the redundant dump-synth option, as it simplifies a bit what is going on in the command executor.
|
|
This removes the dependency on the Expr layer from src/main.
This requires moving the flushing of NodeManager statistics within SmtEngine.
This is a temporary solution until we have a permanent solution for statistics.
|
|
|
|
|
|
This is a step towards migrating Commands to the API. SExpr is an internal module that's not used by the API but is used by the parser and some commands. This PR replaces SExpr with terms of kind SEXPR in the parser and strings in commands (which brings them more inline with the API).
|
|
Should fix the nightlies.
|
|
This is required since symbol manager will use context dependent data structures (in its cpp).
This is required since classes in src/parser/ are not allowed to include private headers.
|
|
This PR passes the symbol manager to Command::invoke.
There are no behavior changes in this PR. This is in preparation for reimplementing several features in the parser related to symbols.
|
|
This add the symbol manager class, which is a Term-level utility, separate of the API. This class manages things like expression and assertion names, which is intentionally done outside the solver.
The symbol manager is intended to live at the same level as the Solver. When parsing input, the symbol manager will be used to model any interaction of e.g. named expressions and assertions. It also stores the symbol table of the parser.
This PR adds the basic interface for the symbol manager and passes it to the parser.
Later PRs will migrate the functionality for named expression out of e.g. SmtEngine and into SymbolManager. Commands will take Solver+SymbolManager instead of Solver. This will allow the parser to be fully migrated to the new API.
Marking "complex" since this impacts further design of the parser and the code that lives in src/main.
FYI @4tXJ7f
|
|
This is work towards eliminating the Expr layer. This PR does the following:
Replace Expr/Type with Term/Sort in the API for commands.
Remove the command export functionality which is not supported.
Since many commands now call the Solver functions instead of the SmtEngine ones, their behavior may be a slightly different. For example, (get-unsat-assumptions) now only works in incremental mode. In some cases, CVC4 will not recover from non-fatal errors.
|
|
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 is work towards migrating commands to the new API. Internal code that creates command objects just for dumping is replaced with direct calls to functions that print the those commands.
|
|
|
|
On Debian (for instance), libraries aren't installed into `/usr/lib/`, but into something like `/usr/lib/x86_64-linux-gnu/`. In particular, this means that setting the `LIBRARY_INSTALL_DIR` to `lib` in the top-level `CMakeLists.txt` file is wrong.
Luckily, there is a simple solution: CMake provides [`CMAKE_INSTALL_LIBDIR`](https://cmake.org/cmake/help/v3.0/module/GNUInstallDirs.html) for this very purpose, which has sensible defaults and can be set by the user. In particular, since `CMAKE_INSTALL_LIBDIR` is a standardized variable, tools like the ones used for building Debian packages can set it to what they want it to be, whereas using a custom variable like `LIBRARY_INSTALL_DIR` wouldn't work in this setting.
Signed-off-by: Fabian Wolff <fabi.wolff@arcor.de>
|
|
dependencies (#4809)
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
|
|
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
|
|
(#4750)
As noted in #4590, CVC4 may leak memory if an exception is thrown that interrupts the command execution loop in runCvc4().
While not a major issue (the binary is terminated anyway in this case, this is also why we label it as feature), we should fix it nevertheless.
This commit makes sure that the current command is properly managed by using `std::unique_ptr` to handle its deletion.
|
|
The new mechanism for --tlimit only works for POSIX compatible systems (that implement setitimer). This PR implements an alternative (though roughly equivalent) approach for windows, based on SetWaitableTimer().
To make this work (without code duplication) we need to call the timeout_handler function from time_limit.cpp as the windows solution employs an asynchronous callback instead of signals. I used the opportunity to rename util.cpp to signal_handlers.cpp (as it really does not do anything else) and reformat the file.
As I do not have a windows system at hand, I have not been able to actually test this apart from making sure that it compiles with the mingw setup.
|
|
As a first step within this project, this PR provides a new implementation that backs --tlimit. It uses setitimer (as timer_settime is not available on MacOS) to make the OS send a signal after the given wall clock time has passed.
In more detail, this PR:
removes the current handling of --tlimit (TlimitListener and its integration in the NodeManager)
adds a new TimeLimitListener that lives in src/main
uses TimeLimitListener directly in runCvc4()
adds a signal handler for SIGALRM (that also uses the existing timeout_handler)
|
|
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 #4130.
This further makes an attempt at more consistent error printing.
|
|
|
|
A recent commit (45e489e) made it so that dump-models did not automatically enable produce-models in the global options object, but instead the SmtEngine enabled produce-models internally. The code for dump-models and dump-proofs was (perhaps out of paranoia) checking produce-models and produce-proofs. This removes this check, which is the correct thing to do since SmtEngine internally ensures produce-models is set.
|
|
Towards disentangling Options / NodeManager / SmtEngine.
This PR removes options --use-theory=NAME and --replay/--replay-log. Both of these options are highly complex, unused, and lead to complications when implementing the way options and our build system work.
The first is motivated by making TheoryEngine use an "alternate" theory, which appears to e.g. make it so that TheoryIdl could entirely replace TheoryArith. I believe this is too heavy handed of a solution: there should a consistent TheoryArith class, and options should be used to enable/disable alternate modules within it.
The second attempts to replay low level decisions from the SAT solver. It is documented as not working (in 1.0). I do not believe this is worth salvaging.
It also removes the solver in src/theory/idl, which cannot be enabled after this commit.
|
|
Supporting SMT-LIB's (reset) command on the API level is dangerous and not required -- it's sufficient to just destroy the solver object and create a new one if necessary. It's dangerous because invalidated objects can be passed in after a reset, and we would need to find a clean way to guard against this. We want to guard against this in the future, but for now it is cleaner to make it explicit (by not having this functionality in the API but forcing the user to destroy and recreate the solver object) that these objects can't be reused.
|
|
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>
|
|
Commit 1c09572e0e2031519a103caa2a4af0d9bd34a9c5 removed the portfolio
build but there were some leftovers. This commit removes them.
|
|
This commit adds support for code generation of options with modes (enums). From now on option enums can be specified in the corresponding *.toml files without the need of extra code. All option enums are now in the options namespace.
|
|
|
