projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1dc23a8) | patch
Ensure uses of ground terms in triggers are preprocessed and registered (#5808)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 25 Jan 2021 17:11:02 +0000 (11:11 -0600)
committerGitHub <noreply@github.com>
Mon, 25 Jan 2021 17:11:02 +0000 (11:11 -0600)
commit7f851ea2e2b40f7e5d6e0c0fbe4e9c6ea0450209
tree2f0f280eebd98631aa839710dbf5713ccac10a89tree
parent1dc23a88520ac3053f15bc16df2e302bbed49765commit | diff
Ensure uses of ground terms in triggers are preprocessed and registered (#5808)

This ensures ground terms in triggers are preprocessed and registered in the master equality engine. This avoids cases where our E-matching algorithm is incomplete where it should not be.

Positive impact (+222-69) on SMT-LIB, 30 second timeout
src/theory/quantifiers/ematching/trigger.cpp diff | blob | history
src/theory/quantifiers/ematching/trigger.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/quantifiers/min-ppgt-em-incomplete.smt2 [new file with mode: 0644] blob
test/regress/regress1/quantifiers/min-ppgt-em-incomplete2.smt2 [new file with mode: 0644] blob