Simplify alpha equivalence module (#5839)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 1 Feb 2021 19:58:14 +0000 (13:58 -0600)
committerGitHub <noreply@github.com>
Mon, 1 Feb 2021 19:58:14 +0000 (13:58 -0600)
commiteac7249ef4e35ad8c37f36098c228965f71a319b
tree823c6dc02896b7f83d94224f2a90736b96fd0e97
parenta85fec1cc9fc4f42dcfefd8c27171d8ce5647449
Simplify alpha equivalence module (#5839)

This class uses a discrimination tree which can compute subsumption as well as alpha-equivalence. This class was initially designed to also support subsumption. However, we were only using this class for alpha-equivalence and hence (canonized) Node comparison suffices and the class can be simplified. It also makes minor cosmetic updates to the module.

If we plan to support subsumption checking later, we will write a new module, and use this class https://github.com/CVC4/CVC4/blob/master/src/expr/match_trie.h which is a more mature version of the class deleted by this PR.

Note: I verified that the new and old implementation was equivalent using a temporary AlwaysAssert.
src/theory/quantifiers/alpha_equivalence.cpp
src/theory/quantifiers/alpha_equivalence.h