Substr fix: (= (str.substr "" 0 3) "xxx") should be SAT in the defintion of SMT-Lib

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index d0876d983efea9c76ba17e812c6c2ca034c600a1..58344964cc0556307547fc08d09b2459001484c6 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -54,8 +54,8 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
     d_equalityEngine.addFunctionKind(kind::STRING_LENGTH);
     d_equalityEngine.addFunctionKind(kind::STRING_CONCAT);
     d_equalityEngine.addFunctionKind(kind::STRING_STRCTN);
-    d_equalityEngine.addFunctionKind(kind::STRING_CHARAT);
-    d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR);
+    //d_equalityEngine.addFunctionKind(kind::STRING_CHARAT);
+    //d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR);
 
     d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
     d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
@@ -1725,20 +1725,6 @@ void TheoryStrings::getConcatVec( Node n, std::vector< Node >& c ) {
 bool TheoryStrings::checkSimple() {
   bool addedLemma = false;
 
-  //Initialize UF
-  if(d_undefSubstr.isNull()) {
-       std::vector< TypeNode > argTypes;
-       argTypes.push_back(NodeManager::currentNM()->stringType());
-       argTypes.push_back(NodeManager::currentNM()->integerType());
-       argTypes.push_back(NodeManager::currentNM()->integerType());
-       d_undefSubstr = NodeManager::currentNM()->mkSkolem("__undefSS", 
-                                               NodeManager::currentNM()->mkFunctionType(
-                                                       argTypes, NodeManager::currentNM()->stringType()),
-                                               "undefined substr",
-                                               NodeManager::SKOLEM_EXACT_NAME);
-  }
-
-
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
   while( !eqcs_i.isFinished() ) {
        Node eqc = (*eqcs_i);
@@ -1780,7 +1766,7 @@ bool TheoryStrings::checkSimple() {
                                                        } else if( n.getKind() == kind::CONST_STRING ) {
                                                                //add lemma
                                                                lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
-                                                       } else if( n.getKind() == kind::STRING_CHARAT ) {
+                                                       } /*else if( n.getKind() == kind::STRING_CHARAT ) {
                                                                lsum = d_one;
                                                                Node sk1 = NodeManager::currentNM()->mkSkolem( "ca1_$$", NodeManager::currentNM()->stringType(), "created for charat" );
                                                                Node sk3 = NodeManager::currentNM()->mkSkolem( "ca3_$$", NodeManager::currentNM()->stringType(), "created for charat" );
@@ -1788,12 +1774,11 @@ bool TheoryStrings::checkSimple() {
                                                                Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT, 
                                                                                                        NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ), n[1] );
                                                                Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, n[1], d_zero);
+                                                               Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 ));
                                                                Node x_eq_123 = n[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk, sk3 ) );
                                                                Node len_sk1_eq_i = n[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
-                                                               Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 ));
                                                                Node lemma = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i );
-                                                               Node uf = sk.eqNode( NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_undefSubstr, n[0], n[1], d_one));
-                                                               lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, lemma, uf) );
+                                                               lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, cond, lemma ) );
                                                                Trace("strings-lemma") << "Strings::Lemma CHARAT : " << lemma << std::endl;
                                                                d_out->lemma(lemma);
                                                        } else if( n.getKind() == kind::STRING_SUBSTR ) {
@@ -1807,16 +1792,14 @@ bool TheoryStrings::checkSimple() {
                                                                Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[1], d_zero);
                                                                Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[2], d_zero);
                                                                Node x_eq_123 = n[0].eqNode(NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk, sk3 ));
+                                                               Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
                                                                Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, n[1],
                                                                                                                NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
-
                                                                Node lemma = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i );
-                                                               Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
-                                                               Node uf = sk.eqNode( NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_undefSubstr, n[0], n[1], n[2]));
-                                                               lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, lemma, uf ) );
+                                                               lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, cond, lemma ) );
                                                                Trace("strings-lemma") << "Strings::Lemma SUBSTR : " << lemma << std::endl;
                                                                d_out->lemma(lemma);
-                                                       }
+                                                       }*/
                                                        Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum );
                                                        ceq = Rewriter::rewrite(ceq);
                                                        Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl;
@@ -2409,6 +2392,18 @@ bool TheoryStrings::checkPosContains() {
 }
 
 bool TheoryStrings::checkNegContains() {
+       //Initialize UF
+       if(d_ufSubstr.isNull()) {
+               std::vector< TypeNode > argTypes;
+               argTypes.push_back(NodeManager::currentNM()->stringType());
+               argTypes.push_back(NodeManager::currentNM()->integerType());
+               argTypes.push_back(NodeManager::currentNM()->integerType());
+               d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS", 
+                                                       NodeManager::currentNM()->mkFunctionType(
+                                                               argTypes, NodeManager::currentNM()->stringType()),
+                                                       "uf substr",
+                                                       NodeManager::SKOLEM_EXACT_NAME);
+       }
        bool is_unk = false;
        bool addedLemma = false;
        for( unsigned i=0; i<d_str_neg_ctn.size(); i++ ){
@@ -2450,8 +2445,10 @@ bool TheoryStrings::checkNegContains() {
                                                        Node g1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, b1, d_zero ),
                                                                                NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::MINUS, lenx, lens ), b1 ) ) );
                                                        Node b2 = NodeManager::currentNM()->mkBoundVar("bj", NodeManager::currentNM()->integerType());
