diff options
Diffstat (limited to 'src/theory/arrays/inference_manager.cpp')
| -rw-r--r-- | src/theory/arrays/inference_manager.cpp | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp index a4b8ecd44..96f2b02c3 100644 --- a/src/theory/arrays/inference_manager.cpp +++ b/src/theory/arrays/inference_manager.cpp @@ -27,9 +27,10 @@ namespace arrays { InferenceManager::InferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm) - : TheoryInferenceManager(t, state, pnm, "theory::arrays"), - d_lemmaPg(pnm ? new EagerProofGenerator( - pnm, state.getUserContext(), "ArrayLemmaProofGenerator") + : TheoryInferenceManager(t, state, pnm, "theory::arrays", false), + d_lemmaPg(pnm ? new EagerProofGenerator(pnm, + state.getUserContext(), + "ArrayLemmaProofGenerator") : nullptr) { } @@ -59,7 +60,7 @@ bool InferenceManager::assertInference(TNode atom, } bool InferenceManager::arrayLemma( - Node conc, InferenceId id, Node exp, PfRule pfr, LemmaProperty p, bool doCache) + Node conc, InferenceId id, Node exp, PfRule pfr, LemmaProperty p) { Trace("arrays-infer") << "TheoryArrays::arrayLemma: " << conc << " by " << exp << "; " << id << std::endl; @@ -72,11 +73,11 @@ bool InferenceManager::arrayLemma( convert(pfr, conc, exp, children, args); // make the trusted lemma based on the eager proof generator and send TrustNode tlem = d_lemmaPg->mkTrustNode(conc, pfr, children, args); - return trustedLemma(tlem, id, p, doCache); + return trustedLemma(tlem, id, p); } // send lemma without proofs Node lem = nm->mkNode(IMPLIES, exp, conc); - return lemma(lem, id, p, doCache); + return lemma(lem, id, p); } void InferenceManager::convert(PfRule& id, |