Age | Commit message (Expand) | Author |
2015-06-12 | Make sygus an output language. Parse declare-fun in sygus. Minor improvemen... | ajreynol |
2015-06-12 | Accelerate sygus solution reconstruction for constants and id functions. Min... | ajreynol |
2015-06-11 | Avoid naming conflicts in sygus, refactor. Add missing regression. Detect St... | ajreynol |
2015-06-11 | Handle duplicate operators in sygus grammars. Parse sygus quoted literals. A... | ajreynol |
2015-06-11 | Update experimental scripts. Support top-level non-terminals in sygus gramma... | ajreynol |
2015-06-10 | Support for printing solutions involving LetGTerm sygus. Bug fix define-fun w... | ajreynol |
2015-06-10 | Parse support for sygus LetGTerm. | ajreynol |
2015-06-03 | Refactoring of sygus parsing, properly parse Constant/Variable constructors. | ajreynol |
2015-06-02 | Flatten sygus grammars during parsing. Remove duplicate operators from grammars. | ajreynol |
2015-05-11 | Allow sygus with no syntactic restrictions for LIA. Add regressions. | ajreynol |
2015-05-11 | Support for arbitrary constants/variables in Sygus grammars. | ajreynol |
2015-04-23 | Added option for --check-unsat-cores and various core bug fixes (merge of Mor... | Liana Hadarean |
2015-04-22 | Merge pull request #73 from kbansal/parser-dont-tokenize | Kshitij Bansal |
2015-04-16 | Handle (degenerate) case of synthesis conjectures for constants. Disable del... | ajreynol |
2015-04-15 | string parser builtinop changes | Kshitij Bansal |
2015-04-15 | fp builtinop parser changes | Kshitij Bansal |
2015-04-15 | THEORY_INTS parser changes | Kshitij Bansal |
2015-04-15 | THEORY_REAL_INTS parser changes | Kshitij Bansal |
2015-04-15 | array theory builtinop | Kshitij Bansal |
2015-04-15 | cleanup | Kshitij Bansal |
2015-04-15 | dont tokenize bv operators (normal ones) | Kshitij Bansal |
2015-03-05 | Minor fixes. Extend cegqi-si to real arithmetic. | ajreynol |
2015-01-21 | Initial work on sygusNormalForm. | ajreynol |
2015-01-20 | Mark datatypes as sygus. Add option to normalize sygus terms in search. Add... | ajreynol |
2015-01-20 | Handle miniscoping of conjunctions in synthesis properties. Refactor constru... | ajreynol |
2015-01-16 | Linearize multiplication by constants in sygus grammars. Handle unary minus i... | ajreynol |
2015-01-14 | sygus input language and benchmark | Morgan Deters |
2014-12-03 | Floating point infrastructure. | Martin Brain |
2014-10-23 | Parsing and infrastructure support for SMT-LIBv2.5 input and output languages. | Morgan Deters |
2014-08-26 | Improved SMT-LIBv2 language support for unsat cores. | Morgan Deters |
2014-07-01 | Update copyrights. | Morgan Deters |
2014-06-29 | sets: "insert" operator | Kshitij Bansal |
2014-06-25 | rename subseteq to subset in smtlib, all kinds and smt operator names are now... | Kshitij Bansal |
2014-06-22 | Renaming of SMT2 operator names, kinds for set theory | Kshitij Bansal |
2014-04-29 | Fix for --force-logic to extend its reach to the parser. | Morgan Deters |
2014-04-10 | Expand definitions in theory datatypes, now has the expected semantics for in... | Andrew Reynolds |
2014-03-19 | Minor usability fixes related to SMT-LIB compliance. | Morgan Deters |
2014-03-05 | Don't tokenize SET_THEORY operators in smt2 parser | Kshitij Bansal |
2013-12-05 | Update copyrights, add missing file-level documentation; fix perms. | Morgan Deters |
2013-09-18 | Support for bv2nat/int2bv in parser and BV rewriter. | Morgan Deters |
2013-09-11 | Theory of strings. | Tianyi Liang |
2013-06-24 | Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk al... | Morgan Deters |
2013-06-07 | Allow disabling include-file feature | Morgan Deters |
2013-06-04 | File inclusion in Smt2 parser. | Morgan Deters |
2013-05-29 | Fix bug where strict mode didn't allow DIV or MOD, and Ints permitted real di... | Morgan Deters |
2013-05-28 | Standardize SMT-LIBv2 set of logics to use LogicInfo. | Morgan Deters |
2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters |
2013-04-01 | update copyrights | Morgan Deters |
2013-03-21 | Add the ability to "mute" commands, needed for SMT-LIB compliance. | Morgan Deters |
2012-10-11 | Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it's | Morgan Deters |