projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e635444) | patch
Supporting seq.nth (#4723)
authoryoni206 <yoni206@users.noreply.github.com>
Tue, 28 Jul 2020 17:44:55 +0000 (10:44 -0700)
committerGitHub <noreply@github.com>
Tue, 28 Jul 2020 17:44:55 +0000 (12:44 -0500)
commit7ad41fe71b9f7d206ee6d1c642bb7926bffea6c7
treefc5d9cb07fbce3a28395eb30aabb6d6633724e02tree
parente63544462eb850a27f7b416f2f0613efb96eef1dcommit | diff
Supporting seq.nth (#4723)

This PR adds support for seq.nth operator by eliminating it during expandDefinitions, based on sub-sequences.
Tests that use this operator are also included.
20 files changed:
src/api/cvc4cpp.cpp diff | blob | history
src/api/cvc4cppkind.h diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/strings/kinds diff | blob | history
src/theory/strings/rewrites.cpp diff | blob | history
src/theory/strings/rewrites.h diff | blob | history
src/theory/strings/sequences_rewriter.cpp diff | blob | history
src/theory/strings/sequences_rewriter.h diff | blob | history
src/theory/strings/skolem_cache.h diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/strings/theory_strings_type_rules.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/seq/intseq.smt2 [new file with mode: 0644] blob
test/regress/regress0/seq/intseq_dt.smt2 [new file with mode: 0644] blob
test/regress/regress0/seq/seq-nth-uf-z.smt2 [new file with mode: 0644] blob
test/regress/regress0/seq/seq-nth-uf.smt2 [new file with mode: 0644] blob
test/regress/regress0/seq/seq-nth-undef.smt2 [new file with mode: 0644] blob
test/regress/regress0/seq/seq-nth.smt2 [new file with mode: 0644] blob