summaryrefslogtreecommitdiff
path: root/src/theory/strings
AgeCommit message (Collapse)Author
2017-09-11Adding reasonable breaks in switch statement in ↵Tim King
TheoryStrings::normalizeRegexp. Minor code reorganization and applying clang-tidy to the function. (#1079)
2017-09-11Addressing a coverity scan complaint in theory_strings.cpp. I believe the ↵Tim King
root cause is that d_normal_forms_exp[r[0]] could have referred to different vectors (as operator[] is inserting for maps). (#1080)
2017-09-05Remove support for conversions between uint32/uint16 and string. (#1069)Andrew Reynolds
* Remove support for conversions between uint32/uint16 and string. * Temporarily disable regression.
2017-08-24Merge pull request #191 from timothy-king/cleanup-regexpAndrew Reynolds
Cleaning up the CVC4::String class.
2017-08-21Cleanup: use Assert rather than C assert. (#1052)Aina Niemetz
2017-07-29Add support for charat in native language, minor cleanup.ajreynol
2017-07-28Fix cache issues for cyclic string equations.ajreynol
2017-07-13Cleaning up the CVC4::String class.Tim King
2017-07-07Update copyright headers.Mathias Preiner
2017-05-10Do not split on cardinality for string equivalence classes with non-constant ↵ajreynol
lengths if disequalities already imply sufficient lower bound. Fixes bug 799.
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
argument.
2017-03-27Minor cleanups to ExtTheory.Tim King
2017-03-27Merge pull request #137 from 4tXJ7f/throw_qualsClark Barrett
Remove throw qualifiers in type enumerators
2017-03-27Making the ExtTheory object a private member of Theory.Tim King
2017-03-27Remove throw qualifiers in type enumeratorsAndres Notzli
This addresses Coverity issues: - 1172154 - 1172156 - 1172157 - 1172158 - 1172159 - 1379612 - 1379612 - 1421430 - 1172166 - 1172144 - 1362709 - 1362696 - 1172145 - 1172147 - 1172148 - 1379610 - 1362772 - 1362676 - 1362704 - 1362749 - 1362876 - 1362843 - 1362837 - 1362881 - 1172223 - 1172155
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
per equivalence class pair.
2017-03-03Fix for collectModelInfo related to finite types + preregistration. ↵ajreynol
Generalize previous fix for sets, minor changes to Datatypes.
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove ↵ajreynol
Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
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 ↵ajreynol
minor changes.
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 + ↵ajreynol
unbounded heaps in sep logic. Fix another simple memory leak in sygus.
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 ↵ajreynol
TheoryStrings to use this.
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 ↵ajreynol
processing. Better handling of disequalities, constant splitting and neg contain approximation. Introduce proxy vars for replace. Refactoring.
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
options (disabled by default).
2016-07-21Fixes for strings, explanations for constant split propagations, substr ↵ajreynol
under concat rewrite. Avoid duplicate re.range length lemmas.
2016-07-20Infer conflicts in strings based on abstracting equality as contains. Minor ↵ajreynol
cleanup.
2016-07-19Add infrastructure for tracking instantiation lemmas (for proofs, and ↵ajreynol
minimization of --dump-instantiations, qe and synthesis solutions). Eliminate quantified arithmetic variables that only have lower/upper bounds. Cleanup strings preprocess, minor fix for str.replace semantics. Reorder cegqi before fmf. Minor cleanup.
2016-07-16Refactor strings extf evaluation info. Ensure strings eager preprocess ↵ajreynol
eliminates all extf symbols during ppRewrite. Add options stringGuessModel and stringUfReduct. Minor optimizations.
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
forms.
2016-07-07Refactoring of strings preprocess module. When enabled, apply eager ↵ajreynol
preprocess during ppRewrite instead of during processAssertions. Simplify reduction for contains. Fix bug in explanations for F_EndpointEq. Minor cleanup for sep.
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback