GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/api/result_black.cpp Lines: 75 75 100.0 %
Date: 2021-03-23 Branches: 198 580 34.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file result_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 Result class
13
 **/
14
15
#include "test_api.h"
16
17
namespace CVC4 {
18
19
using namespace api;
20
21
namespace test {
22
23
28
class TestApiBlackResult : public TestApi
24
{
25
};
26
27
16
TEST_F(TestApiBlackResult, isNull)
28
{
29
4
  CVC4::api::Result res_null;
30
2
  ASSERT_TRUE(res_null.isNull());
31
2
  ASSERT_FALSE(res_null.isSat());
32
2
  ASSERT_FALSE(res_null.isUnsat());
33
2
  ASSERT_FALSE(res_null.isSatUnknown());
34
2
  ASSERT_FALSE(res_null.isEntailed());
35
2
  ASSERT_FALSE(res_null.isNotEntailed());
36
2
  ASSERT_FALSE(res_null.isEntailmentUnknown());
37
4
  Sort u_sort = d_solver.mkUninterpretedSort("u");
38
4
  Term x = d_solver.mkVar(u_sort, "x");
39
2
  d_solver.assertFormula(x.eqTerm(x));
40
4
  CVC4::api::Result res = d_solver.checkSat();
41
2
  ASSERT_FALSE(res.isNull());
42
}
43
44
16
TEST_F(TestApiBlackResult, eq)
45
{
46
4
  Sort u_sort = d_solver.mkUninterpretedSort("u");
47
4
  Term x = d_solver.mkVar(u_sort, "x");
48
2
  d_solver.assertFormula(x.eqTerm(x));
49
4
  CVC4::api::Result res;
50
4
  CVC4::api::Result res2 = d_solver.checkSat();
51
4
  CVC4::api::Result res3 = d_solver.checkSat();
52
2
  res = res2;
53
2
  ASSERT_EQ(res, res2);
54
2
  ASSERT_EQ(res3, res2);
55
}
56
57
16
TEST_F(TestApiBlackResult, isSat)
58
{
59
4
  Sort u_sort = d_solver.mkUninterpretedSort("u");
60
4
  Term x = d_solver.mkVar(u_sort, "x");
61
2
  d_solver.assertFormula(x.eqTerm(x));
62
4
  CVC4::api::Result res = d_solver.checkSat();
63
2
  ASSERT_TRUE(res.isSat());
64
2
  ASSERT_FALSE(res.isSatUnknown());
65
}
66
67
16
TEST_F(TestApiBlackResult, isUnsat)
68
{
69
4
  Sort u_sort = d_solver.mkUninterpretedSort("u");
70
4
  Term x = d_solver.mkVar(u_sort, "x");
71
2
  d_solver.assertFormula(x.eqTerm(x).notTerm());
72
4
  CVC4::api::Result res = d_solver.checkSat();
73
2
  ASSERT_TRUE(res.isUnsat());
74
2
  ASSERT_FALSE(res.isSatUnknown());
75
}
76
77
16
TEST_F(TestApiBlackResult, isSatUnknown)
78
{
79
2
  d_solver.setLogic("QF_NIA");
80
2
  d_solver.setOption("incremental", "false");
81
2
  d_solver.setOption("solve-int-as-bv", "32");
82
4
  Sort int_sort = d_solver.getIntegerSort();
83
4
  Term x = d_solver.mkVar(int_sort, "x");
84
2
  d_solver.assertFormula(x.eqTerm(x).notTerm());
85
4
  CVC4::api::Result res = d_solver.checkSat();
86
2
  ASSERT_FALSE(res.isSat());
87
2
  ASSERT_TRUE(res.isSatUnknown());
88
}
89
90
16
TEST_F(TestApiBlackResult, isEntailed)
91
{
92
2
  d_solver.setOption("incremental", "true");
93
4
  Sort u_sort = d_solver.mkUninterpretedSort("u");
94
4
  Term x = d_solver.mkConst(u_sort, "x");
95
4
  Term y = d_solver.mkConst(u_sort, "y");
96
4
  Term a = x.eqTerm(y).notTerm();
97
4
  Term b = x.eqTerm(y);
98
2
  d_solver.assertFormula(a);
99
4
  CVC4::api::Result entailed = d_solver.checkEntailed(a);
100
2
  ASSERT_TRUE(entailed.isEntailed());
101
2
  ASSERT_FALSE(entailed.isEntailmentUnknown());
102
4
  CVC4::api::Result not_entailed = d_solver.checkEntailed(b);
103
2
  ASSERT_TRUE(not_entailed.isNotEntailed());
104
2
  ASSERT_FALSE(not_entailed.isEntailmentUnknown());
105
}
106
107
16
TEST_F(TestApiBlackResult, isEntailmentUnknown)
108
{
109
2
  d_solver.setLogic("QF_NIA");
110
2
  d_solver.setOption("incremental", "false");
111
2
  d_solver.setOption("solve-int-as-bv", "32");
112
4
  Sort int_sort = d_solver.getIntegerSort();
113
4
  Term x = d_solver.mkVar(int_sort, "x");
114
2
  d_solver.assertFormula(x.eqTerm(x).notTerm());
115
4
  CVC4::api::Result res = d_solver.checkEntailed(x.eqTerm(x));
116
2
  ASSERT_FALSE(res.isEntailed());
117
2
  ASSERT_TRUE(res.isEntailmentUnknown());
118
2
  ASSERT_EQ(res.getUnknownExplanation(), api::Result::UNKNOWN_REASON);
119
}
120
}  // namespace test
121
24
}  // namespace CVC4