src/theory/strings/theory_strings_preprocess.cpp

   1 /*********************                                                        */
   2 /*! \file theory_strings_preprocess.cpp
   3  ** \verbatim
   4  ** Original author: Tianyi Liang
   5  ** Major contributors: Morgan Deters
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Strings Preprocess
  13  **
  14  ** Strings Preprocess.
  15  **/
  16
  17 #include "theory/strings/theory_strings_preprocess.h"
  18 #include "expr/kind.h"
  19 #include "theory/strings/options.h"
  20 #include "smt/logic_exception.h"
  21
  22 namespace CVC4 {
  23 namespace theory {
  24 namespace strings {
  25
  26 StringsPreprocess::StringsPreprocess() {
  27         std::vector< TypeNode > argTypes;
  28         argTypes.push_back(NodeManager::currentNM()->stringType());
  29         argTypes.push_back(NodeManager::currentNM()->integerType());
  30
  31         //Constants
  32         d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
  33 }
  34
  35 void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret, std::vector< Node > &nn ) {
  36         int k = r.getKind();
  37         switch( k ) {
  38                 case kind::STRING_TO_REGEXP:
  39                 {
  40                         Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, r[0] );
  41                         ret.push_back( eq );
  42                 }
  43                         break;
  44                 case kind::REGEXP_CONCAT:
  45                 {
  46                         std::vector< Node > cc;
  47                         for(unsigned i=0; i<r.getNumChildren(); ++i) {
  48                                 if(r[i].getKind() == kind::STRING_TO_REGEXP) {
  49                                         cc.push_back( r[i][0] );
  50                                 } else {
  51                                         Node sk = NodeManager::currentNM()->mkSkolem( "recsym_$$", s.getType(), "created for regular expression concat" );
  52                                         simplifyRegExp( sk, r[i], ret, nn );
  53                                         cc.push_back( sk );
  54                                 }
  55                         }
  56                         Node cc_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s,
  57                                                 NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, cc ) );
  58                         nn.push_back( cc_eq );
  59                 }
  60                         break;
  61                 case kind::REGEXP_OR:
  62                 {
  63                         std::vector< Node > c_or;
  64                         for(unsigned i=0; i<r.getNumChildren(); ++i) {
  65                                 simplifyRegExp( s, r[i], c_or, nn );
  66                         }
  67                         Node eq = NodeManager::currentNM()->mkNode( kind::OR, c_or );
  68                         ret.push_back( eq );
  69                 }
  70                         break;
  71                 case kind::REGEXP_INTER:
  72                         for(unsigned i=0; i<r.getNumChildren(); ++i) {
  73                                 simplifyRegExp( s, r[i], ret, nn );
  74                         }
  75                         break;
  76                 case kind::REGEXP_STAR:
  77                 {
  78                         Node eq = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, s, r );
  79                         ret.push_back( eq );
  80                 }
  81                         break;
  82                 default:
  83                         //TODO: special sym: sigma, none, all
  84                         Trace("strings-preprocess") << "Unsupported term: " << r << " in simplifyRegExp." << std::endl;
  85                         Assert( false );
  86                         break;
  87         }
  88 }
  89
  90 bool StringsPreprocess::checkStarPlus( Node t ) {
  91         if( t.getKind() != kind::REGEXP_STAR && t.getKind() != kind::REGEXP_PLUS ) {
  92                 for( unsigned i = 0; i<t.getNumChildren(); ++i ) {
  93                         if( checkStarPlus(t[i]) ) return true;
  94                 }
  95                 return false;
  96         } else {
  97                 return true;
  98         }
  99 }
 100 int StringsPreprocess::checkFixLenVar( Node t ) {
 101         int ret = 2;
 102         if(t.getKind() == kind::EQUAL) {
 103                 if(t[0].getType().isInteger() && t[0].isConst() && t[1].getKind() == kind::STRING_LENGTH) {
 104                         if(t[1][0].getKind() == kind::VARIABLE) {
 105                                 ret = 0;
 106                         }
 107                 } else if(t[1].getType().isInteger() && t[1].isConst() && t[0].getKind() == kind::STRING_LENGTH) {
 108                         if(t[0][0].getKind() == kind::VARIABLE) {
 109                                 ret = 1;
 110                         }
 111                 }
 112         }
 113         if(ret != 2) {
 114                 int len = t[ret].getConst<Rational>().getNumerator().toUnsignedInt();
 115                 if(len < 2) {
 116                         ret = 2;
 117                 }
 118         }
 119         if(!options::stringExp()) {
 120                 ret = 2;
 121         }
 122         return ret;
 123 }
 124 Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 125     std::hash_map<TNode, Node, TNodeHashFunction>::const_iterator i = d_cache.find(t);
 126     if(i != d_cache.end()) {
 127       return (*i).second.isNull() ? t : (*i).second;
 128     }
 129
 130         Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << std::endl;
 131         Node retNode = t;
 132         /*int c_id = checkFixLenVar(t);
 133         if( c_id != 2 ) {
 134                 int v_id = 1 - c_id;
 135                 int len = t[c_id].getConst<Rational>().getNumerator().toUnsignedInt();
 136                 if(len > 1) {
 137                         Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
 138                         std::vector< Node > vec;
 139                         for(int i=0; i<len; i++) {
 140                                 Node num = NodeManager::currentNM()->mkConst( ::CVC4::Rational(i) );
 141                                 //Node sk = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT, t[v_id][0], num);
 142                                 Node sk = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, t[v_id][0], num, one);
 143                                 vec.push_back(sk);
 144                                 Node cc = one.eqNode(NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ));
 145                                 new_nodes.push_back( cc );
 146                         }
 147                         Node lem = t[v_id][0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, vec ) );
 148                         lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, t, lem );
 149                         new_nodes.push_back( lem );
 150                         d_cache[t] = t;
 151                         retNode = t;
 152                 }
 153         } else */if( t.getKind() == kind::STRING_IN_REGEXP ) {
 154                 // t0 in t1
 155                 Node t0 = simplify( t[0], new_nodes );
 156
 157                 //if(!checkStarPlus( t[1] )) {
 158                         //rewrite it
 159                         std::vector< Node > ret;
 160                         std::vector< Node > nn;
 161                         simplifyRegExp( t0, t[1], ret, nn );
 162                         new_nodes.insert( new_nodes.end(), nn.begin(), nn.end() );
 163
 164                         Node n = ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret );
 165                         d_cache[t] = (t == n) ? Node::null() : n;
 166                         retNode = n;
 167                 //} else {
 168                         // TODO
 169                 //      return (t0 == t[0]) ? t : NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, t0, t[1] );
 170                 //}
 171         } else if( t.getKind() == kind::STRING_SUBSTR_TOTAL ) {
 172                 Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ,
 173                                                         NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ),
 174                                                         NodeManager::currentNM()->mkNode( kind::PLUS, t[1], t[2] ) );
 175                 Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, t[1], d_zero);
 176                 Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, t[2], d_zero);
 177                 Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
 178                 Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" );
 179                 Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" );
 180                 Node x_eq_123 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, t, sk3 ) );
 181                 Node len_sk1_eq_i = t[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
 182                 //Node len_uf_eq_j = t[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, uf ) );
 183                 Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond,
 184                                                 NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i ),
 185                                                 t.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") )) ));
 186                 new_nodes.push_back( lemma );
 187                 retNode = t;
 188                 d_cache[t] = t;
 189         } else if( t.getKind() == kind::STRING_STRIDOF ) {
 190                 if(options::stringExp()) {
 191                         Node sk1 = NodeManager::currentNM()->mkSkolem( "io1_$$", t[0].getType(), "created for indexof" );
 192                         Node sk2 = NodeManager::currentNM()->mkSkolem( "io2_$$", t[0].getType(), "created for indexof" );
 193                         Node sk3 = NodeManager::currentNM()->mkSkolem( "io3_$$", t[0].getType(), "created for indexof" );
 194                         Node sk4 = NodeManager::currentNM()->mkSkolem( "io4_$$", t[0].getType(), "created for indexof" );
 195                         Node skk = NodeManager::currentNM()->mkSkolem( "iok_$$", t[2].getType(), "created for indexof" );
 196                         Node eq = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3, sk4 ) );
 197                         new_nodes.push_back( eq );
 198                         Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
 199                         Node krange = NodeManager::currentNM()->mkNode( kind::GEQ, skk, negone );
 200                         new_nodes.push_back( krange );
 201                         krange = NodeManager::currentNM()->mkNode( kind::GT,
 202                                                 NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), skk);
 203                         new_nodes.push_back( krange );
 204
 205                         //str.len(s1) < y + str.len(s2)
 206                         Node c1 = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::GT,
 207                                                         NodeManager::currentNM()->mkNode( kind::PLUS, t[2], NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[1] )),
 208                                                         NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] )));
 209                         //str.len(t1) = y
 210                         Node c2 = t[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
 211                         //~contain(t234, s2)
 212                         Node c3 = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::STRING_STRCTN,
 213                                                 NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk2, sk3, sk4), t[1] ).negate());
 214                         //left
 215                         Node left = NodeManager::currentNM()->mkNode( kind::OR, c1, NodeManager::currentNM()->mkNode( kind::AND, c2, c3 ) );
 216                         //t3 = s2
 217                         Node c4 = t[1].eqNode( sk3 );
 218                         //~contain(t2, s2)
 219                         Node c5 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, sk2, t[1] ).negate();
 220                         //k=str.len(s1, s2)
 221                         Node c6 = skk.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH,
 222                                                                         NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2 )));
 223                         //right
 224                         Node right = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::AND, c2, c4, c5, c6 ));
 225                         Node cond = skk.eqNode( negone );
 226                         Node rr = NodeManager::currentNM()->mkNode( kind::ITE, cond, left, right );
 227                         new_nodes.push_back( rr );
 228                         d_cache[t] = skk;
 229                         retNode = skk;
 230                 } else {
 231                         throw LogicException("string indexof not supported in this release");
 232                 }
 233         } else if( t.getKind() == kind::STRING_ITOS ) {
 234                 if(options::stringExp()) {
 235                         Node num = t[0];//NodeManager::currentNM()->mkNode(kind::ABS, t[0]);
 236                         Node pret = NodeManager::currentNM()->mkNode(kind::STRING_ITOS, num);
 237                         Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, pret);
 238
 239                         Node b1 = NodeManager::currentNM()->mkBoundVar("x", NodeManager::currentNM()->integerType());
 240                         Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);
 241                         Node g1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, b1, d_zero ),
 242                                                 NodeManager::currentNM()->mkNode( kind::GT, lenp, b1 ) ) );
 243                         Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
 244                         Node nine = NodeManager::currentNM()->mkConst( ::CVC4::Rational(9) );
 245                         Node ten = NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) );
 246
 247                         std::vector< TypeNode > argTypes;
 248                         argTypes.push_back(NodeManager::currentNM()->integerType());
 249                         Node ufP = NodeManager::currentNM()->mkSkolem("ufP_$$",
 250                                                                 NodeManager::currentNM()->mkFunctionType(
 251                                                                         argTypes, NodeManager::currentNM()->integerType()),
 252                                                                 "uf type conv P");
 253                         Node ufM = NodeManager::currentNM()->mkSkolem("ufM_$$",
 254                                                                 NodeManager::currentNM()->mkFunctionType(
 255                                                                         argTypes, NodeManager::currentNM()->integerType()),
 256                                                                 "uf type conv M");
 257
 258                         new_nodes.push_back( num.eqNode(NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero)) );
 259                         new_nodes.push_back( NodeManager::currentNM()->mkNode(kind::GT, lenp, d_zero) );
 260
 261                         Node ufx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, b1);
 262                         Node ufx1 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, NodeManager::currentNM()->mkNode(kind::MINUS,b1,one));
 263                         Node ufMx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, b1);
 264                         Node b1gtz = NodeManager::currentNM()->mkNode(kind::GT, b1, d_zero);
 265                         Node cc1 = ufx1.eqNode( NodeManager::currentNM()->mkNode(kind::PLUS,
 266                                                         NodeManager::currentNM()->mkNode(kind::MULT, ufx, ten),
 267                                                         NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, NodeManager::currentNM()->mkNode(kind::MINUS,b1,one)) ));
 268                         cc1 = NodeManager::currentNM()->mkNode(kind::IMPLIES, b1gtz, cc1);
 269                         Node lstx = lenp.eqNode(NodeManager::currentNM()->mkNode(kind::PLUS, b1, one));
 270                         Node cc2 = ufx.eqNode(ufMx);
 271                         cc2 = NodeManager::currentNM()->mkNode(kind::IMPLIES, lstx, cc2);
 272                         Node cc3 = NodeManager::currentNM()->mkNode(kind::GEQ, ufMx, d_zero);
 273                         Node cc4 = NodeManager::currentNM()->mkNode(kind::GEQ, nine, ufMx);
 274
 275                         Node b21 = NodeManager::currentNM()->mkBoundVar("y", NodeManager::currentNM()->stringType());
 276                         Node b22 = NodeManager::currentNM()->mkBoundVar("z", NodeManager::currentNM()->stringType());
 277                         Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b21, b22);
 278
 279                         Node c21 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, b21).eqNode(
 280                                                 NodeManager::currentNM()->mkNode(kind::MINUS, lenp,     NodeManager::currentNM()->mkNode(kind::PLUS, b1, one) ));
 281                         Node ch =
 282                                 NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(0))),
 283                                 NodeManager::currentNM()->mkConst(::CVC4::String("0")),
 284                                 NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(1))),
 285                                 NodeManager::currentNM()->mkConst(::CVC4::String("1")),
 286                                 NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(2))),
 287                                 NodeManager::currentNM()->mkConst(::CVC4::String("2")),
 288                                 NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(3))),
 289                                 NodeManager::currentNM()->mkConst(::CVC4::String("3")),
 290                                 NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(4))),
 291                                 NodeManager::currentNM()->mkConst(::CVC4::String("4")),
 292                                 NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(5))),
 293                                 NodeManager::currentNM()->mkConst(::CVC4::String("5")),
 294                                 NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(6))),
 295                                 NodeManager::currentNM()->mkConst(::CVC4::String("6")),
 296                                 NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(7))),
 297                                 NodeManager::currentNM()->mkConst(::CVC4::String("7")),
 298                                 NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(8))),
 299                                 NodeManager::currentNM()->mkConst(::CVC4::String("8")),
 300                                 NodeManager::currentNM()->mkConst(::CVC4::String("9")))))))))));
 301                         Node c22 = pret.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, b21, ch, b22) );
 302                         Node cc5 = NodeManager::currentNM()->mkNode(kind::EXISTS, b2v, NodeManager::currentNM()->mkNode(kind::AND, c21, c22));
 303                         //Node pos = NodeManager::currentNM()->mkNode(kind::MINUS, lenp, NodeManager::currentNM()->mkNode(kind::PLUS, b1, one));
 304                         //Node cc5 = ch.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, pret, pos, one) );
 305                         Node conc = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, cc1, cc2, cc3, cc4, cc5) );
 306                         conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, g1, conc );
 307                         conc = NodeManager::currentNM()->mkNode( kind::FORALL, b1v, conc );
 308                         new_nodes.push_back( conc );
 309                         /*
 310                         Node sign = NodeManager::currentNM()->mkNode(kind::ITE,
 311                                                         NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero),
 312                                                         NodeManager::currentNM()->mkConst(::CVC4::String("")),
 313                                                         NodeManager::currentNM()->mkConst(::CVC4::String("-")));
 314                         conc = t.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sign, pret) );
 315                         new_nodes.push_back( conc );*/
 316
 317                         d_cache[t] = t;
 318                         retNode = t;
 319                 } else {
 320                         throw LogicException("string int.to.str not supported in this release");
 321                 }
 322         } else if( t.getKind() == kind::STRING_STOI_TOTAL ) {
 323                 if(options::stringExp()) {
 324                         Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
 325                         Node nine = NodeManager::currentNM()->mkConst( ::CVC4::Rational(9) );
 326                         Node ten = NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) );
 327                         std::vector< TypeNode > argTypes;
 328                         argTypes.push_back(NodeManager::currentNM()->integerType());
 329                         Node ufP = NodeManager::currentNM()->mkSkolem("ufP_$$",
 330                                                                 NodeManager::currentNM()->mkFunctionType(
 331                                                                         argTypes, NodeManager::currentNM()->integerType()),
 332                                                                 "uf type conv P");
 333                         Node ufM = NodeManager::currentNM()->mkSkolem("ufM_$$",
 334                                                                 NodeManager::currentNM()->mkFunctionType(
 335                                                                         argTypes, NodeManager::currentNM()->integerType()),
 336                                                                 "uf type conv M");
 337
 338                         Node ufP0 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero);
 339                         new_nodes.push_back(t.eqNode(ufP0));
 340                         //cc1
 341                         Node cc1 = t[0].eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("")));
 342                         cc1 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(d_zero), cc1);
 343                         //cc2
 344                         Node b1 = NodeManager::currentNM()->mkBoundVar("x", NodeManager::currentNM()->integerType());
 345                         Node z1 = NodeManager::currentNM()->mkBoundVar("z1", NodeManager::currentNM()->stringType());
 346                         Node z2 = NodeManager::currentNM()->mkBoundVar("z2", NodeManager::currentNM()->stringType());
 347                         Node z3 = NodeManager::currentNM()->mkBoundVar("z3", NodeManager::currentNM()->stringType());
 348                         Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1, z1, z2, z3);
 349                         std::vector< Node > vec_n;
 350                         Node g = NodeManager::currentNM()->mkNode(kind::GEQ, b1, d_zero);
 351                         vec_n.push_back(g);
 352                         g = NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, t[0]), b1);
 353                         vec_n.push_back(g);
 354                         g = b1.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, z1) );
 355                         vec_n.push_back(g);
 356                         g = one.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, z2) );
 357                         vec_n.push_back(g);
 358                         g = t[0].eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, z1, z2, z3) );
 359                         vec_n.push_back(g);
 360                         for(unsigned i=0; i<=9; i++) {
 361                                 char ch[2];
 362                                 ch[0] = i + '0'; ch[1] = '\0';
 363                                 std::string stmp(ch);
 364                                 g = z2.eqNode( NodeManager::currentNM()->mkConst(::CVC4::String(stmp)) ).negate();
 365                                 vec_n.push_back(g);
 366                         }
 367                         Node cc2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, vec_n));
 368                         cc2 = NodeManager::currentNM()->mkNode(kind::EXISTS, b1v, cc2);
 369                         cc2 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(d_zero), cc2);
 370                         //cc3
 371                         Node b2 = NodeManager::currentNM()->mkBoundVar("y", NodeManager::currentNM()->integerType());
 372                         Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2);
 373                         Node g2 = NodeManager::currentNM()->mkNode(kind::AND,
 374                                                 NodeManager::currentNM()->mkNode(kind::GEQ, b2, d_zero),
 375                                                 NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, t[0]), b2));
 376                         Node ufx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, b2);
 377                         Node ufx1 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, NodeManager::currentNM()->mkNode(kind::MINUS,b2,one));
 378                         Node ufMx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, b2);
 379                         Node w1 = NodeManager::currentNM()->mkBoundVar("w1", NodeManager::currentNM()->stringType());
 380                         Node w2 = NodeManager::currentNM()->mkBoundVar("w2", NodeManager::currentNM()->stringType());
 381                         Node b3v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, w1, w2);
 382                         Node b2gtz = NodeManager::currentNM()->mkNode(kind::GT, b2, d_zero);
 383                         Node c3c1 = ufx1.eqNode( NodeManager::currentNM()->mkNode(kind::PLUS,
 384                                                         NodeManager::currentNM()->mkNode(kind::MULT, ufx, ten),
 385                                                         NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, NodeManager::currentNM()->mkNode(kind::MINUS,b2,one)) ));
 386                         c3c1 = NodeManager::currentNM()->mkNode(kind::AND, NodeManager::currentNM()->mkNode(kind::GT, ufx, d_zero), c3c1);
 387                         c3c1 = NodeManager::currentNM()->mkNode(kind::IMPLIES, b2gtz, c3c1);
 388                         Node lstx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH,t[0]).eqNode(NodeManager::currentNM()->mkNode(kind::PLUS, b2, one));
 389                         Node c3c2 = ufx.eqNode(ufMx);
 390                         c3c2 = NodeManager::currentNM()->mkNode(kind::IMPLIES, lstx, c3c2);
 391                         Node c3c3 = NodeManager::currentNM()->mkNode(kind::GEQ, ufMx, d_zero);
 392                         Node c3c4 = NodeManager::currentNM()->mkNode(kind::GEQ, nine, ufMx);
 393                         Node rev = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, w1).eqNode(
 394                                                 NodeManager::currentNM()->mkNode(kind::MINUS, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH,t[0]),
 395                                                 NodeManager::currentNM()->mkNode(kind::PLUS, b2, one)));
 396                         Node ch =
 397                                 NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(0))),
 398                                 NodeManager::currentNM()->mkConst(::CVC4::String("0")),
 399                                 NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(1))),
 400                                 NodeManager::currentNM()->mkConst(::CVC4::String("1")),
 401                                 NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(2))),
 402                                 NodeManager::currentNM()->mkConst(::CVC4::String("2")),
 403                                 NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(3))),
 404                                 NodeManager::currentNM()->mkConst(::CVC4::String("3")),
 405                                 NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(4))),
 406                                 NodeManager::currentNM()->mkConst(::CVC4::String("4")),
 407                                 NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(5))),
 408                                 NodeManager::currentNM()->mkConst(::CVC4::String("5")),
 409                                 NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(6))),
 410                                 NodeManager::currentNM()->mkConst(::CVC4::String("6")),
 411                                 NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(7))),
 412                                 NodeManager::currentNM()->mkConst(::CVC4::String("7")),
 413                                 NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(8))),
 414                                 NodeManager::currentNM()->mkConst(::CVC4::String("8")),
 415                                 NodeManager::currentNM()->mkConst(::CVC4::String("9")))))))))));
 416                         Node c3c5 = t[0].eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, w1, ch, w2));
 417                         c3c5 = NodeManager::currentNM()->mkNode(kind::AND, rev, c3c5);
 418                         c3c5 = NodeManager::currentNM()->mkNode(kind::EXISTS, b3v, c3c5);
 419                         Node cc3 = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, c3c1, c3c2, c3c3, c3c4, c3c5) );
 420                         cc3 = NodeManager::currentNM()->mkNode(kind::IMPLIES, g2, cc3);
 421                         cc3 = NodeManager::currentNM()->mkNode(kind::FORALL, b2v, cc3);
 422                         //conc
 423                         Node conc = NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2, cc3);
 424                         new_nodes.push_back( conc );
 425                         d_cache[t] = t;
 426                         retNode = t;
 427                 } else {
 428                         throw LogicException("string int.to.str not supported in this release");
 429                 }
 430         } else if( t.getKind() == kind::STRING_STRREPL ) {
 431                 if(options::stringExp()) {
 432                         Node x = t[0];
 433                         Node y = t[1];
 434                         Node z = t[2];
 435                         Node sk1 = NodeManager::currentNM()->mkSkolem( "rp1_$$", t[0].getType(), "created for replace" );
 436                         Node sk2 = NodeManager::currentNM()->mkSkolem( "rp2_$$", t[0].getType(), "created for replace" );
 437                         Node skw = NodeManager::currentNM()->mkSkolem( "rpw_$$", t[0].getType(), "created for replace" );
 438                         Node cond = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, x, y );
 439                         Node c1 = x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, y, sk2 ) );
 440                         Node c2 = skw.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, z, sk2 ) );
 441                         Node c3 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, sk1, y ).negate();
 442                         Node rr = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond,
 443                                                         NodeManager::currentNM()->mkNode( kind::AND, c1, c2, c3 ),
 444                                                         skw.eqNode(x) ) );
 445                         new_nodes.push_back( rr );
 446
 447                         d_cache[t] = skw;
 448                         retNode = skw;
 449                 } else {
 450                         throw LogicException("string replace not supported in this release");
 451                 }
 452         } else if( t.getNumChildren()>0 ) {
 453                 std::vector< Node > cc;
 454                 if (t.getMetaKind() == kind::metakind::PARAMETERIZED) {
 455                         cc.push_back(t.getOperator());
 456                 }
 457                 bool changed = false;
 458                 for( unsigned i=0; i<t.getNumChildren(); i++ ){
 459                         Node tn = simplify( t[i], new_nodes );
 460                         cc.push_back( tn );
 461                         changed = changed || tn!=t[i];
 462                 }
 463                 if(changed) {
 464                         Node n = NodeManager::currentNM()->mkNode( t.getKind(), cc );
 465                         d_cache[t] = n;
 466                         retNode = n;
 467                 } else {
 468                         d_cache[t] = Node::null();
 469                         retNode = t;
 470                 }
 471         }else{
 472                 d_cache[t] = Node::null();
 473                 retNode = t;
 474         }
 475
 476         Trace("strings-preprocess") << "StringsPreprocess::simplify returns: " << retNode << std::endl;
 477         if(!new_nodes.empty()) {
 478                 Trace("strings-preprocess") << " ... new nodes (" << new_nodes.size() << "):\n";
 479                 for(unsigned int i=0; i<new_nodes.size(); ++i) {
 480                         Trace("strings-preprocess") << "\t" << new_nodes[i] << "\n";
 481                 }
 482         }
 483
 484         return retNode;
 485 }
 486
 487 void StringsPreprocess::simplify(std::vector< Node > &vec_node, std::vector< Node > &new_nodes) {
 488         for( unsigned i=0; i<vec_node.size(); i++ ){
 489                 vec_node[i] = simplify( vec_node[i], new_nodes );
 490         }
 491 }
 492
 493 void StringsPreprocess::simplify(std::vector< Node > &vec_node) {
 494         std::vector< Node > new_nodes;
 495         simplify(vec_node, new_nodes);
 496         vec_node.insert( vec_node.end(), new_nodes.begin(), new_nodes.end() );
 497 }
 498
 499 }/* CVC4::theory::strings namespace */
 500 }/* CVC4::theory namespace */
 501 }/* CVC4 namespace */