b2da91e165912c092abc6adaa4c799e8ed09530c
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())
37 void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine
* ee
)
42 void TheoryInferenceManager::conflictEqConstantMerge(TNode a
, TNode b
)
44 if (!d_theoryState
.isInConflict())
46 TrustNode tconf
= explainConflictEqConstantMerge(a
, b
);
47 d_theoryState
.notifyInConflict();
48 d_out
.trustedConflict(tconf
);
52 void TheoryInferenceManager::conflict(TNode conf
)
54 if (!d_theoryState
.isInConflict())
56 d_theoryState
.notifyInConflict();
61 void TheoryInferenceManager::trustedConflict(TrustNode tconf
)
63 if (!d_theoryState
.isInConflict())
65 d_theoryState
.notifyInConflict();
66 d_out
.trustedConflict(tconf
);
70 bool TheoryInferenceManager::propagateLit(TNode lit
)
72 // If already in conflict, no more propagation
73 if (d_theoryState
.isInConflict())
78 bool ok
= d_out
.propagate(lit
);
81 d_theoryState
.notifyInConflict();
86 TrustNode
TheoryInferenceManager::explainLit(TNode lit
)
88 // TODO (project #37): use proof equality engine if it exists
91 Node exp
= d_ee
->mkExplainLit(lit
);
92 return TrustNode::mkTrustPropExp(lit
, exp
, nullptr);
94 Unimplemented() << "Inference manager for " << d_theory
.getId()
95 << " was asked to explain a propagation but doesn't have an "
96 "equality engine or implement the "
97 "TheoryInferenceManager::explainLit interface!";
100 TrustNode
TheoryInferenceManager::explainConflictEqConstantMerge(TNode a
,
103 // TODO (project #37): use proof equality engine if it exists
106 Node lit
= a
.eqNode(b
);
107 Node conf
= d_ee
->mkExplainLit(lit
);
108 return TrustNode::mkTrustConflict(conf
, nullptr);
110 Unimplemented() << "Inference manager for " << d_theory
.getId()
111 << " mkTrustedConflictEqConstantMerge";
114 LemmaStatus
TheoryInferenceManager::lemma(TNode lem
, LemmaProperty p
)
116 return d_out
.lemma(lem
, p
);
119 LemmaStatus
TheoryInferenceManager::trustedLemma(const TrustNode
& tlem
,
122 return d_out
.trustedLemma(tlem
, p
);
125 void TheoryInferenceManager::assertInternalFact(TNode atom
,
129 // call the pre-notify fact method with preReg = false, isInternal = true
130 if (d_theory
.preNotifyFact(atom
, pol
, fact
, false, true))
132 // handled in a theory-specific way that doesn't require equality engine
135 Assert(d_ee
!= nullptr);
136 Trace("infer-manager") << "TheoryInferenceManager::assertInternalFact: "
137 << fact
<< std::endl
;
138 if (atom
.getKind() == kind::EQUAL
)
140 d_ee
->assertEquality(atom
, pol
, fact
);
144 d_ee
->assertPredicate(atom
, pol
, fact
);
146 // call the notify fact method with isInternal = true
147 d_theory
.notifyFact(atom
, pol
, fact
, true);
148 Trace("infer-manager")
149 << "TheoryInferenceManager::finished assertInternalFact" << std::endl
;
150 // Must reference count the equality and its explanation, which is not done
151 // by the equality engine. Notice that we do *not* need to do this for
152 // external assertions, which enter as facts in theory check.
157 } // namespace theory