summaryrefslogtreecommitdiff
path: root/test/regress/regress1/nl
AgeCommit message (Expand)Author
2021-10-21Refactor regressions script (#7249)Andres Noetzli
2021-10-15Add more regressions for fixed issues (#7382)Andrew Reynolds
2021-10-14Add regressions for fixed issues (#7369)Andrew Reynolds
2021-09-07Refactoring and fixes of set defaults for quantifiers (#7120)Andrew Reynolds
2021-09-02Enable sygus-inst for FP, NIA and NRA. (#7098)Aina Niemetz
2021-08-02Add 'REQUIRES: poly' to regression. (#6966)Aina Niemetz
2021-07-12Fix for learned rewrite pass, add regression (#6850)Andrew Reynolds
2021-05-21Fix tests of unsat cores (#6593)Andrew Reynolds
2021-05-17Improve integration of CAD with nl-Ext (#6542)Gereon Kremer
2021-05-07Move slow regressions and update guidelines. (#6508)Aina Niemetz
2021-04-25More check models (#6439)Andrew Reynolds
2021-03-15Make nonlinear extension account for relevant term set (#6147)Andrew Reynolds
2021-03-06Remove SMT-LIB 2.5 and 2.0 support. (#6068)Mathias Preiner
2021-02-25Move slow regressions to regress1 (#5999)Andrew Reynolds
2021-02-10Fix open proof for factoring lemma (#5885)Andrew Reynolds
2020-12-21Eliminate recursion from the internals of term formula removal (#5701)Andrew Reynolds
2020-12-10Refactor regressions (#5639)Andrew Reynolds
2020-12-07Add bitwise refinement mode for IAND (#5328)makaimann
2020-11-18Do not expand definitions of extended arithmetic operators (#5433)Andrew Reynolds
2020-11-03Reset built model flag at presolve in nonlinear (#5386)Andrew Reynolds
2020-10-27Enable --nl-cad by default (#5345)Gereon Kremer
2020-10-14bv2int: implementing the iand-sum mode (#5265)yoni206
2020-08-21Connect the relevance manager to TheoryEngine and use it in non-linear arithm...Andrew Reynolds
2020-08-19[Regressions] Do not test `--check-proofs` anymore (#4914)Andres Noetzli
2020-07-10Front end support for integer AND (#4717)Andrew Reynolds
2020-06-10(proof-new) Remove arith-snorm option. (#4591)Andrew Reynolds
2020-05-22Refactor operator elimination in arithmetic (#4519)Andrew Reynolds
2020-05-19Renamed operator CHOICE to WITNESS (#4207)mudathirmahgoub
2020-03-11Fix double notify in equality engine (#4036)Andrew Reynolds
2020-03-10Do not set values for non-linear mult terms in collectModelInfo (#3983)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-03Minor fixes to regressions (#3702)Andrew Reynolds
2020-02-03Split on model values when repaired model from non-linear is inconsisent (#3668)Andrew Reynolds
2020-01-30Make eq chain an aggressive rewrite in extended rewriter (#3679)Andrew Reynolds
2019-12-18Increment Taylor degree for tangent and secant plane inferences for transcend...Andrew Reynolds
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
2018-10-18Non-implied mode for model cores (#2653)Andrew Reynolds
2018-09-27Fix Taylor overapproximation for large exponentials (#2538)Andrew Reynolds
2018-09-22cmake: Added regression tests and target make regress.Aina Niemetz
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-08-21Makes the new row propagation system default (#2335)Haniel Barbosa
2018-06-04Only enable transcendentals if logic is N[I]RAT (#2052)Andres Noetzli
2018-05-24Fix nl regression for unsat cores. (#1973)Andrew Reynolds
2018-05-23Generalize check-model in NonLinearExtension for quadratic equations (#1892)Andrew Reynolds
2018-05-01Improve tangent planes for transcendental functions (#1832)Andrew Reynolds
2018-04-30Disable unsat-cores/proofs for slow regression (#1835)Andres Noetzli
2018-04-29Make factoring inference more aggressive (#1825)Andrew Reynolds
2018-04-03Use choice when expanding definitions for inverse transcendental functions (#...Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback