| Age | Commit message (Collapse) | Author |
|---|
|
Work towards supporting multiple solvers running in parallel.
There are now only 5 remaining internal calls to smt::currentSmtEngine.
More will be eliminated on future PRs.
|
|
Work towards a new expression miner for caching satisfiability queries.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
The only code including the old API now are in parser/ and main/ which will require further untangling.
|
|
This PR removes more uses of Expr, mostly related to UnsatCore.
It makes UnsatCore a cvc4_private object storing Node instead of Expr.
|
|
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 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.
|
|
This commit makes the ExprManager constructor private and updates the
initialization of subsolvers, unit tests, and system tests accordingly.
This is a step towards making options part of SmtEngine instead of
NodeManager.
|
|
|
|
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 standardizes the interface for using SMT engines as subsolvers in various approaches. More refactoring is possible, but this is an initial cut at cleaning things up.
This will make it easy to accommodate new feature request for SyGuS (timeouts for calls to verification steps).
Notice this also required adding a missing function (mkGroundTerm/isWellFounded for functions) which was caught after standardizing due to an optimization (don't create SmtEngines to check satisfiability of constant Booleans).
|
|
Fixes 2887.
|
|
|
|
|
|
|
