projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c043de3) | patch
Support some cases of isConst for regular expressions (#8114)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 22 Feb 2022 19:11:45 +0000 (13:11 -0600)
committerGitHub <noreply@github.com>
Tue, 22 Feb 2022 19:11:45 +0000 (19:11 +0000)
commit33fab4e47b9f5cc7dae76a30d7850a82bf8290d7
treebd3931c73d7fd155d846955a1b2a6e07a78ecc07tree
parentc043de3e4668808eb6ee31cbb39f03c64b31031ccommit | diff
Support some cases of isConst for regular expressions (#8114)

Fixes https://github.com/cvc5/cvc5/issues/8111.

Having `isConst` return true is required for some rare use cases of regular expressions, e.g. rewrite rule synthesis involving regular expression variables.
src/theory/strings/kinds diff | blob | history
src/theory/strings/theory_strings_type_rules.cpp diff | blob | history
src/theory/strings/theory_strings_type_rules.h diff | blob | history