strings with new ideas

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 09de0d378d7a15d9e6a37fc7540582e1e0294895..57583324e7b98a4d183f44752b11b11dcddbbaa9 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -124,6 +124,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       case BOOLEAN_TYPE: out << "Bool"; break;
       case REAL_TYPE: out << "Real"; break;
       case INTEGER_TYPE: out << "Int"; break;
+      case STRING_TYPE: out << "String"; break;
       default:
         // fall back on whatever operator<< does on underlying type; we
         // might luck out and be SMT-LIB v2 compliant

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 761348890fed0e2b84c6b97acbac926a63ce14be..406db286fd1efa3e3fb596594e83b48969aebc3c 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -309,6 +309,7 @@ class SmtEnginePrivate : public NodeManagerListener {
    * Function symbol used to implement uninterpreted undefined string
    * semantics.  Needed to deal with partial charat/substr function.
    */
+  Node d_charAtUF;
   Node d_charAtUndef;
   Node d_substrUndef;
 
@@ -440,6 +441,7 @@ public:
     d_fakeContext(),
     d_abstractValueMap(&d_fakeContext),
     d_abstractValues(),
+       d_charAtUF(),
        d_charAtUndef(),
        d_substrUndef(),
     d_divByZero(),
@@ -1534,11 +1536,17 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
         node = expandBVDivByZero(node);
         break;
 
-         case kind::STRING_CHARAT: {
-               if(d_charAtUndef.isNull()) {
+         /*case kind::STRING_CHARAT: {
+               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);
                        d_charAtUndef = NodeManager::currentNM()->mkSkolem("charAt_undef", 
                                                                NodeManager::currentNM()->mkFunctionType(
                                                                        argTypes,
@@ -1551,14 +1559,17 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
                                d_smt.d_logic.lock();
                        }
            }
-               TNode str = n[0], num = n[1];
+               Node str = n[0];
+               Node num = n[1];
+               //Assert(str.getType() == NodeManager::currentNM()->stringType(), "String Type Check 1");
                Node lenx = nm->mkNode(kind::STRING_LENGTH, str);
                Node cond = nm->mkNode(kind::GT, lenx, num);
                Node total = nm->mkNode(kind::STRING_CHARAT_TOTAL, str, num);
                Node undef = nm->mkNode(kind::APPLY_UF, d_charAtUndef, str, num);
                node = nm->mkNode(kind::ITE, cond, total, undef);
+               node = nm->mkNode(kind::APPLY_UF, d_charAtUF, n[0], n[1]);
          }
-               break;
+               break;*/
          case kind::STRING_SUBSTR: {
                if(d_substrUndef.isNull()) {
                        std::vector< TypeNode > argTypes;
@@ -1577,7 +1588,8 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
                                d_smt.d_logic.lock();
                        }
            }
-               TNode str = n[0];
+               Node str = n[0];
+               //Assert(str.getType() == NodeManager::currentNM()->stringType(), "String Type Check 2");
                Node lenx = nm->mkNode(kind::STRING_LENGTH, str);
                Node num = nm->mkNode(kind::PLUS, n[1], n[2]);
                Node cond = nm->mkNode(kind::GEQ, lenx, num);

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 4b479e3482e2208c82ad1b04ba5602bc351a270f..ac50ed21da309dce3ea2b93c80e361f3177d10c0 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -41,6 +41,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
     d_infer(c),
     d_infer_exp(c),
     d_nf_pairs(c),
+       d_length_nodes(c),
        //d_var_lmin( c ),
        //d_var_lmax( c ),
        d_str_pos_ctn( c ),
@@ -53,6 +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_TOTAL);
+    //d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR_TOTAL);
 
     d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
     d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
@@ -104,11 +107,18 @@ Node TheoryStrings::getLengthTerm( Node t ) {
                //typically shouldnt be necessary
                length_term = t;
        }
+       Debug("strings") << "TheoryStrings::getLengthTerm" << t << std::endl;
        return length_term;
 }
 
 Node TheoryStrings::getLength( Node t ) {
-       return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, getLengthTerm( t ) ) );
+       Node retNode;
+       if(t.isConst()) {
+               retNode = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t );
+       } else {
+               retNode = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, getLengthTerm( t ) );
+       }
+       return Rewriter::rewrite( retNode );
 }
 
 void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) {
@@ -370,8 +380,8 @@ void TheoryStrings::preRegisterTerm(TNode n) {
     //d_equalityEngine.addTriggerPredicate(n);
     break;
   default:
-    if(n.getKind() == kind::VARIABLE || n.getKind()==kind::SKOLEM) {
-         if( std::find( d_length_intro_vars.begin(), d_length_intro_vars.end(), n )==d_length_intro_vars.end() ){
+    if(n.getType().isString() && (n.getKind() == kind::VARIABLE || n.getKind()==kind::SKOLEM)) {
+         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,
@@ -1343,6 +1353,12 @@ bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) {
                                                        Node sk1 = NodeManager::currentNM()->mkSkolem( "x_dsplit_$$", ni.getType(), "created for disequality normalization" );
                                                        Node sk2 = NodeManager::currentNM()->mkSkolem( "y_dsplit_$$", ni.getType(), "created for disequality normalization" );
                                                        Node sk3 = NodeManager::currentNM()->mkSkolem( "z_dsplit_$$", ni.getType(), "created for disequality normalization" );
+                                                       Node nemp = sk1.eqNode(d_emptyString).negate();
+                                                       conc.push_back(nemp);
+                                                       nemp = sk2.eqNode(d_emptyString).negate();
+                                                       conc.push_back(nemp);
+                                                       nemp = sk3.eqNode(d_emptyString).negate();
+                                                       conc.push_back(nemp);
                                                        Node lsk1 = getLength( sk1 );
                                                        conc.push_back( lsk1.eqNode( li ) );
                                                        Node lsk2 = getLength( sk2 );
@@ -1350,17 +1366,17 @@ bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) {
                                                        conc.push_back( NodeManager::currentNM()->mkNode( kind::OR,
                                                                                                j.eqNode( mkConcat( sk1, sk3 ) ), i.eqNode( mkConcat( sk2, sk3 ) ) ) );
                                                        
-                                                       sendLemma( mkExplain( antec, antec_new_lits ), NodeManager::currentNM()->mkNode( kind::AND, conc ), "Disequality Normalize" );
+                                                       sendLemma( mkExplain( antec, antec_new_lits ), NodeManager::currentNM()->mkNode( kind::AND, conc ), "D-DISL-Split" );
                                                        return true;
                                                }else if( areEqual( li, lj ) ){
                                                        if( areDisequal( i, j ) ){
                                                                Trace("strings-solve") << "Case 1 : found equal length disequal sub strings " << i << " " << j << std::endl;
-                                                               //we are done
+                                                               //we are done: D-Remove
                                                                return false;
                                                        } else {
                                                                //splitting on demand : try to make them disequal
                                                                Node eq = i.eqNode( j );
-                                                               sendSplit( i, j, "Disequality : disequal terms" );
+                                                               sendSplit( i, j, "D-EQL-Split" );
                                                                eq = Rewriter::rewrite( eq );
                                                                d_pending_req_phase[ eq ] = false;
                                                                return true;
@@ -1368,7 +1384,7 @@ bool TheoryStrings::normalizeDisequality( Node ni, Node nj ) {
                                                }else{
                                                        //splitting on demand : try to make lengths equal
                                                        Node eq = li.eqNode( lj );
-                                                       sendSplit( li, lj, "Disequality : equal length" );
+                                                       sendSplit( li, lj, "D-UNK-Split" );
                                                        eq = Rewriter::rewrite( eq );
                                                        d_pending_req_phase[ eq ] = true;
                                                        return true;
@@ -1429,7 +1445,7 @@ bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) {
 }
 
 void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
-       if( conc.isNull() ){
+       if( conc.isNull() || conc == d_false ){
                d_out->conflict(ant);
                Trace("strings-conflict") << "Strings::Conflict : " << ant << std::endl;
                d_conflict = true;
@@ -1547,34 +1563,40 @@ bool TheoryStrings::checkLengths() {
                        //if n has not instantiatied the concat..length axiom
                        //then, add lemma
                        if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) { // || n.getKind() == kind::STRING_CONCAT ){
-                               if( d_length_inst.find(n)==d_length_inst.end() ) {
-                                       d_length_inst[n] = true;
-                                       Trace("strings-debug") << "get n: " << n << endl;
-                                       Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for concat lemma" );
-                                       d_length_intro_vars.push_back( sk );
-                                       Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n );
-                                       eq = Rewriter::rewrite(eq);
-                                       Trace("strings-lemma") << "Strings::Lemma LENGTH term : " << eq << std::endl;
-                                       d_out->lemma(eq);
-                                       Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
-                                       Node lsum;
-                                       if( n.getKind() == kind::STRING_CONCAT ) {
-                                               //add lemma
-                                               std::vector<Node> node_vec;
-                                               for( unsigned i=0; i<n.getNumChildren(); i++ ) {
-                                                       Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] );
-                                                       node_vec.push_back(lni);
+                               if( d_length_nodes.find(n)==d_length_nodes.end() ) {
+                                       if( d_length_inst.find(n)==d_length_inst.end() ) {
+                                               Node nr = d_equalityEngine.getRepresentative( n );
+                                               if( d_length_nodes.find(nr)==d_length_nodes.end() ) {
+                                                       d_length_inst[n] = true;
+                                                       Trace("strings-debug") << "get n: " << n << endl;
+                                                       Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for concat lemma" );
+                                                       d_length_intro_vars.push_back( sk );
+                                                       Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n );
+                                                       eq = Rewriter::rewrite(eq);
+                                                       Trace("strings-lemma") << "Strings::Lemma LENGTH term : " << eq << std::endl;
+                                                       d_out->lemma(eq);
+                                                       Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
+                                                       Node lsum;
+                                                       if( n.getKind() == kind::STRING_CONCAT ) {
+                                                               //add lemma
+                                                               std::vector<Node> node_vec;
+                                                               for( unsigned i=0; i<n.getNumChildren(); i++ ) {
+                                                                       Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] );
+                                                                       node_vec.push_back(lni);
+                                                               }
+                                                               lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec );
+                                                       } else {
+                                                               //add lemma
+                                                               lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
+                                                       }
+                                                       Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum );
+                                                       ceq = Rewriter::rewrite(ceq);
+                                                       Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl;
+                                                       d_out->lemma(ceq);
+                                                       addedLemma = true;
                                                }
-                                               lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec );
-                                       } else {
-                                               //add lemma
-                                               lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
                                        }
-                                       Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum );
-                                       ceq = Rewriter::rewrite(ceq);
-                                       Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl;
-                                       d_out->lemma(ceq);
-                                       addedLemma = true;
+                                       d_length_nodes[n] = true;
                                }
                        }
                        ++eqc_i;
@@ -2114,7 +2136,7 @@ bool TheoryStrings::checkMemberships() {
 bool TheoryStrings::checkContains() {
        bool addedLemma = checkPosContains();
        Trace("strings-process") << "Done check positive contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
-       if(!addedLemma) {
+       if(!d_conflict && !addedLemma) {
                addedLemma = checkNegContains();
                Trace("strings-process") << "Done check positive contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
        }
@@ -2124,24 +2146,26 @@ bool TheoryStrings::checkContains() {
 bool TheoryStrings::checkPosContains() {
        bool addedLemma = false;
        for( unsigned i=0; i<d_str_pos_ctn.size(); i++ ) {
-               Node atom = d_str_pos_ctn[i];
-               Trace("strings-ctn") << "We have positive contain assertion : " << atom << std::endl;
-               Assert( atom.getKind()==kind::STRING_STRCTN );
-               Node x = atom[0];
-               Node s = atom[1];
-               if( !areEqual( s, d_emptyString ) && !areEqual( s, x ) ) {
-                       if(d_str_pos_ctn_rewritten.find(atom) == d_str_pos_ctn_rewritten.end()) {
-                               Node sk1 = NodeManager::currentNM()->mkSkolem( "sc1_$$", s.getType(), "created for contain" );
-                               Node sk2 = NodeManager::currentNM()->mkSkolem( "sc2_$$", s.getType(), "created for contain" );
-                               Node eq = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, s, sk2 ) ) );
-                               sendLemma( atom, eq, "POS-INC" );
-                               addedLemma = true;
-                               d_str_pos_ctn_rewritten[ atom ] = true;
+               if( !d_conflict ){
+                       Node atom = d_str_pos_ctn[i];
+                       Trace("strings-ctn") << "We have positive contain assertion : " << atom << std::endl;
+                       Assert( atom.getKind()==kind::STRING_STRCTN );
+                       Node x = atom[0];
+                       Node s = atom[1];
+                       if( !areEqual( s, d_emptyString ) && !areEqual( s, x ) ) {
+                               if(d_str_pos_ctn_rewritten.find(atom) == d_str_pos_ctn_rewritten.end()) {
+                                       Node sk1 = NodeManager::currentNM()->mkSkolem( "sc1_$$", s.getType(), "created for contain" );
+                                       Node sk2 = NodeManager::currentNM()->mkSkolem( "sc2_$$", s.getType(), "created for contain" );
+                                       Node eq = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, s, sk2 ) ) );
+                                       sendLemma( atom, eq, "POS-INC" );
+                                       addedLemma = true;
+                                       d_str_pos_ctn_rewritten[ atom ] = true;
+                               } else {
+                                       Trace("strings-ctn") << "... is already rewritten." << std::endl;
+                               }
                        } else {
-                               Trace("strings-ctn") << "... is already rewritten." << std::endl;
+                               Trace("strings-ctn") << "... is satisfied." << std::endl;
                        }
-               } else {
-                       Trace("strings-ctn") << "... is satisfied." << std::endl;
                }
        }
        if( addedLemma ){
@@ -2156,70 +2180,147 @@ bool TheoryStrings::checkNegContains() {
        bool is_unk = false;
        bool addedLemma = false;
        for( unsigned i=0; i<d_str_neg_ctn.size(); i++ ){
-               Node atom = d_str_neg_ctn[i];
-               Trace("strings-ctn") << "We have nagetive contain assertion : (not " << atom << " )" << std::endl;
-               if( areEqual( atom[1], d_emptyString ) ) {
-                       Node ant = NodeManager::currentNM()->mkNode( kind::AND, atom.negate(), atom[1].eqNode( d_emptyString ) );
-                       Node conc = Node::null();
-                       sendLemma( ant, conc, "NEG-CTN Conflict 1" );
-                       addedLemma = true;
-               } else if( areEqual( atom[1], atom[0] ) ) {
-                       Node ant = NodeManager::currentNM()->mkNode( kind::AND, atom.negate(), atom[1].eqNode( atom[0] ) );
-                       Node conc = Node::null();
-                       sendLemma( ant, conc, "NEG-CTN Conflict 2" );
-                       addedLemma = true;
-               } else {
-                       if(options::stringExp()) {
-                               Node x = atom[0];
-                               Node s = atom[1];
-                               Node lenx = getLength(x);
-                               Node lens = getLength(s);
-                               if(areEqual(lenx, lens)) {
-                                       if(d_str_ctn_eqlen.find(atom) == d_str_ctn_eqlen.end()) {
-                                               Node eq = lenx.eqNode(lens);
-                                               Node antc = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, atom.negate(), eq ) );
-                                               Node xneqs = x.eqNode(s).negate();
-                                               d_str_ctn_eqlen[ atom ] = true;
-                                               sendLemma( antc, xneqs, "NEG-CTN-EQL" );
+               if( !d_conflict ){
+                       Node atom = d_str_neg_ctn[i];
+                       Trace("strings-ctn") << "We have nagetive contain assertion : (not " << atom << " )" << std::endl;
+                       if( areEqual( atom[1], d_emptyString ) ) {
+                               Node ant = NodeManager::currentNM()->mkNode( kind::AND, atom.negate(), atom[1].eqNode( d_emptyString ) );
+                               Node conc = Node::null();
+                               sendLemma( ant, conc, "NEG-CTN Conflict 1" );
+                               addedLemma = true;
+                       } else if( areEqual( atom[1], atom[0] ) ) {
+                               Node ant = NodeManager::currentNM()->mkNode( kind::AND, atom.negate(), atom[1].eqNode( atom[0] ) );
+                               Node conc = Node::null();
+                               sendLemma( ant, conc, "NEG-CTN Conflict 2" );
+                               addedLemma = true;
+                       } else {
+                               if(options::stringExp()) {
+                                       Node x = atom[0];
+                                       Node s = atom[1];
+                                       Node lenx = getLength(x);
+                                       Node lens = getLength(s);
+                                       if(areEqual(lenx, lens)) {
+                                               if(d_str_ctn_eqlen.find(atom) == d_str_ctn_eqlen.end()) {
+                                                       Node eq = lenx.eqNode(lens);
+                                                       Node antc = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, atom.negate(), eq ) );
+                                                       Node xneqs = x.eqNode(s).negate();
+                                                       d_str_ctn_eqlen[ atom ] = true;
+                                                       sendLemma( antc, xneqs, "NEG-CTN-EQL" );
+                                                       addedLemma = true;
+                                               }
+                                       } else if(!areDisequal(lenx, lens)) {
+                                               sendSplit(lenx, lens, "NEG-CTN-SP");
                                                addedLemma = true;
+                                       } else {
+                                               if(d_str_neg_ctn_rewritten.find(atom) == d_str_neg_ctn_rewritten.end()) {
+                               /*std::vector< TypeNode > argTypes;
+                               argTypes.push_back(NodeManager::currentNM()->stringType());
+                               argTypes.push_back(NodeManager::currentNM()->integerType());
+                               Node d_charAtUF = NodeManager::currentNM()->mkSkolem("charAt", 
+                                                                       NodeManager::currentNM()->mkFunctionType(
+                                                                               argTypes,
+                                                                               NodeManager::currentNM()->stringType()),
+                                                                       "total charat",
+                                                                       NodeManager::SKOLEM_EXACT_NAME);*/
+                                                       /*
+                                                       Node e1 = NodeManager::currentNM()->mkSkolem( "nc1_$$", s.getType(), "created for contain" );
+                                                       Node e2 = NodeManager::currentNM()->mkSkolem( "nc2_$$", s.getType(), "created for contain" );
+                                                       Node z = NodeManager::currentNM()->mkSkolem( "ncz_$$", s.getType(), "created for contain" );
+                                                       Node w = NodeManager::currentNM()->mkSkolem( "ncw_$$", s.getType(), "created for contain" );
+                                                       std::vector< Node > vec_conc;
+                                                       Node cc = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, e1, z ) ) );
+                                                       vec_conc.push_back(cc);
+                                                       cc = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, w, e2 ) ) );
+                                                       vec_conc.push_back(cc);
+                                                       cc = Rewriter::rewrite( z.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, s, e2 ) ).negate() );
+                                                       vec_conc.push_back(cc);
+                                                       cc = Rewriter::rewrite( w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, e1, s ) ).negate() );
+                                                       vec_conc.push_back(cc);
+                                                       cc = Rewriter::rewrite( lenx.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH,
+                                                                                               NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, e1, s, e2 ) ) ) );
+                                                       vec_conc.push_back(cc);
+                                                       //Incomplete
+                                                       //cc = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, e1, s ).negate();
+                                                       //vec_conc.push_back(cc);
+                                                       //cc = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, e2, s ).negate();
+                                                       //vec_conc.push_back(cc);
+                                                       Node conc = NodeManager::currentNM()->mkNode( kind::AND, vec_conc );
+                                                       */
+                                                       //x[i+j] != y[j]
+                                                       /*Node conc = NodeManager::currentNM()->mkNode( kind::STRING_CHARAT, x , NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ) ).eqNode(
+                                                                                       NodeManager::currentNM()->mkNode( kind::STRING_CHARAT, s , b2) ).negate();
+                                                       Node conc = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, x, NodeManager::currentNM()->mkNode(kind::PLUS, b1, b2)).eqNode(
+                                                                                       NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, s , b2)).negate();
+                                                       conc = NodeManager::currentNM()->mkNode( kind::AND, g2, conc );
+                                                       conc = NodeManager::currentNM()->mkNode( kind::EXISTS, b2v, conc );
+                                                       conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, g1, conc );
+                                                       conc = NodeManager::currentNM()->mkNode( kind::FORALL, b1v, conc );
+                                                       Node xlss = NodeManager::currentNM()->mkNode( kind::GT, lens, lenx );
+                                                       conc = NodeManager::currentNM()->mkNode( kind::OR, xlss, conc );
+                                                       */
+                                                       Node b1 = NodeManager::currentNM()->mkBoundVar("bi", NodeManager::currentNM()->integerType());
+                                                       Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);
+                                                       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 d_charAtUF;
+                       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 s1 = NodeManager::currentNM()->mkBoundVar("s1", NodeManager::currentNM()->stringType());
+                       Node s3 = NodeManager::currentNM()->mkBoundVar("s3", NodeManager::currentNM()->stringType());
+                       Node s4 = NodeManager::currentNM()->mkBoundVar("s4", NodeManager::currentNM()->stringType());
+                       Node s6 = NodeManager::currentNM()->mkBoundVar("s6", NodeManager::currentNM()->stringType());
+                                                       Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2, s1, s3, s4, s6);
+
+                       std::vector< Node > vec_nodes;
+                       Node cc = NodeManager::currentNM()->mkNode( kind::GEQ, b2, d_zero );
+                       vec_nodes.push_back(cc);
+                       cc = NodeManager::currentNM()->mkNode( kind::GEQ, lens, b2 );
+                       vec_nodes.push_back(cc);
+
+                       cc = x.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s1, s2, s3));
+                       vec_nodes.push_back(cc);
+                       cc = s.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s4, s5, s6));
+                       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);
+                       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 );
+                                                       //conc = NodeManager::currentNM()->mkNode( kind::AND, g2, conc );
+                                                       conc = NodeManager::currentNM()->mkNode( kind::EXISTS, b2v, conc );
+                                                       conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, g1, conc );
+                                                       conc = NodeManager::currentNM()->mkNode( kind::FORALL, b1v, conc );
+
+                                                       d_str_neg_ctn_rewritten[ atom ] = true;
+                                                       sendLemma( atom.negate(), conc, "NEG-CTN-BRK" );
+                                                       //d_pending_req_phase[xlss] = true;
+                                                       addedLemma = true;
+                                               }
                                        }
