diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-19 15:18:24 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-19 15:18:24 -0500 |
commit | e0633c091c37b79f9e3a2517cf95113c788db083 (patch) | |
tree | 8e7155ceb28d5b8cfeb6aa5c53ecd8b33cd12cc2 /src/theory/strings/term_registry.cpp | |
parent | f5e2348c7350ce21716f595eb8703635782c6285 (diff) |
(proof-new) Split operator elimination from arithmetic (#4581)
This class will be undergoing further refactoring for the sake of proofs.
This also makes several classes of skolems context-independent instead of user-context-dependent, since this is the expected policy for skolems. Note these skolems will eventually be incorporated into the SkolemManager utility.
Diffstat (limited to 'src/theory/strings/term_registry.cpp')
0 files changed, 0 insertions, 0 deletions