summaryrefslogtreecommitdiff
path: root/src/theory/arith
AgeCommit message (Expand)Author
2020-03-23Change transcendental function app slave list to unordered_set (#4139)Andrew Reynolds
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
2020-03-16Expand the definition of a "simple" farkas proof.Alex Ozdemir
2020-03-10Remove assertion in resolution bound inferences (#3980)Andrew Reynolds
2020-03-10Do not set values for non-linear mult terms in collectModelInfo (#3983)Andrew Reynolds
2020-03-09Fix type issue in arith rewrite equality (#3972)Andrew Reynolds
2020-03-09Fixes for bounds on transcendental functions (#3832)Andrew Reynolds
2020-03-08Rewrite again full for DIV rewrite (#3945)Andrew Reynolds
2020-03-05Add a new arith constraint proof rule: IntTightenAP (#3818)Alex Ozdemir
2020-03-05Revert "Add a new arith constraint proof rule: IntTightenAP (#3818)"Alex Ozdemir
2020-03-05Add a new arith constraint proof rule: IntTightenAP (#3818)Andres Noetzli
2020-03-05Enable -Wshadow and fix warnings. (#3909)Mathias Preiner
2020-02-26Initial work towards -Wshadow (#3817)Andrew Reynolds
2020-02-26Infrastructure for tautological literals in nonlinear solver (#3795)Andrew Reynolds
2020-02-26Use side effect utility for non-linear lemmas (#3780)Andrew Reynolds
2020-02-26Support for witnessing choice in models (#3781)Andrew Reynolds
2020-02-19resource manager: Add statistic for every resource. (#3772)Mathias Preiner
2020-02-18Fix approximate bounds for transcendental functions whose model values rewrit...Andrew Reynolds
2020-02-17 Fix soundness bug in reduction of integer div/mod (#3766)Andrew Reynolds
2020-02-11Fix non-linear equality solving that involves mixed real/integer arithmetic (...Andrew Reynolds
2020-02-06Fix exact sqrt (#3721)Andrew Reynolds
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
2019-12-18Increment Taylor degree for tangent and secant plane inferences for transcend...Andrew Reynolds
2019-12-17Generate code for options with modes. (#3561)Mathias Preiner
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
2019-12-05Make nonlinear solver intercept model assignments from the linear arithmetic ...Andrew Reynolds
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++ AP...makaimann
2019-11-22Minor refactoring of compute model value for nl (#3489)Andrew Reynolds
2019-11-18Fix reduction of `sqrt` (#3478)Andres Noetzli
2019-11-18Use -Wimplicit-fallthrough (#3464)Andres Noetzli
2019-11-12Refactor non-linear extension for model-based refinement (#3452)Andrew Reynolds
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
2019-10-28Fix for non-linear models (#3410)Andrew Reynolds
2019-10-28Fix integer division rewrite (#3415)Andres Noetzli
2019-10-13Eliminate negative constant coefficients in div/mod (#2929)Andrew Reynolds
2019-10-08prefer prefix ++ operator for iteratorsPiotr Trojanek
2019-09-28Introduce template classes for simple type rules (#2835)Andres Noetzli
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