diff options
author | Andres Noetzli <noetzli@stanford.edu> | 2019-08-29 19:38:17 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-29 19:38:17 -0700 |
commit | 974fc1d23c2b6091c26cf316964c4c16c5e2733f (patch) | |
tree | b8e4b597ffc46194ee37687a56248309a63235b1 /test/unit/theory | |
parent | cc7546ff0a4e418de9a21c03ef12b1d5e8801bb8 (diff) |
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>
Diffstat (limited to 'test/unit/theory')
-rw-r--r-- | test/unit/theory/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/unit/theory/regexp_operation_black.h | 152 |
2 files changed, 153 insertions, 0 deletions
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; +}; |