GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/api/grammar_black.cpp Lines: 60 60 100.0 %
Date: 2021-03-23 Branches: 235 654 35.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file grammar_black.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz
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 guards of the C++ API functions.
13
 **
14
 ** Black box testing of the guards of the C++ API functions.
15
 **/
16
17
#include "test_api.h"
18
19
namespace CVC4 {
20
21
using namespace api;
22
23
namespace test {
24
25
16
class TestApiBlackGrammar : public TestApi
26
{
27
};
28
29
13
TEST_F(TestApiBlackGrammar, addRule)
30
{
31
4
  Sort boolean = d_solver.getBooleanSort();
32
4
  Sort integer = d_solver.getIntegerSort();
33
34
4
  Term nullTerm;
35
4
  Term start = d_solver.mkVar(boolean);
36
4
  Term nts = d_solver.mkVar(boolean);
37
38
4
  Grammar g = d_solver.mkSygusGrammar({}, {start});
39
40
2
  ASSERT_NO_THROW(g.addRule(start, d_solver.mkBoolean(false)));
41
42
4
  ASSERT_THROW(g.addRule(nullTerm, d_solver.mkBoolean(false)),
43
2
               CVC4ApiException);
44
4
  ASSERT_THROW(g.addRule(start, nullTerm), CVC4ApiException);
45
4
  ASSERT_THROW(g.addRule(nts, d_solver.mkBoolean(false)), CVC4ApiException);
46
4
  ASSERT_THROW(g.addRule(start, d_solver.mkInteger(0)), CVC4ApiException);
47
48
2
  d_solver.synthFun("f", {}, boolean, g);
49
50
4
  ASSERT_THROW(g.addRule(start, d_solver.mkBoolean(false)), CVC4ApiException);
51
}
52
53
13
TEST_F(TestApiBlackGrammar, addRules)
54
{
55
4
  Sort boolean = d_solver.getBooleanSort();
56
4
  Sort integer = d_solver.getIntegerSort();
57
58
4
  Term nullTerm;
59
4
  Term start = d_solver.mkVar(boolean);
60
4
  Term nts = d_solver.mkVar(boolean);
61
62
4
  Grammar g = d_solver.mkSygusGrammar({}, {start});
63
64
2
  ASSERT_NO_THROW(g.addRules(start, {d_solver.mkBoolean(false)}));
65
66
4
  ASSERT_THROW(g.addRules(nullTerm, {d_solver.mkBoolean(false)}),
67
2
               CVC4ApiException);
68
4
  ASSERT_THROW(g.addRules(start, {nullTerm}), CVC4ApiException);
69
4
  ASSERT_THROW(g.addRules(nts, {d_solver.mkBoolean(false)}), CVC4ApiException);
70
4
  ASSERT_THROW(g.addRules(start, {d_solver.mkInteger(0)}), CVC4ApiException);
71
72
2
  d_solver.synthFun("f", {}, boolean, g);
73
74
4
  ASSERT_THROW(g.addRules(start, {d_solver.mkBoolean(false)}),
75
2
               CVC4ApiException);
76
}
77
78
13
TEST_F(TestApiBlackGrammar, addAnyConstant)
79
{
80
4
  Sort boolean = d_solver.getBooleanSort();
81
82
4
  Term nullTerm;
83
4
  Term start = d_solver.mkVar(boolean);
84
4
  Term nts = d_solver.mkVar(boolean);
85
86
4
  Grammar g = d_solver.mkSygusGrammar({}, {start});
87
88
2
  ASSERT_NO_THROW(g.addAnyConstant(start));
89
2
  ASSERT_NO_THROW(g.addAnyConstant(start));
90
91
4
  ASSERT_THROW(g.addAnyConstant(nullTerm), CVC4ApiException);
92
4
  ASSERT_THROW(g.addAnyConstant(nts), CVC4ApiException);
93
94
2
  d_solver.synthFun("f", {}, boolean, g);
95
96
4
  ASSERT_THROW(g.addAnyConstant(start), CVC4ApiException);
97
}
98
99
13
TEST_F(TestApiBlackGrammar, addAnyVariable)
100
{
101
4
  Sort boolean = d_solver.getBooleanSort();
102
103
4
  Term nullTerm;
104
4
  Term x = d_solver.mkVar(boolean);
105
4
  Term start = d_solver.mkVar(boolean);
106
4
  Term nts = d_solver.mkVar(boolean);
107
108
4
  Grammar g1 = d_solver.mkSygusGrammar({x}, {start});
109
4
  Grammar g2 = d_solver.mkSygusGrammar({}, {start});
110
111
2
  ASSERT_NO_THROW(g1.addAnyVariable(start));
112
2
  ASSERT_NO_THROW(g1.addAnyVariable(start));
113
2
  ASSERT_NO_THROW(g2.addAnyVariable(start));
114
115
4
  ASSERT_THROW(g1.addAnyVariable(nullTerm), CVC4ApiException);
116
4
  ASSERT_THROW(g1.addAnyVariable(nts), CVC4ApiException);
117
118
2
  d_solver.synthFun("f", {}, boolean, g1);
119
120
4
  ASSERT_THROW(g1.addAnyVariable(start), CVC4ApiException);
121
}
122
}  // namespace test
123
15
}  // namespace CVC4