Age | Commit message (Collapse) | Author |
|
TheoryStrings::normalizeRegexp. Minor code reorganization and applying clang-tidy to the function. (#1079)
|
|
root cause is that d_normal_forms_exp[r[0]] could have referred to different vectors (as operator[] is inserting for maps). (#1080)
|
|
* Remove support for conversions between uint32/uint16 and string.
* Temporarily disable regression.
|
|
Cleaning up the CVC4::String class.
|
|
|
|
|
|
|
|
|
|
|
|
lengths if disequalities already imply sufficient lower bound. Fixes bug 799.
|
|
|
|
|
|
argument.
|
|
|
|
Remove throw qualifiers in type enumerators
|
|
|
|
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
|
|
|
|
per equivalence class pair.
|
|
Generalize previous fix for sets, minor changes to Datatypes.
|
|
Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
|
|
|
|
|
|
|
|
|
|
minor changes.
|
|
|
|
|
|
unbounded heaps in sep logic. Fix another simple memory leak in sygus.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
TheoryStrings to use this.
|
|
|
|
processing. Better handling of disequalities, constant splitting and neg contain approximation. Introduce proxy vars for replace. Refactoring.
|
|
|
|
options (disabled by default).
|
|
under concat rewrite. Avoid duplicate re.range length lemmas.
|
|
cleanup.
|
|
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.
|
|
eliminates all extf symbols during ppRewrite. Add options stringGuessModel and stringUfReduct. Minor optimizations.
|
|
|
|
|
|
forms.
|
|
preprocess during ppRewrite instead of during processAssertions. Simplify reduction for contains. Fix bug in explanations for F_EndpointEq. Minor cleanup for sep.
|
|
|
|
|