From 1d5c0a5347e8389e2c40fc5fe0373ff36d151991 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Wed, 23 Oct 2013 11:45:34 -0500 Subject: [PATCH] bug fix for loop rule --- src/theory/strings/theory_strings.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) 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 && -- 2.30.2