projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a96ed15) | patch
Add basic regular expression type enumerator (#7416)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 20 Oct 2021 00:24:32 +0000 (19:24 -0500)
committerGitHub <noreply@github.com>
Wed, 20 Oct 2021 00:24:32 +0000 (00:24 +0000)
commitfc9c1005a398c537bdb491d1b161f3e316b68b5e
tree6a3a4abfc06e43a9e9749e68eeb5539cfb85c758tree
parenta96ed1538245b2ce2cd8a8084e0288d07071ca23commit | diff
Add basic regular expression type enumerator (#7416)

The lack of a type enumerator for regular expressions makes certain things impossible e.g. sygus-based sampling for RE queries.

It is trivial to support a basic RE enumerator that takes singleton languages of strings. This commit adds this utility as the type enumerator for RE.
src/CMakeLists.txt diff | blob | history
src/theory/strings/kinds diff | blob | history
src/theory/strings/regexp_enumerator.cpp [new file with mode: 0644] blob
src/theory/strings/regexp_enumerator.h [new file with mode: 0644] blob