diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-22 23:50:43 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-22 23:50:43 -0500 |
| commit | cfe0fc1346c41048fa76f7e0fc582afbe95364a2 (patch) | |
| tree | aa191e07dd529b6ddad1a9e103cc75172f96f902 /src/preprocessing/preprocessing_pass_registry.h | |
| parent | 24b44a8e559f1d89f309d611922098e667293920 (diff) | |
Allow E-matching by default when strings are enabled (#5117)
This does not disable E-matching when strings are enabled with --strings-exp, due to potential applications where strings are combined with user-provided quantified formulas.
Notice that by default, we do not want E-matching applied to quantified formulas corresponding to reductions for extended string functions. To correct this, all quantified formulas generated by strings are marked with an "internal quantified formula" attribute, which causes E-matching to ignore them. This feature can in theory be generalized later for other internal sources of quantified formulas.
Diffstat (limited to 'src/preprocessing/preprocessing_pass_registry.h')
0 files changed, 0 insertions, 0 deletions