diff options
Diffstat (limited to 'test/unit')
| -rw-r--r-- | test/unit/Makefile.am | 9 | ||||
| -rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 136 |
2 files changed, 141 insertions, 4 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 3d5f2702d..b445583ac 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -7,14 +7,15 @@ UNIT_TESTS = \ if WHITE_AND_BLACK_TESTS UNIT_TESTS += \ theory/logic_info_white \ - theory/theory_engine_white \ - theory/theory_black \ - theory/theory_white \ theory/theory_arith_white \ - theory/theory_bv_white \ + theory/theory_black \ theory/theory_bv_bvgauss_white \ + theory/theory_bv_white \ + theory/theory_engine_white \ theory/theory_quantifiers_bv_instantiator_white \ theory/theory_quantifiers_bv_inverter_white \ + theory/theory_strings_rewriter_white \ + theory/theory_white \ theory/type_enumerator_white \ expr/node_white \ expr/node_black \ diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h new file mode 100644 index 000000000..a1e878f6e --- /dev/null +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -0,0 +1,136 @@ +/********************* */ +/*! \file theory_strings_rewriter_white.h + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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 "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/theory_strings_rewriter.h" + +#include <cxxtest/TestSuite.h> +#include <vector> + +using namespace CVC4; +using namespace CVC4::smt; +using namespace CVC4::theory; +using namespace CVC4::theory::strings; + +class TheoryStringsRewriterWhite : public CxxTest::TestSuite +{ + ExprManager *d_em; + NodeManager *d_nm; + SmtEngine *d_smt; + SmtScope *d_scope; + + public: + TheoryStringsRewriterWhite() {} + + void setUp() + { + Options opts; + opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); + d_em = new ExprManager(opts); + d_nm = NodeManager::fromExprManager(d_em); + d_smt = new SmtEngine(d_em); + d_scope = new SmtScope(d_smt); + } + + void tearDown() + { + delete d_scope; + delete d_smt; + delete d_em; + } + + void testCheckEntailArithWithAssumption() + { + TypeNode intType = d_nm->integerType(); + TypeNode strType = d_nm->stringType(); + + Node x = d_nm->mkVar("x", intType); + Node y = d_nm->mkVar("y", strType); + Node z = d_nm->mkVar("z", intType); + + Node zero = d_nm->mkConst(Rational(0)); + + Node slen_y = d_nm->mkNode(kind::STRING_LENGTH, y); + Node x_plus_slen_y = d_nm->mkNode(kind::PLUS, x, slen_y); + Node x_plus_slen_y_eq_zero = + Rewriter::rewrite(d_nm->mkNode(kind::EQUAL, x_plus_slen_y, zero)); + + // x + (str.len y) = 0 /\ 0 >= x --> true + TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption( + x_plus_slen_y_eq_zero, zero, x, false)); + + // x + (str.len y) = 0 /\ 0 > x --> false + TS_ASSERT(!TheoryStringsRewriter::checkEntailArithWithAssumption( + x_plus_slen_y_eq_zero, zero, x, true)); + + Node x_plus_slen_y_plus_z_eq_zero = Rewriter::rewrite(d_nm->mkNode( + kind::EQUAL, d_nm->mkNode(kind::PLUS, x_plus_slen_y, z), zero)); + + // x + (str.len y) + z = 0 /\ 0 > x --> false + TS_ASSERT(!TheoryStringsRewriter::checkEntailArithWithAssumption( + x_plus_slen_y_plus_z_eq_zero, zero, x, true)); + + Node x_plus_slen_y_plus_slen_y_eq_zero = Rewriter::rewrite(d_nm->mkNode( + kind::EQUAL, d_nm->mkNode(kind::PLUS, x_plus_slen_y, slen_y), zero)); + + // x + (str.len y) + (str.len y) = 0 /\ 0 >= x --> true + TS_ASSERT(TheoryStringsRewriter::checkEntailArithWithAssumption( + x_plus_slen_y_plus_slen_y_eq_zero, zero, x, false)); + } + + void testRewriteSubstr() + { + TypeNode intType = d_nm->integerType(); + TypeNode strType = d_nm->stringType(); + + Node empty = d_nm->mkConst(::CVC4::String("")); + Node a = d_nm->mkConst(::CVC4::String("A")); + Node s = d_nm->mkVar("s", strType); + Node x = d_nm->mkVar("x", intType); + Node y = d_nm->mkVar("y", intType); + + // (str.substr "A" x x) --> "" + Node n = d_nm->mkNode(kind::STRING_SUBSTR, a, x, x); + Node res = TheoryStringsRewriter::rewriteSubstr(n); + TS_ASSERT_EQUALS(res, empty); + + // (str.substr "A" (+ x 1) x) -> "" + n = d_nm->mkNode(kind::STRING_SUBSTR, + a, + d_nm->mkNode(kind::PLUS, x, d_nm->mkConst(Rational(1))), + x); + res = TheoryStringsRewriter::rewriteSubstr(n); + TS_ASSERT_EQUALS(res, empty); + + // (str.substr "A" (+ x (str.len s2)) x) -> "" + n = d_nm->mkNode( + kind::STRING_SUBSTR, + a, + d_nm->mkNode(kind::PLUS, x, d_nm->mkNode(kind::STRING_LENGTH, s)), + x); + res = TheoryStringsRewriter::rewriteSubstr(n); + TS_ASSERT_EQUALS(res, empty); + + // (str.substr "A" x y) -> (str.substr "A" x y) + n = d_nm->mkNode(kind::STRING_SUBSTR, a, x, y); + res = TheoryStringsRewriter::rewriteSubstr(n); + TS_ASSERT_EQUALS(res, n); + } +}; |