projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c8f149f) | patch
Fix cached free variable identifiers in sygus term database (#4394)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 20 May 2020 00:34:18 +0000 (19:34 -0500)
committerGitHub <noreply@github.com>
Wed, 20 May 2020 00:34:18 +0000 (19:34 -0500)
commit9712a20e6585728c7d0453e64e1e3b06a7d37b7f
treeb6941ff3df53fe92b0a1b9ea867c43ce2bb7d014tree
parentc8f149fa83fa16f821f37687fedfa778808809bdcommit | diff
Fix cached free variable identifiers in sygus term database (#4394)

Fixes an issue with over-pruning in SyGuS where using multiple sygus types that map to the same builtin type. Our mapping sygusToBuiltin did not ensure that free variables were unique.

Fixes #4383.
src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp diff | blob | history
src/theory/quantifiers/sygus/term_database_sygus.cpp diff | blob | history
src/theory/quantifiers/sygus/term_database_sygus.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/sygus/issue4383-cache-fv-id.sy [new file with mode: 0644] blob