diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-09-30 11:43:20 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-30 16:53:07 -0400 |
| commit | e2cf7d57b2dc6b33fa305cdfec2f20cb4231a57f (patch) | |
| tree | 7ad136f95eab86337ceec202b6f26441b8fdb312 /src | |
| parent | 0c2eafec69b694a507ac914bf285fe0574be085f (diff) | |
fixed a loop bug
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 7d5edd0f7..b3255c034 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -427,6 +427,7 @@ void TheoryStrings::check(Effort e) { } } } + Trace("strings-check") << "Theory of strings, done check : " << e << std::endl; Trace("strings-process") << "Theory of strings, done check : " << e << std::endl; } @@ -768,6 +769,7 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v d_infer.push_back(eq); d_infer_exp.push_back(eq_exp); return; + }else if( ( normal_forms[i][index_i].getKind()!=kind::CONST_STRING && index_i==normal_forms[i].size()-1 ) || ( normal_forms[j][index_j].getKind()!=kind::CONST_STRING && index_j==normal_forms[j].size()-1 ) ){ Trace("strings-solve-debug") << "Case 3 : at endpoint" << std::endl; @@ -785,10 +787,14 @@ void TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v } eqn.push_back( mkConcat( eqnc ) ); } - conc = eqn[0].eqNode( eqn[1] ); - Node ant = mkExplain( antec, antec_new_lits ); - sendLemma( ant, conc, "Endpoint" ); - return; + if( areEqual( eqn[0], eqn[1] ) ){ + addNormalFormPair( normal_form_src[i], normal_form_src[j] ); + }else{ + conc = eqn[0].eqNode( eqn[1] ); + Node ant = mkExplain( antec, antec_new_lits ); + sendLemma( ant, conc, "Endpoint" ); + return; + } }else{ Trace("strings-solve-debug") << "Case 4 : must compare strings" << std::endl; Node conc; |