20c1fbf3790676c37e13dfd7a89820d87b91ebcd
1 /********************* */
2 /*! \file theory_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 An inference manager for Theory
15 #include "theory/theory_inference_manager.h"
17 #include "theory/theory.h"
18 #include "theory/uf/equality_engine.h"
20 using namespace CVC4::kind
;
25 TheoryInferenceManager::TheoryInferenceManager(Theory
& t
,
27 ProofNodeManager
* pnm
)
30 d_out(t
.getOutputChannel()),
33 d_keep(t
.getSatContext()),
34 d_lemmasSent(t
.getUserContext()),
35 d_numCurrentLemmas(0),
40 void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine
* ee
)
43 // if proofs are enabled, also make a proof equality engine to wrap ee
46 d_pfee
.reset(new eq::ProofEqEngine(d_theoryState
.getSatContext(),
47 d_theoryState
.getUserContext(),
53 void TheoryInferenceManager::reset()
55 d_numCurrentLemmas
= 0;
56 d_numCurrentFacts
= 0;
59 void TheoryInferenceManager::conflictEqConstantMerge(TNode a
, TNode b
)
61 if (!d_theoryState
.isInConflict())
63 TrustNode tconf
= explainConflictEqConstantMerge(a
, b
);
64 d_theoryState
.notifyInConflict();
65 d_out
.trustedConflict(tconf
);
69 void TheoryInferenceManager::conflict(TNode conf
)
71 if (!d_theoryState
.isInConflict())
73 d_theoryState
.notifyInConflict();
78 void TheoryInferenceManager::trustedConflict(TrustNode tconf
)
80 if (!d_theoryState
.isInConflict())
82 d_theoryState
.notifyInConflict();
83 d_out
.trustedConflict(tconf
);
87 bool TheoryInferenceManager::propagateLit(TNode lit
)
89 // If already in conflict, no more propagation
90 if (d_theoryState
.isInConflict())
95 bool ok
= d_out
.propagate(lit
);
98 d_theoryState
.notifyInConflict();
103 TrustNode
TheoryInferenceManager::explainLit(TNode lit
)
105 if (d_pfee
!= nullptr)
107 return d_pfee
->explain(lit
);
111 Node exp
= d_ee
->mkExplainLit(lit
);
112 return TrustNode::mkTrustPropExp(lit
, exp
, nullptr);
114 Unimplemented() << "Inference manager for " << d_theory
.getId()
115 << " was asked to explain a propagation but doesn't have an "
116 "equality engine or implement the "
117 "TheoryInferenceManager::explainLit interface!";
120 TrustNode
TheoryInferenceManager::explainConflictEqConstantMerge(TNode a
,
123 Node lit
= a
.eqNode(b
);
124 if (d_pfee
!= nullptr)
126 return d_pfee
->explain(lit
);
130 Node conf
= d_ee
->mkExplainLit(lit
);
131 return TrustNode::mkTrustConflict(conf
, nullptr);
133 Unimplemented() << "Inference manager for " << d_theory
.getId()
134 << " mkTrustedConflictEqConstantMerge";
137 bool TheoryInferenceManager::lemma(TNode lem
, LemmaProperty p
, bool doCache
)
139 TrustNode tlem
= TrustNode::mkTrustLemma(lem
, nullptr);
140 return trustedLemma(tlem
, p
, doCache
);
143 bool TheoryInferenceManager::trustedLemma(const TrustNode
& tlem
,
149 if (!cacheLemma(tlem
.getNode(), p
))
154 d_numCurrentLemmas
++;
155 d_out
.trustedLemma(tlem
, p
);
159 bool TheoryInferenceManager::hasCachedLemma(TNode lem
, LemmaProperty p
)
161 return d_lemmasSent
.find(lem
) != d_lemmasSent
.end();
164 uint32_t TheoryInferenceManager::numAddedLemmas() const
166 return d_numCurrentLemmas
;
169 bool TheoryInferenceManager::hasAddedLemma() const
171 return d_numCurrentLemmas
!= 0;
174 void TheoryInferenceManager::assertInternalFact(TNode atom
, bool pol
, TNode exp
)
176 processInternalFact(atom
, pol
, PfRule::UNKNOWN
, {exp
}, {}, nullptr);
179 void TheoryInferenceManager::assertInternalFact(TNode atom
,
182 const std::vector
<Node
>& exp
,
183 const std::vector
<Node
>& args
)
185 Assert(id
!= PfRule::UNKNOWN
);
186 processInternalFact(atom
, pol
, id
, exp
, args
, nullptr);
189 void TheoryInferenceManager::assertInternalFact(TNode atom
,
191 const std::vector
<Node
>& exp
,
194 Assert(pg
!= nullptr);
195 processInternalFact(atom
, pol
, PfRule::ASSUME
, exp
, {}, pg
);
198 void TheoryInferenceManager::processInternalFact(TNode atom
,
201 const std::vector
<Node
>& exp
,
202 const std::vector
<Node
>& args
,
205 // make the node corresponding to the explanation
206 Node expn
= NodeManager::currentNM()->mkAnd(exp
);
207 // call the pre-notify fact method with preReg = false, isInternal = true
208 if (d_theory
.preNotifyFact(atom
, pol
, expn
, false, true))
210 // handled in a theory-specific way that doesn't require equality engine
213 Assert(d_ee
!= nullptr);
214 Trace("infer-manager") << "TheoryInferenceManager::assertInternalFact: "
215 << expn
<< std::endl
;
217 // Now, assert the fact. How to do so depends on whether proofs are enabled.
218 // If no proof production, or no proof rule was given
219 if (d_pfee
== nullptr || id
== PfRule::UNKNOWN
)
221 if (atom
.getKind() == kind::EQUAL
)
223 d_ee
->assertEquality(atom
, pol
, expn
);
227 d_ee
->assertPredicate(atom
, pol
, expn
);
229 // Must reference count the equality and its explanation, which is not done
230 // by the equality engine. Notice that we do *not* need to do this for
231 // external assertions, which enter as facts in theory check. This is also
232 // not done if we are asserting to the proof equality engine, which does
233 // this caching itself within ProofEqEngine::assertFact.
239 // Note that we reconstruct the original literal lit here, since both the
240 // original literal is needed for bookkeeping proofs. It is possible to
241 // optimize this so that a few less nodes are created, but at the cost
242 // of a more verbose interface to proof equality engine.
243 Node lit
= pol
? Node(atom
) : atom
.notNode();
246 // use the proof generator interface
247 d_pfee
->assertFact(lit
, expn
, pg
);
251 // use the explict proof step interface
252 d_pfee
->assertFact(lit
, id
, expn
, args
);
255 // call the notify fact method with isInternal = true
256 d_theory
.notifyFact(atom
, pol
, expn
, true);
257 Trace("infer-manager")
258 << "TheoryInferenceManager::finished assertInternalFact" << std::endl
;
261 void TheoryInferenceManager::explain(TNode n
, std::vector
<TNode
>& assumptions
)
263 if (n
.getKind() == kind::AND
)
265 for (const Node
& nc
: n
)
267 d_ee
->explainLit(nc
, assumptions
);
272 d_ee
->explainLit(n
, assumptions
);
276 Node
TheoryInferenceManager::mkExplain(TNode n
)
278 std::vector
<TNode
> assumptions
;
279 explain(n
, assumptions
);
280 return NodeManager::currentNM()->mkAnd(assumptions
);
283 uint32_t TheoryInferenceManager::numAddedFacts() const
285 return d_numCurrentFacts
;
288 bool TheoryInferenceManager::hasAddedFact() const
290 return d_numCurrentFacts
!= 0;
293 bool TheoryInferenceManager::cacheLemma(TNode lem
, LemmaProperty p
)
295 if (d_lemmasSent
.find(lem
) != d_lemmasSent
.end())
299 d_lemmasSent
.insert(lem
);
303 } // namespace theory