projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5bfb18e) | patch
Refactor interfaces for E-matching (#8665)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 29 Apr 2022 15:43:55 +0000 (10:43 -0500)
committerGitHub <noreply@github.com>
Fri, 29 Apr 2022 15:43:55 +0000 (15:43 +0000)
commit25be5c6148c0e0d9ab4666062c0666fb085eee8a
treed2e6b9a62db436b87c05ce2e4b17255f7df7021atree
parent5bfb18e0b31584a50ea0386ce3d43855ee2061d4commit | diff
Refactor interfaces for E-matching (#8665)

InstMatch objects are now fully owned by Triggers. They are passed by reference to InstMatchGenerators.

This also simplifies the interfaces by not passing the quantified formulas.

This is in preparation for making InstMatch objects carry entailment test information.
18 files changed:
src/theory/quantifiers/ematching/im_generator.cpp diff | blob | history
src/theory/quantifiers/ematching/im_generator.h diff | blob | history
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/relational_match_generator.cpp diff | blob | history
src/theory/quantifiers/ematching/relational_match_generator.h diff | blob | history
src/theory/quantifiers/ematching/trigger.cpp diff | blob | history
src/theory/quantifiers/ematching/trigger.h 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
src/theory/quantifiers/inst_match.cpp diff | blob | history
src/theory/quantifiers/inst_match.h diff | blob | history