Fixes for sygus-inst (#8448)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 30 Mar 2022 18:55:21 +0000 (13:55 -0500)
committerGitHub <noreply@github.com>
Wed, 30 Mar 2022 18:55:21 +0000 (18:55 +0000)
commitc0a37b03d674ca0555e01b0aa4b345df806aea7a
tree8db8c17fef2cdca828ee5029e09eea6b3a5cf180
parentcd396280ff2b1a81c7c812c0b08893e72fba8b1e
Fixes for sygus-inst (#8448)

Fixes two issues:

Symmetry breaking was disabled after latest refactoring of sygus options. This meant that the terms considered by sygus-inst were often redundant.
The instantiation constant attribute is set on evaluation variables. This avoids model-unsoundness issues with sygus-inst, which are caused by using the evaluation variable (itself) in instantiations.
The latter issue was discovered by trying the second issue from cvc5/cvc5-projects#487 with --sygus-inst, where it incorrectly says "sat" after the fix from #8447.

Fixed #8456. Fixes #8457.
src/theory/datatypes/theory_datatypes.cpp
src/theory/quantifiers/sygus_inst.cpp
test/regress/cli/CMakeLists.txt
test/regress/cli/regress1/quantifiers/issue8456-2-syqi-ic.smt2 [new file with mode: 0644]
test/regress/cli/regress1/quantifiers/issue8456-syqi-ic.smt2 [new file with mode: 0644]