projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 049203b) | patch
Minor cleaning of instantiation utilities (#7334)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 12 Oct 2021 15:29:38 +0000 (10:29 -0500)
committerGitHub <noreply@github.com>
Tue, 12 Oct 2021 15:29:38 +0000 (15:29 +0000)
commit36b9c04591067491854cb1d4caaf391572357375
treeeb4dc4685a8996c029d367b703dda6d5ec0b3f54tree
parent049203b5060dfb452429318bcb408c6db640a7a6commit | diff
Minor cleaning of instantiation utilities (#7334)

Also fixes a bug in the quantifiers macro utility which did not compute the instantiation constant body of a quantified formula properly.

This is work towards a major refactoring of conflict-based instantiation / entailment checks.
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/instantiate.cpp diff | blob | history
src/theory/quantifiers/instantiate.h diff | blob | history
src/theory/quantifiers/quant_module.cpp diff | blob | history
src/theory/quantifiers/quant_module.h diff | blob | history
src/theory/quantifiers/quantifiers_macros.cpp diff | blob | history
src/theory/quantifiers/quantifiers_registry.cpp diff | blob | history
src/theory/quantifiers/quantifiers_registry.h diff | blob | history