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-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 : : * 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 : 352933 : InferenceManagerBuffered::InferenceManagerBuffered(Env& env,
28 : : Theory& t,
29 : : TheoryState& state,
30 : : const std::string& statsName,
31 : 352933 : bool cacheLemmas)
32 : : : TheoryInferenceManager(env, t, state, statsName, cacheLemmas),
33 : 352933 : d_processingPendingLemmas(false)
34 : : {
35 : 352933 : }
36 : :
37 : 6918790 : bool InferenceManagerBuffered::hasPending() const
38 : : {
39 [ + + ][ + + ]: 6918790 : return hasPendingFact() || hasPendingLemma();
40 : : }
41 : :
42 : 7878630 : bool InferenceManagerBuffered::hasPendingFact() const
43 : : {
44 : 7878630 : return !d_pendingFact.empty();
45 : : }
46 : :
47 : 8207420 : bool InferenceManagerBuffered::hasPendingLemma() const
48 : : {
49 : 8207420 : return !d_pendingLem.empty();
50 : : }
51 : :
52 : 612847 : bool InferenceManagerBuffered::addPendingLemma(Node lem,
53 : : InferenceId id,
54 : : LemmaProperty p,
55 : : ProofGenerator* pg,
56 : : bool checkCache)
57 : : {
58 [ + - ]: 612847 : if (checkCache)
59 : : {
60 : : // check if it is unique up to rewriting
61 : 612847 : Node lemr = rewrite(lem);
62 [ + + ]: 612847 : if (hasCachedLemma(lemr, p))
63 : : {
64 : 414845 : return false;
65 : : }
66 : : }
67 : : // make the simple theory lemma
68 : 198002 : d_pendingLem.emplace_back(new SimpleTheoryLemma(id, lem, p, pg));
69 : 198002 : return true;
70 : : }
71 : :
72 : 38297 : void InferenceManagerBuffered::addPendingLemma(
73 : : std::unique_ptr<TheoryInference> lemma)
74 : : {
75 : 38297 : d_pendingLem.emplace_back(std::move(lemma));
76 : 38297 : }
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 : 85486 : void InferenceManagerBuffered::addPendingFact(
89 : : std::unique_ptr<TheoryInference> fact)
90 : : {
91 : 85486 : d_pendingFact.emplace_back(std::move(fact));
92 : 85486 : }
93 : :
94 : 6856 : void InferenceManagerBuffered::addPendingPhaseRequirement(Node lit, bool pol)
95 : : {
96 : : // it is the responsibility of the caller to ensure lit is rewritten
97 : 6856 : d_pendingReqPhase[lit] = pol;
98 : 6856 : }
99 : :
100 : 7195260 : void InferenceManagerBuffered::doPendingFacts()
101 : : {
102 : 7195260 : size_t i = 0;
103 [ + + ][ + + ]: 7586840 : 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 : 391576 : assertInternalFactTheoryInference(d_pendingFact[i].get());
108 : 391576 : i++;
109 : : }
110 : 7195260 : d_pendingFact.clear();
111 : 7195260 : }
112 : :
113 : 7213100 : void InferenceManagerBuffered::doPendingLemmas()
114 : : {
115 [ + + ]: 7213100 : if (d_processingPendingLemmas)
116 : : {
117 : : // already processing
118 : 16985 : return;
119 : : }
120 : 7196120 : d_processingPendingLemmas = true;
121 : 7196120 : size_t i = 0;
122 [ + + ]: 7468290 : 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 : 272176 : lemmaTheoryInference(d_pendingLem[i].get());
127 : 272175 : i++;
128 : : }
129 : 7196120 : d_pendingLem.clear();
130 : 7196120 : d_processingPendingLemmas = false;
131 : : }
132 : :
133 : 508751 : void InferenceManagerBuffered::doPendingPhaseRequirements()
134 : : {
135 : : // process the pending require phase calls
136 [ + + ]: 515590 : for (const std::pair<const Node, bool>& prp : d_pendingReqPhase)
137 : : {
138 : 6839 : preferPhase(prp.first, prp.second);
139 : : }
140 : 508751 : d_pendingReqPhase.clear();
141 : 508751 : }
142 : 2799240 : void InferenceManagerBuffered::clearPending()
143 : : {
144 : 2799240 : d_pendingFact.clear();
145 : 2799240 : d_pendingLem.clear();
146 : 2799240 : d_pendingReqPhase.clear();
147 : 2799240 : }
148 : 1621 : void InferenceManagerBuffered::clearPendingFacts() { d_pendingFact.clear(); }
149 : 60580 : void InferenceManagerBuffered::clearPendingLemmas() { d_pendingLem.clear(); }
150 : 4565 : void InferenceManagerBuffered::clearPendingPhaseRequirements()
151 : : {
152 : 4565 : d_pendingReqPhase.clear();
153 : 4565 : }
154 : :
155 : 717655 : std::size_t InferenceManagerBuffered::numPendingLemmas() const
156 : : {
157 : 717655 : return d_pendingLem.size();
158 : : }
159 : 0 : std::size_t InferenceManagerBuffered::numPendingFacts() const
160 : : {
161 : 0 : return d_pendingFact.size();
162 : : }
163 : :
164 : 352864 : bool InferenceManagerBuffered::lemmaTheoryInference(TheoryInference* lem)
165 : : {
166 : : // process this lemma
167 : 352864 : LemmaProperty p = LemmaProperty::NONE;
168 : 705728 : TrustNode tlem = lem->processLemma(p);
169 [ - + ][ - + ]: 352864 : Assert(!tlem.isNull());
[ - - ]
170 : : // send the lemma
171 : 705727 : return trustedLemma(tlem, lem->getId(), p);
172 : : }
173 : :
174 : 391576 : void InferenceManagerBuffered::assertInternalFactTheoryInference(
175 : : TheoryInference* fact)
176 : : {
177 : : // process this fact
178 : 783152 : std::vector<Node> exp;
179 : 391576 : ProofGenerator* pg = nullptr;
180 : 783152 : Node lit = fact->processFact(exp, pg);
181 [ - + ][ - + ]: 391576 : Assert(!lit.isNull());
[ - - ]
182 : 391576 : bool pol = lit.getKind() != Kind::NOT;
183 [ + + ]: 391576 : TNode atom = pol ? lit : lit[0];
184 : : // no double negation or conjunctive conclusions
185 [ + - ][ + - ]: 783152 : Assert(atom.getKind() != Kind::NOT && atom.getKind() != Kind::AND);
[ - + ][ - - ]
186 : : // assert the internal fact
187 : 391576 : assertInternalFact(atom, pol, fact->getId(), exp, pg);
188 : 391576 : }
189 : :
190 : 2376760 : void InferenceManagerBuffered::notifyInConflict()
191 : : {
192 : 2376760 : d_theoryState.notifyInConflict();
193 : : // also clear the pending facts, which will be stale after backtracking
194 : 2376760 : clearPending();
195 : 2376760 : }
196 : :
197 : : } // namespace theory
198 : : } // namespace cvc5::internal
|
