From 618a3763373c4e1b0c02664082b6d3dce4070098 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 7 Jul 2016 21:03:25 -0500 Subject: [PATCH] Simplifications for strings normal forms, fix case for concat reps in normal forms. --- src/theory/strings/theory_strings.cpp | 173 +++++++++--------- src/theory/strings/theory_strings.h | 2 +- test/regress/regress0/strings/Makefile.am | 3 +- .../regress0/strings/cmu-5042-0707-2.smt2 | 15 ++ 4 files changed, 100 insertions(+), 93 deletions(-) create mode 100644 test/regress/regress0/strings/cmu-5042-0707-2.smt2 diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 493fbf1de..f6be72241 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1851,37 +1851,36 @@ void TheoryStrings::checkNormalForms(){ for( unsigned i=0; i nf; - std::vector< Node > nf_exp; - normalizeEquivalenceClass( eqc, nf, nf_exp ); + normalizeEquivalenceClass( eqc ); Trace("strings-debug") << "Finished normalizing eqc..." << std::endl; if( hasProcessed() ){ return; }else{ - Node nf_term = mkConcat( nf ); - if( nf_to_eqc.find( nf_term )!=nf_to_eqc.end() ) { - //Trace("strings-debug") << "Merge because of normal form : " << eqc << " and " << nf_to_eqc[nf_term] << " both have normal form " << nf_term << std::endl; + Node nf_term = mkConcat( d_normal_forms[eqc] ); + std::map< Node, Node >::iterator itn = nf_to_eqc.find( nf_term ); + if( itn!=nf_to_eqc.end() ){ //two equivalence classes have same normal form, merge - nf_exp.push_back( eqc_to_exp[nf_to_eqc[nf_term]] ); - Node eq = eqc.eqNode( nf_to_eqc[nf_term] ); + std::vector< Node > nf_exp; + nf_exp.push_back( mkAnd( d_normal_forms_exp[eqc] ) ); + nf_exp.push_back( eqc_to_exp[itn->second] ); + Node eq = d_normal_forms_base[eqc].eqNode( d_normal_forms_base[itn->second] ); sendInference( nf_exp, eq, "Normal_Form" ); } else { nf_to_eqc[nf_term] = eqc; - eqc_to_exp[eqc] = mkAnd( nf_exp ); + eqc_to_exp[eqc] = mkAnd( d_normal_forms_exp[eqc] ); } } Trace("strings-process-debug") << "Done verifying normal forms are the same for " << eqc << std::endl; } - - if(Trace.isOn("strings-nf")) { - Trace("strings-nf") << "**** Normal forms are : " << std::endl; - for( std::map< Node, Node >::iterator it = nf_to_eqc.begin(); it != nf_to_eqc.end(); ++it ){ - Trace("strings-nf") << " N[" << it->second << "] = " << it->first << std::endl; - //Trace("strings-nf") << " exp: " << eqc_to_exp[it->first] << std::endl; - } - Trace("strings-nf") << std::endl; - } if( !hasProcessed() ){ + if(Trace.isOn("strings-nf")) { + Trace("strings-nf") << "**** Normal forms are : " << std::endl; + for( std::map< Node, Node >::iterator it = nf_to_eqc.begin(); it != nf_to_eqc.end(); ++it ){ + Trace("strings-nf") << " N[" << it->second << "] = " << it->first << std::endl; + Trace("strings-nf") << " exp: " << eqc_to_exp[it->first] << std::endl; + } + Trace("strings-nf") << std::endl; + } checkExtendedFuncsEval( 1 ); Trace("strings-process-debug") << "Done check extended functions re-eval, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; if( !hasProcessed() ){ @@ -1900,8 +1899,8 @@ void TheoryStrings::checkNormalForms(){ } } -//nf_exp is conjunction -bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & nf, std::vector< Node > & nf_exp ) { +//compute d_normal_forms_(base,exp,exp_depend)[eqc] +bool TheoryStrings::normalizeEquivalenceClass( Node eqc ) { Trace("strings-process-debug") << "Process equivalence class " << eqc << std::endl; if( areEqual( eqc, d_emptyString ) ) { for( unsigned j=0; j & n d_normal_forms_exp[eqc].clear(); return true; } else { + Assert( d_normal_forms.find(eqc)==d_normal_forms.end() ); bool result; - if( d_normal_forms.find(eqc)==d_normal_forms.end() ){ - //phi => t = s1 * ... * sn - // normal form for each non-variable term in this eqc (s1...sn) - std::vector< std::vector< Node > > normal_forms; - // explanation for each normal form (phi) - std::vector< std::vector< Node > > normal_forms_exp; - // dependency information - std::vector< std::map< Node, std::map< bool, int > > > normal_forms_exp_depend; - // record terms for each normal form (t) - std::vector< Node > normal_form_src; - //Get Normal Forms - result = getNormalForms(eqc, normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend); - if( hasProcessed() ){ + //phi => t = s1 * ... * sn + // normal form for each non-variable term in this eqc (s1...sn) + std::vector< std::vector< Node > > normal_forms; + // explanation for each normal form (phi) + std::vector< std::vector< Node > > normal_forms_exp; + // dependency information + std::vector< std::map< Node, std::map< bool, int > > > normal_forms_exp_depend; + // record terms for each normal form (t) + std::vector< Node > normal_form_src; + //Get Normal Forms + result = getNormalForms(eqc, normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend); + if( hasProcessed() ){ + return true; + }else if( result ){ + if( processNEqc(normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend) ){ return true; - }else if( result ){ - if( processNEqc(normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend) ){ - return true; - } } - //construct the normal form - if( normal_forms.empty() ){ - Trace("strings-solve-debug2") << "construct the normal form" << std::endl; - getConcatVec( eqc, nf ); - d_normal_forms_base[eqc] = eqc; - }else{ - int nf_index = 0; - //nf.insert( nf.end(), normal_forms[nf_index].begin(), normal_forms[nf_index].end() ); - //nf_exp.insert( nf_exp.end(), normal_forms_exp[nf_index].begin(), normal_forms_exp[nf_index].end() ); - //Trace("strings-solve-debug2") << "take normal form ... done" << std::endl; - //d_normal_forms_base[eqc] = normal_form_src[nf_index]; - ///* - std::vector< Node >::iterator itn = std::find( normal_form_src.begin(), normal_form_src.end(), eqc ); - if( itn!=normal_form_src.end() ){ - nf_index = itn - normal_form_src.begin(); - Trace("strings-solve-debug2") << "take normal form " << nf_index << std::endl; - Assert( normal_form_src[nf_index]==eqc ); - }else{ - //just take the first normal form - Trace("strings-solve-debug2") << "take the first normal form" << std::endl; - } - nf.insert( nf.end(), normal_forms[nf_index].begin(), normal_forms[nf_index].end() ); - nf_exp.insert( nf_exp.end(), normal_forms_exp[nf_index].begin(), normal_forms_exp[nf_index].end() ); - if( eqc!=normal_form_src[nf_index] ){ - nf_exp.push_back( eqc.eqNode( normal_form_src[nf_index] ) ); - } - 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::iterator itn = std::find( normal_form_src.begin(), normal_form_src.end(), eqc ); + if( itn!=normal_form_src.end() ){ + nf_index = itn - normal_form_src.begin(); + Trace("strings-solve-debug2") << "take normal form " << nf_index << std::endl; + Assert( normal_form_src[nf_index]==eqc ); + }else{ + //just take the first normal form + Trace("strings-solve-debug2") << "take the first normal form" << std::endl; + } + d_normal_forms[eqc].insert( d_normal_forms[eqc].end(), normal_forms[nf_index].begin(), normal_forms[nf_index].end() ); + d_normal_forms_exp[eqc].insert( d_normal_forms_exp[eqc].end(), normal_forms_exp[nf_index].begin(), normal_forms_exp[nf_index].end() ); + if( eqc!=normal_form_src[nf_index] ){ + d_normal_forms_exp[eqc].push_back( eqc.eqNode( normal_form_src[nf_index] ) ); + } + 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& curr, std::vector< Node >& exp ); //normal forms check void checkNormalForms(); - bool normalizeEquivalenceClass( Node n, std::vector< Node > & nf, std::vector< Node > & nf_exp ); + bool normalizeEquivalenceClass( Node n ); bool 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); bool detectLoop(std::vector< std::vector< Node > > &normal_forms, diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index d23fd866d..bb9b61d8e 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -79,7 +79,8 @@ TESTS = \ strings-native-simple.cvc \ cmu-2db2-extf-reg.smt2 \ norn-nel-bug-052116.smt2 \ - cmu-disagree-0707-dd.smt2 + cmu-disagree-0707-dd.smt2 \ + cmu-5042-0707-2.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/strings/cmu-5042-0707-2.smt2 b/test/regress/regress0/strings/cmu-5042-0707-2.smt2 new file mode 100644 index 000000000..637142dfb --- /dev/null +++ b/test/regress/regress0/strings/cmu-5042-0707-2.smt2 @@ -0,0 +1,15 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(set-option :strings-exp true) + +(declare-fun key2 () String) +(declare-fun key1 () String) + +(assert +(and +(not +(str.contains (str.++ (str.replace (str.substr key2 0 (- (+ (str.indexof key2 "X" 0) 1) 0)) "X" "x") (str.++ (str.replace (str.substr (str.substr key2 (+ (str.indexof key2 "X" 0) 1) (- (str.len key2) (+ (str.indexof key2 "X" 0) 1))) 0 (- (+ (str.indexof (str.substr key2 (+ (str.indexof key2 "X" 0) 1) (- (str.len key2) (+ (str.indexof key2 "X" 0) 1))) "X" 0) 1) 0)) "X" "x") (str.substr (str.substr key2 (+ (str.indexof key2 "X" 0) 1) (- (str.len key2) (+ (str.indexof key2 "X" 0) 1))) (+ (str.indexof (str.substr key2 (+ (str.indexof key2 "X" 0) 1) (- (str.len key2) (+ (str.indexof key2 "X" 0) 1))) "X" 0) 1) (- (str.len (str.substr key2 (+ (str.indexof key2 "X" 0) 1) (- (str.len key2) (+ (str.indexof key2 "X" 0) 1)))) (+ (str.indexof (str.substr key2 (+ (str.indexof key2 "X" 0) 1) (- (str.len key2) (+ (str.indexof key2 "X" 0) 1))) "X" 0) 1))))) "Z")) +(str.contains (str.substr key2 (+ (str.indexof key2 "X" 0) 1) (- (str.len key2) (+ (str.indexof key2 "X" 0) 1))) "X"))) + +(check-sat) + -- 2.30.2