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