From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 2 Feb 2022 20:24:39 +0000 (-0600)
Subject: Fix printing of re.loop as an operator in LFSC (#8029)
X-Git-Tag: cvc5-1.0.0~475
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=86b26766f45b8f1a9850a955599974c369552df9;p=cvc5.git

Fix printing of re.loop as an operator in LFSC (#8029)
---

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<Node>& 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<Node> LfscNodeConverter::getOperatorIndices(Kind k, Node n)
   std::vector<Node> indices;
   switch (k)
   {
+    case REGEXP_LOOP:
+    {
+      RegExpLoop op = n.getConst<RegExpLoop>();
+      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<BitVectorExtract>();
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)