summaryrefslogtreecommitdiff
path: root/src/theory/arith
AgeCommit message (Expand)Author
2020-07-10(proof-new) Update Theory interface for proof-new (#4648)Andrew Reynolds
2020-07-09Associate all lemmas in non-linear arithmetic with an inference identifier (#...Andrew Reynolds
2020-07-07Improve and fix secant and tangent lemmas in the transcendental solver (#4689)Andrew Reynolds
2020-07-01Add solver for integer AND (#4681)Andrew Reynolds
2020-06-29Add internal support for integer and operator (#4668)Andrew Reynolds
2020-06-28Proof Rules and Checker for Arithmetic (#4665)Alex Ozdemir
2020-06-25Update option --nl-ext to enable/disable incremental linearization solver onl...Andrew Reynolds
2020-06-22Add trascendental function kinds to list of unevaluated operators (#4640)Andrew Reynolds
2020-06-19(proof-new) Split operator elimination from arithmetic (#4581)Andrew Reynolds
2020-06-16Update copyright headers.Aina Niemetz
2020-06-10(proof-new) Remove arith-snorm option. (#4591)Andrew Reynolds
2020-06-08Fix Coverity issues (#4587)Andres Noetzli
2020-06-06Use NlLemma utility for all lemmas in non-linear. (#4573)Andrew Reynolds
2020-06-05(proof-new) Rename ProofSkolemCache to SkolemManager (#4556)Andrew Reynolds
2020-06-01Move non-linear files to src/theory/arith/nl (#4548)Andrew Reynolds
2020-05-31Do not cache operator eliminations in arith (#4542)Andres Noetzli
2020-05-22Refactor operator elimination in arithmetic (#4519)Andrew Reynolds
2020-05-19Do not eliminate variables that are equal to unevaluatable terms (#4267)Andrew Reynolds
2020-05-19Renamed operator CHOICE to WITNESS (#4207)mudathirmahgoub
2020-04-10Split the non-linear solver (#4219)Andrew Reynolds
2020-04-08Perform theory widening eagerly (#4044)Andres Noetzli
2020-04-03Update theory rewriter ownership, add stats to strings (#4202)Andres Noetzli
2020-04-01Initialize theory rewriters in theories (#4197)Andres Noetzli
2020-03-27Split transcendental solver to its own file (#4156)Andrew Reynolds
2020-03-26Added unit-cube-like test for branch and bound (#3922)Amalee
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback