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