summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sygus
AgeCommit message (Expand)Author
2021-07-07Fix regressions for competition build (#6846)Andrew Reynolds
2021-07-03Add output tags -o, --output. (#6826)Mathias Preiner
2021-06-11Better support for HOL parsing and set up (#6697)Haniel Barbosa
2021-06-02Remove redundant logic ALL_SUPPORTED. (#6664)Aina Niemetz
2021-05-21Update to sygus standard output for check-synth responses (#6521)Andrew Reynolds
2021-04-15Rename occurrences of CVC4 to CVC5. (#6351)Aina Niemetz
2021-04-14Warn about infeasible SyGuS conjectures (#6345)Andrew Reynolds
2021-04-08Initial support for parametric datatypes in sygus (#6304)Andrew Reynolds
2021-02-25Move slow regressions to regress1 (#5999)Andrew Reynolds
2020-12-22Remove preregister instantiation heuristic (#5713)Andrew Reynolds
2020-12-08Fix a bug with synth-fun printer (#5512)Abdalrhman Mohamed
2020-08-12Fixes for degenerate case of sygus decision tree learning (#4800)Andrew Reynolds
2020-07-13 User-facing print debug option for sygus candidates (#4720)Andrew Reynolds
2020-06-15BV: Add missing type check for INT_TO_BITVECTOR. (#4613)Aina Niemetz
2020-05-19Fix cached free variable identifiers in sygus term database (#4394)Andrew Reynolds
2020-04-20Make option names related to CEGQI consistent (#4316)Andrew Reynolds
2020-04-13Fix SyGuS define-fun printing from benchmarks coming from v1 parser (#4256)Andrew Reynolds
2020-03-28Convert the last few Sygus benchmarks to V2. (#4172)Abdalrhman Mohamed
2020-03-21Convert V1 Sygus files to V2. (#4136)Abdalrhman Mohamed
2020-03-06Support default sygus grammar construction for sets (#3842)Andrew Reynolds
2020-02-26More fixes for printing sygus commands (#3812)Andrew Reynolds
2020-02-03Minor fixes to regressions (#3702)Andrew Reynolds
2020-02-03Fix invariant template inference for trivially infeasible conjecture (#3693)Andrew Reynolds
2020-01-22Fix parameteric sorts involving Booleans in sygus default grammars (#3629)Andrew Reynolds
2019-12-05Refactor mode options for Unif+PI (#3531)Andrew Reynolds
2019-11-29Competition build: Skip parsing error regression (#3511)Andres Noetzli
2019-11-25Better front-end type checking for SyGuS (#3496)Andrew Reynolds
2019-11-04Avoid non-well-founded sygus grammars (#3434)Andrew Reynolds
2019-10-15Fix regression (#3393)Andres Noetzli
2019-10-14Disable regression test for competition build (#3388)Andres Noetzli
2019-10-11Check that logic is set when synth-fun command is encountered (#3384)Andrew Reynolds
2019-10-08Limit cases of sygus inference based on type (#3370)Andrew Reynolds
2019-09-30Trivial solve method for single invocation sygus (#3328)Andrew Reynolds
2019-09-13Disallow let in sygus grammars, check for free variables in sygus constructor...Andrew Reynolds
2019-07-23Fix sygus datatype parsing in sygus v1 format (#3113)Andrew Reynolds
2018-11-21Quickly recognize when PBE conjectures are infeasible (#2718)Andrew Reynolds
2018-11-07Adding default SyGuS grammar construction for arrays (#2685)Haniel Barbosa
2018-10-05Update default options for sygus (#2586)Andrew Reynolds
2018-09-26Makes SyGuS parsing more robust in invariant problems (#2509)Haniel Barbosa
2018-09-22cmake: Added regression tests and target make regress.Aina Niemetz
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-08-22Adds regression test for automatic generation of SyGuS BV grammars (#2345)Haniel Barbosa
2018-07-23 sygusComp2018: add regressions (#2191)Andrew Reynolds
2018-05-21Fix file extension (#1919)Caleb Donovick
2018-05-18Cegis unif defaults to cegis when no unif (#1942)Andrew Reynolds
2018-03-21 Move regression tests to single Makefile.am (#1658)Andres Noetzli
2018-02-15Refactor regressions (#1581)Andrew Reynolds
2018-02-05Statically eliminate redundant sygus constructors (#1560)Andrew Reynolds
2018-02-02Fix remaining synthesis solution regressions (#1557)Andrew Reynolds
2018-02-02Option to check solutions produced by SyGuS solver (#1553)Haniel Barbosa
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback