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 : 49953 : InferenceManager::InferenceManager(Env& env,
28 : : Theory& t,
29 : : TheorySetsRewriter* tr,
30 : 49953 : SolverState& s)
31 : : : InferenceManagerBuffered(env, t, s, "theory::sets::"),
32 : 49953 : d_state(s),
33 [ + + ]: 49953 : d_ipc(isProofEnabled() ? new InferProofCons(env, tr) : nullptr)
34 : : {
35 : 49953 : d_true = nodeManager()->mkConst(true);
36 : 49953 : d_false = nodeManager()->mkConst(false);
37 : 49953 : }
38 : :
39 : 276080 : bool InferenceManager::assertFactRec(Node fact, InferenceId id, Node exp, int inferType)
40 : : {
41 : : // should we send this fact out as a lemma?
42 [ + - ]: 276080 : if (inferType != -1)
43 : : {
44 [ + + ]: 276080 : if (d_state.isEntailed(fact, true))
45 : : {
46 : 225688 : return false;
47 : : }
48 : 50392 : setupAndAddPendingLemma(exp, fact, id);
49 : 50392 : return true;
50 : : }
51 [ - - ]: 0 : Trace("sets-fact") << "Assert fact rec : " << fact << ", exp = " << exp
52 : 0 : << std::endl;
53 [ - - ]: 0 : if (fact.isConst())
54 : : {
55 : : // either trivial or a conflict
56 [ - - ]: 0 : if (fact == d_false)
57 : : {
58 [ - - ]: 0 : Trace("sets-lemma") << "Conflict : " << exp << std::endl;
59 : 0 : setupAndAddPendingLemma(exp, fact, id);
60 : 0 : return true;
61 : : }
62 : 0 : return false;
63 : : }
64 : 0 : else if (fact.getKind() == Kind::AND
65 : 0 : || (fact.getKind() == Kind::NOT && fact[0].getKind() == Kind::OR))
66 : : {
67 : 0 : bool ret = false;
68 [ - - ]: 0 : Node f = fact.getKind() == Kind::NOT ? fact[0] : fact;
69 [ - - ]: 0 : for (unsigned i = 0; i < f.getNumChildren(); i++)
70 : : {
71 : 0 : Node factc = fact.getKind() == Kind::NOT ? f[i].negate() : f[i];
72 : 0 : bool tret = assertFactRec(factc, id, exp, inferType);
73 [ - - ][ - - ]: 0 : ret = ret || tret;
74 [ - - ]: 0 : if (d_state.isInConflict())
75 : : {
76 : 0 : return true;
77 : : }
78 [ - - ]: 0 : }
79 : 0 : return ret;
80 : 0 : }
81 : 0 : bool polarity = fact.getKind() != Kind::NOT;
82 [ - - ]: 0 : TNode atom = polarity ? fact : fact[0];
83 [ - - ]: 0 : if (d_state.isEntailed(atom, polarity))
84 : : {
85 : 0 : return false;
86 : : }
87 : : // things we can assert to equality engine
88 : 0 : if (atom.getKind() == Kind::SET_MEMBER
89 : 0 : || (atom.getKind() == Kind::EQUAL && atom[0].getType().isSet()))
90 : : {
91 : : // send to equality engine
92 [ - - ]: 0 : if (assertSetsFact(atom, polarity, id, exp))
93 : : {
94 : : // return true if this wasn't redundant
95 : 0 : return true;
96 : : }
97 : : }
98 : : else
99 : : {
100 : : // must send as lemma
101 : 0 : setupAndAddPendingLemma(exp, fact, id);
102 : 0 : return true;
103 : : }
104 : 0 : return false;
105 : 0 : }
106 : :
107 : 739 : void InferenceManager::assertSetsConflict(const Node& conf, InferenceId id)
108 : : {
109 [ + + ]: 739 : if (d_ipc)
110 : : {
111 : 305 : d_ipc->notifyConflict(conf, id);
112 : : }
113 [ + + ]: 739 : TrustNode trn = TrustNode::mkTrustConflict(conf, d_ipc.get());
114 : 739 : trustedConflict(trn, id);
115 : 739 : }
116 : :
117 : 12215 : bool InferenceManager::assertSetsFact(Node atom,
118 : : bool polarity,
119 : : InferenceId id,
120 : : Node exp)
121 : : {
122 [ + - ]: 12215 : Node conc = polarity ? atom : atom.notNode();
123 : : // notify before asserting below, since that call may induce a conflict which
124 : : // needs immediate explanation.
125 [ + + ]: 12215 : if (d_ipc)
126 : : {
127 : 3646 : d_ipc->notifyFact(conc, exp, id);
128 : : }
129 : 36645 : return assertInternalFact(atom, polarity, id, {exp}, d_ipc.get());
130 : 12215 : }
131 : :
132 : 276080 : void InferenceManager::assertInference(Node fact,
133 : : InferenceId id,
134 : : Node exp,
135 : : int inferType)
136 : : {
137 [ + + ]: 276080 : if (assertFactRec(fact, id, exp, inferType))
138 : : {
139 [ + - ]: 100784 : Trace("sets-lemma") << "Sets::Lemma : " << fact << " from " << exp << " by "
140 : 50392 : << id << std::endl;
141 [ + - ]: 100784 : Trace("sets-assertion") << "(assert (=> " << exp << " " << fact
142 : 50392 : << ")) ; by " << id << std::endl;
143 : : }
144 : 276080 : }
145 : :
146 : 239342 : void InferenceManager::assertInference(Node fact,
147 : : InferenceId id,
148 : : std::vector<Node>& exp,
149 : : int inferType)
150 : : {
151 : : Node exp_n =
152 : 239342 : exp.empty()
153 : 6585 : ? d_true
154 [ + + ][ + + ]: 239342 : : (exp.size() == 1 ? exp[0] : nodeManager()->mkNode(Kind::AND, exp));
155 : 239342 : assertInference(fact, id, exp_n, inferType);
156 : 239342 : }
157 : :
158 : 10967 : void InferenceManager::assertInference(std::vector<Node>& conc,
159 : : InferenceId id,
160 : : Node exp,
161 : : int inferType)
162 : : {
163 [ + + ]: 10967 : if (!conc.empty())
164 : : {
165 : : Node fact =
166 [ + + ]: 760 : conc.size() == 1 ? conc[0] : nodeManager()->mkNode(Kind::AND, conc);
167 : 760 : assertInference(fact, id, exp, inferType);
168 : 760 : }
169 : 10967 : }
170 : 0 : void InferenceManager::assertInference(std::vector<Node>& conc,
171 : : InferenceId id,
172 : : std::vector<Node>& exp,
173 : : int inferType)
174 : : {
175 : : Node exp_n =
176 : 0 : exp.empty()
177 : 0 : ? d_true
178 : 0 : : (exp.size() == 1 ? exp[0] : nodeManager()->mkNode(Kind::AND, exp));
179 : 0 : assertInference(conc, id, exp_n, inferType);
180 : 0 : }
181 : :
182 : 3114 : void InferenceManager::split(Node n, InferenceId id, int reqPol)
183 : : {
184 : 3114 : n = rewrite(n);
185 : 6228 : Node lem = nodeManager()->mkNode(Kind::OR, n, n.negate());
186 : : // send the lemma
187 : 3114 : lemma(lem, id);
188 [ + - ]: 3114 : Trace("sets-lemma") << "Sets::Lemma split : " << lem << std::endl;
189 [ + + ]: 3114 : if (reqPol != 0)
190 : : {
191 [ + - ]: 624 : Trace("sets-lemma") << "Sets::Require phase " << n << " " << (reqPol > 0)
192 : 312 : << std::endl;
193 : 312 : preferPhase(n, reqPol > 0);
194 : : }
195 : 3114 : }
196 : :
197 : 50392 : void InferenceManager::setupAndAddPendingLemma(const Node& exp,
198 : : const Node& conc,
199 : : InferenceId id)
200 : : {
201 [ + + ]: 50392 : if (conc == d_false)
202 : : {
203 [ + + ]: 8 : if (d_ipc)
204 : : {
205 : 4 : d_ipc->notifyConflict(exp, id);
206 : : }
207 [ + + ]: 8 : TrustNode trn = TrustNode::mkTrustConflict(exp, d_ipc.get());
208 : 8 : trustedConflict(trn, id);
209 : 8 : return;
210 : 8 : }
211 : 50384 : Node lem = conc;
212 [ + + ]: 50384 : if (exp != d_true)
213 : : {
214 : 42261 : lem = nodeManager()->mkNode(Kind::IMPLIES, exp, conc);
215 : : }
216 [ + + ]: 50384 : if (d_ipc)
217 : : {
218 : 23003 : d_ipc->notifyLemma(lem, id);
219 : : }
220 [ + + ]: 50384 : addPendingLemma(lem, id, LemmaProperty::NONE, d_ipc.get());
221 : 50384 : }
222 : :
223 : : } // namespace sets
224 : : } // namespace theory
225 : : } // namespace cvc5::internal
|