-                               } else if(!areDisequal(lenx, lens)) {
-                                       sendSplit(lenx, lens, "NEG-CTN-SP");
-                                       addedLemma = true;
                                } else {
-                                       if(d_str_neg_ctn_rewritten.find(atom) == d_str_neg_ctn_rewritten.end()) {
-                                               Node e1 = NodeManager::currentNM()->mkSkolem( "nc1_$$", s.getType(), "created for contain" );
-                                               Node e2 = NodeManager::currentNM()->mkSkolem( "nc2_$$", s.getType(), "created for contain" );
-                                               Node z = NodeManager::currentNM()->mkSkolem( "ncz_$$", s.getType(), "created for contain" );
-                                               Node w = NodeManager::currentNM()->mkSkolem( "ncw_$$", s.getType(), "created for contain" );
-                                               std::vector< Node > vec_conc;
-                                               Node cc = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, e1, z ) ) );
-                                               vec_conc.push_back(cc);
-                                               cc = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, w, e2 ) ) );
-                                               vec_conc.push_back(cc);
-                                               cc = Rewriter::rewrite( z.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, s, e2 ) ).negate() );
-                                               vec_conc.push_back(cc);
-                                               cc = Rewriter::rewrite( w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, e1, s ) ).negate() );
-                                               vec_conc.push_back(cc);
-                                               cc = Rewriter::rewrite( lenx.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH,
-                                                                                       NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, e1, s, e2 ) ) ) );
-                                               vec_conc.push_back(cc);
-                                               //Incomplete
-                                               //cc = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, e1, s ).negate();
-                                               //vec_conc.push_back(cc);
-                                               //cc = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, e2, s ).negate();
-                                               //vec_conc.push_back(cc);
-                                               Node conc = NodeManager::currentNM()->mkNode( kind::AND, vec_conc );
-                                               Node xlss = NodeManager::currentNM()->mkNode( kind::GT, lens, lenx );
-                                               conc = NodeManager::currentNM()->mkNode( kind::OR, xlss, conc );
-                                               d_str_neg_ctn_rewritten[ atom ] = true;
-                                               sendLemma( atom.negate(), conc, "NEG-INC-BRK" );
-                                               addedLemma = true;
-                                       }
+                                       Trace("strings-ctn") << "Strings Incomplete (due to Negative Contain) by default." << std::endl;
+                                       is_unk = true;
                                }
