projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7430455) | patch
Simplify interface to instantiate (#5926)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 19 Feb 2021 18:16:42 +0000 (12:16 -0600)
committerGitHub <noreply@github.com>
Fri, 19 Feb 2021 18:16:42 +0000 (12:16 -0600)
commitd278cfe019534f8765a9979c3181ae1f8fbc8470
treec40e959f08829f1c483d0c0ad745332364e2848atree
parent7430455bc71b6641f121edb3ec0cf1706bf40235commit | diff
Simplify interface to instantiate (#5926)

Does not support InstMatch interfaces anymore, which are spurious.
src/theory/quantifiers/ematching/ho_trigger.cpp diff | blob | history
src/theory/quantifiers/ematching/inst_match_generator.h diff | blob | history
src/theory/quantifiers/ematching/inst_match_generator_multi.cpp diff | blob | history
src/theory/quantifiers/ematching/inst_match_generator_multi.h diff | blob | history
src/theory/quantifiers/ematching/inst_match_generator_simple.cpp diff | blob | history
src/theory/quantifiers/ematching/trigger.cpp diff | blob | history
src/theory/quantifiers/fmf/model_engine.cpp diff | blob | history
src/theory/quantifiers/inst_match_trie.cpp diff | blob | history
src/theory/quantifiers/inst_match_trie.h diff | blob | history
src/theory/quantifiers/instantiate.cpp diff | blob | history
src/theory/quantifiers/instantiate.h diff | blob | history