projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 86ec941) | patch
Refactor strings equality rewriting (#2513)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 25 Sep 2018 02:28:31 +0000 (21:28 -0500)
committerAndres Noetzli <andres.noetzli@gmail.com>
Tue, 25 Sep 2018 02:28:31 +0000 (19:28 -0700)
commit510788587866b16d9ba49bb36a492278ac5fd144
tree99b77a465e235d1a8790d0f2eb48cd49b401b0cctree
parent86ec94126885dc0756abe2e00ecbe71288c13410commit | diff
Refactor strings equality rewriting (#2513)

This moves the extended rewrites for string equality to the main strings rewriter as a function rewriteEqualityExt, and makes this function called on every equality that is generated (from non-equalities) by our rewriter.
src/theory/quantifiers/extended_rewrite.cpp diff | blob | history
src/theory/strings/theory_strings_rewriter.cpp diff | blob | history
src/theory/strings/theory_strings_rewriter.h diff | blob | history