From 21439d98e9afe1541bb0f5371c4ab0011666bd5e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 14 Sep 2020 02:52:28 -0500 Subject: Standardize uses of inference manager in datatypes (#5035) Datatypes now has an inference manager. This is work towards making it use the inference manager in all places where it should. In particular, this makes many of the places where conflicts are determined using `InferenceManager::conflictExp` (explained conflict) instead of `InferenceManager::conflict` + custom calls to explain in TheoryDatatypes. The goal here is to ensure that all explanations from the equality engine are managed by inference manager, which is required for proofs. --- src/theory/uf/proof_equality_engine.cpp | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/theory/uf') diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index 00e4662f9..fa9482094 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -221,6 +221,7 @@ TrustNode ProofEqEngine::assertConflict(const std::vector& exp, TrustNode ProofEqEngine::assertConflict(const std::vector& exp, ProofGenerator* pg) { + Assert(pg != nullptr); Trace("pfee") << "pfee::assertConflict " << exp << " via generator" << std::endl; return assertLemma(d_false, exp, {}, pg); @@ -306,6 +307,7 @@ TrustNode ProofEqEngine::assertLemma(Node conc, const std::vector& noExplain, ProofGenerator* pg) { + Assert(pg != nullptr); Trace("pfee") << "pfee::assertLemma " << conc << ", exp = " << exp << ", noExplain = " << noExplain << " via buffer with generator" << std::endl; -- cgit v1.2.3