From 81ac7cd609ef011b615dccefde702fd5b3a5c39f Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 3 Nov 2020 11:55:52 -0800 Subject: [PATCH] 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.^. --- src/printer/smt2/smt2_printer.cpp | 16 +++++- test/unit/CMakeLists.txt | 1 + test/unit/printer/CMakeLists.txt | 14 ++++++ test/unit/printer/smt2_printer_black.h | 68 ++++++++++++++++++++++++++ 4 files changed, 98 insertions(+), 1 deletion(-) create mode 100644 test/unit/printer/CMakeLists.txt create mode 100644 test/unit/printer/smt2_printer_black.h diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index cdaa61295..5ef1eca2b 100644 --- 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().bvs.d_size << ")"; break; + case kind::REGEXP_REPEAT_OP: + out << "(_ re.^ " << n.getConst().d_repeatAmount << ")"; + break; + case kind::REGEXP_LOOP_OP: + out << "(_ re.loop " << n.getConst().d_loopMinOcc << " " + << n.getConst().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 f29785a56..bb53c15b0 100644 --- 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 index 000000000..3b040d1fc --- /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 index 000000000..8540c3cc8 --- /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 + +#include + +#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 d_slv; + NodeManager* d_nm; +}; -- 2.30.2