projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 524c2d9) | patch
Use term canonizer utility locally in quantifiers (#5823)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 27 Jan 2021 02:45:26 +0000 (20:45 -0600)
committerGitHub <noreply@github.com>
Wed, 27 Jan 2021 02:45:26 +0000 (20:45 -0600)
commit693ed2fd482791e29e5d86420d0aa2ac835b7260
tree010caa4fae9f97a62c2d5c3b2afe5ad842281911tree
parent524c2d9f44a7c4297422dd1356fe3dc377166180commit | diff
Use term canonizer utility locally in quantifiers (#5823)

Term canonization was used in two places, which are unrelated and don't need to share the instance.
Also removes a few unnecessary methods from QuantifiersEngine.
src/theory/quantifiers/alpha_equivalence.cpp diff | blob | history
src/theory/quantifiers/alpha_equivalence.h diff | blob | history
src/theory/quantifiers/conjecture_generator.cpp diff | blob | history
src/theory/quantifiers/conjecture_generator.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history