summaryrefslogtreecommitdiff
path: root/src/parser
AgeCommit message (Expand)Author
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
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-13Remove private #include.Morgan Deters
2015-01-13Fix typo.Morgan Deters
2015-01-09blocked unprintable characters in string literals;Tianyi Liang
2014-12-12Add cvc parsing support for cardinality constraints. Bug fix for enumerating...ajreynol
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-17Resource-limiting work.Liana Hadarean
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
2014-10-16Add dt.size to datatypes theory. Add option for fairness strategy used by CE...ajreynol
2014-10-10CleanupMorgan Deters
2014-10-10Add owner map to better manage QuantifiersModules. Initial infrastructure fo...ajreynol
2014-10-08Add unsat cores support to CVC native language.Morgan Deters
2014-10-07Refactor quantifiers attributes.ajreynol
2014-10-07define-const is an extended command, not permitted in strict mode.Morgan Deters
2014-10-06Clear out decls/defs with RESET command.Morgan Deters
2014-10-06Merge branch '1.4.x'Morgan Deters
2014-10-06Fix native language parsing of chained-store expressions (resolves bug 585). ...Morgan Deters
2014-10-06Support for RESET command in CVC native language (and infrastructure for supp...Morgan Deters
2014-10-03Merge branch '1.4.x'Morgan Deters
2014-10-03Improve error in CVC parser in presence of unrecognized command name.Morgan Deters
2014-10-03More array constants and parsing: better error messages, extend to CVC presen...Morgan Deters
2014-10-03SMT-LIB parser support for array constants (Z3 syntax).Morgan Deters
2014-09-23Support :no-pattern.ajreynol
2014-09-17Fix fix. There are no unsat cores in 1.4Kshitij Bansal
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback