diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-02-11 15:55:31 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-11 15:55:31 +0100 |
commit | 1d0492104a200f6fa5cc7a1cee539436ee26ea99 (patch) | |
tree | a66ff6b0bc869f1e84dceb03ddbcc7910e23c77c /src/theory/strings/theory_strings.cpp | |
parent | b3f05d5c25facaf0c34ee79faed060bda3f61a8d (diff) |
Merge InferenceIds into one enum (#5892)
This PR is the first step in consolidating the various variants of Inferences, InferenceIds and InferenceManagers of the theories.
It merges all InferencedIds into one global enum and makes all theories use them.
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index f25f9e29c..48d461f7a 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -921,7 +921,7 @@ void TheoryStrings::checkCodes() if (!d_state.areEqual(cc, vc)) { std::vector<Node> emptyVec; - d_im.sendInference(emptyVec, cc.eqNode(vc), Inference::CODE_PROXY); + d_im.sendInference(emptyVec, cc.eqNode(vc), InferenceId::STRINGS_CODE_PROXY); } const_codes.push_back(vc); } @@ -961,7 +961,7 @@ void TheoryStrings::checkCodes() deq = Rewriter::rewrite(deq); d_im.addPendingPhaseRequirement(deq, false); std::vector<Node> emptyVec; - d_im.sendInference(emptyVec, inj_lem, Inference::CODE_INJ); + d_im.sendInference(emptyVec, inj_lem, InferenceId::STRINGS_CODE_INJ); } } } |