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 : : * Implementation of the inference manager for the theory of sets.
11 : : */
12 : :
13 : : #include "theory/sets/inference_manager.h"
14 : :
15 : : #include "options/sets_options.h"
16 : : #include "proof/trust_id.h"
17 : : #include "theory/builtin/proof_checker.h"
18 : : #include "theory/rewriter.h"
19 : :
20 : : using namespace std;
21 : : using namespace cvc5::internal::kind;
22 : :
23 : : namespace cvc5::internal {
24 : : namespace theory {
25 : : namespace sets {
26 : :
27 : 27723 : InferenceManager::InferenceManager(Env& env,
28 : : Theory& t,
29 : : TheorySetsRewriter* tr,
30 : 27723 : SolverState& s)
31 : : : InferenceManagerBuffered(env, t, s, "theory::sets::"),
32 : 27723 : d_state(s),
33 [ + + ]: 27723 : d_ipc(isProofEnabled() ? new InferProofCons(env, tr) : nullptr)
34 : : {
35 : 27723 : d_true = nodeManager()->mkConst(true);
36 : 27723 : d_false = nodeManager()->mkConst(false);
37 : 27723 : }
38 : :
39 : 239813 : bool InferenceManager::assertFactRec(Node fact,
40 : : InferenceId id,
41 : : Node exp,
42 : : int inferType)
43 : : {
44 : : // should we send this fact out as a lemma?
45 [ + - ]: 239813 : if (inferType != -1)
46 : : {
47 [ + + ]: 239813 : if (d_state.isEntailed(fact, true))
48 : : {
49 : 197729 : return false;
50 : : }
51 : 42084 : setupAndAddPendingLemma(exp, fact, id);
52 : 42084 : return true;
53 : : }
54 [ - - ]: 0 : Trace("sets-fact") << "Assert fact rec : " << fact << ", exp = " << exp
55 : 0 : << std::endl;
56 [ - - ]: 0 : if (fact.isConst())
57 : : {
58 : : // either trivial or a conflict
59 [ - - ]: 0 : if (fact == d_false)
60 : : {
61 [ - - ]: 0 : Trace("sets-lemma") << "Conflict : " << exp << std::endl;
62 : 0 : setupAndAddPendingLemma(exp, fact, id);
63 : 0 : return true;
64 : : }
65 : 0 : return false;
66 : : }
67 : 0 : else if (fact.getKind() == Kind::AND
68 : 0 : || (fact.getKind() == Kind::NOT && fact[0].getKind() == Kind::OR))
69 : : {
70 : 0 : bool ret = false;
71 [ - - ]: 0 : Node f = fact.getKind() == Kind::NOT ? fact[0] : fact;
72 [ - - ]: 0 : for (unsigned i = 0; i < f.getNumChildren(); i++)
73 : : {
74 : 0 : Node factc = fact.getKind() == Kind::NOT ? f[i].negate() : f[i];
75 : 0 : bool tret = assertFactRec(factc, id, exp, inferType);
76 [ - - ][ - - ]: 0 : ret = ret || tret;
77 [ - - ]: 0 : if (d_state.isInConflict())
78 : : {
79 : 0 : return true;
80 : : }
81 [ - - ]: 0 : }
82 : 0 : return ret;
83 : 0 : }
84 : 0 : bool polarity = fact.getKind() != Kind::NOT;
85 [ - - ]: 0 : TNode atom = polarity ? fact : fact[0];
86 [ - - ]: 0 : if (d_state.isEntailed(atom, polarity))
87 : : {
88 : 0 : return false;
89 : : }
90 : : // things we can assert to equality engine
91 : 0 : if (atom.getKind() == Kind::SET_MEMBER
92 : 0 : || (atom.getKind() == Kind::EQUAL && atom[0].getType().isSet()))
93 : : {
94 : : // send to equality engine
95 [ - - ]: 0 : if (assertSetsFact(atom, polarity, id, exp))
96 : : {
97 : : // return true if this wasn't redundant
98 : 0 : return true;
99 : : }
100 : : }
101 : : else
102 : : {
103 : : // must send as lemma
104 : 0 : setupAndAddPendingLemma(exp, fact, id);
105 : 0 : return true;
106 : : }
107 : 0 : return false;
108 : 0 : }
109 : :
110 : 762 : void InferenceManager::assertSetsConflict(const Node& conf, InferenceId id)
111 : : {
112 [ + + ]: 762 : if (d_ipc)
113 : : {
114 : 257 : d_ipc->notifyConflict(conf, id);
115 : : }
116 [ + + ]: 762 : TrustNode trn = TrustNode::mkTrustConflict(conf, d_ipc.get());
117 : 762 : trustedConflict(trn, id);
118 : 762 : }
119 : :
120 : 6980 : bool InferenceManager::assertSetsFact(Node atom,
121 : : bool polarity,
122 : : InferenceId id,
123 : : Node exp)
124 : : {
125 [ + - ]: 6980 : Node conc = polarity ? atom : atom.notNode();
126 : : // notify before asserting below, since that call may induce a conflict which
127 : : // needs immediate explanation.
128 [ + + ]: 6980 : if (d_ipc)
129 : : {
130 : 1683 : d_ipc->notifyFact(conc, exp, id);
131 : : }
132 : 20940 : return assertInternalFact(atom, polarity, id, {exp}, d_ipc.get());
133 : 6980 : }
134 : :
135 : 239813 : void InferenceManager::assertInference(Node fact,
136 : : InferenceId id,
137 : : Node exp,
138 : : int inferType)
139 : : {
140 [ + + ]: 239813 : if (assertFactRec(fact, id, exp, inferType))
141 : : {
142 [ + - ]: 84168 : Trace("sets-lemma") << "Sets::Lemma : " << fact << " from " << exp << " by "
143 : 42084 : << id << std::endl;
144 [ + - ]: 84168 : Trace("sets-assertion") << "(assert (=> " << exp << " " << fact
145 : 42084 : << ")) ; by " << id << std::endl;
146 : : }
147 : 239813 : }
148 : :
149 : 208140 : void InferenceManager::assertInference(Node fact,
150 : : InferenceId id,
151 : : std::vector<Node>& exp,
152 : : int inferType)
153 : : {
154 : : Node exp_n =
155 : 208140 : exp.empty()
156 : 6063 : ? d_true
157 [ + + ][ + + ]: 208140 : : (exp.size() == 1 ? exp[0] : nodeManager()->mkNode(Kind::AND, exp));
158 : 208140 : assertInference(fact, id, exp_n, inferType);
159 : 208140 : }
160 : :
161 : 9928 : void InferenceManager::assertInference(std::vector<Node>& conc,
162 : : InferenceId id,
163 : : Node exp,
164 : : int inferType)
165 : : {
166 [ + + ]: 9928 : if (!conc.empty())
167 : : {
168 : : Node fact =
169 [ + + ]: 730 : conc.size() == 1 ? conc[0] : nodeManager()->mkNode(Kind::AND, conc);
170 : 730 : assertInference(fact, id, exp, inferType);
171 : 730 : }
172 : 9928 : }
173 : 0 : void InferenceManager::assertInference(std::vector<Node>& conc,
174 : : InferenceId id,
175 : : std::vector<Node>& exp,
176 : : int inferType)
177 : : {
178 : : Node exp_n =
179 : 0 : exp.empty()
180 : 0 : ? d_true
181 : 0 : : (exp.size() == 1 ? exp[0] : nodeManager()->mkNode(Kind::AND, exp));
182 : 0 : assertInference(conc, id, exp_n, inferType);
183 : 0 : }
184 : :
185 : 2772 : void InferenceManager::split(Node n, InferenceId id, int reqPol)
186 : : {
187 : 2772 : n = rewrite(n);
188 : 5544 : Node lem = nodeManager()->mkNode(Kind::OR, n, n.negate());
189 : : // send the lemma
190 : 2772 : lemma(lem, id);
191 [ + - ]: 2772 : Trace("sets-lemma") << "Sets::Lemma split : " << lem << std::endl;
192 [ + + ]: 2772 : if (reqPol != 0)
193 : : {
194 [ + - ]: 476 : Trace("sets-lemma") << "Sets::Require phase " << n << " " << (reqPol > 0)
195 : 238 : << std::endl;
196 : 238 : preferPhase(n, reqPol > 0);
197 : : }
198 : 2772 : }
199 : :
200 : 386 : void InferenceManager::sendAxiomLemma(const Node& lem, InferenceId id)
201 : : {
202 [ + - ]: 772 : Trace("sets-lemma") << "Sets::Lemma axiom : " << lem << " by " << id
203 : 386 : << std::endl;
204 [ + + ]: 386 : if (d_ipc)
205 : : {
206 : 122 : d_ipc->notifyLemma(lem, id);
207 : : }
208 [ + + ]: 386 : trustedLemma(TrustNode::mkTrustLemma(lem, d_ipc.get()), id);
209 : 386 : }
210 : :
211 : 42084 : void InferenceManager::setupAndAddPendingLemma(const Node& exp,
212 : : const Node& conc,
213 : : InferenceId id)
214 : : {
215 [ + + ]: 42084 : if (conc == d_false)
216 : : {
217 [ + + ]: 7 : if (d_ipc)
218 : : {
219 : 3 : d_ipc->notifyConflict(exp, id);
220 : : }
221 [ + + ]: 7 : TrustNode trn = TrustNode::mkTrustConflict(exp, d_ipc.get());
222 : 7 : trustedConflict(trn, id);
223 : 7 : return;
224 : 7 : }
225 : 42077 : Node lem = conc;
226 [ + + ]: 42077 : if (exp != d_true)
227 : : {
228 : 34485 : lem = nodeManager()->mkNode(Kind::IMPLIES, exp, conc);
229 : : }
230 [ + + ]: 42077 : if (d_ipc)
231 : : {
232 : 15352 : d_ipc->notifyLemma(lem, id);
233 : : }
234 [ + + ]: 42077 : addPendingLemma(lem, id, LemmaProperty::NONE, d_ipc.get());
235 : 42077 : }
236 : :
237 : : } // namespace sets
238 : : } // namespace theory
239 : : } // namespace cvc5::internal
|
