From fa24a2bf6b511c4db580ded8cd4dec0792a1b392 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Fri, 24 Jan 2014 22:32:45 -0600 Subject: [PATCH] minor fix, indexof rewriter opt --- src/theory/strings/theory_strings_preprocess.cpp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 1d55fb193..11642a4d2 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -267,11 +267,10 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node cond = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, x, y ); Node c1 = x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, y, sk2 ) ); Node c2 = skw.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, z, sk2 ) ); - Node iof = NodeManager::currentNM()->mkNode( kind::STRING_STRIDOF, x, y, zero ); - Node c3 = iof.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) ); - Node rr = NodeManager::currentNM()->mkNode( kind::ITE, cond, + Node c3 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, sk1, y ).negate(); + Node rr = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, NodeManager::currentNM()->mkNode( kind::AND, c1, c2, c3 ), - skw.eqNode(x) ); + skw.eqNode(x) ) ); new_nodes.push_back( rr ); d_cache[t] = skw; retNode = skw; -- 2.30.2