Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Gereon Kremer, Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Implementation of the inference manager for the theory of sets.
14 : : */
15 : :
16 : : #include "theory/sets/inference_manager.h"
17 : :
18 : : #include "options/sets_options.h"
19 : : #include "proof/trust_id.h"
20 : : #include "theory/builtin/proof_checker.h"
21 : : #include "theory/rewriter.h"
22 : :
23 : : using namespace std;
24 : : using namespace cvc5::internal::kind;
25 : :
26 : : namespace cvc5::internal {
27 : : namespace theory {
28 : : namespace sets {
29 : :
30 : 50343 : InferenceManager::InferenceManager(Env& env,
31 : : Theory& t,
32 : : TheorySetsRewriter* tr,
33 : 50343 : SolverState& s)
34 : : : InferenceManagerBuffered(env, t, s, "theory::sets::"),
35 : : d_state(s),
36 [ + + ]: 50343 : d_ipc(isProofEnabled() ? new InferProofCons(env, tr) : nullptr)
37 : : {
38 : 50343 : d_true = nodeManager()->mkConst(true);
39 : 50343 : d_false = nodeManager()->mkConst(false);
40 : 50343 : }
41 : :
42 : 276080 : bool InferenceManager::assertFactRec(Node fact, InferenceId id, Node exp, int inferType)
43 : : {
44 : : // should we send this fact out as a lemma?
45 [ + - ]: 276080 : if (inferType != -1)
46 : : {
47 [ + + ]: 276080 : if (d_state.isEntailed(fact, true))
48 : : {
49 : 225688 : return false;
50 : : }
51 : 50392 : setupAndAddPendingLemma(exp, fact, id);
52 : 50392 : 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 : : }
82 : 0 : return ret;
83 : : }
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 : : }
109 : :
110 : 739 : void InferenceManager::assertSetsConflict(const Node& conf, InferenceId id)
111 : : {
112 [ + + ]: 739 : if (d_ipc)
113 : : {
114 : 305 : d_ipc->notifyConflict(conf, id);
115 : : }
116 [ + + ]: 739 : TrustNode trn = TrustNode::mkTrustConflict(conf, d_ipc.get());
117 : 739 : trustedConflict(trn, id);
118 : 739 : }
119 : :
120 : 12215 : bool InferenceManager::assertSetsFact(Node atom,
121 : : bool polarity,
122 : : InferenceId id,
123 : : Node exp)
124 : : {
125 [ + - ]: 12215 : Node conc = polarity ? atom : atom.notNode();
126 : : // notify before asserting below, since that call may induce a conflict which
127 : : // needs immediate explanation.
128 [ + + ]: 12215 : if (d_ipc)
129 : : {
130 : 3646 : d_ipc->notifyFact(conc, exp, id);
131 : : }
132 : 36645 : return assertInternalFact(atom, polarity, id, {exp}, d_ipc.get());
133 : : }
134 : :
135 : 276080 : void InferenceManager::assertInference(Node fact,
136 : : InferenceId id,
137 : : Node exp,
138 : : int inferType)
139 : : {
140 [ + + ]: 276080 : if (assertFactRec(fact, id, exp, inferType))
141 : : {
142 [ + - ]: 100784 : Trace("sets-lemma") << "Sets::Lemma : " << fact << " from " << exp << " by "
143 : 50392 : << id << std::endl;
144 [ + - ]: 100784 : Trace("sets-assertion") << "(assert (=> " << exp << " " << fact
145 : 50392 : << ")) ; by " << id << std::endl;
146 : : }
147 : 276080 : }
148 : :
149 : 239342 : void InferenceManager::assertInference(Node fact,
150 : : InferenceId id,
151 : : std::vector<Node>& exp,
152 : : int inferType)
153 : : {
154 : : Node exp_n =
155 : 239342 : exp.empty()
156 : 6585 : ? d_true
157 [ + + ][ + + ]: 239342 : : (exp.size() == 1 ? exp[0] : nodeManager()->mkNode(Kind::AND, exp));
158 : 239342 : assertInference(fact, id, exp_n, inferType);
159 : 239342 : }
160 : :
161 : 10967 : void InferenceManager::assertInference(std::vector<Node>& conc,
162 : : InferenceId id,
163 : : Node exp,
164 : : int inferType)
165 : : {
166 [ + + ]: 10967 : if (!conc.empty())
167 : : {
168 : : Node fact =
169 [ + + ]: 760 : conc.size() == 1 ? conc[0] : nodeManager()->mkNode(Kind::AND, conc);
170 : 760 : assertInference(fact, id, exp, inferType);
171 : : }
172 : 10967 : }
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 : 3114 : void InferenceManager::split(Node n, InferenceId id, int reqPol)
186 : : {
187 : 3114 : n = rewrite(n);
188 : 9342 : Node lem = nodeManager()->mkNode(Kind::OR, n, n.negate());
189 : : // send the lemma
190 : 3114 : lemma(lem, id);
191 [ + - ]: 3114 : Trace("sets-lemma") << "Sets::Lemma split : " << lem << std::endl;
192 [ + + ]: 3114 : if (reqPol != 0)
193 : : {
194 [ + - ]: 624 : Trace("sets-lemma") << "Sets::Require phase " << n << " " << (reqPol > 0)
195 : 312 : << std::endl;
196 : 312 : preferPhase(n, reqPol > 0);
197 : : }
198 : 3114 : }
199 : :
200 : 50392 : void InferenceManager::setupAndAddPendingLemma(const Node& exp,
201 : : const Node& conc,
202 : : InferenceId id)
203 : : {
204 [ + + ]: 50392 : 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 : : }
214 : 50384 : Node lem = conc;
215 [ + + ]: 50384 : if (exp != d_true)
216 : : {
217 : 42261 : lem = nodeManager()->mkNode(Kind::IMPLIES, exp, conc);
218 : : }
219 [ + + ]: 50384 : if (d_ipc)
220 : : {
221 : 23003 : d_ipc->notifyLemma(lem, id);
222 : : }
223 [ + + ]: 50384 : addPendingLemma(lem, id, LemmaProperty::NONE, d_ipc.get());
224 : : }
225 : :
226 : : } // namespace sets
227 : : } // namespace theory
228 : : } // namespace cvc5::internal
|
