summaryrefslogtreecommitdiff
path: root/src/parser/smt2
AgeCommit message (Expand)Author
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-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-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
2015-01-16Allow uninterpreted/defined functions in Sygus grammars. Fix bug regarding de...ajreynol
2015-01-16Minor: Ensure indexed terms are in EE. Add support for bv constants in sygus...ajreynol
2015-01-14sygus input language and benchmarkMorgan Deters
2015-01-13Fix typo.Morgan Deters
2015-01-09blocked unprintable characters in string literals;Tianyi Liang
2014-12-03Floating point infrastructure.Martin Brain
2014-11-25Fix bug in --term-db-mode=relevant with variable triggers. Support inst-clos...ajreynol
2014-11-12Fix tokenization of "reset" in SMT-LIB v2.0. It's a reserved word only in 2.5.Morgan Deters
2014-10-28Preprocessing step for finding finite runs of well-defined function definitio...ajreynol
2014-10-28Initial infrastructure for function definition quantifiers, internal parsing ...ajreynol
2014-10-24Minor parser performance fix.Morgan Deters
2014-10-23Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback