summaryrefslogtreecommitdiff
path: root/src/theory/strings
AgeCommit message (Expand)Author
2017-07-07Update copyright headers.Mathias Preiner
2017-05-10Do not split on cardinality for string equivalence classes with non-constant ...ajreynol
2017-05-09Change str.replace for empty string.ajreynol
2017-04-05Fix several spelling errorsFabian Wolff
2017-04-04Simplify Theory::collectModelInfo interface to not take deprecated fullModel ...ajreynol
2017-03-27Minor cleanups to ExtTheory.Tim King
2017-03-27Merge pull request #137 from 4tXJ7f/throw_qualsClark Barrett
2017-03-27Making the ExtTheory object a private member of Theory.Tim King
2017-03-27Remove throw qualifiers in type enumeratorsAndres Notzli
2017-03-22Fix more cases of rewritten explanations in strings for bug 784. Minor.ajreynol
2017-03-21Improve computeCareGraph functions to check shared term equality status once ...ajreynol
2017-03-03Fix for collectModelInfo related to finite types + preregistration. Generaliz...ajreynol
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole...ajreynol
2017-01-30Fix regexp cache issue in strings, add regression.ajreynol
2017-01-13Do not rewrite explanations in strings.ajreynol
2016-12-07Add sets regression, fixes bug 754. Minor fix to regexp in strings.ajreynol
2016-12-07Fix nf exp tracking for non-linear string equalities, fixes bug 768.ajreynol
2016-12-01Improvement and bug fix for str.indexof reduction, add regression. Other mino...ajreynol
2016-11-18Add support for set-logic ALL, fix compiler error in GCC 6.1Clark Barrett
2016-11-08Minor fixes related to ExtTheory + incremental, fixes bug760.ajreynol
2016-11-03Add priorities to getNextDecision. Properly handle case for finite types + un...ajreynol
2016-10-13Merging bv parts of ajr/bvExt branch, minor additions to ExtTheory.ajreynol
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback