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 : : * White box testing of cvc5::prop::cadical::CadicalPropagator, in particular
11 : : * the user level assigned to clauses added during search.
12 : : */
13 : :
14 : : #include <cadical/cadical.hpp>
15 : :
16 : : #include "context/context.h"
17 : : #include "prop/cadical/cdclt_propagator.h"
18 : : #include "prop/cadical/util.h"
19 : : #include "prop/sat_solver_types.h"
20 : : #include "test.h"
21 : : #include "util/statistics_registry.h"
22 : :
23 : : namespace cvc5::internal {
24 : :
25 : : using namespace prop;
26 : : using namespace prop::cadical;
27 : :
28 : : namespace test {
29 : :
30 : : class TestPropWhiteCadicalPropagator : public TestInternal
31 : : {
32 : : protected:
33 : 7 : void SetUp() override
34 : : {
35 : 7 : d_stats.reset(new StatisticsRegistry());
36 : 7 : d_context.reset(new context::Context());
37 : 7 : d_solver.reset(new CaDiCaL::Solver());
38 : 7 : d_prop.reset(
39 : 7 : new CadicalPropagator(nullptr, d_context.get(), *d_solver, *d_stats));
40 : : // Observed variables require a connected external propagator.
41 : 7 : d_solver->connect_external_propagator(d_prop.get());
42 : :
43 : : // Build three user levels. This mirrors CadicalSolver::push(), which
44 : : // creates the activation literal *after* incrementing the user level, so
45 : : // the activation literal's introduction level is the new user level.
46 : : //
47 : : // level 0: variables 1, 2
48 : : // level 1: activation literal 3, variable 4
49 : : // level 2: activation literal 5, variable 6
50 : 7 : d_prop->add_new_var(1, true);
51 : 7 : d_prop->add_new_var(2, true);
52 : :
53 : 7 : d_prop->user_push();
54 : 7 : d_prop->add_new_var(3, false);
55 : 7 : d_prop->set_activation_lit(3);
56 : 7 : d_prop->add_new_var(4, true);
57 : :
58 : 7 : d_prop->user_push();
59 : 7 : d_prop->add_new_var(5, false);
60 : 7 : d_prop->set_activation_lit(5);
61 : 7 : d_prop->add_new_var(6, true);
62 : 7 : }
63 : :
64 : 7 : void TearDown() override
65 : : {
66 : 7 : d_solver->disconnect_external_propagator();
67 : 7 : d_prop.reset(nullptr);
68 : 7 : d_solver.reset(nullptr);
69 : 7 : d_context.reset(nullptr);
70 : 7 : d_stats.reset(nullptr);
71 : 7 : }
72 : :
73 : : /**
74 : : * Drain the next clause buffered by add_clause() (during search) via the
75 : : * external-clause callbacks and return its CaDiCaL literals (without the
76 : : * terminating 0).
77 : : */
78 : 3 : std::vector<int> nextClause()
79 : : {
80 : 3 : std::vector<int> clause;
81 : 3 : bool forgettable = true;
82 [ - + ]: 3 : EXPECT_TRUE(d_prop->cb_has_external_clause(forgettable));
83 [ + + ]: 10 : for (int lit = d_prop->cb_add_external_clause_lit(); lit != 0;
84 : 7 : lit = d_prop->cb_add_external_clause_lit())
85 : : {
86 : 7 : clause.push_back(lit);
87 : : }
88 : 6 : return clause;
89 : 0 : }
90 : :
91 : : std::unique_ptr<StatisticsRegistry> d_stats;
92 : : std::unique_ptr<context::Context> d_context;
93 : : std::unique_ptr<CaDiCaL::Solver> d_solver;
94 : : std::unique_ptr<CadicalPropagator> d_prop;
95 : : };
96 : :
97 : 4 : TEST_F(TestPropWhiteCadicalPropagator, activation_lit_indexing)
98 : : {
99 [ - + ][ + - ]: 1 : ASSERT_EQ(d_prop->current_user_level(), 2u);
100 : : // Level 0 (base level) has no activation literal.
101 [ - + ][ + - ]: 1 : ASSERT_EQ(d_prop->activation_lit(0), undefSatLiteral);
102 [ - + ][ + - ]: 1 : ASSERT_EQ(d_prop->activation_lit(1), SatLiteral(3));
103 [ - + ][ + - ]: 1 : ASSERT_EQ(d_prop->activation_lit(2), SatLiteral(5));
104 [ - + ][ + - ]: 1 : ASSERT_EQ(d_prop->current_activation_lit(), SatLiteral(5));
105 : : }
106 : :
107 : 4 : TEST_F(TestPropWhiteCadicalPropagator, learned_clause_uses_max_intro_level)
108 : : {
109 : : // A clause learned during search whose highest-level literal was introduced
110 : : // at user level 1 must be guarded by level 1's activation literal (3), not
111 : : // the current level's (5), so it survives popping level 2.
112 : 1 : d_prop->in_search(true);
113 : 1 : SatClause clause{SatLiteral(4)}; // variable 4 was introduced at level 1
114 : 1 : d_prop->add_clause(clause);
115 [ - + ]: 2 : EXPECT_EQ(nextClause(),
116 : : (std::vector<int>{toCadicalLit(SatLiteral(3)),
117 : 1 : toCadicalLit(SatLiteral(4))}));
118 : 1 : }
119 : :
120 : 4 : TEST_F(TestPropWhiteCadicalPropagator, learned_clause_takes_max_over_literals)
121 : : {
122 : : // max over several literals: {1 (level 0), 4 (level 1)} -> level 1 -> 3.
123 : 1 : d_prop->in_search(true);
124 : 1 : SatClause clause{SatLiteral(1), SatLiteral(4)};
125 : 1 : d_prop->add_clause(clause);
126 [ - + ]: 2 : EXPECT_EQ(nextClause(),
127 : : (std::vector<int>{toCadicalLit(SatLiteral(3)),
128 : : toCadicalLit(SatLiteral(1)),
129 : 1 : toCadicalLit(SatLiteral(4))}));
130 : 1 : }
131 : :
132 : 4 : TEST_F(TestPropWhiteCadicalPropagator, learned_clause_over_base_level)
133 : : {
134 : : // A clause over only base-level (level 0) literals is globally valid and
135 : : // must not get any activation literal, even at user level 2.
136 : 1 : d_prop->in_search(true);
137 : 1 : SatClause clause{SatLiteral(1), SatLiteral(2)};
138 : 1 : d_prop->add_clause(clause);
139 [ - + ]: 2 : EXPECT_EQ(nextClause(),
140 : : (std::vector<int>{toCadicalLit(SatLiteral(1)),
141 : 1 : toCadicalLit(SatLiteral(2))}));
142 : 1 : }
143 : :
144 : 4 : TEST_F(TestPropWhiteCadicalPropagator, input_clause_uses_current_level)
145 : : {
146 : : // Outside search, the clause is guarded by the current user level's
147 : : // activation literal, even if all its literals were introduced at a lower
148 : : // level (the conservative, pre-existing behavior).
149 [ - + ][ + - ]: 1 : ASSERT_FALSE(d_prop->in_search());
150 [ - + ]: 1 : ASSERT_EQ(d_prop->activation_lit(d_prop->current_user_level()),
151 [ + - ]: 1 : d_prop->current_activation_lit());
152 : : }
153 : :
154 : : // The following tests cover the reason path (cb_add_reason_clause_lit()), which
155 : : // guards the reason with activation_lit(clause_user_level(reason)). We exercise
156 : : // that computation directly rather than driving the callback, since the
157 : : // callback obtains the reason via TheoryProxy::explainPropagation() and setting
158 : : // up a TheoryProxy requires a full theory engine. explainPropagation() returns
159 : : // the propagated literal followed by the negated antecedents, so the reason's
160 : : // user level is the max introduction level over all of them.
161 : :
162 : 4 : TEST_F(TestPropWhiteCadicalPropagator, reason_clause_user_level)
163 : : {
164 : : // Propagated literal at level 1 with a base-level antecedent: max -> level 1.
165 : 1 : SatClause level1{SatLiteral(4), SatLiteral(1)};
166 [ - + ]: 1 : EXPECT_EQ(d_prop->clause_user_level(level1), 1u);
167 : :
168 : : // Highest literal at level 2 dominates: max -> level 2.
169 : 2 : SatClause level2{SatLiteral(1), SatLiteral(4), SatLiteral(6)};
170 [ - + ]: 1 : EXPECT_EQ(d_prop->clause_user_level(level2), 2u);
171 : :
172 : : // Reason derived purely from base-level facts: level 0.
173 : 2 : SatClause base{SatLiteral(1), SatLiteral(2)};
174 [ - + ]: 1 : EXPECT_EQ(d_prop->clause_user_level(base), 0u);
175 : 1 : }
176 : :
177 : 4 : TEST_F(TestPropWhiteCadicalPropagator, reason_clause_guard)
178 : : {
179 : : // The activation literal cb_add_reason_clause_lit() prepends to the reason is
180 : : // activation_lit(clause_user_level(reason)).
181 : :
182 : : // A reason depending on level 1 is guarded by level 1's activation literal
183 : : // (3), not the current level's (5), so it survives popping level 2.
184 : 1 : SatClause level1{SatLiteral(4), SatLiteral(1)};
185 [ - + ]: 1 : EXPECT_EQ(d_prop->activation_lit(d_prop->clause_user_level(level1)),
186 : 1 : SatLiteral(3));
187 : :
188 : : // A reason depending on level 2 is guarded by level 2's activation literal.
189 : 2 : SatClause level2{SatLiteral(6), SatLiteral(4)};
190 [ - + ]: 1 : EXPECT_EQ(d_prop->activation_lit(d_prop->clause_user_level(level2)),
191 : 1 : SatLiteral(5));
192 : :
193 : : // A reason over only base-level literals is globally valid and gets no
194 : : // activation literal guard.
195 : 2 : SatClause base{SatLiteral(1), SatLiteral(2)};
196 [ - + ]: 1 : EXPECT_EQ(d_prop->activation_lit(d_prop->clause_user_level(base)),
197 : 1 : undefSatLiteral);
198 : 1 : }
199 : :
200 : : } // namespace test
201 : : } // namespace cvc5::internal
|
