summaryrefslogtreecommitdiff
path: root/test/regress/regress0/quantifiers
AgeCommit message (Expand)Author
2021-06-02Remove redundant logic ALL_SUPPORTED. (#6664)Aina Niemetz
2021-05-27Fix CEGQI for datatypes with Boolean subfields (#6630)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-04-25More check models (#6439)Andrew Reynolds
2021-04-24Improve getValue for non-evaluated operators (#6436)Andrew Reynolds
2021-04-22Fix models for sygus-inference, bv2int, real2int (#6421)Andrew Reynolds
2021-04-19Fully incorporate quantifiers macros into ppAssert / non-clausal simplificati...Andrew Reynolds
2021-04-13Refactor quantifiers macros (#6348)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-09[quantifiers] Fix prenex computation (#5879)Haniel Barbosa
2020-12-17Simplify and fix check models (#5685)Andrew Reynolds
2020-12-16Mark quantifier instantiations as needs justify (#5684)Andrew Reynolds
2020-12-14Properly implement datatype selector triggers (#5624)Andrew Reynolds
2020-12-10Refactor regressions (#5639)Andrew Reynolds
2020-12-08Ensure CEGQI is applied for parametric datatypes when applicable (#5628)Andrew Reynolds
2020-12-07Fix issue with free variables introduced by quantifier rewriter (#5602)Andrew Reynolds
2020-11-18Do not expand definitions of extended arithmetic operators (#5433)Andrew Reynolds
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-06-06Fix destruction order in NodeManager (#4578)Andres Noetzli
2020-06-05Skip parse-error regression for comp builds (#4567)Andres Noetzli
2020-06-03Do not apply unconstrained simplification when quantifiers are present (#4532)Andrew Reynolds
2020-06-02Fix scope issue with pulling ITEs in extended rewriter. (#4547)Andrew Reynolds
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-04-22Convert V2.5 SMT regressions to V2.6. (#4319)Abdalrhman Mohamed
2020-04-20Make option names related to CEGQI consistent (#4316)Andrew Reynolds
2020-04-16SyGuS instantiation quantifiers module (#3910)Mathias Preiner
2020-04-15Do not normalize to representatives for variable equalities in conflict-based...Andrew Reynolds
2020-03-31Rename checkValid/query to checkEntailed. (#4191)Aina Niemetz
2020-03-18Fix issue with multiple infinities in CEGQI for LIRA (#4114)Andrew Reynolds
2020-03-06Remove tester name from APIs (#3929)Andrew Reynolds
2020-02-28Replace conditional rewrite pass in quantifiers with the extended rewriter (#...Andrew Reynolds
2020-02-08Make "unknown" non-critical for unsat cores check (#3728)Andres Noetzli
2019-09-04Remove duplicate regression tests. (#3227)Mathias Preiner
2019-06-04Add check that result matches benchmark status (#3028)Andres Noetzli
2019-04-16Minor simplifications to theory quantifiers (#2953)Andrew Reynolds
2018-11-05Increasing coverage (#2683)yoni206
2018-09-24Fix quantifiers selector over store rewrite (#2510)Andrew Reynolds
2018-09-22cmake: Added regression tests and target make regress.Aina Niemetz
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-09-06Refactor and document quantifiers variable elimination and conditional splitt...Andrew Reynolds
2018-09-04Make quantifiers strategies exit immediately when in conflict (#2099)Andrew Reynolds
2018-08-20Remove support for *.expect files in regressions (#2341)Andres Noetzli
2018-08-07Fix inference of pre and post conditions for non variable arguments. (#2237)Andrew Reynolds
2018-06-01Fix quantified bv variable elimination (#2039)Andrew Reynolds
2018-06-01 Use monomial sum utility to solve for quantifiers macros (#2038)Andrew Reynolds
2018-05-22Set same options for proofs as for unsat cores (#1957)Andres Noetzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback