GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/api/solver_white.cpp Lines: 21 21 100.0 %
Date: 2021-03-23 Branches: 55 134 41.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file solver_white.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Makai Mann, 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 Black box testing of the Solver class of the  C++ API.
13
 **
14
 ** Black box testing of the Solver class of the  C++ API.
15
 **/
16
17
#include "base/configuration.h"
18
#include "test_api.h"
19
20
namespace CVC4 {
21
22
using namespace api;
23
24
namespace test {
25
26
4
class TestApiWhiteSolver : public TestApi
27
{
28
};
29
30
10
TEST_F(TestApiWhiteSolver, getOp)
31
{
32
4
  DatatypeDecl consListSpec = d_solver.mkDatatypeDecl("list");
33
4
  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
34
2
  cons.addSelector("head", d_solver.getIntegerSort());
35
2
  cons.addSelectorSelf("tail");
36
2
  consListSpec.addConstructor(cons);
37
4
  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
38
2
  consListSpec.addConstructor(nil);
39
4
  Sort consListSort = d_solver.mkDatatypeSort(consListSpec);
40
4
  Datatype consList = consListSort.getDatatype();
41
42
4
  Term nilTerm = consList.getConstructorTerm("nil");
43
4
  Term consTerm = consList.getConstructorTerm("cons");
44
4
  Term headTerm = consList["cons"].getSelectorTerm("head");
45
46
4
  Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm);
47
  Term listcons1 = d_solver.mkTerm(
48
4
      APPLY_CONSTRUCTOR, consTerm, d_solver.mkInteger(1), listnil);
49
4
  Term listhead = d_solver.mkTerm(APPLY_SELECTOR, headTerm, listcons1);
50
51
2
  ASSERT_EQ(listnil.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
52
2
  ASSERT_EQ(listcons1.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
53
2
  ASSERT_EQ(listhead.getOp(), Op(&d_solver, APPLY_SELECTOR));
54
}
55
56
}  // namespace test
57
6
}  // namespace CVC4