summaryrefslogtreecommitdiff
path: root/src/util
AgeCommit message (Expand)Author
2016-01-08Adding a new Listener utility class. Changing the ResourceManager to use List...Tim King
2016-01-08Removing StatisticsRegistry's static functions current() and registerStat().Tim King
2016-01-05Moving sexpr.{cpp,h,i} from expr/ back into util/.Tim King
2016-01-05Add SmtGlobals ClassTim King
2015-12-30Shuffling around public vs. private headersTim King
2015-12-24Miscellaneous fixesTim King
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2015-11-10Fix infinite loop in datatype enumerator. Minor fixes and improvements to cbq...ajreynol
2015-10-23This patch slightly generalizes how the std::isfinite function in <cmath> is ...Tim King
2015-10-06More improvements to strings rewriter for regexps, contains, indexof, replace...ajreynol
2015-10-02Improvements to rewriter for regexp, contains, indexof. Improvements and fixe...ajreynol
2015-09-09Working towards a fair enumerator for codatatypes.ajreynol
2015-06-27Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by de...ajreynol
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback