adds smt2 print for strings

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index c56d87da66a3157ac4da0c4e59d6111173f5b771..409c9b4dd491c21fc5818f60ae379bca85be2c9c 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -273,6 +273,24 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::STORE:
   case kind::ARRAY_TYPE: out << smtKindString(k) << " "; break;
 
+  // string theory
+  case kind::STRING_CONCAT: out << "str.++ "; break;
+  case kind::STRING_IN_REGEXP: out << "str.in.re "; break;
+  case kind::STRING_LENGTH: out << "str.len "; break;
+  case kind::STRING_SUBSTR: out << "str.substr "; break;
+  case kind::STRING_STRCTN: out << "str.contain "; break;
+  case kind::STRING_CHARAT: out << "str.at "; break;
+  case kind::STRING_STRIDOF: out << "str.indexof "; break;
+  case kind::STRING_STRREPL: out << "str.replace "; break;
+  case kind::STRING_TO_REGEXP: out << "str.to.re "; break;
+  case kind::REGEXP_CONCAT: out << "re.++ "; break;
+  case kind::REGEXP_OR: out << "re.or "; break;
+  case kind::REGEXP_INTER: out << "re.itr "; break;
+  case kind::REGEXP_STAR: out << "re.* "; break;
+  case kind::REGEXP_PLUS: out << "re.+ "; break;
+  case kind::REGEXP_OPT: out << "re.opt "; break;
+  case kind::REGEXP_RANGE: out << "re.range "; break;
+
     // bv theory
   case kind::BITVECTOR_CONCAT: out << "concat "; break;
   case kind::BITVECTOR_AND: out << "bvand "; break;

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index a2b21aa403df722ab561ebd653a22e107726343d..4b479e3482e2208c82ad1b04ba5602bc351a270f 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -43,7 +43,8 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
     d_nf_pairs(c),
        //d_var_lmin( c ),
        //d_var_lmax( c ),
-       d_str_ctn( c ),
+       d_str_pos_ctn( c ),
+       d_str_neg_ctn( c ),
        d_reg_exp_mem( c ),
        d_curr_cardinality( c, 0 )
 {
@@ -310,7 +311,7 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
                        }
                }
        }
-       Trace("strings-model") << "String Model : Finished." << std::endl;
+       Trace("strings-model") << "String Model : Pure Assigned." << std::endl;
        //step 4 : assign constants to all other equivalence classes
        for( unsigned i=0; i<nodes.size(); i++ ){
                if( processed.find( nodes[i] )==processed.end() ){
@@ -338,6 +339,20 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) {
                        m->assertEquality( nodes[i], cc, true );
                }
        }
+       Trace("strings-model") << "String Model : Assigned." << std::endl;
+       //check for negative contains
+       /*
+       Trace("strings-model") << "String Model : Check Neg Contains, size = " << d_str_neg_ctn.size() << std::endl;
+       for( unsigned i=0; i<d_str_neg_ctn.size(); i++ ) {
+               Node x = d_str_neg_ctn[i][0];
+               Node y = d_str_neg_ctn[i][1];
+               Trace("strings-model") << "String Model : Check Neg contains: ~contains(" << x << ", " << y << ")." << std::endl;
+               //Node xv = m->getValue(x);
+               //Node yv = m->getValue(y);
+               //Trace("strings-model") << "String Model : Check Neg contains Value: ~contains(" << xv << ", " << yv << ")." << std::endl;
+       }
+       */
+       Trace("strings-model") << "String Model : Finished." << std::endl;
 }
 
 /////////////////////////////////////////////////////////////////////////////
@@ -408,7 +423,11 @@ void TheoryStrings::check(Effort e) {
        if ( atom.getKind() == kind::STRING_IN_REGEXP ) {
                d_reg_exp_mem.push_back( assertion );
        } else if (atom.getKind() == kind::STRING_STRCTN) {
-               d_str_ctn.push_back( assertion );
+               if(polarity) {
+                       d_str_pos_ctn.push_back( atom );
+               } else {
+                       d_str_neg_ctn.push_back( atom );
+               }
                d_equalityEngine.assertPredicate(atom, polarity, fact);
     } else if (atom.getKind() == kind::EQUAL) {
                d_equalityEngine.assertEquality(atom, polarity, fact);
@@ -2093,68 +2112,114 @@ bool TheoryStrings::checkMemberships() {
 }
 
 bool TheoryStrings::checkContains() {
-       bool is_unk = false;
+       bool addedLemma = checkPosContains();
+       Trace("strings-process") << "Done check positive contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+       if(!addedLemma) {
+               addedLemma = checkNegContains();
+               Trace("strings-process") << "Done check positive contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+       }
+       return addedLemma;
+}
+
+bool TheoryStrings::checkPosContains() {
        bool addedLemma = false;
-       for( unsigned i=0; i<d_str_ctn.size(); i++ ){
-               Node assertion = d_str_ctn[i];
-               Trace("strings-ctn") << "We have contain assertion : " << assertion << std::endl;
-               Node atom = assertion.getKind()==kind::NOT ? assertion[0] : assertion;
-               bool polarity = assertion.getKind()!=kind::NOT;
-               if( polarity ) {
-                       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_ctn_rewritten.find(atom) == d_str_ctn_rewritten.end()) {
-                                       // Add lemma
-                                       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( assertion, eq, "POS-INC" );
-                                       addedLemma = true;
-                                       d_str_ctn_rewritten[ atom ] = true;
-                               } else {
-                                       Trace("strings-ctn") << "... is already rewritten." << std::endl;
-                               }
+       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;
                        } else {
-                               Trace("strings-ctn") << "... is satisfied." << std::endl;
+                               Trace("strings-ctn") << "... is already rewritten." << std::endl;
                        }
                } else {
-                       if( areEqual( atom[1], d_emptyString ) ) {
-                               Node ant = NodeManager::currentNM()->mkNode( kind::AND, assertion, 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, assertion, 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 = getLengthTerm(x);
-                                       Node lens = getLengthTerm(s);
-                                       if(areEqual(lenx, lens)) {
-                                               if(d_str_ctn_eqlen.find(assertion) == d_str_ctn_eqlen.end()) {
-                                                       Node eq = lenx.eqNode(lens);
-                                                       Node antc = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, assertion, eq ) );
-                                                       Node xneqs = x.eqNode(s).negate();
-                                                       d_str_ctn_eqlen[ assertion ] = true;
-                                                       sendLemma( antc, xneqs, "NEG-CTN-EQL" );
-                                                       addedLemma = true;
-                                               }
-                                       } else if(!areDisequal(lenx, lens)) {
-                                               sendSplit(lenx, lens, "NEG-CTN-SP");
+                       Trace("strings-ctn") << "... is satisfied." << std::endl;
+               }
+       }
+       if( addedLemma ){
+               doPendingLemmas();
+               return true;
+       } else {
+               return false;
+       }
+}
+
+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" );
                                                addedLemma = true;
-                                       } else {
-                                               addedLemma = processNegContains(assertion);
                                        }
