projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 329700e) | patch
Move VTS term cache to term registry (#8656)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 25 Apr 2022 20:07:51 +0000 (15:07 -0500)
committerGitHub <noreply@github.com>
Mon, 25 Apr 2022 20:07:51 +0000 (20:07 +0000)
commitc7b4826b817abfb605884181e22ebac75afd5024
tree58ff128acc3dc06ed61f9ae7e196e06f46cef91ftree
parent329700eb5c88e984bd3fccef77fe5f13511233f0commit | diff
Move VTS term cache to term registry (#8656)

This is in preparation for simplifying the interface to Instantiate::addInstantiation, where the VTS cache can be consulted to ask if VTS is necessary.
src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp diff | blob | history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp diff | blob | history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.h diff | blob | history
src/theory/quantifiers/cegqi/vts_term_cache.cpp diff | blob | history
src/theory/quantifiers/cegqi/vts_term_cache.h diff | blob | history
src/theory/quantifiers/term_registry.cpp diff | blob | history
src/theory/quantifiers/term_registry.h diff | blob | history