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_delete(d_tm);
39 : 7 : }
40 : : Cvc5TermManager* d_tm;
41 : : Cvc5* d_solver;
42 : : Cvc5Sort d_bool;
43 : : Cvc5Sort d_real;
44 : : Cvc5Sort d_uninterpreted;
45 : : };
46 : :
47 : 4 : TEST_F(TestCApiBlackResult, is_null)
48 : : {
49 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_result_is_null(nullptr), "invalid result");
[ - + ][ + - ]
[ + - ][ + - ]
50 : 1 : Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x");
51 : 1 : std::vector<Cvc5Term> args = {x, x};
52 : 1 : cvc5_assert_formula(
53 : 1 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data()));
54 : 1 : Cvc5Result res = cvc5_check_sat(d_solver);
55 [ - + ][ + - ]: 1 : ASSERT_FALSE(cvc5_result_is_null(res));
56 : : }
57 : :
58 : 4 : TEST_F(TestCApiBlackResult, is_equal_disequal)
59 : : {
60 : 1 : cvc5_set_option(d_solver, "incremental", "true");
61 : 1 : Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x");
62 : 1 : std::vector<Cvc5Term> args = {x, x};
63 : 1 : cvc5_assert_formula(
64 : 1 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data()));
65 : 1 : Cvc5Result res1 = cvc5_check_sat(d_solver);
66 : 1 : cvc5_assert_formula(
67 : : d_solver,
68 : 1 : cvc5_mk_term(d_tm, CVC5_KIND_DISTINCT, args.size(), args.data()));
69 : 1 : Cvc5Result res2 = cvc5_check_sat(d_solver);
70 [ - + ][ + - ]: 1 : ASSERT_TRUE(cvc5_result_is_equal(res1, res1));
71 [ - + ][ + - ]: 1 : ASSERT_FALSE(cvc5_result_is_equal(res1, res2));
72 [ - + ][ + - ]: 1 : ASSERT_FALSE(cvc5_result_is_equal(res1, nullptr));
73 [ - + ][ + - ]: 1 : ASSERT_FALSE(cvc5_result_is_equal(nullptr, res1));
74 [ - + ][ + - ]: 1 : ASSERT_FALSE(cvc5_result_is_disequal(res1, res1));
75 [ - + ][ + - ]: 1 : ASSERT_TRUE(cvc5_result_is_disequal(res1, res2));
76 [ - + ][ + - ]: 1 : ASSERT_TRUE(cvc5_result_is_disequal(res1, nullptr));
77 [ - + ][ + - ]: 1 : ASSERT_TRUE(cvc5_result_is_disequal(nullptr, res1));
78 [ + - ]: 1 : }
79 : :
80 : 4 : TEST_F(TestCApiBlackResult, is_sat)
81 : : {
82 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_result_is_sat(nullptr), "invalid result");
[ - + ][ + - ]
[ + - ][ + - ]
83 : :
84 : 1 : Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x");
85 : 1 : std::vector<Cvc5Term> args = {x, x};
86 : 1 : cvc5_assert_formula(
87 : 1 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data()));
88 : 1 : Cvc5Result res = cvc5_check_sat(d_solver);
89 [ - + ][ + - ]: 1 : ASSERT_TRUE(cvc5_result_is_sat(res));
90 [ - + ][ + - ]: 1 : ASSERT_FALSE(cvc5_result_is_unsat(res));
91 [ - + ][ + - ]: 1 : ASSERT_FALSE(cvc5_result_is_unknown(res));
92 : : }
93 : :
94 : 4 : TEST_F(TestCApiBlackResult, is_unsat)
95 : : {
96 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_result_is_unsat(nullptr), "invalid result");
[ - + ][ + - ]
[ + - ][ + - ]
97 : :
98 : 1 : Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x");
99 : 1 : std::vector<Cvc5Term> args = {x, x};
100 : 1 : cvc5_assert_formula(
101 : : d_solver,
102 : 1 : cvc5_mk_term(d_tm, CVC5_KIND_DISTINCT, args.size(), args.data()));
103 : 1 : Cvc5Result res = cvc5_check_sat(d_solver);
104 [ - + ][ + - ]: 1 : ASSERT_FALSE(cvc5_result_is_sat(res));
105 [ - + ][ + - ]: 1 : ASSERT_TRUE(cvc5_result_is_unsat(res));
106 [ - + ][ + - ]: 1 : ASSERT_FALSE(cvc5_result_is_unknown(res));
107 : : }
108 : :
109 : 4 : TEST_F(TestCApiBlackResult, is_unknown)
110 : : {
111 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_result_is_unknown(nullptr), "invalid result");
[ - + ][ + - ]
[ + - ][ + - ]
112 : :
113 : 1 : cvc5_set_logic(d_solver, "QF_NIA");
114 : 1 : cvc5_set_option(d_solver, "incremental", "false");
115 : 1 : cvc5_set_option(d_solver, "solve-real-as-int", "true");
116 : 1 : Cvc5Term x = cvc5_mk_const(d_tm, d_real, "x");
117 : 1 : std::vector<Cvc5Term> args = {cvc5_mk_real(d_tm, "0.0"), x};
118 : 1 : cvc5_assert_formula(
119 : 1 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_LT, args.size(), args.data()));
120 : 1 : args = {x, cvc5_mk_real(d_tm, "1.0")};
121 : 1 : cvc5_assert_formula(
122 : 1 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_LT, args.size(), args.data()));
123 : 1 : Cvc5Result res = cvc5_check_sat(d_solver);
124 [ - + ][ + - ]: 1 : ASSERT_FALSE(cvc5_result_is_sat(res));
125 [ - + ][ + - ]: 1 : ASSERT_FALSE(cvc5_result_is_unsat(res));
126 [ - + ][ + - ]: 1 : ASSERT_TRUE(cvc5_result_is_unknown(res));
127 : 1 : Cvc5UnknownExplanation ue = cvc5_result_get_unknown_explanation(res);
128 [ - + ][ + - ]: 1 : ASSERT_EQ(ue, CVC5_UNKNOWN_EXPLANATION_INCOMPLETE);
129 [ - + ][ + - ]: 1 : ASSERT_EQ(cvc5_unknown_explanation_to_string(ue), std::string("INCOMPLETE"));
130 : : }
131 : :
132 : 4 : TEST_F(TestCApiBlackResult, hash)
133 : : {
134 : 1 : cvc5_set_option(d_solver, "incremental", "true");
135 : 1 : Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x");
136 : 1 : std::vector<Cvc5Term> args = {x, x};
137 : 1 : cvc5_assert_formula(
138 : 1 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data()));
139 : 1 : Cvc5Result res1 = cvc5_check_sat(d_solver);
140 : 1 : cvc5_assert_formula(
141 : : d_solver,
142 : 1 : cvc5_mk_term(d_tm, CVC5_KIND_DISTINCT, args.size(), args.data()));
143 : 1 : Cvc5Result res2 = cvc5_check_sat(d_solver);
144 [ - + ][ + - ]: 1 : ASSERT_EQ(cvc5_result_hash(res1), cvc5_result_hash(res1));
145 [ - + ][ + - ]: 1 : ASSERT_NE(cvc5_result_hash(res1), cvc5_result_hash(res2));
146 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_result_hash(nullptr), "invalid result");
[ - + ][ + - ]
[ + - ][ + - ]
147 [ + - ]: 1 : }
148 : :
149 : 4 : TEST_F(TestCApiBlackResult, copy_release)
150 : : {
151 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_result_copy(nullptr), "invalid result");
[ - + ][ + - ]
[ + - ][ + - ]
152 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_result_release(nullptr), "invalid result");
[ - + ][ + - ]
[ + - ][ + - ]
153 : 1 : Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x");
154 : 1 : std::vector<Cvc5Term> args = {x, x};
155 : 1 : cvc5_assert_formula(
156 : 1 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data()));
157 : 1 : Cvc5Result res1 = cvc5_check_sat(d_solver);
158 : 1 : Cvc5Result res2 = cvc5_result_copy(res1);
159 [ - + ][ + - ]: 1 : ASSERT_EQ(cvc5_result_hash(res1), cvc5_result_hash(res2));
160 : 1 : cvc5_result_release(res1);
161 [ - + ][ + - ]: 1 : ASSERT_EQ(cvc5_result_hash(res1), cvc5_result_hash(res2));
162 : 1 : cvc5_result_release(res1);
163 : : // we cannot reliably check that querying on the (now freed) result fails
164 : : // unless ASAN is enabled
165 : : }
166 : :
167 : : } // namespace cvc5::internal::test
|
