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.

5 files changed, 107 insertions, 8 deletions

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>();
     String t = n2[0].getConst<String>();
-    // 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 <cxxtest/TestSuite.h>
+
+#include <iostream>
+#include <memory>
+#include <vector>
+
+#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;
+};