Slava Pestov 156fa2cc04 RequirementMachine: Speed up term simplification with a prefix trie ...

Previously RewriteSystem::simplify() would attempt to apply every
rewrite rule at every position in the original term, which was
obviously a source of overhead.

The trie itself is somewhat unoptimized; for example, with a bit of
effort it could merge a node with its only child, if nodes stored
a range of elements to compare rather than a single element.

2021-08-05 21:42:50 -04:00

7.6 KiB

Raw Blame History

View Raw