1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Makai Mann, Aina Niemetz, Andrew Reynolds |
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 |
|
* White box testing of the Term class. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "test_api.h" |
17 |
|
|
18 |
|
namespace cvc5 { |
19 |
|
|
20 |
|
using namespace api; |
21 |
|
|
22 |
|
namespace test { |
23 |
|
|
24 |
4 |
class TestApiWhiteTerm : public TestApi |
25 |
|
{ |
26 |
|
}; |
27 |
|
|
28 |
10 |
TEST_F(TestApiWhiteTerm, getOp) |
29 |
|
{ |
30 |
4 |
Sort intsort = d_solver.getIntegerSort(); |
31 |
4 |
Sort bvsort = d_solver.mkBitVectorSort(8); |
32 |
4 |
Sort arrsort = d_solver.mkArraySort(bvsort, intsort); |
33 |
4 |
Sort funsort = d_solver.mkFunctionSort(intsort, bvsort); |
34 |
|
|
35 |
4 |
Term x = d_solver.mkConst(intsort, "x"); |
36 |
4 |
Term a = d_solver.mkConst(arrsort, "a"); |
37 |
4 |
Term b = d_solver.mkConst(bvsort, "b"); |
38 |
|
|
39 |
4 |
Term ab = d_solver.mkTerm(SELECT, a, b); |
40 |
4 |
Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0); |
41 |
4 |
Term extb = d_solver.mkTerm(ext, b); |
42 |
|
|
43 |
2 |
ASSERT_EQ(ab.getOp(), Op(&d_solver, SELECT)); |
44 |
|
// can compare directly to a Kind (will invoke Op constructor) |
45 |
2 |
ASSERT_EQ(ab.getOp(), Op(&d_solver, SELECT)); |
46 |
|
|
47 |
4 |
Term f = d_solver.mkConst(funsort, "f"); |
48 |
4 |
Term fx = d_solver.mkTerm(APPLY_UF, f, x); |
49 |
|
|
50 |
2 |
ASSERT_EQ(fx.getOp(), Op(&d_solver, APPLY_UF)); |
51 |
|
// testing rebuild from op and children |
52 |
|
|
53 |
|
// Test Datatypes Ops |
54 |
4 |
Sort sort = d_solver.mkParamSort("T"); |
55 |
4 |
DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort); |
56 |
4 |
DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); |
57 |
4 |
DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); |
58 |
2 |
cons.addSelector("head", sort); |
59 |
2 |
cons.addSelectorSelf("tail"); |
60 |
2 |
listDecl.addConstructor(cons); |
61 |
2 |
listDecl.addConstructor(nil); |
62 |
4 |
Sort listSort = d_solver.mkDatatypeSort(listDecl); |
63 |
|
Sort intListSort = |
64 |
4 |
listSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}); |
65 |
4 |
Term c = d_solver.mkConst(intListSort, "c"); |
66 |
4 |
Datatype list = listSort.getDatatype(); |
67 |
|
// list datatype constructor and selector operator terms |
68 |
4 |
Term consOpTerm = list.getConstructorTerm("cons"); |
69 |
4 |
Term nilOpTerm = list.getConstructorTerm("nil"); |
70 |
4 |
Term headOpTerm = list["cons"].getSelectorTerm("head"); |
71 |
4 |
Term tailOpTerm = list["cons"].getSelectorTerm("tail"); |
72 |
|
|
73 |
4 |
Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilOpTerm); |
74 |
|
Term consTerm = d_solver.mkTerm( |
75 |
4 |
APPLY_CONSTRUCTOR, consOpTerm, d_solver.mkInteger(0), nilTerm); |
76 |
4 |
Term headTerm = d_solver.mkTerm(APPLY_SELECTOR, headOpTerm, consTerm); |
77 |
4 |
Term tailTerm = d_solver.mkTerm(APPLY_SELECTOR, tailOpTerm, consTerm); |
78 |
|
|
79 |
2 |
ASSERT_EQ(nilTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR)); |
80 |
2 |
ASSERT_EQ(consTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR)); |
81 |
2 |
ASSERT_EQ(headTerm.getOp(), Op(&d_solver, APPLY_SELECTOR)); |
82 |
2 |
ASSERT_EQ(tailTerm.getOp(), Op(&d_solver, APPLY_SELECTOR)); |
83 |
|
} |
84 |
|
} // namespace test |
85 |
6 |
} // namespace cvc5 |