projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 442bc26) | patch
Moving instantiate and skolemize into quantifiers inference manager (#6188)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 23 Mar 2021 01:32:32 +0000 (20:32 -0500)
committerGitHub <noreply@github.com>
Tue, 23 Mar 2021 01:32:32 +0000 (01:32 +0000)
commit61b9dadc88de3bf7d52538f9e914cfb61cbb7bb6
treef40523a4d2b095101063975145b578c94da7e941tree
parent442bc26b6ce093efed14bfd6764dac30bfdf918fcommit | diff
Moving instantiate and skolemize into quantifiers inference manager (#6188)

After this PR, utilities for instantiation are available from the quantifiers inference manager instead of quantifiers engine. This means that the majority of the dependencies on quantifiers engine will (finally) start being cleaned up after this PR.
src/theory/quantifiers/instantiate.cpp diff | blob | history
src/theory/quantifiers/instantiate.h diff | blob | history
src/theory/quantifiers/quantifiers_inference_manager.cpp diff | blob | history
src/theory/quantifiers/quantifiers_inference_manager.h diff | blob | history
src/theory/quantifiers/theory_quantifiers.cpp diff | blob | history
src/theory/quantifiers/theory_quantifiers.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history