Add support for printing `re.loop` and `re.^` (#5392)

In the new SMT-LIB string standard, re.loop and re.^ are indexed
operators but the printer was not updated to print them correctly. This
commit adds support for printing re.loop and re.^.

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index cdaa61295814f2c287ef061e04b9fd01aa10d7e7..5ef1eca2b7d637a6b5589a64ab38a133c117f94d 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -367,6 +367,13 @@ void Smt2Printer::toStream(std::ostream& out,
       out << "(_ fp.to_sbv_total "
           << n.getConst<FloatingPointToSBVTotal>().bvs.d_size << ")";
       break;
+    case kind::REGEXP_REPEAT_OP:
+      out << "(_ re.^ " << n.getConst<RegExpRepeat>().d_repeatAmount << ")";
+      break;
+    case kind::REGEXP_LOOP_OP:
+      out << "(_ re.loop " << n.getConst<RegExpLoop>().d_loopMinOcc << " "
+          << n.getConst<RegExpLoop>().d_loopMaxOcc << ")";
+      break;
     default:
       // fall back on whatever operator<< does on underlying type; we
       // might luck out and be SMT-LIB v2 compliant
@@ -669,7 +676,6 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::REGEXP_PLUS:
   case kind::REGEXP_OPT:
   case kind::REGEXP_RANGE:
-  case kind::REGEXP_LOOP:
   case kind::REGEXP_COMPLEMENT:
   case kind::REGEXP_DIFF:
   case kind::REGEXP_EMPTY:
@@ -677,6 +683,13 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::SEQ_UNIT:
   case kind::SEQ_NTH:
   case kind::SEQUENCE_TYPE: out << smtKindString(k, d_variant) << " "; break;
+  case kind::REGEXP_REPEAT:
+  case kind::REGEXP_LOOP:
+  {
+    out << n.getOperator() << ' ';
+    stillNeedToPrintParams = false;
+    break;
+  }
 
   case kind::CARDINALITY_CONSTRAINT: out << "fmf.card "; break;
   case kind::CARDINALITY_VALUE: out << "fmf.card.val "; break;
@@ -1262,6 +1275,7 @@ static string smtKindString(Kind k, Variant v)
   case kind::REGEXP_PLUS: return "re.+";
   case kind::REGEXP_OPT: return "re.opt";
   case kind::REGEXP_RANGE: return "re.range";
+  case kind::REGEXP_REPEAT: return "re.^";
   case kind::REGEXP_LOOP: return "re.loop";
   case kind::REGEXP_COMPLEMENT: return "re.comp";
   case kind::REGEXP_DIFF: return "re.diff";

diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index f29785a5672c7d6298f63767e8686177ae9036b2..bb53c15b04217ab18c2c3277c8235801c0f8dc2b 100644 (file)
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -116,6 +116,7 @@ add_subdirectory(context)
 add_subdirectory(expr)
 add_subdirectory(main)
 add_subdirectory(parser)
+add_subdirectory(printer)
 add_subdirectory(prop)
 add_subdirectory(theory)
 add_subdirectory(preprocessing)

diff --git a/test/unit/printer/CMakeLists.txt b/test/unit/printer/CMakeLists.txt
new file mode 100644 (file)
index 0000000..3b040d1
--- /dev/null
+++ b/test/unit/printer/CMakeLists.txt
@@ -0,0 +1,14 @@
+#####################
+## CMakeLists.txt
+## Top contributors (to current version):
+##   Andres Noetzli
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+## in the top-level source directory and their institutional affiliations.
+## All rights reserved.  See the file COPYING in the top-level source
+## directory for licensing information.
+##
+#-----------------------------------------------------------------------------#
+# Add unit tests
+
+cvc4_add_unit_test_black(smt2_printer_black printer)

diff --git a/test/unit/printer/smt2_printer_black.h b/test/unit/printer/smt2_printer_black.h
new file mode 100644 (file)
index 0000000..8540c3c
--- /dev/null
+++ b/test/unit/printer/smt2_printer_black.h
@@ -0,0 +1,68 @@
+/*********************                                                        */
+/*! \file smt2_printer_black.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of the SMT2 printer
+ **
+ ** Black box testing of the SMT2 printer.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <iostream>
+
+#include "api/cvc4cpp.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "options/language.h"
+#include "smt/smt_engine.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+
+class Smt2PrinterBlack : public CxxTest::TestSuite
+{
+ public:
+  void setUp() override
+  {
+    d_slv.reset(new api::Solver());
+    d_nm = d_slv->getSmtEngine()->getNodeManager();
+  }
+
+  void tearDown() override { d_slv.reset(); }
+
+  void checkToString(TNode n, const std::string& expected)
+  {
+    std::stringstream ss;
+    ss << Node::setdepth(-1)
+       << Node::setlanguage(language::output::LANG_SMTLIB_V2_6) << n;
+    TS_ASSERT_EQUALS(ss.str(), expected);
+  }
+
+  void testRegexpRepeat()
+  {
+    Node n = d_nm->mkNode(
+        d_nm->mkConst(RegExpRepeat(5)),
+        d_nm->mkNode(STRING_TO_REGEXP, d_nm->mkConst(String("x"))));
+    checkToString(n, "((_ re.^ 5) (str.to_re \"x\"))");
+  }
+
+  void testRegexpLoop()
+  {
+    Node n = d_nm->mkNode(
+        d_nm->mkConst(RegExpLoop(1, 3)),
+        d_nm->mkNode(STRING_TO_REGEXP, d_nm->mkConst(String("x"))));
+    checkToString(n, "((_ re.loop 1 3) (str.to_re \"x\"))");
+  }
+
+ private:
+  std::unique_ptr<api::Solver> d_slv;
+  NodeManager* d_nm;
+};