-                                                       Node s2 = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ));
-                                                       Node s5 = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT, s, b2);
+                                                       //Node s2 = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ));
+                                                       //Node s5 = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT, s, b2);
+                                                       Node s2 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ), d_one);
+                                                       Node s5 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, s, b2, d_one);
 
                                                        Node s1 = NodeManager::currentNM()->mkBoundVar("s1", NodeManager::currentNM()->stringType());
                                                        Node s3 = NodeManager::currentNM()->mkBoundVar("s3", NodeManager::currentNM()->stringType());
@@ -2476,6 +2473,12 @@ bool TheoryStrings::checkNegContains() {
                                                        cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s4).eqNode(b2);
                                                        vec_nodes.push_back(cc);
 
+                                                       // charAt length
+                                                       cc = d_one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s2));
+                                                       vec_nodes.push_back(cc);
+                                                       cc = d_one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s5));
+                                                       vec_nodes.push_back(cc);
+
                                                        Node conc = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, vec_nodes) );
                                                        Node xlss = NodeManager::currentNM()->mkNode( kind::GT, lens, lenx );
                                                        conc = NodeManager::currentNM()->mkNode( kind::OR, xlss, conc );

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 05e6ebf71afb01dca3e772b25ece8d5bc6def875..5d8ff016ffb705255be52c11d94233b96d23757c 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -115,7 +115,7 @@ private:
     Node d_false;
     Node d_zero;
        Node d_one;
-       Node d_undefSubstr;
+       Node d_ufSubstr;
        // Options
        bool d_all_warning;
        bool d_opt_fmf;

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index ae5303d9df8056812b3c1483fedd9eb96665487f..707fae459008f8260600847246fcb4d616622ac9 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -127,18 +127,35 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
       return (*i).second.isNull() ? t : (*i).second;
     }
 
+       //Initialize UF
+       if(d_ufSubstr.isNull()) {
+               std::vector< TypeNode > argTypes;
+               argTypes.push_back(NodeManager::currentNM()->stringType());
+               argTypes.push_back(NodeManager::currentNM()->integerType());
+               argTypes.push_back(NodeManager::currentNM()->integerType());
+               d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS", 
+                                                       NodeManager::currentNM()->mkFunctionType(
+                                                               argTypes, NodeManager::currentNM()->stringType()),
+                                                       "uf substr",
+                                                       NodeManager::SKOLEM_EXACT_NAME);
+       }
+
        Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << std::endl;
        Node retNode = t;
-       int c_id = checkFixLenVar(t);
+       /*int c_id = checkFixLenVar(t);
        if( c_id != 2 ) {
                int v_id = 1 - c_id;
                int len = t[c_id].getConst<Rational>().getNumerator().toUnsignedInt();
                if(len > 1) {
+                       Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
                        std::vector< Node > vec;
                        for(int i=0; i<len; i++) {
                                Node num = NodeManager::currentNM()->mkConst( ::CVC4::Rational(i) );
-                               Node sk = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT, t[v_id][0], num);
+                               //Node sk = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT, t[v_id][0], num);
+                               Node sk = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, t[v_id][0], num, one);
                                vec.push_back(sk);
+                               Node cc = one.eqNode(NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ));
+                               new_nodes.push_back( cc );
                        }
                        Node lem = t[v_id][0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, vec ) );
                        lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, t, lem );
@@ -146,7 +163,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                        d_cache[t] = t;
                        retNode = t;
                }
-       } else if( t.getKind() == kind::STRING_IN_REGEXP ) {
+       } else */if( t.getKind() == kind::STRING_IN_REGEXP ) {
                // t0 in t1
                Node t0 = simplify( t[0], new_nodes );
                
@@ -164,7 +181,42 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                        // TODO
                //      return (t0 == t[0]) ? t : NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, t0, t[1] );
                //}
-       } else if( t.getKind() == kind::STRING_STRIDOF ){
+       } else if( t.getKind() == kind::STRING_CHARAT ) {
+               Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT, 
+                                                       NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), t[1] );
+               Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, t[1], d_zero);
+               Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 ));
+               Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
+               Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, t[0], t[1], one);
+               Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" );
+               Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" );
+               Node x_eq_123 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, uf, sk3 ) );
+               Node len_sk1_eq_i = t[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
+               Node len_uf_eq_j = one.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, uf ) );
+               Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, cond, 
+                                               NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, len_uf_eq_j )) );
+               new_nodes.push_back( lemma );
+               retNode = uf;
+               d_cache[t] = uf;
+       } else if( t.getKind() == kind::STRING_SUBSTR ) {
+               Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, 
+                                                       NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ),
+                                                       NodeManager::currentNM()->mkNode( kind::PLUS, t[1], t[2] ) );
+               Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, t[1], d_zero);
+               Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, t[2], d_zero);
+               Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
+               Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, t[0], t[1], t[2]);
+               Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" );
+               Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" );
+               Node x_eq_123 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, uf, sk3 ) );
+               Node len_sk1_eq_i = t[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
+               Node len_uf_eq_j = t[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, uf ) );
+               Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, cond, 
+                                               NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, len_uf_eq_j )) );
+               new_nodes.push_back( lemma );
+               retNode = uf;
+               d_cache[t] = uf;
+       } 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" );

diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index 630c7595c6d5d6fbff80df1b6d15eb4e5be6baee..a8074861efc62366abba1b7930debfc509f8a2da 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -31,7 +31,9 @@ namespace strings {
 class StringsPreprocess {
        // NOTE: this class is NOT context-dependent
        std::hash_map<TNode, Node, TNodeHashFunction> d_cache;
+       //Constants
        Node d_zero;
+       Node d_ufSubstr;
 private:
        bool checkStarPlus( Node t );
        int checkFixLenVar( Node t );