GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/theory/theory_bv_white.cpp Lines: 37 37 100.0 %
Date: 2021-03-23 Branches: 105 224 46.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_bv_white.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Abdalrhman Mohamed, Mathias Preiner
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 "context/context.h"
21
#include "expr/node.h"
22
#include "test_smt.h"
23
#include "theory/bv/bitblast/eager_bitblaster.h"
24
#include "theory/bv/bv_solver_lazy.h"
25
#include "theory/theory.h"
26
#include "theory/theory_engine.h"
27
28
namespace CVC4 {
29
30
using namespace theory;
31
using namespace theory::bv;
32
using namespace theory::bv::utils;
33
using namespace expr;
34
using namespace context;
35
36
namespace test {
37
38
8
class TestTheoryWhiteBv : public TestSmtNoFinishInit
39
{
40
};
41
42
11
TEST_F(TestTheoryWhiteBv, bitblaster_core)
43
{
44
2
  d_smtEngine->setLogic("QF_BV");
45
46
2
  d_smtEngine->setOption("bitblast", "eager");
47
2
  d_smtEngine->setOption("incremental", "false");
48
  // Notice that this unit test uses the theory engine of a created SMT
49
  // engine d_smtEngine. We must ensure that d_smtEngine is properly initialized
50
  // via the following call, which constructs its underlying theory engine.
51
2
  d_smtEngine->finishInit();
52
2
  TheoryBV* tbv = dynamic_cast<TheoryBV*>(
53
4
      d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_BV]);
54
2
  BVSolverLazy* bvsl = dynamic_cast<BVSolverLazy*>(tbv->d_internal.get());
55
  std::unique_ptr<EagerBitblaster> bb(
56
4
      new EagerBitblaster(bvsl, d_smtEngine->getContext()));
57
58
4
  Node x = d_nodeManager->mkVar("x", d_nodeManager->mkBitVectorType(16));
59
4
  Node y = d_nodeManager->mkVar("y", d_nodeManager->mkBitVectorType(16));
60
4
  Node x_plus_y = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, x, y);
61
4
  Node one = d_nodeManager->mkConst<BitVector>(BitVector(16, 1u));
62
4
  Node x_shl_one = d_nodeManager->mkNode(kind::BITVECTOR_SHL, x, one);
63
4
  Node eq = d_nodeManager->mkNode(kind::EQUAL, x_plus_y, x_shl_one);
64
  Node not_x_eq_y = d_nodeManager->mkNode(
65
4
      kind::NOT, d_nodeManager->mkNode(kind::EQUAL, x, y));
66
67
2
  bb->bbFormula(eq);
68
2
  bb->bbFormula(not_x_eq_y);
69
70
2
  ASSERT_EQ(bb->solve(), false);
71
}
72
73
11
TEST_F(TestTheoryWhiteBv, mkUmulo)
74
{
75
2
  d_smtEngine->setOption("incremental", "true");
76
32
  for (uint32_t w = 1; w < 16; ++w)
77
  {
78
30
    d_smtEngine->push();
79
60
    Node x = d_nodeManager->mkVar("x", d_nodeManager->mkBitVectorType(w));
80
60
    Node y = d_nodeManager->mkVar("y", d_nodeManager->mkBitVectorType(w));
81
82
60
    Node zx = mkConcat(mkZero(w), x);
83
60
    Node zy = mkConcat(mkZero(w), y);
84
60
    Node mul = d_nodeManager->mkNode(kind::BITVECTOR_MULT, zx, zy);
85
    Node lhs = d_nodeManager->mkNode(
86
60
        kind::DISTINCT, mkExtract(mul, 2 * w - 1, w), mkZero(w));
87
60
    Node rhs = mkUmulo(x, y);
88
60
    Node eq = d_nodeManager->mkNode(kind::DISTINCT, lhs, rhs);
89
30
    d_smtEngine->assertFormula(eq);
90
60
    Result res = d_smtEngine->checkSat();
91
30
    ASSERT_EQ(res.isSat(), Result::UNSAT);
92
30
    d_smtEngine->pop();
93
  }
94
}
95
}  // namespace test
96
11217905
}  // namespace CVC4