summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sygus/Makefile.am
AgeCommit message (Expand)Author
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-01-21Refactor and fix solveBvLit for CBQI BV. (#1526)Aina Niemetz
2017-12-07Fixes related to SyGuS + real arithmetic (#1432)Andrew Reynolds
2017-12-01Refactor and generalize PBE strategies (#1410)Andrew Reynolds
2017-11-21Cegqi bv remove extract terms preprocess pass (#1376)Andrew Reynolds
2017-11-13Argument Relevance for Synthesis Conjectures (#1311)Andrew Reynolds
2017-11-03Suppport SAT logic (#1310)Andrew Reynolds
2017-10-23Document sygus programming-by-examples utility (#1260)Andrew Reynolds
2017-10-12Sygus logics (#1226)Andrew Reynolds
2017-09-30SyGuS streaming solution mode (#1131)Andrew Reynolds
2017-09-21Sygus inv templ refactor (#1110)Andrew Reynolds
2017-07-20Fix a few bugs related to sygus.ajreynol
2017-07-10Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ...ajreynol
2016-11-17Fix Makefiles in testAndres Notzli
2016-10-21Move slow regress0 benchmarks to regress1, increment regress1 through regress3.ajreynol
2016-05-16Enable --sygus-direct-eval by default, limit to terms that do not induce Bool...ajreynol
2016-05-06Minor clean up, fixes related to sygus.ajreynol
2016-05-05Compute term indices lazily in TermDb. Optimization for qcf to recognize irre...ajreynol
2016-03-08Extend synthesis solver to handle single invocation with additional universal...ajreynol
2015-11-25Infrastructure for partially single invocation properties. Bug fix for uncons...ajreynol
2015-11-10Fix infinite loop in datatype enumerator. Minor fixes and improvements to cbq...ajreynol
2015-09-29Fix for fmf+incremental. Restrict cbqi to literals from ce body. Add regress...ajreynol
2015-09-24Counterexample-guided instantiation for datatypes. Make sygus parsing more l...ajreynol
2015-09-18Allow most smt2 commands as sygus commands. Fix bug in fmf-fun regarding quan...ajreynol
2015-08-27Modify slow regressions.ajreynol
2015-08-01Support for default grammar for datatypes in sygus. Support vts for infinity.ajreynol
2015-07-31Sygus support for inductive datatypes.ajreynol
2015-07-20Squashed merge of SygusComp 2015 branch.ajreynol
2015-06-11Avoid naming conflicts in sygus, refactor. Add missing regression. Detect St...ajreynol
2015-06-11Handle duplicate operators in sygus grammars. Parse sygus quoted literals. A...ajreynol
2015-06-11Update experimental scripts. Support top-level non-terminals in sygus gramma...ajreynol
2015-06-10Support for printing solutions involving LetGTerm sygus. Bug fix define-fun w...ajreynol
2015-06-02Flatten sygus grammars during parsing. Remove duplicate operators from grammars.ajreynol
2015-05-11Allow sygus with no syntactic restrictions for LIA. Add regressions.ajreynol
2015-05-11Support for arbitrary constants/variables in Sygus grammars.ajreynol
2015-04-24Fix sygus parser for non-tokenized operators, reenable regression. Fix for --...ajreynol
2015-04-16disable failing sygus testsKshitij Bansal
2015-02-26Robust strategy for single invocation LIA synthesis conjectures. Add regress...ajreynol
2015-01-20Mark datatypes as sygus. Add option to normalize sygus terms in search. Add...ajreynol
2015-01-14sygus input language and benchmarkMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback