replace charat uf with internal one

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index effbbca2e24acad49da7b69327b191ba90b499e6..4deb0a9d9ae5d251bf533ac5764e787753feae74 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -44,7 +44,6 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
        d_length_nodes(c),
        //d_var_lmin( c ),
        //d_var_lmax( c ),
-       d_charAtUF(),
        d_str_pos_ctn( c ),
        d_str_neg_ctn( c ),
        d_reg_exp_mem( c ),
@@ -55,10 +54,11 @@ 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_TOTAL);
+    d_equalityEngine.addFunctionKind(kind::STRING_CHARAT_TOTAL);
     //d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR_TOTAL);
 
     d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
+    d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
     d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
     d_true = NodeManager::currentNM()->mkConst( true );
     d_false = NodeManager::currentNM()->mkConst( false );
@@ -384,13 +384,19 @@ void TheoryStrings::preRegisterTerm(TNode n) {
   default:
     if(n.getType().isString() && n.getKind() != kind::CONST_STRING && n.getKind()!=kind::STRING_CONCAT ) {
          if( std::find( d_length_intro_vars.begin(), d_length_intro_vars.end(), n )==d_length_intro_vars.end() ) {
-                 Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
-                 Node n_len_eq_z = n_len.eqNode( d_zero );
-                 Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, n_len_eq_z,
-                                                                       NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) );
-                 Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << n_len_geq_zero << std::endl;
-                 d_out->lemma(n_len_geq_zero);
-                 d_out->requirePhase( n_len_eq_z, true );
+                 if(n.getKind() == kind::STRING_CHARAT_TOTAL) {
+                         Node lenc_eq_one = d_one.eqNode(NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n));
+                         Trace("strings-lemma") << "Strings::Lemma LEN(CHAR) = 1 : " << lenc_eq_one << std::endl;
+                         d_out->lemma(lenc_eq_one);
+                 } else {
+                         Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
+                         Node n_len_eq_z = n_len.eqNode( d_zero );
+                         Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, n_len_eq_z,
+                                                                               NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) );
+                         Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << n_len_geq_zero << std::endl;
+                         d_out->lemma(n_len_geq_zero);
+                         d_out->requirePhase( n_len_eq_z, true );
+                 }
          }
          // FMF
          if( n.getKind() == kind::VARIABLE ) {//options::stringFMF() && 
@@ -469,14 +475,14 @@ void TheoryStrings::check(Effort e) {
                        addedLemma = checkLengthsEqc();
                        Trace("strings-process") << "Done check lengths, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
                        if(!d_conflict && !addedLemma) {
-                               addedLemma = checkCardinality();
-                               Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+                               addedLemma = checkContains();
+                               Trace("strings-process") << "Done check contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
                                if( !d_conflict && !addedLemma ) {
                                        addedLemma = checkMemberships();
                                        Trace("strings-process") << "Done check membership constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
                                        if( !d_conflict && !addedLemma ) {
-                                               addedLemma = checkContains();
-                                               Trace("strings-process") << "Done check contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+                                               addedLemma = checkCardinality();
+                                               Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
                                        }
                                }
                        }
@@ -994,12 +1000,11 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
                                bool success;
                                do
                                {
-                                       //---------------------do simple stuff first
+                                       //simple check
                                        if( processSimpleNEq( normal_forms, normal_form_src, curr_exp, i, j, index_i, index_j, false ) ){
                                                //added a lemma, return
                                                return true;
                                        }
-                                       //----------------------
 
                                        success = false;
                                        //if we are at the end
@@ -1097,11 +1102,6 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
                                                                                }
                                                                        }
 
-                                                                       //Node sk = NodeManager::currentNM()->mkSkolem( "v_spt_$$", normal_forms[i][index_i].getType(), "created for v/v split" );
-                                                                       //Node eq1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i],
-                                                                       //                      NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[j][index_j], sk ) ) );
-                                                                       //Node eq2 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[j][index_j],
-                                                                       //                      NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[i][index_i], sk ) ) );
                                                                        Node eq1 = mkSplitEq( "v_spt_l_$$", "created for v/v split", normal_forms[i][index_i], normal_forms[j][index_j], true );
                                                                        Node eq2 = mkSplitEq( "v_spt_r_$$", "created for v/v split", normal_forms[j][index_j], normal_forms[i][index_i], true );
                                                                        conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
@@ -1358,10 +1358,10 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) {
                std::vector< Node > nfj;
                nfj.insert( nfj.end(), d_normal_forms[nj].begin(), d_normal_forms[nj].end() );
 
-               //int revRet = processReverseDeq( nfi, nfj, ni, nj );
-               //if( revRet!=0 ){
-               //      return revRet==-1;
-               //}
+               int revRet = processReverseDeq( nfi, nfj, ni, nj );
+               if( revRet!=0 ){
+                       return revRet==-1;
+               }
                
                nfi.clear();
                nfi.insert( nfi.end(), d_normal_forms[ni].begin(), d_normal_forms[ni].end() );
@@ -2366,19 +2366,8 @@ 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());
-                                                       if(d_charAtUF.isNull()) {
-                                                               std::vector< TypeNode > argTypes;
-                                                               argTypes.push_back(NodeManager::currentNM()->stringType());
-                                                               argTypes.push_back(NodeManager::currentNM()->integerType());
-                                                               d_charAtUF = NodeManager::currentNM()->mkSkolem("charAt", 
-                                                                                               NodeManager::currentNM()->mkFunctionType(
-                                                                                               argTypes,
-                                                                                               NodeManager::currentNM()->stringType()),
-                                                                                               "total charat",
-                                                                                               NodeManager::SKOLEM_EXACT_NAME);
-                                                       }
-                                                       Node s2 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ));
-                                                       Node s5 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, s, b2);
+                                                       Node s2 = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT_TOTAL, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ));
+                                                       Node s5 = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT_TOTAL, s, b2);
 
                                                        Node s1 = NodeManager::currentNM()->mkBoundVar("s1", NodeManager::currentNM()->stringType());
                                                        Node s3 = NodeManager::currentNM()->mkBoundVar("s3", NodeManager::currentNM()->stringType());
@@ -2398,10 +2387,6 @@ bool TheoryStrings::checkNegContains() {
                                                        vec_nodes.push_back(cc);
                                                        cc = s2.eqNode(s5).negate();
                                                        vec_nodes.push_back(cc);
-                                                       cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s2).eqNode(NodeManager::currentNM()->mkConst( Rational(1)));
-                                                       vec_nodes.push_back(cc);
-                                                       cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s5).eqNode(NodeManager::currentNM()->mkConst( Rational(1)));
-                                                       vec_nodes.push_back(cc);
                                                        cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s1).eqNode(NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ));
                                                        vec_nodes.push_back(cc);
                                                        cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s4).eqNode(b2);

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 1f69c81be4c083fedf92e2207ee6f1a5fa25a217..1dae7336006e72f567c3f8500ff88cf0a4e0de0d 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -114,6 +114,7 @@ private:
     Node d_true;
     Node d_false;
     Node d_zero;
+       Node d_one;
        // Options
        bool d_all_warning;
        bool d_opt_fmf;
@@ -286,7 +287,6 @@ private:
        int getMaxPossibleLength( Node x );
 
        // Special String Functions
-       Node d_charAtUF;
        NodeList d_str_pos_ctn;
        NodeList d_str_neg_ctn;
        std::map< Node, bool > d_str_ctn_eqlen;

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 11642a4d2cb615de84209edd2791038a1c8f7f02..00d02e0159f7bb1a554233b616e42de9df3d2b1b 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -27,12 +27,6 @@ StringsPreprocess::StringsPreprocess() {
        std::vector< TypeNode > argTypes;
        argTypes.push_back(NodeManager::currentNM()->stringType());
        argTypes.push_back(NodeManager::currentNM()->integerType());
-       d_charAtUF = NodeManager::currentNM()->mkSkolem("charAt", 
-                                               NodeManager::currentNM()->mkFunctionType(
-                                                       argTypes,
-                                                       NodeManager::currentNM()->stringType()),
-                                               "total charat",
-                                               NodeManager::SKOLEM_EXACT_NAME);
 }
 
 void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret, std::vector< Node > &nn ) {
@@ -137,14 +131,11 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                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::APPLY_UF, d_charAtUF, t[v_id][0], num);
+                               Node sk = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT_TOTAL, t[v_id][0], num);
                                vec.push_back(sk);
-                               Node lem = one.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ) );
-                               new_nodes.push_back( lem );
                        }
                        Node lem = t[v_id][0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, vec ) );
                        lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, t, lem );
@@ -189,26 +180,6 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                tp = NodeManager::currentNM()->mkNode( kind::IMPLIES, lenxgti, tp );
                new_nodes.push_back( tp );
 
-               d_cache[t] = sk2;
-               retNode = sk2;
-       } else if( t.getKind() == kind::STRING_CHARAT_TOTAL ){
-               Node sk1 = NodeManager::currentNM()->mkSkolem( "ca1_$$", NodeManager::currentNM()->stringType(), "created for charat" );
-               Node sk2 = NodeManager::currentNM()->mkSkolem( "ca2_$$", NodeManager::currentNM()->stringType(), "created for charat" );
-               Node sk3 = NodeManager::currentNM()->mkSkolem( "ca3_$$", NodeManager::currentNM()->stringType(), "created for charat" );
-               Node x = simplify( t[0], new_nodes );
-               Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT, 
-                                                       NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ), t[1] );
-               Node x_eq_123 = NodeManager::currentNM()->mkNode( kind::EQUAL,
-                                                       NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ), x );
-               Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, t[1],
-                                                               NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
-               Node len_sk2_eq_1 = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkConst( Rational( 1 ) ),
-                                                               NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) );
-
-               Node tp = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, len_sk2_eq_1 );
-               tp = NodeManager::currentNM()->mkNode( kind::IMPLIES, lenxgti, tp );
-               new_nodes.push_back( tp );
-
                d_cache[t] = sk2;
                retNode = sk2;
        } else if( t.getKind() == kind::STRING_STRIDOF ){
@@ -278,7 +249,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                        throw LogicException("string replace not supported in this release");
                }
        } else if(t.getKind() == kind::STRING_CHARAT) {
-               Node sk2 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, t[0], t[1]);
+               Node sk2 = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT_TOTAL, t[0], t[1]);
                Node sk1 = NodeManager::currentNM()->mkSkolem( "ca1_$$", NodeManager::currentNM()->stringType(), "created for charat" );
                Node sk3 = NodeManager::currentNM()->mkSkolem( "ca3_$$", NodeManager::currentNM()->stringType(), "created for charat" );
                Node x = simplify( t[0], new_nodes );
@@ -288,16 +259,12 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                Node len_sk1_eq_i = t[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
                Node tp = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i );
                tp = NodeManager::currentNM()->mkNode( kind::IMPLIES, lenxgti, tp );
-               Node len_sk2_eq_1 = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkConst( Rational( 1 ) ),
-                                                               NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) );
-               tp = NodeManager::currentNM()->mkNode( kind::AND, len_sk2_eq_1, tp );
-
                new_nodes.push_back( tp );
 
                d_cache[t] = sk2;
                retNode = sk2;
        } else if(t.getKind() == kind::STRING_SUBSTR) {
-               InternalError("CharAt and Substr should not be reached here.");
+               InternalError("Substr should not be reached here.");
        } else if( t.getNumChildren()>0 ) {
                std::vector< Node > cc;
                if (t.getMetaKind() == kind::metakind::PARAMETERIZED) {

diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index 27808f0b25cc1e8db41926546cbf65a85ff7fcf8..99312ddc06d031db0e3ec8038fc85f0594f60239 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -31,7 +31,6 @@ namespace strings {
 class StringsPreprocess {
        // NOTE: this class is NOT context-dependent
        std::hash_map<TNode, Node, TNodeHashFunction> d_cache;
-       Node d_charAtUF;
 private:
        bool checkStarPlus( Node t );
        int checkFixLenVar( Node t );

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 78731d469f53743eebf00739e1b6f564f0fed100..86af2ffa8e101b51bf9f8efbfe349d0099b66943 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -323,16 +323,22 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
     } else if(node.getKind() == kind::STRING_LENGTH) {
         if(node[0].isConst()) {
             retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( node[0].getConst<String>().size() ) );
+        } else if(node[0].getKind() == kind::STRING_CHARAT_TOTAL) {
+            retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) );
         } else if(node[0].getKind() == kind::STRING_CONCAT) {
             Node tmpNode = rewriteConcatString(node[0]);
             if(tmpNode.isConst()) {
                 retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode.getConst<String>().size() ) );
+            } else if(tmpNode.getKind() == kind::STRING_CHARAT_TOTAL) {
+                               retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) );
             } else {
                 // it has to be string concat
                 std::vector<Node> node_vec;
                 for(unsigned int i=0; i<tmpNode.getNumChildren(); ++i) {
                     if(tmpNode[i].isConst()) {
                         node_vec.push_back( NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode[i].getConst<String>().size() ) ) );
+                                       } else if(tmpNode[i].getKind() == kind::STRING_CHARAT_TOTAL) {
+                        node_vec.push_back( NodeManager::currentNM()->mkConst( ::CVC4::Rational( 1 ) ) );
                     } else {
                         node_vec.push_back( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, tmpNode[i]) );
                     }
@@ -360,7 +366,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
                                retNode = NodeManager::currentNM()->mkConst( false );
                        }
                }
-       } else if(node.getKind() == kind::STRING_CHARAT) {
+       } else if(node.getKind() == kind::STRING_CHARAT || node.getKind() == kind::STRING_CHARAT_TOTAL) {
                if( node[0].isConst() && node[1].isConst() ) {
                        int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
                        if( node[0].getConst<String>().size() > (unsigned) i ) {