projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2886976) | patch
Refactor InstMatch (#8646)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 26 Apr 2022 21:43:27 +0000 (16:43 -0500)
committerGitHub <noreply@github.com>
Tue, 26 Apr 2022 21:43:27 +0000 (16:43 -0500)
commit412c9d57d0af0cc85c745a0cd32642a0aee8e7e8
treec678543c9b29555343ab48a3f5f7e81a6a746858tree
parent28869764c41725a0c98df4f1b8de5bfd618551c3commit | diff
Refactor InstMatch (#8646)

Also simplifies the (old) version of multi trigger matching, which copied InstMatch objects unnecessarily, and also used EqualityEngine iteration instead of iterating on a trie.

This is in preparation for making InstMatch objects optionally track fast (and generalized) failures based on configurable criteria.
src/theory/quantifiers/ematching/inst_match_generator.cpp diff | blob | history
src/theory/quantifiers/ematching/inst_match_generator_multi.cpp diff | blob | history
src/theory/quantifiers/ematching/relational_match_generator.cpp 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/inst_match.cpp diff | blob | history
src/theory/quantifiers/inst_match.h diff | blob | history