1 /********************* */
2 /*! \file inference_manager.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 Implementation of the inference manager for the theory of strings.
15 #include "theory/arith/inference_manager.h"
17 #include "options/arith_options.h"
18 #include "theory/arith/theory_arith.h"
19 #include "theory/rewriter.h"
25 InferenceManager::InferenceManager(TheoryArith
& ta
,
27 ProofNodeManager
* pnm
)
28 : InferenceManagerBuffered(ta
, astate
, pnm
), d_lemmasPp(ta
.getUserContext())
32 void InferenceManager::addPendingArithLemma(std::unique_ptr
<ArithLemma
> lemma
,
35 lemma
->d_node
= Rewriter::rewrite(lemma
->d_node
);
36 if (hasCachedLemma(lemma
->d_node
, lemma
->d_property
))
40 if (isEntailedFalse(*lemma
))
49 d_theoryState
.notifyInConflict();
54 d_waitingLem
.emplace_back(std::move(lemma
));
58 d_pendingLem
.emplace_back(std::move(lemma
));
61 void InferenceManager::addPendingArithLemma(const ArithLemma
& lemma
,
64 addPendingArithLemma(std::unique_ptr
<ArithLemma
>(new ArithLemma(lemma
)),
67 void InferenceManager::addPendingArithLemma(const Node
& lemma
,
68 nl::Inference inftype
,
71 addPendingArithLemma(std::unique_ptr
<ArithLemma
>(new ArithLemma(
72 lemma
, LemmaProperty::NONE
, nullptr, inftype
)),
76 void InferenceManager::flushWaitingLemmas()
78 for (auto& lem
: d_waitingLem
)
80 d_pendingLem
.emplace_back(std::move(lem
));
85 void InferenceManager::addConflict(const Node
& conf
, nl::Inference inftype
)
87 conflict(Rewriter::rewrite(conf
));
90 std::size_t InferenceManager::numWaitingLemmas() const
92 return d_waitingLem
.size();
95 bool InferenceManager::hasCachedLemma(TNode lem
, LemmaProperty p
)
97 if (isLemmaPropertyPreprocess(p
))
99 return d_lemmasPp
.find(lem
) != d_lemmasPp
.end();
101 return TheoryInferenceManager::hasCachedLemma(lem
, p
);
104 bool InferenceManager::cacheLemma(TNode lem
, LemmaProperty p
)
106 if (isLemmaPropertyPreprocess(p
))
108 if (d_lemmasPp
.find(lem
) != d_lemmasPp
.end())
112 d_lemmasPp
.insert(lem
);
115 return TheoryInferenceManager::cacheLemma(lem
, p
);
118 bool InferenceManager::isEntailedFalse(const ArithLemma
& lem
)
120 if (options::nlExtEntailConflicts())
122 Node ch_lemma
= lem
.d_node
.negate();
123 ch_lemma
= Rewriter::rewrite(ch_lemma
);
124 Trace("arith-inf-manager") << "InferenceManager::Check entailment of "
125 << ch_lemma
<< "..." << std::endl
;
127 std::pair
<bool, Node
> et
= d_theory
.getValuation().entailmentCheck(
128 options::TheoryOfMode::THEORY_OF_TYPE_BASED
, ch_lemma
);
129 Trace("arith-inf-manager") << "entailment test result : " << et
.first
<< " "
130 << et
.second
<< std::endl
;
133 Trace("arith-inf-manager")
134 << "*** Lemma entailed to be in conflict : " << lem
.d_node
143 } // namespace theory