Age | Commit message (Collapse) | Author |
|
Also makes CVC4::theory::arith::nl namespace.
This includes some formatting changes.
|
|
This splits the "non-linear solver" from "NonlinearExtension". The non-linear solver is the module that implements the inference schemas whereas NonlinearExtension is the glue code that manages the solver(s) for non-linear.
This also involves moving utilities from the non-linear solver to their own file.
|
|
* Attempting to split transcendental function solver
* Clean
* Format
* More
* Format
* Attempt link
* Format
* Fix
* Another refactor
* More
* More
* Rename
* Format
Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
|
|
Fixes #4112.
|
|
* Fix assertion in resolution bound inferences
* Format
* Minor
Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
|
|
This PR refactors and fixes how bounds are set for transcendental functions. The new code ensures that all transcendental function applications are given bounds. (Our previous failures to do so were hindering our ability to say "sat", due to NlModel::checkModel failures).
There were previously two issues on why transcendental function applications were not being assigned bounds:
"Slave" transcendental functions (e.g. those that we reduce via sin(t) = sin(y) ^ -pi <= y <= pi ^ y + 2*pi*N = t) were not being given bounds explicitly,
Transcendental functions that are congruent to others (e.g. f(x) where f(y) exists and x=y in the current context) were being ignored and hence not bound.
This PR clarifies the master/slave relationship that tracks which transcendental function applications have been purified, and furthermore tracks congruence classes.
The setting of bounds and the check-model is further simplified by setting bounds on the original terms, whereas the current code sets bounds on the model values of terms. In other words, previously if we had term sin(y) and y^M = c, then we'd set bounds for sin(c), whereas the new code sets the bound on sin(y) directly.
Fixes #3783. We answer unknown without an assertion failure on that benchmark now. Further work based on ignoring literals from internally generated lemmas is necessary for solving it sat.
|
|
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>
|
|
|
|
Work towards CVC4/cvc4-projects#113 and #3783.
This PR adds the ability to mark certain literals as being tautological, since they can be assumed to hold in all models. This is important for internally generated literals whose purpose is to guide models generated by the linear solver but should not hinder our ability to answer "sat".
This PR is required for further refactoring of check-model for transcendental functions.
|
|
Fixes #3647.
Previously, when doing incremental linearization for transcedental functions, we would add points to the list of secant points at the time when linearization lemmas were generated. However, our strategy has been updated such that lemmas may be abandoned (say in the case that a higher priority lemma is found). Thus, our list of secant points had spurious points corresponding to lemmas that weren't sent. This led to assertion failures, and likely led to gaps in our linearization, hindering our ability to say sat/unsat.
This PR introduces a "lemma side effect" class to ensure that modifications to the state of the nonlinear solver are in sync with the lemmas we send out.
|
|
Fixes #3300.
This adds an option --model-witness-choice that ensures that choices in models are of the form (choice ((x Int)) (or (= x c) P)), which is helpful if the user wants to know a potential value in the range of the choice.
|
|
rewrite (#3747)
* Fix bounds for negative sine apps
* Format
* Comment
Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
|
|
|
|
transcendentals (#3577)
|
|
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.
|
|
|
|
solver (#3525)
|
|
|
|
* Refactor non-linear extension for model-based refinement
* Format
* Minor
* Address
|
|
|
|
|
|
* Split arith util
* Cleaner
* cpp
* Format
* Minor
|
|
* Towards fix for non-linear models
* Format
* Fix
* More
* Improve
* Format
* More
|
|
|
|
|
|
|
|
|
|
|
|
|
|
assertions (#2458)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(#1742)
|
|
|
|
NonLinearExtension (#1633)
|
|
Also adds parsing support for PI in smt2 with syntax "real.pi".
|