diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-14 02:52:28 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-14 00:52:28 -0700 |
| commit | 21439d98e9afe1541bb0f5371c4ab0011666bd5e (patch) | |
| tree | 4d7d96a58350aae1177c3711d8cd90676bc53820 /src/theory/uf | |
| parent | 3a8a27994584ca2168ef71d5eb0ce46ef558ba34 (diff) | |
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.
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/proof_equality_engine.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
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<Node>& exp, TrustNode ProofEqEngine::assertConflict(const std::vector<Node>& 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<Node>& noExplain, ProofGenerator* pg) { + Assert(pg != nullptr); Trace("pfee") << "pfee::assertLemma " << conc << ", exp = " << exp << ", noExplain = " << noExplain << " via buffer with generator" << std::endl; |