projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8fe459b) | patch
Support sequences of fixed finite cardinality (#7371)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 19 Oct 2021 23:01:11 +0000 (18:01 -0500)
committerGitHub <noreply@github.com>
Tue, 19 Oct 2021 23:01:11 +0000 (18:01 -0500)
commitbda77d20d51b0ebdd8dec4bd50c6ce5faef7f218
tree8a814346774eea7f3b4a8af27ef0a8eb5177126btree
parent8fe459b1fb3843ebdbda86f24a414c46b986aa90commit | diff
Support sequences of fixed finite cardinality (#7371)

The only open case is dynamic cardinality types (e.g. uninterpreted sorts when FMF is enabled).
src/theory/incomplete_id.cpp diff | blob | history
src/theory/incomplete_id.h diff | blob | history
src/theory/strings/base_solver.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/strings/seq-cardinality.smt2 [new file with mode: 0644] blob