projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9c0ec4e) | patch
Fix care graph computation for higher-order (#7474)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 27 Oct 2021 18:40:18 +0000 (13:40 -0500)
committerGitHub <noreply@github.com>
Wed, 27 Oct 2021 18:40:18 +0000 (18:40 +0000)
commit7461cd576c0ad4c19e996644157a63920c67649b
tree55dcf2ce80bc8de77962fd7d9d8d1ad783715ca5tree
parent9c0ec4ead7a013c2da36c16d9d17471d921ca00ecommit | diff
Fix care graph computation for higher-order (#7474)

Since we apply a lazy schema for app completion, this may omit terms from the care graph that are relevant for theory combination. This corrects the care graph for UF when higher-order is enabled by considering the HO_APPLY version of all partially and fully applied prefixes of APPLY_UF terms during TheoryUF::computeCareGraph.

Fixes #5741. Fixes #5744. Fixes #5201. Fixes #5078. Fixes #4758.
src/theory/uf/theory_uf.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/ho/issue5741-1-cg-model.smt2 [new file with mode: 0644] blob
test/regress/regress0/ho/issue5741-3-cg-model.smt2 [new file with mode: 0644] blob
test/regress/regress0/ho/issue5744-cg-model.smt2 [new file with mode: 0644] blob
test/regress/regress0/ho/qgu-fuzz-ho-1-dd.smt2 [new file with mode: 0644] blob
test/regress/regress1/ho/issue4758.smt2 [new file with mode: 0644] blob
test/regress/regress1/ho/issue5078-small.smt2 [new file with mode: 0644] blob
test/regress/regress1/ho/issue5201-1.smt2 [new file with mode: 0644] blob