summaryrefslogtreecommitdiff
path: root/src/parser/smt2/smt2.cpp
AgeCommit message (Expand)Author
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-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-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-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-15string parser builtinop changesKshitij Bansal
2015-04-15fp builtinop parser changesKshitij 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-03-05Minor fixes. Extend cegqi-si to real arithmetic.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-16Linearize multiplication by constants in sygus grammars. Handle unary minus i...ajreynol
2015-01-14sygus input language and benchmarkMorgan Deters
2014-12-03Floating point infrastructure.Martin Brain
2014-10-23Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.Morgan Deters
2014-08-26Improved SMT-LIBv2 language support for unsat cores.Morgan Deters
2014-07-01Update copyrights.Morgan Deters
2014-06-29sets: "insert" operatorKshitij Bansal
2014-06-25rename subseteq to subset in smtlib, all kinds and smt operator names are now...Kshitij Bansal
2014-06-22Renaming of SMT2 operator names, kinds for set theoryKshitij Bansal
2014-04-29Fix for --force-logic to extend its reach to the parser.Morgan Deters
2014-04-10Expand definitions in theory datatypes, now has the expected semantics for in...Andrew Reynolds
2014-03-19Minor usability fixes related to SMT-LIB compliance.Morgan Deters
2014-03-05Don't tokenize SET_THEORY operators in smt2 parserKshitij Bansal
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-09-18Support for bv2nat/int2bv in parser and BV rewriter.Morgan Deters
2013-09-11Theory of strings.Tianyi Liang
2013-06-24Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk al...Morgan Deters
2013-06-07Allow disabling include-file featureMorgan Deters
2013-06-04File inclusion in Smt2 parser.Morgan Deters
2013-05-29Fix bug where strict mode didn't allow DIV or MOD, and Ints permitted real di...Morgan Deters
2013-05-28Standardize SMT-LIBv2 set of logics to use LogicInfo.Morgan Deters
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-03-21Add the ability to "mute" commands, needed for SMT-LIB compliance.Morgan Deters
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback