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 : : * A buffered inference manager.
14 : : */
15 : :
16 : : #include "theory/inference_manager_buffered.h"
17 : :
18 : : #include "theory/rewriter.h"
19 : : #include "theory/theory.h"
20 : : #include "theory/theory_state.h"
21 : :
22 : : using namespace cvc5::internal::kind;
23 : :
24 : : namespace cvc5::internal {
25 : : namespace theory {
26 : :
27 : 356958 : InferenceManagerBuffered::InferenceManagerBuffered(Env& env,
28 : : Theory& t,
29 : : TheoryState& state,
30 : : const std::string& statsName,
31 : 356958 : bool cacheLemmas)
32 : : : TheoryInferenceManager(env, t, state, statsName, cacheLemmas),
33 : 356958 : d_processingPendingLemmas(false)
34 : : {
35 : 356958 : }
36 : :
37 : 7309270 : bool InferenceManagerBuffered::hasPending() const
38 : : {
39 [ + + ][ + + ]: 7309270 : return hasPendingFact() || hasPendingLemma();
40 : : }
41 : :
42 : 8344080 : bool InferenceManagerBuffered::hasPendingFact() const
43 : : {
44 : 8344080 : return !d_pendingFact.empty();
45 : : }
46 : :
47 : 8679100 : bool InferenceManagerBuffered::hasPendingLemma() const
48 : : {
49 : 8679100 : return !d_pendingLem.empty();
50 : : }
51 : :
52 : 660394 : bool InferenceManagerBuffered::addPendingLemma(Node lem,
53 : : InferenceId id,
54 : : LemmaProperty p,
55 : : ProofGenerator* pg,
56 : : bool checkCache)
57 : : {
58 [ + - ]: 660394 : if (checkCache)
59 : : {
60 : : // check if it is unique up to rewriting
61 : 660394 : Node lemr = rewrite(lem);
62 [ + + ]: 660394 : if (hasCachedLemma(lemr, p))
63 : : {
64 : 417296 : return false;
65 : : }
66 : : }
67 : : // make the simple theory lemma
68 : 243098 : d_pendingLem.emplace_back(new SimpleTheoryLemma(id, lem, p, pg));
69 : 243098 : return true;
70 : : }
71 : :
72 : 40953 : void InferenceManagerBuffered::addPendingLemma(
73 : : std::unique_ptr<TheoryInference> lemma)
74 : : {
75 : 40953 : d_pendingLem.emplace_back(std::move(lemma));
76 : 40953 : }
77 : :
78 : 0 : void InferenceManagerBuffered::addPendingFact(Node conc,
79 : : InferenceId id,
80 : : Node exp,
81 : : ProofGenerator* pg)
82 : : {
83 : : // make a simple theory internal fact
84 : 0 : Assert(conc.getKind() != Kind::AND && conc.getKind() != Kind::OR);
85 : 0 : d_pendingFact.emplace_back(new SimpleTheoryInternalFact(id, conc, exp, pg));
86 : 0 : }
87 : :
88 : 89968 : void InferenceManagerBuffered::addPendingFact(
89 : : std::unique_ptr<TheoryInference> fact)
90 : : {
91 : 89968 : d_pendingFact.emplace_back(std::move(fact));
92 : 89968 : }
93 : :
94 : 7305 : void InferenceManagerBuffered::addPendingPhaseRequirement(Node lit, bool pol)
95 : : {
96 : : // it is the responsibility of the caller to ensure lit is rewritten
97 : 7305 : d_pendingReqPhase[lit] = pol;
98 : 7305 : }
99 : :
100 : 8613530 : void InferenceManagerBuffered::doPendingFacts()
101 : : {
102 : 8613530 : size_t i = 0;
103 [ + + ][ + + ]: 9091500 : while (!d_theoryState.isInConflict() && i < d_pendingFact.size())
[ + + ]
104 : : {
105 : : // assert the internal fact, which notice may enqueue more pending facts in
106 : : // this loop, or result in a conflict.
107 : 477966 : assertInternalFactTheoryInference(d_pendingFact[i].get());
108 : 477966 : i++;
109 : : }
110 : 8613530 : d_pendingFact.clear();
111 : 8613530 : }
112 : :
113 : 8573820 : void InferenceManagerBuffered::doPendingLemmas()
114 : : {
115 [ + + ]: 8573820 : if (d_processingPendingLemmas)
116 : : {
117 : : // already processing
118 : 17873 : return;
119 : : }
120 : 8555950 : d_processingPendingLemmas = true;
121 : 8555950 : size_t i = 0;
122 [ + + ]: 8880810 : while (i < d_pendingLem.size())
123 : : {
124 : : // process this lemma, which notice may enqueue more pending lemmas in this
125 : : // loop, or clear the lemmas.
126 : 324863 : lemmaTheoryInference(d_pendingLem[i].get());
127 : 324862 : i++;
128 : : }
129 : 8555950 : d_pendingLem.clear();
130 : 8555950 : d_processingPendingLemmas = false;
131 : : }
132 : :
133 : 524542 : void InferenceManagerBuffered::doPendingPhaseRequirements()
134 : : {
135 : : // process the pending require phase calls
136 [ + + ]: 531830 : for (const std::pair<const Node, bool>& prp : d_pendingReqPhase)
137 : : {
138 : 7288 : preferPhase(prp.first, prp.second);
139 : : }
140 : 524542 : d_pendingReqPhase.clear();
141 : 524542 : }
142 : 2796820 : void InferenceManagerBuffered::clearPending()
143 : : {
144 : 2796820 : d_pendingFact.clear();
145 : 2796820 : d_pendingLem.clear();
146 : 2796820 : d_pendingReqPhase.clear();
147 : 2796820 : }
148 : 1871 : void InferenceManagerBuffered::clearPendingFacts() { d_pendingFact.clear(); }
149 : 61698 : void InferenceManagerBuffered::clearPendingLemmas() { d_pendingLem.clear(); }
150 : 5117 : void InferenceManagerBuffered::clearPendingPhaseRequirements()
151 : : {
152 : 5117 : d_pendingReqPhase.clear();
153 : 5117 : }
154 : :
155 : 732022 : std::size_t InferenceManagerBuffered::numPendingLemmas() const
156 : : {
157 : 732022 : return d_pendingLem.size();
158 : : }
159 : 0 : std::size_t InferenceManagerBuffered::numPendingFacts() const
160 : : {
161 : 0 : return d_pendingFact.size();
162 : : }
163 : :
164 : 405451 : bool InferenceManagerBuffered::lemmaTheoryInference(TheoryInference* lem)
165 : : {
166 : : // process this lemma
167 : 405451 : LemmaProperty p = LemmaProperty::NONE;
168 : 810902 : TrustNode tlem = lem->processLemma(p);
169 [ - + ][ - + ]: 405451 : Assert(!tlem.isNull());
[ - - ]
170 : : // send the lemma
171 : 810901 : return trustedLemma(tlem, lem->getId(), p);
172 : : }
173 : :
174 : 477966 : void InferenceManagerBuffered::assertInternalFactTheoryInference(
175 : : TheoryInference* fact)
176 : : {
177 : : // process this fact
178 : 955932 : std::vector<Node> exp;
179 : 477966 : ProofGenerator* pg = nullptr;
180 : 955932 : Node lit = fact->processFact(exp, pg);
181 [ - + ][ - + ]: 477966 : Assert(!lit.isNull());
[ - - ]
182 : 477966 : bool pol = lit.getKind() != Kind::NOT;
183 [ + + ]: 477966 : TNode atom = pol ? lit : lit[0];
184 : : // no double negation or conjunctive conclusions
185 [ + - ][ + - ]: 955932 : Assert(atom.getKind() != Kind::NOT && atom.getKind() != Kind::AND);
[ - + ][ - - ]
186 : : // assert the internal fact
187 : 477966 : assertInternalFact(atom, pol, fact->getId(), exp, pg);
188 : 477966 : }
189 : :
190 : 2361300 : void InferenceManagerBuffered::notifyInConflict()
191 : : {
192 : 2361300 : d_theoryState.notifyInConflict();
193 : : // also clear the pending facts, which will be stale after backtracking
194 : 2361300 : clearPending();
195 : 2361300 : }
196 : :
197 : : } // namespace theory
198 : : } // namespace cvc5::internal
|
