diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-19 09:26:36 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-19 09:26:36 -0600 |
| commit | c4822869beac8d4a0eac4b234e0662d3db49f995 (patch) | |
| tree | d34b86c54b0ac8de6df4734e1e76afa5f43d5efb /src/theory/arrays/inference_manager.cpp | |
| parent | 00479d03cdeac3e864a1930dddb16c71c5bf2ce9 (diff) | |
Refactoring theory inference process (#5920)
This PR refactors TheoryInference so that it is not responsible for calling back into InferenceManager, instead it sets data so that InferenceManagerBuffered has enough information to do this itself. It also makes the decision of whether to cache lemmas in theory inference manager a global choice per-theory instead of per-lemma.
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, |