diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-06-13 13:08:15 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-06-13 13:08:15 -0500 |
commit | f61ad6919fc80cbc19fde9c295beb5082a6e0d79 (patch) | |
tree | 0ccbd5e336fec5a23e716ba5d05473029dee4def | |
parent | c324e6a40974040c02c8c9f948dbb332401b624c (diff) |
Shorten explanation for strings inference I_Norm_S (#3051)
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 67f032193..ba0c16d02 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1464,6 +1464,7 @@ void TheoryStrings::checkInit() { Trace("strings-process-debug") << " congruent term by singular : " << n << " " << c[0] << std::endl; //singular case if( !areEqual( c[0], n ) ){ + Node ns; std::vector< Node > exp; //explain empty components bool foundNEmpty = false; @@ -1474,15 +1475,13 @@ void TheoryStrings::checkInit() { } }else{ Assert( !foundNEmpty ); - if( n[i]!=c[0] ){ - exp.push_back( n[i].eqNode( c[0] ) ); - } + ns = n[i]; foundNEmpty = true; } } AlwaysAssert( foundNEmpty ); //infer the equality - sendInference( exp, n.eqNode( c[0] ), "I_Norm_S" ); + sendInference(exp, n.eqNode(ns), "I_Norm_S"); } d_congruent.insert( n ); congruent[k]++; |