projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3ff70d6) | patch
Support indexed operators re.loop and re.^ (#4167)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 30 Mar 2020 21:29:23 +0000 (16:29 -0500)
committerGitHub <noreply@github.com>
Mon, 30 Mar 2020 21:29:23 +0000 (16:29 -0500)
commit6838885b1250e0abbb1b8d56e6b400a5d7f3ca95
tree3c1a7417d471aeea531a36024a460d605cb5d5f1tree
parent3ff70d61c111b70d5bf770669b0aa3f1d47a502ecommit | diff
Support indexed operators re.loop and re.^ (#4167)

Towards support for the strings standard.

This modifies our interface so that we accept the SMT-LIB standard versions of re.loop and re.^. This means re.loop no longer accepts 3 arguments but 1 (with 2 indices).

This means we no longer accept re.loop with only a lower bound and no upper bound on the number of repetitions.

Also fixes #4161.
23 files changed:
src/CMakeLists.txt diff | blob | history
src/api/cvc4cpp.cpp diff | blob | history
src/api/cvc4cppkind.h diff | blob | history
src/bindings/java/CMakeLists.txt diff | blob | history
src/cvc4.i diff | blob | history
src/parser/cvc/Cvc.g diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/theory/strings/kinds diff | blob | history
src/theory/strings/regexp_operation.cpp diff | blob | history
src/theory/strings/sequences_rewriter.cpp diff | blob | history
src/theory/strings/theory_strings_utils.cpp diff | blob | history
src/theory/strings/theory_strings_utils.h diff | blob | history
src/util/CMakeLists.txt diff | blob | history
src/util/regexp.cpp [new file with mode: 0644] blob
src/util/regexp.h [new file with mode: 0644] blob
src/util/regexp.i [new file with mode: 0644] blob
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/strings/bug002.smt2 diff | blob | history
test/regress/regress0/strings/loop-wrong-sem.smt2 [new file with mode: 0644] blob
test/regress/regress1/strings/bug686dd.smt2 diff | blob | history
test/regress/regress1/strings/pierre150331.smt2 diff | blob | history
test/regress/regress1/strings/reloop.smt2 diff | blob | history
test/regress/regress2/strings/range-perf.smt2 diff | blob | history