summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-01-24Add --lte-restrict-inst-closure option. Push dt.size fairness constraints in...ajreynol
2015-01-23Refactor sygus arg nf. Minor improvements.ajreynol
2015-01-23CEGQI fairness based on term height. Fix sygus-nf fairness bug for wrongly a...ajreynol
2015-01-23Rework inst-closure.ajreynol
2015-01-22Narrow sygus search space based on NNF and rewriting constant arguments.ajreynol
2015-01-22Add option --lte-partial-inst. Remove inst-closure.ajreynol
2015-01-22Do not drop patterns during boolean term rewriting. Narrow sygus search space...ajreynol
2015-01-21Avoid redundant constant arguments for SygusNormalForm. Refactor.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-19Adding tests for get-value output for arithmetic.Tim King
2015-01-19Adding an additional search path to configure.ac for cxxtestgen to reflect th...Tim King
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 #line numbering.Morgan Deters
2015-01-13Fix a memory issue in ResourceManager on 32-bit (resolves bug #606).Morgan Deters
2015-01-13Remove private #include.Morgan Deters
2015-01-13Fix typo.Morgan Deters
2015-01-12Remove old .orig files that were added to the repository.Morgan Deters
2015-01-11adjusted to both v2.0 and v2.5 string literalsTianyi Liang
2015-01-09blocked unprintable characters in string literals;Tianyi Liang
2015-01-08switch ascii encoding to unsigned charTianyi Liang
2015-01-07patch to the last commitTianyi Liang
2015-01-07bug fix, thanks to Pierre's reportTianyi Liang
2015-01-07Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2015-01-07added initial AX rules;Tianyi Liang
2015-01-07added initial AX rules;Tianyi Liang
2014-12-28Disable prenex by default when using fmf bound int, minor improvement to data...ajreynol
2014-12-26Adding an option to the equality engine constructor to treat all constants asDejan Jovanovic
2014-12-22Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2014-12-22bug fix for constant regular expression model buildingTianyi Liang
2014-12-22bug fix for constant regular expression model buildingTianyi Liang
2014-12-22Do not collapse wrongly applied selectors for non-well-founded codatatypes pr...ajreynol
2014-12-22Add misc trigger options.ajreynol
2014-12-16Fix oversight in dumping assertions in preprocessing.Morgan Deters
2014-12-12Add cvc parsing support for cardinality constraints. Bug fix for enumerating...ajreynol
2014-12-11Minor fixes to language bindings. (Resolves #607.)Morgan Deters
2014-12-11Option to enable/disable cyclicity check in datatypes.ajreynol
2014-12-10bug fix, thanks to Guy's example.Tianyi Liang
2014-12-09Better error description (related to bug 605).Morgan Deters
2014-12-09Cleanup.Morgan Deters
2014-12-06Added string constant in java api example.Tianyi Liang
2014-12-06Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2014-12-06Added C++/Java api examples;Tianyi Liang
2014-12-06Added C++/Java api examples;Tianyi Liang
2014-12-06Fix dt.size care graph.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback