summaryrefslogtreecommitdiff
path: root/src/theory/strings
AgeCommit message (Expand)Author
2016-04-14Add missing function for regexp to expr manager.ajreynol
2016-04-03Updating the copyright headers and scripts.Tim King
2016-03-07Minor change to F-Length inference in strings. No internal tracking of cardin...ajreynol
2016-03-03Add missing code to track dependencies recursively for string explanations as...ajreynol
2016-03-01Shorter explanations for strings based on tracking which parts of normal form...ajreynol
2016-02-26Refactoring of inferences in strings. Add several options.ajreynol
2016-02-25Minor improvement to partial qe. Add options for representative selection in ...ajreynol
2016-02-24Add entailment checks between length terms to reduce splitting in strings sol...ajreynol
2016-02-02Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. ...Tim King
2016-01-28Adding listeners to Options.Tim King
2016-01-15Type enumerators take optional argument indicating fixed cardinalities of uni...ajreynol
2016-01-13Lemma cache datatypes. Do not send true lemma in quantifiers. Minor fix for d...ajreynol
2016-01-08Removing StatisticsRegistry's static functions current() and registerStat().Tim King
2016-01-05Add SmtGlobals ClassTim King
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2015-11-17Improve relevant domain computation for arithmetic, full saturation strategy....ajreynol
2015-10-24Fixes related to string contains.ajreynol
2015-10-21Minor refactoring in strings related to length.ajreynol
2015-10-20Refactor strings, remove old cycle checks in normalize eqc.ajreynol
2015-10-20Clean up explanations involving string length. Add regression.ajreynol
2015-10-19Improve stratification of strings extended function reductions, add regressio...ajreynol
2015-10-19Improve regexp rewriter, simplify regexp preprocess, add basic trans closure ...ajreynol
2015-10-15Fix congruence check in strings, fixes bug 686.ajreynol
2015-10-15Change semantics of str.substr to allow endpoint out of bounds, and return em...ajreynol
2015-10-15Decompose string contains, minor refactoring.ajreynol
2015-10-11Fix strings preprocessing + incremental, fixes bug 682. Add initial infrastru...ajreynol
2015-10-08Minor improvements to strings. Refactor rewriter. Enable fairness for multipl...ajreynol
2015-10-07Minor improvements, add endpoint eq inference to strings.ajreynol
2015-10-06More improvements to strings rewriter for regexps, contains, indexof, replace...ajreynol
2015-10-02Fixes related to explanations for cycles, sym inferences. Minor fixes and imp...ajreynol
2015-10-02Improvements to rewriter for regexp, contains, indexof. Improvements and fixe...ajreynol
2015-10-01Evaluate extended operators on partially concrete arguments. More aggressive ...ajreynol
2015-10-01More improvements to strings. More aggressive inference of constant eqc, redu...ajreynol
2015-09-30Refactor strings, bug fix inferences vs lemmas.ajreynol
2015-09-28Minor fixajreynol
2015-09-28Minor fixes to strings, add regressions.ajreynol
2015-09-28Fix bug for trivial extf inferences in strings. Improve caching for splits in...ajreynol
2015-09-27Improved handling of extended operators. Do preprocess on memberships eagerl...ajreynol
2015-09-26Lazy preprocessing of extended operators in strings. Add regressions. Fixes ...ajreynol
2015-09-09Fix bug in strings rewriter regarding lengths of substr terms.ajreynol
2015-08-27Do ITE term bookkeeping when solving Sygus inputs. Add missing script from S...ajreynol
2015-08-17fix for bug663Tianyi Liang
2015-07-30Implement virtual term substitution for non-nested quantifiers. Fix soundnes...ajreynol
2015-07-27minor change to the last fixTianyi Liang
2015-07-27Hotfix for substr function.Tianyi Liang
2015-04-27Disambiguate namespaces in options, fix permissionsClark Barrett
2015-04-21Changes needed to compile at Google, plus some bug fixes from Google.Clark Barrett
2015-04-17Patch for Kshitij's fix on requriePhaseTianyi Liang
2015-04-09Fix unsat-core issues related to rewrite rules, quantifiers preprocessing, an...ajreynol
2015-04-09Bug fix negative contains cache.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback