diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-10-23 11:45:34 -0500 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-10-23 11:45:34 -0500 |
| commit | 1d5c0a5347e8389e2c40fc5fe0373ff36d151991 (patch) | |
| tree | 7e5e2070311ef22397a14fc412d0cfd9209288c8 /src | |
| parent | 152e3546328f5aa327fe54463f2214497596422b (diff) | |
bug fix for loop rule
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 11024e351..7c3e7ebbc 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -991,8 +991,15 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v //try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop sendSplit( normal_forms[loop_n_index][loop_index], d_emptyString, "Loop Empty" ); return true; - }else{ + } else if( !areDisequal( t_yz, d_emptyString ) ) { + //TODO........... + //try to make normal_forms[loop_n_index][loop_index] equal to empty to avoid loop + sendSplit( t_yz, d_emptyString, "Loop Empty" ); + return true; + } else { //need to break + antec.push_back( normal_forms[loop_n_index][loop_index].eqNode( d_emptyString ).negate() ); + antec.push_back( t_yz.eqNode( d_emptyString ).negate() ); Node ant = mkExplain( antec, antec_new_lits ); Node str_in_re; if( s_zy == t_yz && |