-                       } else {
-                               Trace("strings-ctn") << "Strings Incomplete (due to Negative Contain) by default." << std::endl;
-                               is_unk = true;
                        }
                }
        }
@@ -2228,7 +2329,7 @@ bool TheoryStrings::checkNegContains() {
                return true;
        } else {
                if( is_unk ){
-                       Trace("strings-ctn") << "Strings::inc: possibly incomplete." << std::endl;
+                       Trace("strings-ctn") << "Strings::CTN: possibly incomplete." << std::endl;
                        d_out->setIncomplete();
                }
                return false;

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 1d92abbd279253801937efe95dfa799fba52936d..6b4899c80e9fdbd90553854341e006c519a25968 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -190,6 +190,7 @@ private:
        EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true );
        //maintain which concat terms have the length lemma instantiated
        std::map< Node, bool > d_length_inst;
+       NodeBoolMap d_length_nodes;
 private:
        void mergeCstVec(std::vector< Node > &vec_strings);
     bool getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 11e206eebaf1a5b2b998b1bac7313b347e267d94..7edddbe760d8de60217e92a01728799d4f454f1f 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -119,9 +119,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                //      return (t0 == t[0]) ? t : NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, t0, t[1] );
                //}
        } else if( t.getKind() == kind::STRING_SUBSTR_TOTAL ){
-               Node sk1 = NodeManager::currentNM()->mkSkolem( "st1_$$", t.getType(), "created for substr" );
-               Node sk2 = NodeManager::currentNM()->mkSkolem( "st2_$$", t.getType(), "created for substr" );
-               Node sk3 = NodeManager::currentNM()->mkSkolem( "st3_$$", t.getType(), "created for substr" );
+               Node sk1 = NodeManager::currentNM()->mkSkolem( "st1_$$", NodeManager::currentNM()->stringType(), "created for substr" );
+               Node sk2 = NodeManager::currentNM()->mkSkolem( "st2_$$", NodeManager::currentNM()->stringType(), "created for substr" );
+               Node sk3 = NodeManager::currentNM()->mkSkolem( "st3_$$", NodeManager::currentNM()->stringType(), "created for substr" );
                Node x = simplify( t[0], new_nodes );
                Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, 
                                                        NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, x ),
