summaryrefslogtreecommitdiff
path: root/src/theory/arith/nonlinear_extension.cpp
AgeCommit message (Collapse)Author
2020-06-01Move non-linear files to src/theory/arith/nl (#4548)Andrew Reynolds
Also makes CVC4::theory::arith::nl namespace. This includes some formatting changes.
2020-04-10Split the non-linear solver (#4219)Andrew Reynolds
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.
2020-03-27Split transcendental solver to its own file (#4156)Andrew Reynolds
* 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>
2020-03-23Change transcendental function app slave list to unordered_set (#4139)Andrew Reynolds
Fixes #4112.
2020-03-10Remove assertion in resolution bound inferences (#3980)Andrew Reynolds
* Fix assertion in resolution bound inferences * Format * Minor Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
2020-03-09Fixes for bounds on transcendental functions (#3832)Andrew Reynolds
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.
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-26Initial work towards -Wshadow (#3817)Andrew Reynolds
2020-02-26Infrastructure for tautological literals in nonlinear solver (#3795)Andrew Reynolds
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.
2020-02-26Use side effect utility for non-linear lemmas (#3780)Andrew Reynolds
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.
2020-02-26Support for witnessing choice in models (#3781)Andrew Reynolds
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.
2020-02-18Fix approximate bounds for transcendental functions whose model values ↵Andrew Reynolds
rewrite (#3747) * Fix bounds for negative sine apps * Format * Comment Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
2020-02-03Split on model values when repaired model from non-linear is inconsisent (#3668)Andrew Reynolds
2019-12-18Increment Taylor degree for tangent and secant plane inferences for ↵Andrew Reynolds
transcendentals (#3577)
2019-12-17Generate code for options with modes. (#3561)Mathias Preiner
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.
2019-12-11Do not substitute beneath arithmetic terms in the non-linear solver (#3324)Andrew Reynolds
2019-12-05Make nonlinear solver intercept model assignments from the linear arithmetic ↵Andrew Reynolds
solver (#3525)
2019-12-03Improve flexibility of lemma output in non-linear solver (#3518)Andrew Reynolds
2019-11-12Refactor non-linear extension for model-based refinement (#3452)Andrew Reynolds
* Refactor non-linear extension for model-based refinement * Format * Minor * Address
2019-11-05Separate model object in non-linear extension (#3426)Andrew Reynolds
2019-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
2019-10-29Split some generic utilities from the non-linear extension (#3419)Andrew Reynolds
* Split arith util * Cleaner * cpp * Format * Minor
2019-10-28Fix for non-linear models (#3410)Andrew Reynolds
* Towards fix for non-linear models * Format * Fix * More * Improve * Format * More
2019-08-23Fix argument in nonlinear extension. (#3216)Andrew Reynolds
2019-06-11NA Tangent reverse implication (#3050)Ahmed Irfan
2019-03-26Update copyright headers.Aina Niemetz
2019-03-14Use zero slope tangent planes for transcendental functions (#2803)Andrew Reynolds
2018-09-27Fix Taylor overapproximation for large exponentials (#2538)Andrew Reynolds
2018-09-24 Improve non-linear check model error handling (#2497)Andrew Reynolds
2018-09-13Simplify storing of transcendental function applications that occur in ↵Andrew Reynolds
assertions (#2458)
2018-08-16Move node algorithms to separate file (#2311)Andres Noetzli
2018-07-17 Purify applications of exp to transcendental arguments (#2097)Andrew Reynolds
2018-07-06Split ext theory to own file and document (#1809)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2018-05-25Fix various nl assertions. (#1980)Andrew Reynolds
2018-05-24Fix (#1975)Andrew Reynolds
2018-05-24Fixes for non-linear check model (#1974)Andrew Reynolds
2018-05-23Remove spurious assertion in nonlinear extension (#1972)Andrew Reynolds
2018-05-23Generalize check-model in NonLinearExtension for quadratic equations (#1892)Andrew Reynolds
2018-05-03Option to interleave tangent plane inferences (#1833)Andrew Reynolds
2018-05-01Improve tangent planes for transcendental functions (#1832)Andrew Reynolds
2018-04-29Make factoring inference more aggressive (#1825)Andrew Reynolds
2018-04-29Refactor nonlinear check (#1814)Andrew Reynolds
2018-04-29Improvements to simple transcendental function check model. (#1823)Andrew Reynolds
2018-04-27Simplify tangent plane direction (#1824)Andrew Reynolds
2018-04-25Remove nl solve subs option. (#1803)Andrew Reynolds
2018-04-03Use choice when expanding definitions for inverse transcendental functions ↵Andrew Reynolds
(#1742)
2018-03-30Do not use factoring inference for transcendental functions (#1707)Andrew Reynolds
2018-03-20Internally remove redundant assertions and infer equalities in ↵Andrew Reynolds
NonLinearExtension (#1633)
2018-02-20Minor fixes and additions for transcendental functions (#1612)Andrew Reynolds
Also adds parsing support for PI in smt2 with syntax "real.pi".
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback