diff options
author | Gereon Kremer <gkremer@stanford.edu> | 2021-02-11 21:25:50 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-11 21:25:50 +0100 |
commit | e8333750e5932ab5ce9a8a491b53aef4ffa4b0aa (patch) | |
tree | a6de942fd32afb4dcb67d33884cdff7252c6f14f /src/theory/arrays | |
parent | f5486884229348516ac26300273e4f5458a74208 (diff) |
Make most methods of TheoryInferenceManager expect an InferenceId. (#5897)
This PR makes most methods of the TheoryInferenceManager expect an InferenceId.
All classes that inherit from TheoryInferenceManager are adapted accordingly and InferenceIds are passed everywhere.
In some cases, there are no appropriate InferenceIds yet. We use InferenceId::UNKNOWN for the time being and introduce proper values in future PRs.
The InferenceIds are not yet used, but will be used for statistics and debug output.
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/inference_manager.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp index f2c805d38..be2972444 100644 --- a/src/theory/arrays/inference_manager.cpp +++ b/src/theory/arrays/inference_manager.cpp @@ -53,9 +53,9 @@ bool InferenceManager::assertInference(TNode atom, std::vector<Node> args; // convert to proof rule application convert(id, fact, reason, children, args); - return assertInternalFact(atom, polarity, id, children, args); + return assertInternalFact(atom, polarity, InferenceId::UNKNOWN, id, children, args); } - return assertInternalFact(atom, polarity, reason); + return assertInternalFact(atom, polarity, InferenceId::UNKNOWN, reason); } bool InferenceManager::arrayLemma( @@ -72,11 +72,11 @@ bool InferenceManager::arrayLemma( convert(id, conc, exp, children, args); // make the trusted lemma based on the eager proof generator and send TrustNode tlem = d_lemmaPg->mkTrustNode(conc, id, children, args); - return trustedLemma(tlem, p, doCache); + return trustedLemma(tlem, InferenceId::UNKNOWN, p, doCache); } // send lemma without proofs Node lem = nm->mkNode(IMPLIES, exp, conc); - return lemma(lem, p, doCache); + return lemma(lem, InferenceId::UNKNOWN, p, doCache); } void InferenceManager::convert(PfRule& id, |