adbcc303330cc0d5656093fa11915863b1f5aabe
1 /********************* */
2 /*! \file inference_manager_buffered.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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.\endverbatim
12 ** \brief A buffered inference manager
15 #include "theory/inference_manager_buffered.h"
17 #include "theory/rewriter.h"
18 #include "theory/theory.h"
20 using namespace CVC4::kind
;
25 InferenceManagerBuffered::InferenceManagerBuffered(Theory
& t
,
27 ProofNodeManager
* pnm
)
28 : TheoryInferenceManager(t
, state
, pnm
)
32 bool InferenceManagerBuffered::hasProcessed() const
34 return d_theoryState
.isInConflict() || !d_pendingLem
.empty()
35 || !d_pendingFact
.empty();
38 bool InferenceManagerBuffered::hasPendingFact() const
40 return !d_pendingFact
.empty();
43 bool InferenceManagerBuffered::hasPendingLemma() const
45 return !d_pendingLem
.empty();
48 void InferenceManagerBuffered::addPendingLemma(Node lem
,
52 d_pendingLem
.push_back(std::make_shared
<Lemma
>(lem
, p
, pg
));
55 void InferenceManagerBuffered::addPendingLemma(std::shared_ptr
<Lemma
> lemma
)
57 d_pendingLem
.emplace_back(std::move(lemma
));
60 void InferenceManagerBuffered::addPendingFact(Node fact
, Node exp
)
62 Assert(fact
.getKind() != AND
&& fact
.getKind() != OR
);
63 d_pendingFact
.push_back(std::pair
<Node
, Node
>(fact
, exp
));
66 void InferenceManagerBuffered::addPendingPhaseRequirement(Node lit
, bool pol
)
68 // must ensure rewritten
69 lit
= Rewriter::rewrite(lit
);
70 d_pendingReqPhase
[lit
] = pol
;
73 void InferenceManagerBuffered::doPendingFacts()
76 while (!d_theoryState
.isInConflict() && i
< d_pendingFact
.size())
78 std::pair
<Node
, Node
>& pfact
= d_pendingFact
[i
];
79 Node fact
= pfact
.first
;
80 Node exp
= pfact
.second
;
81 bool polarity
= fact
.getKind() != NOT
;
82 TNode atom
= polarity
? fact
: fact
[0];
83 // no double negation or conjunctive conclusions
84 Assert(atom
.getKind() != NOT
&& atom
.getKind() != AND
);
85 assertInternalFact(atom
, polarity
, exp
);
88 d_pendingFact
.clear();
91 void InferenceManagerBuffered::doPendingLemmas()
93 // process all the pending lemmas
94 for (const std::shared_ptr
<Lemma
>& plem
: d_pendingLem
)
96 if (!plem
->notifySend())
98 // the lemma indicated that it should not be sent after all
101 Node lem
= plem
->d_node
;
102 LemmaProperty p
= plem
->d_property
;
103 ProofGenerator
* pg
= plem
->d_pg
;
104 Assert(!lem
.isNull());
105 // send (trusted) lemma on the output channel with property p
106 trustedLemma(TrustNode::mkTrustLemma(lem
, pg
), p
);
108 d_pendingLem
.clear();
111 void InferenceManagerBuffered::doPendingPhaseRequirements()
113 // process the pending require phase calls
114 for (const std::pair
<const Node
, bool>& prp
: d_pendingReqPhase
)
116 d_out
.requirePhase(prp
.first
, prp
.second
);
118 d_pendingReqPhase
.clear();
121 } // namespace theory