GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/theory/theory_strings_skolem_cache_black.cpp Lines: 15 15 100.0 %
Date: 2021-03-23 Branches: 58 124 46.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_strings_skolem_cache_black.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Andres Noetzli
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 Black box testing of the skolem cache of the theory of strings.
13
 **/
14
15
#include <memory>
16
17
#include "expr/node.h"
18
#include "test_smt.h"
19
#include "theory/strings/skolem_cache.h"
20
#include "util/rational.h"
21
#include "util/string.h"
22
23
namespace CVC4 {
24
25
using namespace theory::strings;
26
27
namespace test {
28
29
4
class TestTheoryBlackStringsSkolemCache : public TestSmt
30
{
31
};
32
33
10
TEST_F(TestTheoryBlackStringsSkolemCache, mkSkolemCached)
34
{
35
4
  Node zero = d_nodeManager->mkConst(Rational(0));
36
4
  Node n = d_nodeManager->mkSkolem("n", d_nodeManager->integerType());
37
4
  Node a = d_nodeManager->mkSkolem("a", d_nodeManager->stringType());
38
4
  Node b = d_nodeManager->mkSkolem("b", d_nodeManager->stringType());
39
4
  Node c = d_nodeManager->mkSkolem("c", d_nodeManager->stringType());
40
4
  Node d = d_nodeManager->mkSkolem("d", d_nodeManager->stringType());
41
  Node sa = d_nodeManager->mkNode(
42
      kind::STRING_SUBSTR,
43
      a,
44
      zero,
45
4
      d_nodeManager->mkNode(kind::STRING_STRIDOF, a, b, zero));
46
4
  Node sc = d_nodeManager->mkNode(kind::STRING_SUBSTR, c, zero, n);
47
48
4
  SkolemCache sk;
49
50
  // Check that skolems are shared between:
51
  //
52
  // SK_FIRST_CTN(a, b)
53
  //
54
  // SK_FIRST_CTN(a, b)
55
  {
56
4
    Node s1 = sk.mkSkolemCached(a, b, SkolemCache::SK_FIRST_CTN_PRE, "foo");
57
4
    Node s2 = sk.mkSkolemCached(a, b, SkolemCache::SK_FIRST_CTN_PRE, "foo");
58
2
    ASSERT_EQ(s1, s2);
59
  }
60
}
61
}  // namespace test
62
268984
}  // namespace CVC4