f026aa37422d18070d0da278aa5a2bc530bcb4a4
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::shared_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 addPendingLemma(std::move(lemma
));
61 void InferenceManager::addPendingArithLemma(const ArithLemma
& lemma
,
64 addPendingArithLemma(std::make_shared
<ArithLemma
>(lemma
), isWaiting
);
66 void InferenceManager::addPendingArithLemma(const Node
& lemma
,
67 nl::Inference inftype
,
70 addPendingArithLemma(std::make_shared
<ArithLemma
>(
71 lemma
, LemmaProperty::NONE
, nullptr, inftype
),
75 void InferenceManager::flushWaitingLemmas()
77 for (auto& lem
: d_waitingLem
)
79 addPendingLemma(std::move(lem
));
84 void InferenceManager::addConflict(const Node
& conf
, nl::Inference inftype
)
86 conflict(Rewriter::rewrite(conf
));
89 std::size_t InferenceManager::numWaitingLemmas() const
91 return d_waitingLem
.size();
94 bool InferenceManager::hasCachedLemma(TNode lem
, LemmaProperty p
)
96 if (isLemmaPropertyPreprocess(p
))
98 return d_lemmasPp
.find(lem
) != d_lemmasPp
.end();
100 return TheoryInferenceManager::hasCachedLemma(lem
, p
);
103 bool InferenceManager::cacheLemma(TNode lem
, LemmaProperty p
)
105 if (isLemmaPropertyPreprocess(p
))
107 if (d_lemmasPp
.find(lem
) != d_lemmasPp
.end())
111 d_lemmasPp
.insert(lem
);
114 return TheoryInferenceManager::cacheLemma(lem
, p
);
117 bool InferenceManager::isEntailedFalse(const ArithLemma
& lem
)
119 if (options::nlExtEntailConflicts())
121 Node ch_lemma
= lem
.d_node
.negate();
122 ch_lemma
= Rewriter::rewrite(ch_lemma
);
123 Trace("arith-inf-manager") << "InferenceManager::Check entailment of "
124 << ch_lemma
<< "..." << std::endl
;
126 std::pair
<bool, Node
> et
= d_theory
.getValuation().entailmentCheck(
127 options::TheoryOfMode::THEORY_OF_TYPE_BASED
, ch_lemma
);
128 Trace("arith-inf-manager") << "entailment test result : " << et
.first
<< " "
129 << et
.second
<< std::endl
;
132 Trace("arith-inf-manager")
133 << "*** Lemma entailed to be in conflict : " << lem
.d_node
142 } // namespace theory