@@ -140,9 +140,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                d_cache[t] = sk2;
                retNode = sk2;
        } else if( t.getKind() == kind::STRING_CHARAT_TOTAL ){
-               Node sk1 = NodeManager::currentNM()->mkSkolem( "ca1_$$", t.getType(), "created for charat" );
-               Node sk2 = NodeManager::currentNM()->mkSkolem( "ca2_$$", t.getType(), "created for charat" );
-               Node sk3 = NodeManager::currentNM()->mkSkolem( "ca3_$$", t.getType(), "created for charat" );
+               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] );
@@ -226,7 +226,37 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                } else {
                        throw LogicException("string replace not supported in this release");
                }
-       } else if(t.getKind() == kind::STRING_CHARAT || t.getKind() == kind::STRING_SUBSTR) {
+       } else if(t.getKind() == kind::STRING_CHARAT) {
+               Node d_charAtUF;
+               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 sk2 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_charAtUF, 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 );
+               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_SUBSTR) {
                InternalError("CharAt and Substr should not be reached here.");
        } else if( t.getNumChildren()>0 ) {
                std::vector< Node > cc;

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 9f278aac2c276cab5db6d97fae2f1a199db0bd5a..a4c12dfdc6aca948d7b8d24a80889c107198f172 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -360,7 +360,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
                                retNode = NodeManager::currentNM()->mkConst( false );
                        }
                }
