diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-24 09:39:56 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-24 09:39:56 -0500 |
| commit | b00667a21984dc3f6b960a1a2d22845c7096bc35 (patch) | |
| tree | 8a6dc1bbe37bcc1617f672403800999dd1cc203a /src/theory/bags/term_registry.cpp | |
| parent | 0e9fed387aaf5d0cb1844ab20551fbebfcb8893d (diff) | |
Better formalization of regular expression unfolding skolems (#6602)
This replaces our previous formalization of RE unfolding skolems with a more explicit one that is amenable to external proof conversion. It adds a few associated utility methods to SkolemManager required for LFSC proof conversion for RE_UNFOLD_POS.
It also changes the order of equalities in the RE_UNFOLD_POS rule, which simplifies LFSC proof checking.
Diffstat (limited to 'src/theory/bags/term_registry.cpp')
0 files changed, 0 insertions, 0 deletions