diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-03 10:02:34 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-03 10:02:34 -0600 |
commit | ea514f2aa787998ac31f8546bd202890f6bac056 (patch) | |
tree | ce10881d55132e86285c1ec5194890d80d185d33 /src/theory | |
parent | dd67a250541d28d2a6fdaee02c9ae71fea272f87 (diff) |
Add missing code to track dependencies recursively for string explanations as well.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index d8a46f0ed..9f474a3ca 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1747,10 +1747,18 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & n Trace("strings-solve-debug2") << "take normal form ... done" << std::endl; d_normal_forms_base[eqc] = normal_form_src[nf_index]; //*/ + //track dependencies + for( unsigned i=0; i<normal_forms_exp[nf_index].size(); i++ ){ + Node exp = normal_forms_exp[nf_index][i]; + for( unsigned r=0; r<2; r++ ){ + d_normal_forms_exp_depend[eqc][exp][r==0] = normal_forms_exp_depend[nf_index][exp][r==0]; + } + } } d_normal_forms[eqc].insert( d_normal_forms[eqc].end(), nf.begin(), nf.end() ); d_normal_forms_exp[eqc].insert( d_normal_forms_exp[eqc].end(), nf_exp.begin(), nf_exp.end() ); + Trace("strings-process-debug") << "Return process equivalence class " << eqc << " : returned, size = " << nf.size() << std::endl; }else{ Trace("strings-process-debug") << "Return process equivalence class " << eqc << " : already computed, size = " << d_normal_forms[eqc].size() << std::endl; @@ -1811,7 +1819,7 @@ bool TheoryStrings::getNormalForms( Node &eqc, std::vector< std::vector< Node > if( k==0 ){ nf_exp_depend_n[exp][false] = orig_size + prev_dep; }else if( k==1 ){ - //store forward index (restored to reverse index below) + //store forward index (converted back to reverse index below) nf_exp_depend_n[exp][true] = orig_size + ( add_size - prev_dep ); } } |