-       } else if(node.getKind() == kind::STRING_CHARAT_TOTAL) {
+       } else if(node.getKind() == kind::STRING_CHARAT) {
                if( node[0].isConst() && node[1].isConst() ) {
                        int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
                        if( node[0].getConst<String>().size() > (unsigned) i ) {

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index e55d6a9c95947da0684a4f04c5369de2c76c0ee5..ff84e63b7673909611278465322636cc9ea6150a 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -419,11 +419,9 @@ void TheoryEngine::check(Theory::Effort effort) {
     if(!d_inConflict && Theory::fullEffort(effort) && d_masterEqualityEngine != NULL && !d_lemmasAdded) {
       AlwaysAssert(d_masterEqualityEngine->consistent());
     }
-
   } catch(const theory::Interrupted&) {
     Trace("theory") << "TheoryEngine::check() => interrupted" << endl;
   }
-
   // If fulleffort, check all theories
   if(Dump.isOn("theory::fullcheck") && Theory::fullEffort(effort)) {
     if (!d_inConflict && !needCheck()) {

diff --git a/test/regress/regress0/strings/at001.smt2 b/test/regress/regress0/strings/at001.smt2
index 855957430d795bbeb72c18337bd911974c38bcfd..616189d96bf7b1151cebc8c0f9b8718a79330384 100644 (file)
--- a/test/regress/regress0/strings/at001.smt2
+++ b/test/regress/regress0/strings/at001.smt2
@@ -5,8 +5,8 @@
 (declare-fun i () Int)\r
 \r
 (assert (= (str.at x i) "b"))\r
-(assert (> i 5))\r
-(assert (< (str.len x) 4))\r
+(assert (and (>= i 4) (< i (str.len x))))\r
+(assert (< (str.len x) 7))\r
 (assert (> (str.len x) 2))\r
 \r
 (check-sat)\r