GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/theory/evaluator_white.cpp Lines: 68 68 100.0 %
Date: 2021-03-22 Branches: 216 496 43.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file evaluator_white.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 [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include <vector>
19
20
#include "expr/node.h"
21
#include "test_smt.h"
22
#include "theory/bv/theory_bv_utils.h"
23
#include "theory/evaluator.h"
24
#include "theory/rewriter.h"
25
#include "util/rational.h"
26
27
namespace CVC4 {
28
29
using namespace theory;
30
31
namespace test {
32
33
16
class TestTheoryWhiteEvaluator : public TestSmt
34
{
35
};
36
37
13
TEST_F(TestTheoryWhiteEvaluator, simple)
38
{
39
4
  TypeNode bv64Type = d_nodeManager->mkBitVectorType(64);
40
41
4
  Node w = d_nodeManager->mkVar("w", bv64Type);
42
4
  Node x = d_nodeManager->mkVar("x", bv64Type);
43
4
  Node y = d_nodeManager->mkVar("y", bv64Type);
44
4
  Node z = d_nodeManager->mkVar("z", bv64Type);
45
46
4
  Node zero = d_nodeManager->mkConst(BitVector(64, (unsigned int)0));
47
4
  Node one = d_nodeManager->mkConst(BitVector(64, (unsigned int)1));
48
4
  Node c1 = d_nodeManager->mkConst(BitVector(
49
      64,
50
6
      (unsigned int)0b0000000100000101001110111001101000101110011101011011110011100111));
51
4
  Node c2 = d_nodeManager->mkConst(BitVector(
52
      64,
53
6
      (unsigned int)0b0000000100000101001110111001101000101110011101011011110011100111));
54
55
  Node t = d_nodeManager->mkNode(
56
4
      kind::ITE, d_nodeManager->mkNode(kind::EQUAL, y, one), x, w);
57
58
4
  std::vector<Node> args = {w, x, y, z};
59
4
  std::vector<Node> vals = {c1, zero, one, c1};
60
61
  Evaluator eval;
62
4
  Node r = eval.eval(t, args, vals);
63
2
  ASSERT_EQ(r,
64
            Rewriter::rewrite(t.substitute(
65
2
                args.begin(), args.end(), vals.begin(), vals.end())));
66
}
67
68
13
TEST_F(TestTheoryWhiteEvaluator, loop)
69
{
70
4
  TypeNode bv64Type = d_nodeManager->mkBitVectorType(64);
71
72
4
  Node w = d_nodeManager->mkBoundVar(bv64Type);
73
4
  Node x = d_nodeManager->mkVar("x", bv64Type);
74
75
4
  Node zero = d_nodeManager->mkConst(BitVector(1, (unsigned int)0));
76
4
  Node one = d_nodeManager->mkConst(BitVector(64, (unsigned int)1));
77
4
  Node c = d_nodeManager->mkConst(BitVector(
78
      64,
79
6
      (unsigned int)0b0001111000010111110000110110001101011110111001101100000101010100));
80
81
4
  Node largs = d_nodeManager->mkNode(kind::BOUND_VAR_LIST, w);
82
  Node lbody = d_nodeManager->mkNode(
83
4
      kind::BITVECTOR_CONCAT, bv::utils::mkExtract(w, 62, 0), zero);
84
4
  Node lambda = d_nodeManager->mkNode(kind::LAMBDA, largs, lbody);
85
  Node t =
86
      d_nodeManager->mkNode(kind::BITVECTOR_AND,
87
4
                            d_nodeManager->mkNode(kind::APPLY_UF, lambda, one),
88
8
                            d_nodeManager->mkNode(kind::APPLY_UF, lambda, x));
89
90
4
  std::vector<Node> args = {x};
91
4
  std::vector<Node> vals = {c};
92
  Evaluator eval;
93
4
  Node r = eval.eval(t, args, vals);
94
2
  ASSERT_EQ(r,
95
            Rewriter::rewrite(t.substitute(
96
2
                args.begin(), args.end(), vals.begin(), vals.end())));
97
}
98
99
13
TEST_F(TestTheoryWhiteEvaluator, strIdOf)
100
{
101
4
  Node a = d_nodeManager->mkConst(String("A"));
102
4
  Node empty = d_nodeManager->mkConst(String(""));
103
4
  Node one = d_nodeManager->mkConst(Rational(1));
104
4
  Node two = d_nodeManager->mkConst(Rational(2));
105
106
4
  std::vector<Node> args;
107
4
  std::vector<Node> vals;
108
  Evaluator eval;
109
110
  {
111
4
    Node n = d_nodeManager->mkNode(kind::STRING_STRIDOF, a, empty, one);
112
4
    Node r = eval.eval(n, args, vals);
113
2
    ASSERT_EQ(r, Rewriter::rewrite(n));
114
  }
115
116
  {
117
4
    Node n = d_nodeManager->mkNode(kind::STRING_STRIDOF, a, a, one);
118
4
    Node r = eval.eval(n, args, vals);
119
2
    ASSERT_EQ(r, Rewriter::rewrite(n));
120
  }
121
122
  {
123
4
    Node n = d_nodeManager->mkNode(kind::STRING_STRIDOF, a, empty, two);
124
4
    Node r = eval.eval(n, args, vals);
125
2
    ASSERT_EQ(r, Rewriter::rewrite(n));
126
  }
127
128
  {
129
4
    Node n = d_nodeManager->mkNode(kind::STRING_STRIDOF, a, a, two);
130
4
    Node r = eval.eval(n, args, vals);
131
2
    ASSERT_EQ(r, Rewriter::rewrite(n));
132
  }
133
}
134
135
13
TEST_F(TestTheoryWhiteEvaluator, code)
136
{
137
4
  Node a = d_nodeManager->mkConst(String("A"));
138
4
  Node empty = d_nodeManager->mkConst(String(""));
139
140
4
  std::vector<Node> args;
141
4
  std::vector<Node> vals;
142
  Evaluator eval;
143
144
  // (str.code "A") ---> 65
145
  {
146
4
    Node n = d_nodeManager->mkNode(kind::STRING_TO_CODE, a);
147
4
    Node r = eval.eval(n, args, vals);
148
2
    ASSERT_EQ(r, d_nodeManager->mkConst(Rational(65)));
149
  }
150
151
  // (str.code "") ---> -1
152
  {
153
4
    Node n = d_nodeManager->mkNode(kind::STRING_TO_CODE, empty);
154
4
    Node r = eval.eval(n, args, vals);
155
2
    ASSERT_EQ(r, d_nodeManager->mkConst(Rational(-1)));
156
  }
157
}
158
}  // namespace test
159
67275
}  // namespace CVC4