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 : 28738 : InferenceManager::InferenceManager(Env& env,
28 : : Theory& t,
29 : : TheorySetsRewriter* tr,
30 : 28738 : SolverState& s)
31 : : : InferenceManagerBuffered(env, t, s, "theory::sets::"),
32 : 28738 : d_state(s),
33 [ + + ]: 28738 : d_ipc(isProofEnabled() ? new InferProofCons(env, tr) : nullptr)
34 : : {
35 : 28738 : d_true = nodeManager()->mkConst(true);
36 : 28738 : d_false = nodeManager()->mkConst(false);
37 : 28738 : }
38 : :
39 : 249427 : 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 [ + - ]: 249427 : if (inferType != -1)
46 : : {
47 [ + + ]: 249427 : if (d_state.isEntailed(fact, true))
48 : : {
49 : 200247 : return false;
50 : : }
51 : 49180 : setupAndAddPendingLemma(exp, fact, id);
52 : 49180 : 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 : 745 : void InferenceManager::assertSetsConflict(const Node& conf, InferenceId id)
111 : : {
112 [ + + ]: 745 : if (d_ipc)
113 : : {
114 : 305 : d_ipc->notifyConflict(conf, id);
115 : : }
116 [ + + ]: 745 : TrustNode trn = TrustNode::mkTrustConflict(conf, d_ipc.get());
117 : 745 : trustedConflict(trn, id);
118 : 745 : }
119 : :
120 : 11991 : bool InferenceManager::assertSetsFact(Node atom,
121 : : bool polarity,
122 : : InferenceId id,
123 : : Node exp)
124 : : {
125 [ + - ]: 11991 : Node conc = polarity ? atom : atom.notNode();
126 : : // notify before asserting below, since that call may induce a conflict which
127 : : // needs immediate explanation.
128 [ + + ]: 11991 : if (d_ipc)
129 : : {
130 : 3598 : d_ipc->notifyFact(conc, exp, id);
131 : : }
132 : 35973 : return assertInternalFact(atom, polarity, id, {exp}, d_ipc.get());
133 : 11991 : }
134 : :
135 : 249427 : void InferenceManager::assertInference(Node fact,
136 : : InferenceId id,
137 : : Node exp,
138 : : int inferType)
139 : : {
140 [ + + ]: 249427 : if (assertFactRec(fact, id, exp, inferType))
141 : : {
142 [ + - ]: 98360 : Trace("sets-lemma") << "Sets::Lemma : " << fact << " from " << exp << " by "
143 : 49180 : << id << std::endl;
144 [ + - ]: 98360 : Trace("sets-assertion") << "(assert (=> " << exp << " " << fact
145 : 49180 : << ")) ; by " << id << std::endl;
146 : : }
147 : 249427 : }
148 : :
149 : 212919 : void InferenceManager::assertInference(Node fact,
150 : : InferenceId id,
151 : : std::vector<Node>& exp,
152 : : int inferType)
153 : : {
154 : : Node exp_n =
155 : 212919 : exp.empty()
156 : 6525 : ? d_true
157 [ + + ][ + + ]: 212919 : : (exp.size() == 1 ? exp[0] : nodeManager()->mkNode(Kind::AND, exp));
158 : 212919 : assertInference(fact, id, exp_n, inferType);
159 : 212919 : }
160 : :
161 : 10655 : void InferenceManager::assertInference(std::vector<Node>& conc,
162 : : InferenceId id,
163 : : Node exp,
164 : : int inferType)
165 : : {
166 [ + + ]: 10655 : if (!conc.empty())
167 : : {
168 : : Node fact =
169 [ + + ]: 756 : conc.size() == 1 ? conc[0] : nodeManager()->mkNode(Kind::AND, conc);
170 : 756 : assertInference(fact, id, exp, inferType);
171 : 756 : }
172 : 10655 : }
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 : 3077 : void InferenceManager::split(Node n, InferenceId id, int reqPol)
186 : : {
187 : 3077 : n = rewrite(n);
188 : 6154 : Node lem = nodeManager()->mkNode(Kind::OR, n, n.negate());
189 : : // send the lemma
190 : 3077 : lemma(lem, id);
191 [ + - ]: 3077 : Trace("sets-lemma") << "Sets::Lemma split : " << lem << std::endl;
192 [ + + ]: 3077 : if (reqPol != 0)
193 : : {
194 [ + - ]: 578 : Trace("sets-lemma") << "Sets::Require phase " << n << " " << (reqPol > 0)
195 : 289 : << std::endl;
196 : 289 : preferPhase(n, reqPol > 0);
197 : : }
198 : 3077 : }
199 : :
200 : 49180 : void InferenceManager::setupAndAddPendingLemma(const Node& exp,
201 : : const Node& conc,
202 : : InferenceId id)
203 : : {
204 [ + + ]: 49180 : if (conc == d_false)
205 : : {
206 [ + + ]: 8 : if (d_ipc)
207 : : {
208 : 4 : d_ipc->notifyConflict(exp, id);
209 : : }
210 [ + + ]: 8 : TrustNode trn = TrustNode::mkTrustConflict(exp, d_ipc.get());
211 : 8 : trustedConflict(trn, id);
212 : 8 : return;
213 : 8 : }
214 : 49172 : Node lem = conc;
215 [ + + ]: 49172 : if (exp != d_true)
216 : : {
217 : 41109 : lem = nodeManager()->mkNode(Kind::IMPLIES, exp, conc);
218 : : }
219 [ + + ]: 49172 : if (d_ipc)
220 : : {
221 : 23531 : d_ipc->notifyLemma(lem, id);
222 : : }
223 [ + + ]: 49172 : addPendingLemma(lem, id, LemmaProperty::NONE, d_ipc.get());
224 : 49172 : }
225 : :
226 : : } // namespace sets
227 : : } // namespace theory
228 : : } // namespace cvc5::internal
|
