GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/theory/theory_bv_rewriter_white.cpp Lines: 30 30 100.0 %
Date: 2021-03-22 Branches: 87 190 45.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_bv_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 bit-vector rewriter
13
 **
14
 ** Unit tests for the bit-vector rewriter.
15
 **/
16
17
#include <iostream>
18
#include <memory>
19
#include <vector>
20
21
#include "expr/node.h"
22
#include "test_smt.h"
23
#include "theory/rewriter.h"
24
#include "util/bitvector.h"
25
26
namespace CVC4 {
27
28
using namespace kind;
29
using namespace theory;
30
31
namespace test {
32
33
8
class TestTheoryWhiteBvRewriter : public TestSmt
34
{
35
 protected:
36
6
  Node boolToBv(Node b)
37
  {
38
    return d_nodeManager->mkNode(ITE,
39
                                 b,
40
12
                                 d_nodeManager->mkConst(BitVector(1, 1u)),
41
18
                                 d_nodeManager->mkConst(BitVector(1, 0u)));
42
  }
43
};
44
45
11
TEST_F(TestTheoryWhiteBvRewriter, rewrite_to_fixpoint)
46
{
47
4
  TypeNode boolType = d_nodeManager->booleanType();
48
4
  TypeNode bvType = d_nodeManager->mkBitVectorType(1);
49
50
4
  Node zero = d_nodeManager->mkConst(BitVector(1, 0u));
51
4
  Node b1 = d_nodeManager->mkVar("b1", boolType);
52
4
  Node b2 = d_nodeManager->mkVar("b2", boolType);
53
4
  Node b3 = d_nodeManager->mkVar("b3", boolType);
54
4
  Node bv = d_nodeManager->mkVar("bv", bvType);
55
56
  Node n = d_nodeManager->mkNode(
57
      BITVECTOR_ITE,
58
4
      boolToBv(b1),
59
12
      d_nodeManager->mkNode(
60
          BITVECTOR_ITE,
61
4
          boolToBv(b2),
62
4
          d_nodeManager->mkNode(BITVECTOR_ITE, boolToBv(b3), zero, bv),
63
          bv),
64
12
      bv);
65
4
  Node nr = Rewriter::rewrite(n);
66
2
  ASSERT_EQ(nr, Rewriter::rewrite(nr));
67
}
68
69
11
TEST_F(TestTheoryWhiteBvRewriter, rewrite_bv_ite)
70
{
71
4
  TypeNode boolType = d_nodeManager->booleanType();
72
4
  TypeNode bvType = d_nodeManager->mkBitVectorType(1);
73
74
4
  Node zero = d_nodeManager->mkConst(BitVector(1, 0u));
75
4
  Node c1 = d_nodeManager->mkVar("c1", bvType);
76
4
  Node c2 = d_nodeManager->mkVar("c2", bvType);
77
78
4
  Node ite = d_nodeManager->mkNode(BITVECTOR_ITE, c2, zero, zero);
79
4
  Node n = d_nodeManager->mkNode(BITVECTOR_ITE, c1, ite, ite);
80
4
  Node nr = Rewriter::rewrite(n);
81
2
  ASSERT_EQ(nr, Rewriter::rewrite(nr));
82
}
83
}  // namespace test
84
32101
}  // namespace CVC4