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