Infer conflicts based on regular expression inclusion (#3234)

We have a conflict if we have `str.in.re(x, R1)` and `~str.in.re(x, R2)`
and `R2` includes `R1` because there is no possible value for `x` that
satisfies both memberships. This commit adds code to detect regular
expression inclusion for a small fragment of regular expressions: string
literals with single char (`re.allchar`) and multichar wildcards
(`re.*(re.allchar)`).

Signed-off-by: Andres Noetzli <anoetzli@amazon.com>

5 files changed, 182 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 80b7c33bf..444a740ea 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -862,6 +862,8 @@ set(regress_0_tests
   regress0/strings/norn-31.smt2
   regress0/strings/norn-simp-rew.smt2
   regress0/strings/re.all.smt2
+  regress0/strings/regexp_inclusion.smt2
+  regress0/strings/regexp_inclusion_reduction.smt2
   regress0/strings/repl-rewrites2.smt2
   regress0/strings/replace-const.smt2
   regress0/strings/replaceall-eval.smt2
diff --git a/test/regress/regress0/strings/regexp_inclusion.smt2 b/test/regress/regress0/strings/regexp_inclusion.smt2
new file mode 100644
index 000000000..c5c68a408
--- /dev/null
+++ b/test/regress/regress0/strings/regexp_inclusion.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --strings-exp --no-re-elim
+(set-info :status unsat)
+(set-logic ALL)
+(declare-const actionName String)
+
+(assert
+(str.in.re actionName (re.++ (str.to.re "wiz") (re.* re.allchar) (str.to.re "foobar") (re.* re.allchar) (str.to.re "baz/") (re.* re.allchar))))
+
+(assert (not
+(str.in.re actionName (re.++ (str.to.re "wiz") (re.* re.allchar) (re.++ (str.to.re "foo") re.allchar (str.to.re "ar")) (re.* re.allchar) (str.to.re "baz/") (re.* re.allchar)))
+))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/regexp_inclusion_reduction.smt2 b/test/regress/regress0/strings/regexp_inclusion_reduction.smt2
new file mode 100644
index 000000000..c10c287bb
--- /dev/null
+++ b/test/regress/regress0/strings/regexp_inclusion_reduction.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --strings-exp --no-re-elim
+(set-info :status sat)
+(set-logic QF_SLIA)
+(declare-const x String)
+(declare-const y String)
+
+(assert (str.in.re x (re.++ (str.to.re "bar") (re.* re.allchar) (str.to.re "bar"))))
+(assert (str.in.re x (re.++ (str.to.re "ba") re.allchar (re.* re.allchar) (str.to.re "bar"))))
+
+(assert (not (str.in.re y (re.++ (str.to.re "bar") (re.* re.allchar) (str.to.re "bar")))))
+(assert (not (str.in.re y (re.++ (str.to.re "ba") re.allchar (re.* re.allchar) (str.to.re "bar")))))
+(assert (not (= y "")))
+
+(check-sat)
diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index 963466b09..02ca5d8b5 100644
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -1,3 +1,4 @@
+cvc4_add_unit_test_black(regexp_operation_black theory)
 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)
diff --git a/test/unit/theory/regexp_operation_black.h b/test/unit/theory/regexp_operation_black.h
new file mode 100644
index 000000000..81f5cf34a
--- /dev/null
+++ b/test/unit/theory/regexp_operation_black.h
@@ -0,0 +1,152 @@
+/*********************                                                        */
+/*! \file regexp_operation_black.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 symbolic regular expression operations
+ **
+ ** Unit tests for symbolic regular expression operations.
+ **/
+
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "theory/strings/regexp_operation.h"
+
+#include <cxxtest/TestSuite.h>
+#include <iostream>
+#include <memory>
+#include <vector>
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::smt;
+using namespace CVC4::theory;
+using namespace CVC4::theory::strings;
+
+class RegexpOperationBlack : public CxxTest::TestSuite
+{
+ public:
+  RegexpOperationBlack() {}
+
+  void setUp() override
+  {
+    Options opts;
+    opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
+    d_em = new ExprManager(opts);
+    d_smt = new SmtEngine(d_em);
+    d_scope = new SmtScope(d_smt);
+    d_regExpOpr = new RegExpOpr();
+
+    d_nm = NodeManager::currentNM();
+  }
+
+  void tearDown() override
+  {
+    delete d_regExpOpr;
+    delete d_scope;
+    delete d_smt;
+    delete d_em;
+  }
+
+  void includes(Node r1, Node r2)
+  {
+    r1 = Rewriter::rewrite(r1);
+    r2 = Rewriter::rewrite(r2);
+    std::cout << r1 << " includes " << r2 << std::endl;
+    TS_ASSERT(d_regExpOpr->regExpIncludes(r1, r2));
+  }
+
+  void doesNotInclude(Node r1, Node r2)
+  {
+    r1 = Rewriter::rewrite(r1);
+    r2 = Rewriter::rewrite(r2);
+    std::cout << r1 << " does not include " << r2 << std::endl;
+    TS_ASSERT(!d_regExpOpr->regExpIncludes(r1, r2));
+  }
+
+  void testBasic()
+  {
+    Node sigma = d_nm->mkNode(REGEXP_SIGMA, std::vector<Node>{});
+    Node sigmaStar = d_nm->mkNode(REGEXP_STAR, sigma);
+    Node a = d_nm->mkNode(STRING_TO_REGEXP, d_nm->mkConst(String("a")));
+    Node c = d_nm->mkNode(STRING_TO_REGEXP, d_nm->mkConst(String("c")));
+    Node abc = d_nm->mkNode(STRING_TO_REGEXP, d_nm->mkConst(String("abc")));
+    Node sigma3 = d_nm->mkNode(REGEXP_CONCAT, sigma, sigma, sigma);
+    Node asc = d_nm->mkNode(REGEXP_CONCAT, a, sigma, c);
+    Node asw = d_nm->mkNode(REGEXP_CONCAT, a, sigma, sigmaStar);
+
+    includes(sigma3, abc);
+    doesNotInclude(abc, sigma3);
+
+    includes(sigma3, asc);
+    doesNotInclude(asc, sigma3);
+
+    includes(asc, abc);
+    doesNotInclude(abc, asc);
+
+    includes(asw, asc);
+    doesNotInclude(asc, asw);
+  }
+
+  void testStarWildcards()
+  {
+    Node sigma = d_nm->mkNode(REGEXP_SIGMA, std::vector<Node>{});
+    Node sigmaStar = d_nm->mkNode(REGEXP_STAR, sigma);
+    Node a = d_nm->mkNode(STRING_TO_REGEXP, d_nm->mkConst(String("a")));
+    Node c = d_nm->mkNode(STRING_TO_REGEXP, d_nm->mkConst(String("c")));
+    Node abc = d_nm->mkNode(STRING_TO_REGEXP, d_nm->mkConst(String("abc")));
+
+    Node _abc_ = d_nm->mkNode(REGEXP_CONCAT, sigmaStar, abc, sigmaStar);
+    Node _asc_ = d_nm->mkNode(REGEXP_CONCAT, sigmaStar, a, sigma, c, sigmaStar);
+    Node _sc_ = Rewriter::rewrite(
+        d_nm->mkNode(REGEXP_CONCAT, sigmaStar, sigma, c, sigmaStar));
+    Node _as_ = Rewriter::rewrite(
+        d_nm->mkNode(REGEXP_CONCAT, sigmaStar, a, sigma, sigmaStar));
+    Node _assc_ = d_nm->mkNode(
+        REGEXP_CONCAT,
+        std::vector<Node>{sigmaStar, a, sigma, sigma, c, sigmaStar});
+    Node _csa_ = d_nm->mkNode(REGEXP_CONCAT, sigmaStar, c, sigma, a, sigmaStar);
+    Node _c_a_ =
+        d_nm->mkNode(REGEXP_CONCAT, sigmaStar, c, sigmaStar, a, sigmaStar);
+    Node _s_s_ = Rewriter::rewrite(d_nm->mkNode(
+        REGEXP_CONCAT, sigmaStar, sigma, sigmaStar, sigma, sigmaStar));
+    Node _a_abc_ = Rewriter::rewrite(
+        d_nm->mkNode(REGEXP_CONCAT, sigmaStar, a, sigmaStar, abc, sigmaStar));
+
+    includes(_asc_, _abc_);
+    doesNotInclude(_abc_, _asc_);
+    doesNotInclude(_csa_, _abc_);
+    doesNotInclude(_assc_, _asc_);
+    doesNotInclude(_asc_, _assc_);
+    includes(_sc_, abc);
+    includes(_sc_, _abc_);
+    includes(_sc_, _asc_);
+    includes(_sc_, _assc_);
+    doesNotInclude(_sc_, _csa_);
+    includes(_as_, abc);
+    includes(_as_, _abc_);
+    includes(_as_, _asc_);
+    includes(_as_, _assc_);
+    doesNotInclude(_sc_, _csa_);
+    includes(_s_s_, _c_a_);
+    doesNotInclude(_c_a_, _s_s_);
+    includes(_abc_, _a_abc_);
+    doesNotInclude(_a_abc_, _abc_);
+  }
+
+ private:
+  ExprManager* d_em;
+  SmtEngine* d_smt;
+  SmtScope* d_scope;
+  RegExpOpr* d_regExpOpr;
+
+  NodeManager* d_nm;
+};