From 41554fa3d4a8258bbc842aedad87cd218460ee0a Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 1 Dec 2020 08:58:06 -0800 Subject: [PATCH] Improve rewriting of str.<= (#4848) This commit improves our rewriting of str.<= slightly. If we have constant prefixes that are different, we can always rewrite the term to a constant. Previously, we were only doing so when the result was false. --- src/theory/strings/strings_rewriter.cpp | 14 ++-- test/regress/CMakeLists.txt | 1 + test/regress/regress0/strings/leq.smt2 | 10 +++ test/unit/theory/CMakeLists.txt | 1 + test/unit/theory/strings_rewriter_white.h | 89 +++++++++++++++++++++++ 5 files changed, 107 insertions(+), 8 deletions(-) create mode 100644 test/regress/regress0/strings/leq.smt2 create mode 100644 test/unit/theory/strings_rewriter_white.h diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp index 932b5c8cc..575c33501 100644 --- a/src/theory/strings/strings_rewriter.cpp +++ b/src/theory/strings/strings_rewriter.cpp @@ -251,15 +251,13 @@ Node StringsRewriter::rewriteStringLeq(Node n) { String s = n1[0].getConst(); String t = n2[0].getConst(); - // only need to truncate if s is longer - if (s.size() > t.size()) + size_t prefixLen = std::min(s.size(), t.size()); + s = s.prefix(prefixLen); + t = t.prefix(prefixLen); + // if the prefixes are not the same, then we can already decide the outcome + if (s != t) { - s = s.prefix(t.size()); - } - // if prefix is not leq, then entire string is not leq - if (!s.isLeq(t)) - { - Node ret = nm->mkConst(false); + Node ret = nm->mkConst(s.isLeq(t)); return returnRewrite(n, ret, Rewrite::STR_LEQ_CPREFIX); } } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 1a2451147..fb8914a36 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1019,6 +1019,7 @@ set(regress_0_tests regress0/strings/itos-entail.smt2 regress0/strings/large-model.smt2 regress0/strings/leadingzero001.smt2 + regress0/strings/leq.smt2 regress0/strings/loop001.smt2 regress0/strings/loop-wrong-sem.smt2 regress0/strings/model001.smt2 diff --git a/test/regress/regress0/strings/leq.smt2 b/test/regress/regress0/strings/leq.smt2 new file mode 100644 index 000000000..b3bd40739 --- /dev/null +++ b/test/regress/regress0/strings/leq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --strings-exp +(set-logic QF_SLIA) +(declare-const x String) +(declare-const y String) +(assert (or + (not (str.<= (str.++ "A" x) (str.++ "B" y))) + (not (str.<= (str.++ "A" x) (str.++ "BC" y))) + (str.<= (str.++ "A" "D" x) (str.++ "AC" y)))) +(set-info :status unsat) +(check-sat) diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 8cfd43989..0eccbf436 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -13,6 +13,7 @@ cvc4_add_unit_test_black(theory_black theory) cvc4_add_unit_test_white(evaluator_white theory) cvc4_add_unit_test_white(logic_info_white theory) cvc4_add_unit_test_white(sequences_rewriter_white theory) +cvc4_add_unit_test_white(strings_rewriter_white theory) cvc4_add_unit_test_white(theory_arith_white theory) cvc4_add_unit_test_white(theory_bags_normal_form_white theory) cvc4_add_unit_test_white(theory_bags_rewriter_white theory) diff --git a/test/unit/theory/strings_rewriter_white.h b/test/unit/theory/strings_rewriter_white.h new file mode 100644 index 000000000..f5c7cced8 --- /dev/null +++ b/test/unit/theory/strings_rewriter_white.h @@ -0,0 +1,89 @@ +/********************* */ +/*! \file strings_rewriter_white.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 Unit tests for the strings rewriter + ** + ** Unit tests for the strings rewriter. + **/ + +#include + +#include +#include +#include + +#include "expr/node.h" +#include "expr/node_manager.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "theory/rewriter.h" +#include "theory/strings/strings_rewriter.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::smt; +using namespace CVC4::theory; +using namespace CVC4::theory::strings; + +class StringsRewriterWhite : public CxxTest::TestSuite +{ + public: + StringsRewriterWhite() {} + + void setUp() override + { + Options opts; + opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); + d_em = new ExprManager; + d_nm = NodeManager::fromExprManager(d_em); + d_smt = new SmtEngine(d_nm, &opts); + d_scope = new SmtScope(d_smt); + d_smt->finishInit(); + } + + void tearDown() override + { + delete d_scope; + delete d_smt; + delete d_em; + } + + void testRewriteLeq() + { + TypeNode intType = d_nm->integerType(); + TypeNode strType = d_nm->stringType(); + + Node a = d_nm->mkConst(::CVC4::String("A")); + Node bc = d_nm->mkConst(::CVC4::String("BC")); + Node x = d_nm->mkVar("x", strType); + Node y = d_nm->mkVar("y", strType); + + Node ax = d_nm->mkNode(STRING_CONCAT, a, x); + Node bcy = d_nm->mkNode(STRING_CONCAT, bc, y); + + { + Node leq = d_nm->mkNode(STRING_LEQ, ax, bcy); + TS_ASSERT_EQUALS(Rewriter::rewrite(leq), d_nm->mkConst(true)); + } + + { + Node leq = d_nm->mkNode(STRING_LEQ, bcy, ax); + TS_ASSERT_EQUALS(Rewriter::rewrite(leq), d_nm->mkConst(false)); + } + } + + private: + ExprManager* d_em; + SmtEngine* d_smt; + SmtScope* d_scope; + + NodeManager* d_nm; +}; -- 2.30.2