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