projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 160a3f5) | patch
Use original quantified formula for single invocation reconstruction (#5129)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 26 Sep 2020 13:51:57 +0000 (08:51 -0500)
committerGitHub <noreply@github.com>
Sat, 26 Sep 2020 13:51:57 +0000 (08:51 -0500)
commit6ad02b5e0599149e0bd1548855aec8ac890f5a87
tree5607fd85c45102426314241f193bec9bc2308040tree
parent160a3f55bf4dbfdbc1385ce4898c62b1fd3a8c78commit | diff
Use original quantified formula for single invocation reconstruction (#5129)

This fixes an issue with single invocation solution reconstruction where the preprocessed quantified formula contains internal skolems, thus prohibiting reconstruction. The solution is to use the original quantified formula when doing solution reconstruction. This adds a regression demonstrating the issue.
src/theory/quantifiers/sygus/ce_guided_single_inv.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/sygus/ground-ite-free-constant-si.sy [new file with mode: 0644] blob