diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-06 19:00:13 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-06 19:00:13 -0500 |
commit | fab7010523fd2e635c2c9dfd382acdefdb96d6b4 (patch) | |
tree | d69370211e672c9d32534a39d01d6108c24e2261 /src/theory/strings/theory_strings.cpp | |
parent | 45e489e2d48e3edde15be2187e32893fc35d859b (diff) |
Enum for all remaining string inferences (#4220)
Merges the Flat Form inferences enum into Inferences. Adds documentation for (most of) these inferences. Removes the old infrastructure for inferences based on a debug string in InferenceManager.
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 92116582f..da8c3583d 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1014,7 +1014,7 @@ void TheoryStrings::checkCodes() Node vc = nm->mkNode(STRING_TO_CODE, cp); if (!d_state.areEqual(cc, vc)) { - d_im.sendInference(d_empty_vec, cc.eqNode(vc), "Code_Proxy"); + d_im.sendInference(d_empty_vec, cc.eqNode(vc), Inference::CODE_PROXY); } const_codes.push_back(vc); } @@ -1052,7 +1052,7 @@ void TheoryStrings::checkCodes() // str.code(x)==-1 V str.code(x)!=str.code(y) V x==y Node inj_lem = nm->mkNode(kind::OR, eq_no, deq, eqn); d_im.sendPhaseRequirement(deq, false); - d_im.sendInference(d_empty_vec, inj_lem, "Code_Inj"); + d_im.sendInference(d_empty_vec, inj_lem, Inference::CODE_INJ); } } } |