projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: be67191) | patch
Fix combinations of cegqi and non-standard triggers (#4271)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 15 Apr 2020 02:28:57 +0000 (21:28 -0500)
committerGitHub <noreply@github.com>
Wed, 15 Apr 2020 02:28:57 +0000 (21:28 -0500)
commit4fb65ae4d0018dc01fe79df8bbf7f3ec0ff583b9
tree8237d54731d6c0190cd2c56b2b594a6f126c3485tree
parentbe6719144c88921fa39823976376961fe03f17a7commit | diff
Fix combinations of cegqi and non-standard triggers (#4271)

Counterexample-guided instantiation may produce quantified formulas with INST_CONSTANT nodes, which are also used as patterns for non-standard triggers for E-matching. This fixes a few combinations that were problematic.

Fixes #4250, fixes #4254, fixes #4269 and fixes #4281.
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/trigger.cpp diff | blob | history
src/theory/quantifiers/inst_match.cpp diff | blob | history
src/theory/quantifiers/inst_match.h diff | blob | history