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