diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-06-10 15:51:21 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-06-10 15:51:21 -0500 |
commit | 736713253104bcc5c3c0e19b0abcda4d20c68ab7 (patch) | |
tree | b9762b3e1155f870c92b746d16bb12e3a3d88a16 | |
parent | 6b01e8740111e69219e5d733e1123955f8cd2ea7 (diff) |
Optimization for strings normalize disequalities (#3047)
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 34 |
1 files changed, 22 insertions, 12 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 1947f1730..67f032193 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -4468,19 +4468,29 @@ void TheoryStrings::checkNormalFormsDeq() for( unsigned j=0; j<cols[i].size(); j++ ){ for( unsigned k=(j+1); k<cols[i].size(); k++ ){ //for strings that are disequal, but have the same length - if( areDisequal( cols[i][j], cols[i][k] ) ){ - Assert( !d_conflict ); - if (Trace.isOn("strings-solve")) + if (cols[i][j].isConst() && cols[i][k].isConst()) + { + // if both are constants, they should be distinct, and its trivial + Assert(cols[i][j] != cols[i][k]); + } + else + { + if (areDisequal(cols[i][j], cols[i][k])) { - Trace("strings-solve") << "- Compare " << cols[i][j] << " "; - printConcat(getNormalForm(cols[i][j]).d_nf, "strings-solve"); - Trace("strings-solve") << " against " << cols[i][k] << " "; - printConcat(getNormalForm(cols[i][k]).d_nf, "strings-solve"); - Trace("strings-solve") << "..." << std::endl; - } - processDeq( cols[i][j], cols[i][k] ); - if( hasProcessed() ){ - return; + Assert(!d_conflict); + if (Trace.isOn("strings-solve")) + { + Trace("strings-solve") << "- Compare " << cols[i][j] << " "; + printConcat(getNormalForm(cols[i][j]).d_nf, "strings-solve"); + Trace("strings-solve") << " against " << cols[i][k] << " "; + printConcat(getNormalForm(cols[i][k]).d_nf, "strings-solve"); + Trace("strings-solve") << "..." << std::endl; + } + processDeq(cols[i][j], cols[i][k]); + if (hasProcessed()) + { + return; + } } } } |