diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-07 10:18:16 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-07 10:18:16 -0600 |
commit | 0e956da9b32ce8a8fcf20ec65e5a2820b4e31324 (patch) | |
tree | 97d5d40da911ce9bd5f458e301b381986e7cba40 | |
parent | 4db65cbaf87f87dba3682e88563f5a923f265152 (diff) |
Fix nf exp tracking for non-linear string equalities, fixes bug 768.
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 40 | ||||
-rw-r--r-- | test/regress/regress0/strings/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/strings/bug768.smt2 | 10 |
3 files changed, 38 insertions, 15 deletions
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) |