diff options
author | Gereon Kremer <gkremer@stanford.edu> | 2021-02-17 15:39:42 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-17 15:39:42 +0100 |
commit | fb5e3113312322c21a00062b22c358c30fa27101 (patch) | |
tree | e3809bd67d9f897f5d99b90a8c514acad6ff1976 /src/theory/arrays/inference_manager.cpp | |
parent | 2d6de44a51fed47a625ae73181efbcc3dac0c751 (diff) |
Add InferenceIds for theory of arrays (#5910)
This PR introduces new InferenceIds for the theory of arrays and uses them instead of InferenceId::UNKNOWN.
Diffstat (limited to 'src/theory/arrays/inference_manager.cpp')
-rw-r--r-- | src/theory/arrays/inference_manager.cpp | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp index be2972444..afcc9a719 100644 --- a/src/theory/arrays/inference_manager.cpp +++ b/src/theory/arrays/inference_manager.cpp @@ -37,8 +37,9 @@ InferenceManager::InferenceManager(Theory& t, bool InferenceManager::assertInference(TNode atom, bool polarity, + InferenceId id, TNode reason, - PfRule id) + PfRule pfr) { Trace("arrays-infer") << "TheoryArrays::assertInference: " << (polarity ? Node(atom) : atom.notNode()) << " by " @@ -52,14 +53,14 @@ bool InferenceManager::assertInference(TNode atom, std::vector<Node> children; std::vector<Node> args; // convert to proof rule application - convert(id, fact, reason, children, args); - return assertInternalFact(atom, polarity, InferenceId::UNKNOWN, id, children, args); + convert(pfr, fact, reason, children, args); + return assertInternalFact(atom, polarity, id, pfr, children, args); } - return assertInternalFact(atom, polarity, InferenceId::UNKNOWN, reason); + return assertInternalFact(atom, polarity, id, reason); } bool InferenceManager::arrayLemma( - Node conc, Node exp, PfRule id, LemmaProperty p, bool doCache) + Node conc, InferenceId id, Node exp, PfRule pfr, LemmaProperty p, bool doCache) { Trace("arrays-infer") << "TheoryArrays::arrayLemma: " << conc << " by " << exp << "; " << id << std::endl; @@ -69,14 +70,14 @@ bool InferenceManager::arrayLemma( std::vector<Node> children; std::vector<Node> args; // convert to proof rule application - convert(id, conc, exp, children, args); + convert(pfr, 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, InferenceId::UNKNOWN, p, doCache); + TrustNode tlem = d_lemmaPg->mkTrustNode(conc, pfr, children, args); + return trustedLemma(tlem, id, p, doCache); } // send lemma without proofs Node lem = nm->mkNode(IMPLIES, exp, conc); - return lemma(lem, InferenceId::UNKNOWN, p, doCache); + return lemma(lem, id, p, doCache); } void InferenceManager::convert(PfRule& id, |