From 0e956da9b32ce8a8fcf20ec65e5a2820b4e31324 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 7 Dec 2016 10:18:16 -0600
Subject: [PATCH] Fix nf exp tracking for non-linear string equalities, fixes
 bug 768.

---
 src/theory/strings/theory_strings.cpp     | 40 +++++++++++++++--------
 test/regress/regress0/strings/Makefile.am |  3 +-
 test/regress/regress0/strings/bug768.smt2 | 10 ++++++
 3 files changed, 38 insertions(+), 15 deletions(-)
 create mode 100644 test/regress/regress0/strings/bug768.smt2

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 8b44b5cac..db07a0b51 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -2071,6 +2071,27 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc ) {
   }
 }
 
+void trackNfExpDependency( std::vector< Node >& nf_exp_n, std::map< Node, std::map< bool, int > >& nf_exp_depend_n, Node exp, int new_val, int new_rev_val ){
+  if( std::find( nf_exp_n.begin(), nf_exp_n.end(), exp )==nf_exp_n.end() ){
+    nf_exp_n.push_back( exp );
+  }
+  for( unsigned k=0; k<2; k++ ){
+    int val = k==0 ? new_val : new_rev_val;
+    std::map< bool, int >::iterator itned = nf_exp_depend_n[exp].find( k==1 );
+    if( itned==nf_exp_depend_n[exp].end() ){
+      Trace("strings-process-debug") << "Deps : set dependency on " << exp << " to " << val << " isRev=" << (k==0) << std::endl;
+      nf_exp_depend_n[exp][k==1] = val;
+    }else{
+      Trace("strings-process-debug") << "Deps : Multiple dependencies on " << exp << " : " << itned->second << " " << val << " isRev=" << (k==0) << std::endl;
+      //if we already have a dependency (in the case of non-linear string equalities), it is min/max
+      bool cmp = val > itned->second;
+      if( cmp==(k==1) ){
+        nf_exp_depend_n[exp][k==1] = val;
+      }
+    }
+  }
+}
+
 void TheoryStrings::getNormalForms( Node &eqc, std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
                                     std::vector< std::vector< Node > > &normal_forms_exp, std::vector< std::map< Node, std::map< bool, int > > >& normal_forms_exp_depend ) {
   //constant for equivalence class
@@ -2115,25 +2136,16 @@ void TheoryStrings::getNormalForms( Node &eqc, std::vector< std::vector< Node >
 
             for( unsigned j=0; j<d_normal_forms_exp[nr].size(); j++ ){
               Node exp = d_normal_forms_exp[nr][j];
-              nf_exp_n.push_back( exp );
               //track depends
-              for( unsigned k=0; k<2; k++ ){
-                int prev_dep = d_normal_forms_exp_depend[nr][exp][k==1];
-                if( k==0 ){
-                  nf_exp_depend_n[exp][false] = orig_size + prev_dep;
-                }else if( k==1 ){
-                  //store forward index (converted back to reverse index below)
-                  nf_exp_depend_n[exp][true] = orig_size + ( add_size - prev_dep );
-                }
-              }
+              trackNfExpDependency( nf_exp_n, nf_exp_depend_n, exp,
+                                    orig_size + d_normal_forms_exp_depend[nr][exp][false], 
+                                    orig_size + ( add_size - d_normal_forms_exp_depend[nr][exp][true] ) );
             }
             if( d_normal_forms_base[nr]!=n[i] ){
               Assert( d_normal_forms_base.find( nr )!=d_normal_forms_base.end() );
               Node eq = n[i].eqNode( d_normal_forms_base[nr] );
-              nf_exp_n.push_back( eq );
-              //track depends
-              nf_exp_depend_n[eq][false] = orig_size;
-              nf_exp_depend_n[eq][true] = orig_size + add_size;
+              //track depends : entire current segment is dependent upon base equality
+              trackNfExpDependency( nf_exp_n, nf_exp_depend_n, eq, orig_size, orig_size + add_size );
             }
           }
           //convert forward indices to reverse indices
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 70fec7b82..a77c2bd6c 100644
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -84,7 +84,8 @@ TESTS = \
   cmu-substr-rw.smt2 \
   gm-inc-071516-2.smt2 \
   cmu-inc-nlpp-071516.smt2 \
-  strings-index-empty.smt2
+  strings-index-empty.smt2 \
+  bug768.smt2
 
 FAILING_TESTS =
 
diff --git a/test/regress/regress0/strings/bug768.smt2 b/test/regress/regress0/strings/bug768.smt2
new file mode 100644
index 000000000..be3f24200
--- /dev/null
+++ b/test/regress/regress0/strings/bug768.smt2
@@ -0,0 +1,10 @@
+(set-logic QF_S)
+(set-info :status sat)
+(declare-fun f0 () String)
+(declare-fun c0 () String)
+(declare-fun f1 () String)
+(declare-fun f2 () String)
+
+(assert (= (str.++ f0 f1 f0 c0 f1 c0 f2 f2) "f(,f(c,c))"))
+
+(check-sat)
-- 
2.30.2