projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 854ab7e) | patch
Add state and inference manager to inst match generator (#5968)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 24 Feb 2021 01:51:21 +0000 (19:51 -0600)
committerGitHub <noreply@github.com>
Wed, 24 Feb 2021 01:51:21 +0000 (19:51 -0600)
commitdc6a56da3c03fc6ba110f5a3292fd3cdcc0f36b1
treed147af87bd55b29d059283dac8955094e94b67a5tree
parent854ab7e1adce90ebd822cc29ffabf5546d13f5cccommit | diff
Add state and inference manager to inst match generator (#5968)

In preparation for refactoring E-matching to not pass QuantifiersEngine pointer to its utilities.
src/theory/quantifiers/ematching/inst_match_generator.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_multi_linear.cpp diff | blob | history
src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h diff | blob | history
src/theory/quantifiers/ematching/inst_match_generator_simple.cpp diff | blob | history
src/theory/quantifiers/ematching/inst_match_generator_simple.h diff | blob | history
src/theory/quantifiers/ematching/trigger.cpp diff | blob | history
src/theory/quantifiers/ematching/var_match_generator.cpp diff | blob | history
src/theory/quantifiers/ematching/var_match_generator.h diff | blob | history