From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Thu, 30 Jan 2020 02:29:15 +0000 (-0800)
Subject: Better heuristics for marking congruent variables (#3677)
X-Git-Tag: cvc5-1.0.0~3713
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e3361a428a1b24369d782120de1f050874a8ac44;p=cvc5.git

Better heuristics for marking congruent variables (#3677)
---

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);
             }
           }
         }