Branch data Line data Source code
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-2024 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 result functions of the C API.
14 : : */
15 : :
16 : : extern "C" {
17 : : #include <cvc5/c/cvc5.h>
18 : : }
19 : :
20 : : #include "base/check.h"
21 : : #include "base/output.h"
22 : : #include "gtest/gtest.h"
23 : :
24 : : namespace cvc5::internal::test {
25 : :
26 : : class TestCApiBlackResult : public ::testing::Test
27 : : {
28 : : protected:
29 : 40 : void SetUp() override
30 : : {
31 : 40 : d_tm = cvc5_term_manager_new();
32 : 40 : d_solver = cvc5_new(d_tm);
33 : 40 : d_bool = cvc5_get_boolean_sort(d_tm);
34 : 40 : d_real = cvc5_get_real_sort(d_tm);
35 : 40 : d_uninterpreted = cvc5_mk_uninterpreted_sort(d_tm, "u");
36 : 40 : }
37 : 33 : void TearDown() override
38 : : {
39 : 33 : cvc5_delete(d_solver);
40 : 33 : cvc5_term_manager_delete(d_tm);
41 : 33 : }
42 : : Cvc5TermManager* d_tm;
43 : : Cvc5* d_solver;
44 : : Cvc5Sort d_bool;
45 : : Cvc5Sort d_real;
46 : : Cvc5Sort d_uninterpreted;
47 : : };
48 : :
49 : 16 : TEST_F(TestCApiBlackResult, is_null)
50 : : {
51 : 8 : ASSERT_DEATH(cvc5_result_is_null(nullptr), "invalid result");
52 : 7 : Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x");
53 : 7 : std::vector<Cvc5Term> args = {x, x};
54 : 7 : cvc5_assert_formula(
55 : 7 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data()));
56 : 7 : Cvc5Result res = cvc5_check_sat(d_solver);
57 [ - + ]: 7 : ASSERT_FALSE(cvc5_result_is_null(res));
58 : : }
59 : :
60 : 14 : TEST_F(TestCApiBlackResult, is_equal_disequal)
61 : : {
62 : 7 : cvc5_set_option(d_solver, "incremental", "true");
63 : 7 : Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x");
64 : 7 : std::vector<Cvc5Term> args = {x, x};
65 : 7 : cvc5_assert_formula(
66 : 7 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data()));
67 : 7 : Cvc5Result res1 = cvc5_check_sat(d_solver);
68 : 7 : cvc5_assert_formula(
69 : : d_solver,
70 : 7 : cvc5_mk_term(d_tm, CVC5_KIND_DISTINCT, args.size(), args.data()));
71 : 7 : Cvc5Result res2 = cvc5_check_sat(d_solver);
72 [ - + ]: 7 : ASSERT_TRUE(cvc5_result_is_equal(res1, res1));
73 [ - + ]: 7 : ASSERT_FALSE(cvc5_result_is_equal(res1, res2));
74 [ - + ]: 7 : ASSERT_FALSE(cvc5_result_is_equal(res1, nullptr));
75 [ - + ]: 7 : ASSERT_FALSE(cvc5_result_is_equal(nullptr, res1));
76 [ - + ]: 7 : ASSERT_FALSE(cvc5_result_is_disequal(res1, res1));
77 [ - + ]: 7 : ASSERT_TRUE(cvc5_result_is_disequal(res1, res2));
78 [ - + ]: 7 : ASSERT_TRUE(cvc5_result_is_disequal(res1, nullptr));
79 [ - + ]: 7 : ASSERT_TRUE(cvc5_result_is_disequal(nullptr, res1));
80 : : }
81 : :
82 : 14 : TEST_F(TestCApiBlackResult, is_sat)
83 : : {
84 : 7 : ASSERT_DEATH(cvc5_result_is_sat(nullptr), "invalid result");
85 : :
86 : 6 : Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x");
87 : 6 : std::vector<Cvc5Term> args = {x, x};
88 : 6 : cvc5_assert_formula(
89 : 6 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data()));
90 : 6 : Cvc5Result res = cvc5_check_sat(d_solver);
91 [ - + ]: 6 : ASSERT_TRUE(cvc5_result_is_sat(res));
92 [ - + ]: 6 : ASSERT_FALSE(cvc5_result_is_unsat(res));
93 [ - + ]: 6 : ASSERT_FALSE(cvc5_result_is_unknown(res));
94 : : }
95 : :
96 : 12 : TEST_F(TestCApiBlackResult, is_unsat)
97 : : {
98 : 6 : ASSERT_DEATH(cvc5_result_is_unsat(nullptr), "invalid result");
99 : :
100 : 5 : Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x");
101 : 5 : std::vector<Cvc5Term> args = {x, x};
102 : 5 : cvc5_assert_formula(
103 : : d_solver,
104 : 5 : cvc5_mk_term(d_tm, CVC5_KIND_DISTINCT, args.size(), args.data()));
105 : 5 : Cvc5Result res = cvc5_check_sat(d_solver);
106 [ - + ]: 5 : ASSERT_FALSE(cvc5_result_is_sat(res));
107 [ - + ]: 5 : ASSERT_TRUE(cvc5_result_is_unsat(res));
108 [ - + ]: 5 : ASSERT_FALSE(cvc5_result_is_unknown(res));
109 : : }
110 : :
111 : 10 : TEST_F(TestCApiBlackResult, is_unknown)
112 : : {
113 : 5 : ASSERT_DEATH(cvc5_result_is_unknown(nullptr), "invalid result");
114 : :
115 : 4 : cvc5_set_logic(d_solver, "QF_NIA");
116 : 4 : cvc5_set_option(d_solver, "incremental", "false");
117 : 4 : cvc5_set_option(d_solver, "solve-real-as-int", "true");
118 : 4 : Cvc5Term x = cvc5_mk_const(d_tm, d_real, "x");
119 : 4 : std::vector<Cvc5Term> args = {cvc5_mk_real(d_tm, "0.0"), x};
120 : 4 : cvc5_assert_formula(
121 : 4 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_LT, args.size(), args.data()));
122 : 4 : args = {x, cvc5_mk_real(d_tm, "1.0")};
123 : 4 : cvc5_assert_formula(
124 : 4 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_LT, args.size(), args.data()));
125 : 4 : Cvc5Result res = cvc5_check_sat(d_solver);
126 [ - + ]: 4 : ASSERT_FALSE(cvc5_result_is_sat(res));
127 [ - + ]: 4 : ASSERT_FALSE(cvc5_result_is_unsat(res));
128 [ - + ]: 4 : ASSERT_TRUE(cvc5_result_is_unknown(res));
129 : 4 : Cvc5UnknownExplanation ue = cvc5_result_get_unknown_explanation(res);
130 [ - + ]: 4 : ASSERT_EQ(ue, CVC5_UNKNOWN_EXPLANATION_INCOMPLETE);
131 [ - + ]: 4 : ASSERT_EQ(cvc5_unknown_explanation_to_string(ue),
132 : : std::string("INCOMPLETE"));
133 : : }
134 : :
135 : 8 : TEST_F(TestCApiBlackResult, hash)
136 : : {
137 : 4 : cvc5_set_option(d_solver, "incremental", "true");
138 : 4 : Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x");
139 : 4 : std::vector<Cvc5Term> args = {x, x};
140 : 4 : cvc5_assert_formula(
141 : 4 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data()));
142 : 4 : Cvc5Result res1 = cvc5_check_sat(d_solver);
143 : 4 : cvc5_assert_formula(
144 : : d_solver,
145 : 4 : cvc5_mk_term(d_tm, CVC5_KIND_DISTINCT, args.size(), args.data()));
146 : 4 : Cvc5Result res2 = cvc5_check_sat(d_solver);
147 [ - + ]: 4 : ASSERT_EQ(cvc5_result_hash(res1), cvc5_result_hash(res1));
148 [ - + ]: 4 : ASSERT_NE(cvc5_result_hash(res1), cvc5_result_hash(res2));
149 : 4 : ASSERT_DEATH(cvc5_result_hash(nullptr), "invalid result");
150 : : }
151 : :
152 : 6 : TEST_F(TestCApiBlackResult, copy_release)
153 : : {
154 : 3 : ASSERT_DEATH(cvc5_result_copy(nullptr), "invalid result");
155 : 2 : ASSERT_DEATH(cvc5_result_release(nullptr), "invalid result");
156 : 1 : Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x");
157 : 1 : std::vector<Cvc5Term> args = {x, x};
158 : 1 : cvc5_assert_formula(
159 : 1 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data()));
160 : 1 : Cvc5Result res1 = cvc5_check_sat(d_solver);
161 : 1 : Cvc5Result res2 = cvc5_result_copy(res1);
162 [ - + ]: 1 : ASSERT_EQ(cvc5_result_hash(res1), cvc5_result_hash(res2));
163 : 1 : cvc5_result_release(res1);
164 [ - + ]: 1 : ASSERT_EQ(cvc5_result_hash(res1), cvc5_result_hash(res2));
165 : 1 : cvc5_result_release(res1);
166 : : // we cannot reliably check that querying on the (now freed) result fails
167 : : // unless ASAN is enabled
168 : : }
169 : :
170 : : } // namespace cvc5::internal::test
|
