From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Tue, 13 May 2014 02:02:24 +0000 (-0500)
Subject: Fix a bug in the IndexOf function.
X-Git-Tag: cvc5-1.0.0~6907^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=053b6958efcfcbecc0f44a23cd3bd340d5647785;p=cvc5.git

Fix a bug in the IndexOf function.
---

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index be419a36a..a26d00925 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -196,18 +196,24 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     d_cache[t] = t;
   } else if( t.getKind() == kind::STRING_STRIDOF ) {
     if(options::stringExp()) {
-      Node sk1 = NodeManager::currentNM()->mkSkolem( "io1", t[0].getType(), "created for indexof" );
-      Node sk2 = NodeManager::currentNM()->mkSkolem( "io2", t[0].getType(), "created for indexof" );
-      Node sk3 = NodeManager::currentNM()->mkSkolem( "io3", t[0].getType(), "created for indexof" );
-      Node sk4 = NodeManager::currentNM()->mkSkolem( "io4", t[0].getType(), "created for indexof" );
-      Node skk = NodeManager::currentNM()->mkSkolem( "iok", t[2].getType(), "created for indexof" );
+      Node sk1 = NodeManager::currentNM()->mkSkolem( "io1", NodeManager::currentNM()->stringType(), "created for indexof" );
+      Node sk2 = NodeManager::currentNM()->mkSkolem( "io2", NodeManager::currentNM()->stringType(), "created for indexof" );
+      Node sk3 = NodeManager::currentNM()->mkSkolem( "io3", NodeManager::currentNM()->stringType(), "created for indexof" );
+      Node sk4 = NodeManager::currentNM()->mkSkolem( "io4", NodeManager::currentNM()->stringType(), "created for indexof" );
+      Node skk = NodeManager::currentNM()->mkSkolem( "iok", NodeManager::currentNM()->integerType(), "created for indexof" );
       Node eq = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3, sk4 ) );
       new_nodes.push_back( eq );
       Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
       Node krange = NodeManager::currentNM()->mkNode( kind::GEQ, skk, negone );
       new_nodes.push_back( krange );
-      krange = NodeManager::currentNM()->mkNode( kind::GT,
-            NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), skk);
+      krange = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GT,
+            NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), skk) );
+      new_nodes.push_back( krange );
+      krange = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GT,
+            NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[1] ), d_zero) );
+      new_nodes.push_back( krange );
+      krange = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GEQ,
+            t[2], d_zero) );
       new_nodes.push_back( krange );
 
       //str.len(s1) < y + str.len(s2)
@@ -224,7 +230,13 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
       //t3 = s2
       Node c4 = t[1].eqNode( sk3 );
       //~contain(t2, s2)
-      Node c5 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, sk2, t[1] ).negate();
+      Node c5 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, 
+                  NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sk2,
+                    NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, t[1], d_zero,
+                      NodeManager::currentNM()->mkNode(kind::MINUS,
+                        NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, t[1]),
+                        NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) )))),
+                  t[1] ).negate();
       //k=str.len(s1, s2)
       Node c6 = skk.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH,
                   NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2 )));