summaryrefslogtreecommitdiff
path: root/test/regress/regress1/sygus
AgeCommit message (Expand)Author
2021-06-16Make symfpu a required dependency. (#6749)Aina Niemetz
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-21Fix tests of unsat cores (#6593)Andrew Reynolds
2021-05-21Update to sygus standard output for check-synth responses (#6521)Andrew Reynolds
2021-05-18Loop over terms to reconstruct instead of obligations. (#6504)Abdalrhman Mohamed
2021-04-25More check models (#6439)Andrew Reynolds
2021-04-24Improve getValue for non-evaluated operators (#6436)Andrew Reynolds
2021-04-14Merge equivalent sub-obligations instead of discarding them. (#6353)Abdalrhman Mohamed
2021-04-14Warn about infeasible SyGuS conjectures (#6345)Andrew Reynolds
2021-04-07Fixes for abducts (#6279)Andrew Reynolds
2021-03-23Removing unused build options and deprecated proof compile flag (#6195)Haniel Barbosa
2021-03-23Replace old sygus term reconstruction algorithm with a new one. (#5779)Abdalrhman Mohamed
2021-02-25Move slow regressions to regress1 (#5999)Andrew Reynolds
2020-12-22Remove preregister instantiation heuristic (#5713)Andrew Reynolds
2020-12-10Refactor regressions (#5639)Andrew Reynolds
2020-12-09Remove obsolete regressions (#5633)Andrew Reynolds
2020-12-07Do not expand theory definitions at the beginning of preprocessing (#5544)Andrew Reynolds
2020-11-18Do not expand definitions of extended arithmetic operators (#5433)Andrew Reynolds
2020-10-08reset-assertions: Remove all non-global symbols in the parser (#5229)Andres Noetzli
2020-09-27Fix sygus quantifier elimination preprocess for multiple functions (#5130)Andrew Reynolds
2020-09-26Use original quantified formula for single invocation reconstruction (#5129)Andrew Reynolds
2020-09-23Disable cegqi-bv when using sygus (#5124)Andrew Reynolds
2020-09-14Interpolation: Add implementation for SyGuS interpolation module (final) (#5063)Ying Sheng
2020-09-09Fixes for regular expressions + sygus (#5044)Andrew Reynolds
2020-08-21Connect the relevance manager to TheoryEngine and use it in non-linear arithm...Andrew Reynolds
2020-07-21Support uninterpreted constants in the evaluator (#4777)Andrew Reynolds
2020-07-07Transfer ownership of internal Options from NodeManager to SmtEngine (#4682)Andrew Reynolds
2020-06-17Improve polynomial anyterm grammar (#3566)Haniel Barbosa
2020-04-20Make option names related to CEGQI consistent (#4316)Andrew Reynolds
2020-04-10Ensure exported sygus solutions match grammar (#4270)Andrew Reynolds
2020-03-28Change is-cons to (_ is cons) in Sygus benchmarks. (#4174)Abdalrhman Mohamed
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-20Fix variable shadowing issue in sygus-inference (#4121)Andrew Reynolds
2020-03-19Fix regression output related to sygus+bv-div-zero (#4122)Andrew Reynolds
2020-03-12Do not make models for quantified function variables (#4039)Andrew Reynolds
2020-03-11Guard against null relevancy condition in SyGuS (#4033)Andrew Reynolds
2020-03-11Fix duplicate variable issue in sygus-qe-preproc (#4013)Andrew Reynolds
2020-03-09Rename sygus option name (#3977)Andrew Reynolds
2020-03-09Ensure standard miniscoping is applied before aggressive miniscoping (#3974)Andrew Reynolds
2020-03-08Rewrite again full for DIV rewrite (#3945)Andrew Reynolds
2020-03-06Support default sygus grammar construction for sets (#3842)Andrew Reynolds
2020-02-28Replace conditional rewrite pass in quantifiers with the extended rewriter (#...Andrew Reynolds
2020-02-26Fix regression (#3827)Andrew Reynolds
2020-02-26More fixes for printing sygus commands (#3812)Andrew Reynolds
2020-02-26Use default consts when not using any const during grammar normalization (#3807)Andrew Reynolds
2020-02-12Ensure ext rewrites for associative ops dont throw assertions for kind aritie...Andrew Reynolds
2020-01-30Eliminate spurious postprocessing step for single invocation (#3674)Andrew Reynolds
2020-01-28Do not insist on bound values being constant in arithmetic instantiation (#3643)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback