diff options
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 5 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 3 | ||||
| -rw-r--r-- | test/regress/regress0/strings/re.all.smt2 | 6 |
3 files changed, 13 insertions, 1 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 71ba81124..2e1abf710 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -122,6 +122,11 @@ void Smt2::addBitvectorOperators() { } void Smt2::addStringOperators() { + defineVar("re.all", + getSolver() + ->mkTerm(api::REGEXP_STAR, getSolver()->mkRegexpSigma()) + .getExpr()); + addOperator(kind::STRING_CONCAT, "str.++"); addOperator(kind::STRING_LENGTH, "str.len"); addOperator(kind::STRING_SUBSTR, "str.substr" ); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 8ab86e772..b767d6c12 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -841,6 +841,7 @@ set(regress_0_tests regress0/strings/ncontrib-rewrites.smt2 regress0/strings/norn-31.smt2 regress0/strings/norn-simp-rew.smt2 + regress0/strings/re.all.smt2 regress0/strings/repl-rewrites2.smt2 regress0/strings/replaceall-eval.smt2 regress0/strings/rewrites-re-concat.smt2 @@ -882,7 +883,6 @@ set(regress_0_tests regress0/test9.cvc regress0/tptp/ARI086=1.p regress0/tptp/DAT001=1.p - regress0/tptp/is_rat_simple.p regress0/tptp/KRS018+1.p regress0/tptp/KRS063+1.p regress0/tptp/MGT019+2.p @@ -896,6 +896,7 @@ set(regress_0_tests regress0/tptp/SYN000_1.p regress0/tptp/SYN000_2.p regress0/tptp/SYN075-1.p + regress0/tptp/is_rat_simple.p regress0/tptp/tff0-arith.p regress0/tptp/tff0.p regress0/tptp/tptp_parser.p diff --git a/test/regress/regress0/strings/re.all.smt2 b/test/regress/regress0/strings/re.all.smt2 new file mode 100644 index 000000000..5200b924f --- /dev/null +++ b/test/regress/regress0/strings/re.all.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-const x String) +(assert (str.in.re x (re.++ (str.to.re "abc") re.all))) +(assert (not (str.prefixof "abc" x))) +(check-sat) |