projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8c46772) | patch
Add sygus datatype substitution utility method (#4390)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 4 Jun 2020 17:38:36 +0000 (12:38 -0500)
committerGitHub <noreply@github.com>
Thu, 4 Jun 2020 17:38:36 +0000 (12:38 -0500)
commitc5bf818456ebe2dee833fecd4a0970f0105919f0
tree367e0d467361386d35c7eda10ad08a2839130430tree
parent8c467723be3746ed711c609fa6dafb19a5a49e8bcommit | diff
Add sygus datatype substitution utility method (#4390)

This makes the method for substiutiton and generalization of sygus datatypes a generic utility method. It updates the abduction method to use it. Interpolation is another target user of this utility.
src/theory/datatypes/theory_datatypes_utils.cpp diff | blob | history
src/theory/datatypes/theory_datatypes_utils.h diff | blob | history
src/theory/quantifiers/sygus/sygus_abduct.cpp diff | blob | history