summaryrefslogtreecommitdiff
path: root/src/theory/arith
AgeCommit message (Collapse)Author
2020-03-23Change transcendental function app slave list to unordered_set (#4139)Andrew Reynolds
Fixes #4112.
2020-03-16clang-formatAlex Ozdemir
2020-03-16Fix simplicity check in propAlex Ozdemir
2020-03-16Fix antecedent loop. WhoopsAlex Ozdemir
2020-03-16Only save farkas+tightening proofs. Error on holesAlex Ozdemir
I'll remove the error later
2020-03-16Expand the definition of a "simple" farkas proof.Alex Ozdemir
Before, a "simple farkas proof" was one that just applied the farkas lemma. Now it allows for the antecedents to (optionally) be tightened. Note that hasSimpleFarkasProof was (and is) dead code. We will use it to decide whether to print a proof or a hole.
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-10Do not set values for non-linear mult terms in collectModelInfo (#3983)Andrew Reynolds
Fixes #3803. When non-linear arithmetic determines there is a model, then it should not send model values for multiplication terms that the linear solver assigned when abstracting (non-linear) multiplication. This avoids conflicts if the non-linear solver changed a value for a variable occurring in a non-linear monomial. This avoids check-model failures.
2020-03-09Fix type issue in arith rewrite equality (#3972)Andrew Reynolds
Fixes #3952 and fixes #3940 and fixes #3941 and fixes #3968.
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-08Rewrite again full for DIV rewrite (#3945)Andrew Reynolds
Fixes #3944.
2020-03-05Add a new arith constraint proof rule: IntTightenAP (#3818)Alex Ozdemir
This rule is used when a bound on an integer expression is tightened because of integer reasoning. Before this rule was subsumed by IntHoleAP, a catch-all rule for integer reasoning. We are now articulating IntTightenAP separately, because we can produce proofs for it. For IntHoleAP, we will have to omit a hole.
2020-03-05Revert "Add a new arith constraint proof rule: IntTightenAP (#3818)"Alex Ozdemir
This reverts commit c360b3af4371cf871935a8bae96be5f8fecf741b.
2020-03-05Add a new arith constraint proof rule: IntTightenAP (#3818)Andres Noetzli
This rule is used when a bound on an integer expression is tightened because of integer reasoning. Before this rule was subsumed by IntHoleAP, a catch-all rule for integer reasoning. We are now articulating IntTightenAP separately, because we can produce proofs for it. For IntHoleAP, we will have to omit a hole.
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-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.
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-17 Fix soundness bug in reduction of integer div/mod (#3766)Andrew Reynolds
This was introduced 7 years ago in https://github.com/CVC4/CVC4/commit/9098391fe334d829ec4101f190b8f1fa21c30752. This impacted any case of integer div/mod of the form `(mod c t)` or `(div c t)` where c is a constant and `t` is not. Fixes #3765. Also improves `--dump=t-lemmas` trace to result in smt-lib compatible output, which was required for debugging this.
2020-02-11Fix non-linear equality solving that involves mixed real/integer arithmetic ↵Andrew Reynolds
(#3739) * Fix non-linear equality solving that involves mixed real/integer. * Format * Fix * Revert Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
2020-02-06Fix exact sqrt (#3721)Andrew Reynolds
Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
2020-02-04Articulate proof-related debug statements in arith (#3700)Alex Ozdemir
2020-02-03Split on model values when repaired model from non-linear is inconsisent (#3668)Andrew Reynolds
2020-01-31Fix arithmetic rewriter for exponential (#3688)Andres Noetzli
2020-01-22Fix substitution in nl solver (#3638)Andrew Reynolds
* Fix for 3614 * Add regression * Remove regression Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
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-09Make theory rewriters non-static (#3547)Andres Noetzli
This commit changes theory rewriters to be non-static. This refactoring is needed as a stepping stone to making our rewriter configurable: If we have multiple solver objects with different rewrite configurations, we cannot use `static` variables for the rewriter table in the BV rewriter for example. It is also in line with our goal of getting rid of singletons in general. Note that the `Rewriter` class is still a singleton, which will be changed in a future commit.
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-12-02OpTerm Refactor: Allow retrieving OpTerm used to create Term in public C++ ↵makaimann
API (#3355) * Treat uninterpreted functions as a child in Term iteration * Remove unnecessary const_iterator constructor * Add parameter comments to const_iterator constructor * Use operator[] instead of storing a vector of Expr children * Switch pos member variable from int to uint32_t * Add comment about how UFs are treated in iteration * Allow OpTerm to contain a single Kind, update OpTerm construction * Update mkTerm to use only an OpTerm (and not also a Kind) * Remove unnecessary function checkMkOpTerm * Update mkOpTerm comments to not use _OP Kinds * Update examples to use new mkTerm * First pass on fixing unit test * Override kind for Constructor and Selector Terms * More fixes to unit tests * Updates to parser * Remove old assert (for Kind, OpTerm pattern which was removed) * Remove *_OP kinds from public API * Add hasOpTerm and getOpTerm methods to Term * Add test for UF iteration * Add unit test for getOpTerm * Move OpTerm implementation above Term implemenation to match header file Moved in header because Term::getOpTerm() returns an OpTerm and the compiler complains if OpTerm is not defined earlier. Simply moving the declaration is easier/cleaner than forward declaring within the same file that it's declared. * Fix mkTerm in datatypes-new.cpp example * Use helper function for creating term from Kind to avoid nested API calls * Rename: OpTerm->Op in API * Update OpTerm->Op in examples/tests/parser * Add case for APPLY_TESTER * operator term -> operator * Update src/api/cvc4cpp.h Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com> * Comment comment suggestion Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com> * Add not-null checks and implement Op from a single Kind constructor * Undo sed mistake for OpTerm replacement * Add 'd_' prefix to member vars * Fix comment and remove old commented-out code * Formatting * Revert "Formatting" This reverts commit d1d5fc1fb71496daeba668e97cad84c213200ba9. * More fixes for sed mistakes * Minor formatting * Undo changes in CVC parser * Add isIndexed and prefix with d_ * Create helper function for isIndexed to avoid calling API functions in other API functions
2019-11-22Minor refactoring of compute model value for nl (#3489)Andrew Reynolds
* Refactor compute model value for nl * Format
2019-11-18Fix reduction of `sqrt` (#3478)Andres Noetzli
2019-11-18Use -Wimplicit-fallthrough (#3464)Andres Noetzli
This commit enables compiler warnings for implicit fallthroughs in switch statements that are not explicitly marked as such. The commit introduces a new macro `CVC4_FALLTHROUGH` that can be used to indicate that a fallthrough is intentional. The commit fixes existing warnings and a bug in the arithmetic rewriter for `abs` (the bug likely couldn't be triggered easily because we rewrite `abs` to an `ite` while expanding definitions). To have the new macro also available in the parser, the commit changes `src/base/check.h` to be visible to the parser (it includes `cvc4_private_library.h` now instead of `cvc4_private.h`).
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-31Fix Unimplemented() macros missed in #3366. (#3424)Mathias Preiner
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-10-28Fix integer division rewrite (#3415)Andres Noetzli
2019-10-13Eliminate negative constant coefficients in div/mod (#2929)Andrew Reynolds
Fixes #1399.
2019-10-08prefer prefix ++ operator for iteratorsPiotr Trojanek
Detected with cppcheck static analyser, which said: (performance) Prefer prefix ++/-- operators for non-primitive types. Reformat with clang-format as needed. Signed-off-by: Piotr Trojanek <piotr.trojanek@gmail.com>
2019-09-28Introduce template classes for simple type rules (#2835)Andres Noetzli
This commit introduces two template classes `SimpleTypeRule` and `SimpleTypeRuleVar` to help define simple type rules without writing lots of redundant code. The main advantages of this approach are: - Less code - More consistent error reporting - Easier to extend type checking with other functionality (e.g. getting the type of a symbol)
2019-09-04 Fixes related to destructing null (#3231)Andrew Reynolds
2019-08-24fix mismatch between "delete" and "new []" (#2795)Piotr Trojanek
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback