summaryrefslogtreecommitdiff
path: root/src/theory/strings
AgeCommit message (Expand)Author
2016-10-01Incorporate non-bv parts of ajr/bvExt branchajreynol
2016-09-29Address some coverity warnings, add another stat.ajreynol
2016-09-25Disambiguating a type issue. Coverity scan reported a MISMATCHED_ITERATOR here.Tim King
2016-09-18Minor fix for stringsajreynol
2016-08-26Basic support for EPR+CBQI. Minor cleanup.ajreynol
2016-08-16Initial infrastructure for ExtTheory, generalize extended term handling in Th...ajreynol
2016-08-11Minor change to strings, introduce proxy vars only when necessary.ajreynol
2016-08-10Improvements to strings: work on propagations for reverse normal form process...ajreynol
2016-07-30Prioritize inferences when processing normal forms in strings.ajreynol
2016-07-26Minor improvements to strings related to constant splitting, including a few ...ajreynol
2016-07-21Fixes for strings, explanations for constant split propagations, substr under...ajreynol
2016-07-20Infer conflicts in strings based on abstracting equality as contains. Minor c...ajreynol
2016-07-19Add infrastructure for tracking instantiation lemmas (for proofs, and minimiz...ajreynol
2016-07-16Refactor strings extf evaluation info. Ensure strings eager preprocess elimin...ajreynol
2016-07-15Minor simplification to normal form explanations.ajreynol
2016-07-08Minor fix to last commit.ajreynol
2016-07-07Simplifications for strings normal forms, fix case for concat reps in normal ...ajreynol
2016-07-07Refactoring of strings preprocess module. When enabled, apply eager preproces...ajreynol
2016-07-06Minor cleanup in strings, mostly related to negated str.contains.ajreynol
2016-07-06Add comment field for model, resolves hack for printing sep logic models.ajreynol
2016-06-03Remove NodeListMap from strings, fixes memory leaks. Fix for regexp intersect...ajreynol
2016-06-01Initial infrastructure for bounded set quantification (disabled). Refactoring...ajreynol
2016-05-21Minor fix for strings.ajreynol
2016-05-20Minor fix to strings, cleanup in datatypes.ajreynol
2016-05-20Improvements to theory combination + strings: do not return trivial care grap...ajreynol
2016-05-06Minor clean up, fixes related to sygus.ajreynol
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback