projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ea0c166) | patch
Split entailment check from term database (#7342)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 14 Oct 2021 19:15:29 +0000 (14:15 -0500)
committerGitHub <noreply@github.com>
Thu, 14 Oct 2021 19:15:29 +0000 (19:15 +0000)
commit5c481b34eef5860d29ea1f2f62cea696fea01619
treec727ba605c0ce589aad900973923c95298c260d6tree
parentea0c1665d7bb59d328a55f132acd1b08abed74f8commit | diff
Split entailment check from term database (#7342)

Towards addressing some bottlenecks on Facebook benchmarks.
src/CMakeLists.txt diff | blob | history
src/theory/quantifiers/conjecture_generator.cpp diff | blob | history
src/theory/quantifiers/ematching/ho_trigger.cpp diff | blob | history
src/theory/quantifiers/entailment_check.cpp [new file with mode: 0644] blob
src/theory/quantifiers/entailment_check.h [new file with mode: 0644] blob
src/theory/quantifiers/instantiate.cpp diff | blob | history
src/theory/quantifiers/quant_conflict_find.cpp diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.h diff | blob | history
src/theory/quantifiers/term_registry.cpp diff | blob | history
src/theory/quantifiers/term_registry.h diff | blob | history