+                               } else if(!areDisequal(lenx, lens)) {
+                                       sendSplit(lenx, lens, "NEG-CTN-SP");
+                                       addedLemma = true;
                                } else {
-                                       Trace("strings-ctn") << "Strings Incomplete (due to Negative Contain) by default." << std::endl;
-                                       is_unk = true;
+                                       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;
+                                       }
                                }
+                       } else {
+                               Trace("strings-ctn") << "Strings Incomplete (due to Negative Contain) by default." << std::endl;
+                               is_unk = true;
                        }
                }
        }
@@ -2163,34 +2228,13 @@ bool TheoryStrings::checkContains() {
                return true;
        } else {
                if( is_unk ){
-                       Trace("strings-inc") << "Strings::inc: possibly incomplete." << std::endl;
+                       Trace("strings-ctn") << "Strings::inc: possibly incomplete." << std::endl;
                        d_out->setIncomplete();
                }
                return false;
        }
 }
 
-bool TheoryStrings::processNegContains(Node assertion) {
-       Node atom = assertion[0];
-       Node x = atom[0];
-       Node s = atom[1];
-       Node lenx = getLengthTerm(x);
-       Node lens = getLengthTerm(s);
-
-       if(d_str_ctn_rewritten.find(assertion) == d_str_ctn_rewritten.end()) {
-               Node sk1 = NodeManager::currentNM()->mkSkolem( "sc3_$$", s.getType(), "created for contain" );
-               Node sk2 = NodeManager::currentNM()->mkSkolem( "sc4_$$", s.getType(), "created for contain" );
-               Node eq = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, s, sk2 ) ) );
-               Node gt = NodeManager::currentNM()->mkNode( kind::GT, lenx, lens );
-               Node antc = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, assertion, eq, gt ) );
-               d_str_ctn_rewritten[ assertion ] = true;
-               sendLemma( antc, d_false, "NEG-INC-BRK" );
-               return true;
-       } else {
-               return false;
-       }
-}
-
 CVC4::String TheoryStrings::getHeadConst( Node x ) {
        if( x.isConst() ) {
                return x.getConst< String >();

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 77ea298bdde098aea51e625c8ee576592c301993..1d92abbd279253801937efe95dfa799fba52936d 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -218,7 +218,8 @@ private:
     bool checkInductiveEquations();
        bool checkMemberships();
        bool checkContains();
-       bool processNegContains(Node assertion);
+       bool checkPosContains();
+       bool checkNegContains();
 
 public:
        void preRegisterTerm(TNode n);
@@ -273,9 +274,11 @@ private:
        int getMaxPossibleLength( Node x );
 
        // Special String Functions
-       NodeList d_str_ctn;
+       NodeList d_str_pos_ctn;
+       NodeList d_str_neg_ctn;
        std::map< Node, bool > d_str_ctn_eqlen;
-       std::map< Node, bool > d_str_ctn_rewritten;
+       std::map< Node, bool > d_str_pos_ctn_rewritten;
+       std::map< Node, bool > d_str_neg_ctn_rewritten;
 
        // Regular Expression
 private:

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index f68deda54fef30bf78a1bed98c7b691cb41e5258..d217548208cd56124d25fa2e30422abeffce111f 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -352,7 +352,9 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
                        }
                }
        } else if(node.getKind() == kind::STRING_STRCTN) {
-               if( node[0].isConst() && node[1].isConst() ) {
+               if( node[0] == node[1] ) {
+                       retNode = NodeManager::currentNM()->mkConst( true );
+               } else if( node[0].isConst() && node[1].isConst() ) {
                        CVC4::String s = node[0].getConst<String>();
                        CVC4::String t = node[1].getConst<String>();
                        if( s.find(t) != std::string::npos ) {