GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/theory/strings_rewriter_white.cpp Lines: 15 15 100.0 %
Date: 2021-03-22 Branches: 47 110 42.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file strings_rewriter_white.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Unit tests for the strings rewriter
13
 **
14
 ** Unit tests for the strings rewriter.
15
 **/
16
17
#include <iostream>
18
#include <memory>
19
#include <vector>
20
21
#include "expr/node.h"
22
#include "expr/node_manager.h"
23
#include "test_smt.h"
24
#include "theory/rewriter.h"
25
#include "theory/strings/strings_rewriter.h"
26
27
namespace CVC4 {
28
29
using namespace kind;
30
using namespace theory;
31
using namespace theory::strings;
32
33
namespace test {
34
35
4
class TestTheoryWhiteStringsRewriter : public TestSmt
36
{
37
};
38
39
10
TEST_F(TestTheoryWhiteStringsRewriter, rewrite_leq)
40
{
41
4
  TypeNode intType = d_nodeManager->integerType();
42
4
  TypeNode strType = d_nodeManager->stringType();
43
44
4
  Node a = d_nodeManager->mkConst(::CVC4::String("A"));
45
4
  Node bc = d_nodeManager->mkConst(::CVC4::String("BC"));
46
4
  Node x = d_nodeManager->mkVar("x", strType);
47
4
  Node y = d_nodeManager->mkVar("y", strType);
48
49
4
  Node ax = d_nodeManager->mkNode(STRING_CONCAT, a, x);
50
4
  Node bcy = d_nodeManager->mkNode(STRING_CONCAT, bc, y);
51
52
  {
53
4
    Node leq = d_nodeManager->mkNode(STRING_LEQ, ax, bcy);
54
2
    ASSERT_EQ(Rewriter::rewrite(leq), d_nodeManager->mkConst(true));
55
  }
56
57
  {
58
4
    Node leq = d_nodeManager->mkNode(STRING_LEQ, bcy, ax);
59
2
    ASSERT_EQ(Rewriter::rewrite(leq), d_nodeManager->mkConst(false));
60
  }
61
}
62
63
}  // namespace test
64
16068
}  // namespace CVC4