diff options
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 16 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.h | 2 |
2 files changed, 14 insertions, 4 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 5179ddab3..d02f079a9 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3083,15 +3083,21 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal Trace("strings-solve-debug") << "Non-simple Case 2 : must compare strings" << std::endl; int loop_in_i = -1; int loop_in_j = -1; + bool loopDetected = false; if( detectLoop( normal_forms, i, j, index, loop_in_i, loop_in_j, rproc ) ){ if( !isRev ){ //FIXME getExplanationVectorForPrefixEq( normal_forms, normal_form_src, normal_forms_exp, normal_forms_exp_depend, i, j, -1, -1, isRev, info.d_ant ); //set info - if( processLoop( normal_forms, normal_form_src, i, j, loop_in_i!=-1 ? i : j, loop_in_i!=-1 ? j : i, loop_in_i!=-1 ? loop_in_i : loop_in_j, index, info ) ){ + bool loopSuccess; + if( processLoop( normal_forms, normal_form_src, i, j, loop_in_i!=-1 ? i : j, loop_in_i!=-1 ? j : i, loop_in_i!=-1 ? loop_in_i : loop_in_j, index, info, loopSuccess) ){ info_valid = true; } + if (loopSuccess) + loopDetected = true; } - }else{ + } + + if (!loopDetected) { //AJR: length entailment here? if( normal_forms[i][index].getKind() == kind::CONST_STRING || normal_forms[j][index].getKind() == kind::CONST_STRING ){ unsigned const_k = normal_forms[i][index].getKind() == kind::CONST_STRING ? i : j; @@ -3312,7 +3318,8 @@ bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms //xs(zy)=t(yz)xr bool TheoryStrings::processLoop( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, - int i, int j, int loop_n_index, int other_n_index, int loop_index, int index, InferInfo& info ){ + int i, int j, int loop_n_index, int other_n_index, int loop_index, int index, InferInfo& info, bool& loopSuccess){ + loopSuccess = true; if( options::stringAbortLoop() ){ std::stringstream ss; ss << "Looping word equation encountered." << std::endl; @@ -3464,6 +3471,9 @@ bool TheoryStrings::processLoop( std::vector< std::vector< Node > > &normal_form } else { + loopSuccess = false; + return false; + Trace("strings-loop") << "Strings::Loop: Normal Loop Breaking." << std::endl; // right diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index aa86f1bc1..6bf721e1d 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -521,7 +521,7 @@ private: 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, int i, int j, int index, int &loop_in_i, int &loop_in_j, unsigned rproc ); bool processLoop( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, - int i, int j, int loop_n_index, int other_n_index,int loop_index, int index, InferInfo& info ); + int i, int j, int loop_n_index, int other_n_index,int loop_index, int index, InferInfo& info, bool& loopSuccess ); void processNEqc( 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 ); void processReverseNEq( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src, |