summaryrefslogtreecommitdiff
path: root/src/parser
AgeCommit message (Expand)Author
2015-09-24Counterexample-guided instantiation for datatypes. Make sygus parsing more l...ajreynol
2015-09-18More work mixing UF and sygus.ajreynol
2015-09-18Allow most smt2 commands as sygus commands. Fix bug in fmf-fun regarding quan...ajreynol
2015-08-01Simplification/improvement to solving deltas in LRA cbqi. Bug fix sygus datat...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-25Add option --sygus-inv-templ for synthesizing strengthening/weakening of pre/...ajreynol
2015-07-20Squashed merge of SygusComp 2015 branch.ajreynol
2015-06-12Make sygus an output language. Parse declare-fun in sygus. Minor improvemen...ajreynol
2015-06-12Accelerate sygus solution reconstruction for constants and id functions. Min...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-10Bug fix parsing constant constructor sygus.ajreynol
2015-06-10Support for printing solutions involving LetGTerm sygus. Bug fix define-fun w...ajreynol
2015-06-10Parse support for sygus LetGTerm.ajreynol
2015-06-03Refactoring of sygus parsing, properly parse Constant/Variable constructors.ajreynol
2015-06-02Flatten sygus grammars during parsing. Remove duplicate operators from grammars.ajreynol
2015-06-02Add casc 25 tfn script. Change tff script to output instantiations. Work tow...ajreynol
2015-05-28added options for controlling resource step-count for various solving stagesLiana Hadarean
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-24More parser related bug fixes (define-funs-rec, declare-funs). Bug fix for fm...ajreynol
2015-04-24Fix sygus parser for non-tokenized operators, reenable regression. Fix for --...ajreynol
2015-04-23Added option for --check-unsat-cores and various core bug fixes (merge of Mor...Liana Hadarean
2015-04-22Merge pull request #73 from kbansal/parser-dont-tokenizeKshitij Bansal
2015-04-16Handle (degenerate) case of synthesis conjectures for constants. Disable del...ajreynol
2015-04-16update commentKshitij Bansal
2015-04-15string parser builtinop changesKshitij Bansal
2015-04-15bv parserchanges cleanupKshitij Bansal
2015-04-15fp builtinop parser changesKshitij Bansal
2015-04-15fp reorder tokens to match other occurencesKshitij Bansal
2015-04-15THEORY_INTS parser changesKshitij Bansal
2015-04-15THEORY_REAL_INTS parser changesKshitij Bansal
2015-04-15array theory builtinopKshitij Bansal
2015-04-15cleanupKshitij Bansal
2015-04-15dont tokenize bv operators (normal ones)Kshitij Bansal
2015-04-08Make fun-def quantifiers carry the function app they define, make fun-def uti...ajreynol
2015-03-23Parsing support for define-fun-rec/define-funs-rec.ajreynol
2015-03-05Minor fixes. Extend cegqi-si to real arithmetic.ajreynol
2015-02-13Handle recursive singleton case for codatatypes, add regression. Simplify im...ajreynol
2015-02-06Handle missing cases for single inv solution reconstruction. Minor fixes. Re...ajreynol
2015-01-26Output solutions for synthesis conjectures with --dump-synth. Minor refactor...ajreynol
2015-01-23Rework inst-closure.ajreynol
2015-01-22Add option --lte-partial-inst. Remove inst-closure.ajreynol
2015-01-21Initial work on sygusNormalForm.ajreynol
2015-01-20Mark datatypes as sygus. Add option to normalize sygus terms in search. Add...ajreynol
2015-01-20Handle miniscoping of conjunctions in synthesis properties. Refactor constru...ajreynol
2015-01-17Avoid name conflicts for multiple synth-fun.ajreynol
2015-01-16Linearize multiplication by constants in sygus grammars. Handle unary minus i...ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback