From 86b26766f45b8f1a9850a955599974c369552df9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 2 Feb 2022 14:24:39 -0600 Subject: [PATCH] Fix printing of re.loop as an operator in LFSC (#8029) --- src/proof/lfsc/lfsc_node_converter.cpp | 9 ++++++++- test/regress/CMakeLists.txt | 1 + .../regress1/strings/instance1079-re-loop-cong.smt2 | 8 ++++++++ 3 files changed, 17 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress1/strings/instance1079-re-loop-cong.smt2 diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp index 8d1273dd2..56326a2fe 100644 --- a/src/proof/lfsc/lfsc_node_converter.cpp +++ b/src/proof/lfsc/lfsc_node_converter.cpp @@ -732,7 +732,7 @@ void LfscNodeConverter::getCharVectorInternal(Node c, std::vector& chars) bool LfscNodeConverter::isIndexedOperatorKind(Kind k) { - return k == BITVECTOR_EXTRACT || k == BITVECTOR_REPEAT + return k == REGEXP_LOOP || k == BITVECTOR_EXTRACT || k == BITVECTOR_REPEAT || k == BITVECTOR_ZERO_EXTEND || k == BITVECTOR_SIGN_EXTEND || k == BITVECTOR_ROTATE_LEFT || k == BITVECTOR_ROTATE_RIGHT || k == INT_TO_BITVECTOR || k == IAND || k == APPLY_UPDATER @@ -745,6 +745,13 @@ std::vector LfscNodeConverter::getOperatorIndices(Kind k, Node n) std::vector indices; switch (k) { + case REGEXP_LOOP: + { + RegExpLoop op = n.getConst(); + indices.push_back(nm->mkConstInt(Rational(op.d_loopMinOcc))); + indices.push_back(nm->mkConstInt(Rational(op.d_loopMaxOcc))); + break; + } case BITVECTOR_EXTRACT: { BitVectorExtract p = n.getConst(); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 72d8b0cc9..0085730e5 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2326,6 +2326,7 @@ set(regress_1_tests regress1/strings/idof-neg-index.smt2 regress1/strings/idof-triv.smt2 regress1/strings/ilc-l-nt.smt2 + regress1/strings/instance1079-re-loop-cong.smt2 regress1/strings/instance2984-null-term.smt2 regress1/strings/instance3303-delta.smt2 regress1/strings/instance7075-delta.smt2 diff --git a/test/regress/regress1/strings/instance1079-re-loop-cong.smt2 b/test/regress/regress1/strings/instance1079-re-loop-cong.smt2 new file mode 100644 index 000000000..50b32b26f --- /dev/null +++ b/test/regress/regress1/strings/instance1079-re-loop-cong.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: unsat +(set-logic QF_S) +(set-info :status unsat) +(declare-const X String) +(assert (not (str.in_re X (re.++ ((_ re.loop 0 16) (re.union re.allchar (str.to_re "\u{0a}"))) (str.to_re "\u{0a}"))))) +(assert (str.in_re X (str.to_re "//cdmax/Ui\u{0a}"))) +(check-sat) -- 2.30.2