GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/api/term_white.cpp Lines: 42 42 100.0 %
Date: 2021-03-23 Branches: 121 298 40.6 %

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