diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-29 18:29:15 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-01-29 20:29:15 -0600 |
commit | e3361a428a1b24369d782120de1f050874a8ac44 (patch) | |
tree | 2ded393febd12e43d7548c0872fb99ffa52989ee | |
parent | 33cabd5c723d33a5aa4c85856af83b141cbbbd87 (diff) |
Better heuristics for marking congruent variables (#3677)
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 21 |
1 files changed, 17 insertions, 4 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 7b1b34917..755e6b4df 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1401,11 +1401,24 @@ void TheoryStrings::checkInit() { } }else{ if( d_congruent.find( n )==d_congruent.end() ){ - if( var.isNull() ){ + // We mark all but the oldest variable in the equivalence class as + // congruent. + if (var.isNull()) + { var = n; - }else{ - Trace("strings-process-debug") << " congruent variable : " << n << std::endl; - d_congruent.insert( n ); + } + else if (var > n) + { + Trace("strings-process-debug") + << " congruent variable : " << var << std::endl; + d_congruent.insert(var); + var = n; + } + else + { + Trace("strings-process-debug") + << " congruent variable : " << n << std::endl; + d_congruent.insert(n); } } } |