summaryrefslogtreecommitdiff
path: root/src/util
AgeCommit message (Expand)Author
2015-06-13Robust check to avoid store all instantiations. Fix prior commit for sort inf...ajreynol
2015-06-13Fix for sort inference involving mixed Int/Real equalities.ajreynol
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-10Support for printing solutions involving LetGTerm sygus. Bug fix define-fun w...ajreynol
2015-05-29changed resource step options to unsignedlianah
2015-05-28added options for controlling resource step-count for various solving stagesLiana Hadarean
2015-05-13Refactor interface for incompleteness in quantifiers engine, cbqi. Minor fix ...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-27Fixed problem with private/public header clashClark Barrett
2015-04-23Merge branch 'master' into googleClark Barrett
2015-04-23Added option for --check-unsat-cores and various core bug fixes (merge of Mor...Liana Hadarean
2015-04-21Changes needed to compile at Google, plus some bug fixes from Google.Clark Barrett
2015-04-09Fix unsat-core issues related to rewrite rules, quantifiers preprocessing, an...ajreynol
2015-03-28printer change for string smtlib2Tianyi Liang
2015-02-27Revert "dummy commit to force nightly builds"Kshitij Bansal
2015-02-18dummy commit to force nightly buildsKshitij Bansal
2015-02-14Fix unit tests.ajreynol
2015-02-13Minor cleanup, remove unused files.ajreynol
2015-02-13Handle recursive singleton case for codatatypes, add regression. Simplify im...ajreynol
2015-01-26Output solutions for synthesis conjectures with --dump-synth. Minor 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-14sygus input language and benchmarkMorgan Deters
2015-01-13Fix a memory issue in ResourceManager on 32-bit (resolves bug #606).Morgan Deters
2015-01-11adjusted to both v2.0 and v2.5 string literalsTianyi Liang
2015-01-08switch ascii encoding to unsigned charTianyi Liang
2014-12-22Do not collapse wrongly applied selectors for non-well-founded codatatypes pr...ajreynol
2014-12-11Minor fixes to language bindings. (Resolves #607.)Morgan Deters
2014-12-06Added C++/Java api examples;Tianyi Liang
2014-12-03Fix UnsatCore in language bindings.Morgan Deters
2014-12-03Floating point infrastructure.Martin Brain
2014-11-22added number of resource units used as a statlianah
2014-11-19Distribute UnsafeInterruptException interface file for SWIG.Morgan Deters
2014-11-18All Minisat solve calls now return lbool (fixes bug 599)lianah
2014-11-17Resource-limiting work.Liana Hadarean
2014-11-10Do not eliminate variables only occurring in patterns. Minor improvements to...ajreynol
2014-11-07Properly distinguish which EQC to assign values in datatypes, use assertRepre...ajreynol
2014-10-23Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.Morgan Deters
2014-10-21Fixed bug 589Tianyi Liang
2014-10-02Merge branch '1.4.x'.Morgan Deters
2014-10-02Fix for an array-of-record model generation assert-fail (assert was too strong).Morgan Deters
2014-09-26Merge branch '1.4.x'Morgan Deters
2014-09-26Clarify some licensing-related things.Morgan Deters
2014-09-23Do not throw error when codatatype is not well-founded. Add option for disab...ajreynol
2014-08-26Improved SMT-LIBv2 language support for unsat cores.Morgan Deters
2014-08-24remove some debugging codeKshitij Bansal
2014-08-24improvements to sets sharingKshitij Bansal
2014-08-23Unsat core printing.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback