src/theory/strings/theory_strings_preprocess.cpp

   1 /*********************                                                        */
   2 /*! \file theory_strings_preprocess.cpp
   3  ** \verbatim
   4  ** Original author: Tianyi Liang
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): Morgan Deters
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  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 #include <stdint.h>
  22
  23 namespace CVC4 {
  24 namespace theory {
  25 namespace strings {
  26
  27 StringsPreprocess::StringsPreprocess() {
  28   //Constants
  29   d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
  30 }
  31
  32 void StringsPreprocess::processRegExp( Node s, Node r, std::vector< Node > &ret ) {
  33   int k = r.getKind();
  34   switch( k ) {
  35     case kind::REGEXP_EMPTY: {
  36       Node eq = NodeManager::currentNM()->mkConst( false );
  37       ret.push_back( eq );
  38       break;
  39     }
  40     case kind::REGEXP_SIGMA: {
  41       Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
  42       Node eq = one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s));
  43       ret.push_back( eq );
  44       break;
  45     }
  46     case kind::REGEXP_RANGE: {
  47       Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
  48       Node eq = one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s));
  49       ret.push_back( eq );
  50       eq = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, s, r );
  51       ret.push_back( eq );
  52       break;
  53     }
  54     case kind::STRING_TO_REGEXP: {
  55       Node eq = s.eqNode( r[0] );
  56       ret.push_back( eq );
  57       break;
  58     }
  59     case kind::REGEXP_CONCAT: {
  60       bool flag = true;
  61       std::vector< Node > cc;
  62       for(unsigned i=0; i<r.getNumChildren(); ++i) {
  63         if(r[i].getKind() == kind::STRING_TO_REGEXP) {
  64           cc.push_back( r[i][0] );
  65         } else {
  66           flag = false;
  67           break;
  68         }
  69       }
  70       if(flag) {
  71         Node eq = s.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, cc));
  72         ret.push_back(eq);
  73       } else {
  74         Node eq = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, s, r );
  75         ret.push_back( eq );
  76       }
  77       break;
  78     }
  79     case kind::REGEXP_UNION: {
  80       std::vector< Node > c_or;
  81       for(unsigned i=0; i<r.getNumChildren(); ++i) {
  82         std::vector< Node > ntmp;
  83         processRegExp( s, r[i], ntmp );
  84         Node lem = ntmp.size()==1 ? ntmp[0] : NodeManager::currentNM()->mkNode(kind::AND, ntmp);
  85         c_or.push_back( lem );
  86       }
  87       Node eq = NodeManager::currentNM()->mkNode(kind::OR, c_or);
  88       ret.push_back( eq );
  89       break;
  90     }
  91     case kind::REGEXP_INTER: {
  92       for(unsigned i=0; i<r.getNumChildren(); ++i) {
  93         processRegExp( s, r[i], ret );
  94       }
  95       break;
  96     }
  97     case kind::REGEXP_STAR: {
  98       if(r[0].getKind() == kind::REGEXP_SIGMA) {
  99         ret.push_back(NodeManager::currentNM()->mkConst(true));
 100       } else {
 101         Node eq = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, s, r );
 102         ret.push_back( eq );
 103       }
 104       break;
 105     }
 106     case kind::REGEXP_LOOP: {
 107       Node eq = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, s, r );
 108       ret.push_back( eq );
 109       break;
 110     }
 111     default: {
 112       Trace("strings-error") << "Unsupported term: " << r << " in simplifyRegExp." << std::endl;
 113       Assert( false, "Unsupported Term" );
 114     }
 115   }
 116 }
 117
 118 bool StringsPreprocess::checkStarPlus( Node t ) {
 119   if( t.getKind() != kind::REGEXP_STAR && t.getKind() != kind::REGEXP_PLUS ) {
 120     for( unsigned i = 0; i<t.getNumChildren(); ++i ) {
 121       if( checkStarPlus(t[i]) ) return true;
 122     }
 123     return false;
 124   } else {
 125     return true;
 126   }
 127 }
 128 int StringsPreprocess::checkFixLenVar( Node t ) {
 129   int ret = 2;
 130   if(t.getKind() == kind::EQUAL) {
 131     if(t[0].getType().isInteger() && t[0].isConst() && t[1].getKind() == kind::STRING_LENGTH) {
 132       if(t[1][0].getKind() == kind::VARIABLE) {
 133         ret = 0;
 134       }
 135     } else if(t[1].getType().isInteger() && t[1].isConst() && t[0].getKind() == kind::STRING_LENGTH) {
 136       if(t[0][0].getKind() == kind::VARIABLE) {
 137         ret = 1;
 138       }
 139     }
 140   }
 141   if(ret != 2) {
 142     unsigned len = t[ret].getConst<Rational>().getNumerator().toUnsignedInt();
 143     if(len < 2) {
 144       ret = 2;
 145     }
 146   }
 147   if(!options::stringExp()) {
 148     ret = 2;
 149   }
 150   return ret;
 151 }
 152 Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 153   std::hash_map<TNode, Node, TNodeHashFunction>::const_iterator i = d_cache.find(t);
 154   if(i != d_cache.end()) {
 155     return (*i).second.isNull() ? t : (*i).second;
 156   }
 157
 158   Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << std::endl;
 159   Node retNode = t;
 160   /*int c_id = checkFixLenVar(t);
 161   if( c_id != 2 ) {
 162     int v_id = 1 - c_id;
 163     int len = t[c_id].getConst<Rational>().getNumerator().toUnsignedInt();
 164     if(len > 1) {
 165       Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
 166       std::vector< Node > vec;
 167       for(int i=0; i<len; i++) {
 168         Node num = NodeManager::currentNM()->mkConst( ::CVC4::Rational(i) );
 169         //Node sk = NodeManager::currentNM()->mkNode(kind::STRING_CHARAT, t[v_id][0], num);
 170         Node sk = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, t[v_id][0], num, one);
 171         vec.push_back(sk);
 172         Node cc = one.eqNode(NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ));
 173         new_nodes.push_back( cc );
 174       }
 175       Node lem = t[v_id][0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, vec ) );
 176       lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, t, lem );
 177       new_nodes.push_back( lem );
 178       d_cache[t] = t;
 179       retNode = t;
 180     }
 181   } else */
 182   if( t.getKind() == kind::STRING_IN_REGEXP ) {
 183     Node t0 = simplify( t[0], new_nodes );
 184
 185     //rewrite it
 186     std::vector< Node > ret;
 187     processRegExp( t0, t[1], ret );
 188
 189     Node n = ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret );
 190     n = Rewriter::rewrite(n);
 191     d_cache[t] = (t == n) ? Node::null() : n;
 192     retNode = n;
 193   } else if( t.getKind() == kind::STRING_SUBSTR_TOTAL ) {
 194     Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ,
 195           NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ),
 196           NodeManager::currentNM()->mkNode( kind::PLUS, t[1], t[2] ) );
 197     Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, t[1], d_zero);
 198     Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, t[2], d_zero);
 199     Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
 200     Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1", NodeManager::currentNM()->stringType(), "created for charat/substr" );
 201     Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3", NodeManager::currentNM()->stringType(), "created for charat/substr" );
 202     Node x_eq_123 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, t, sk3 ) );
 203     Node len_sk1_eq_i = t[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
 204     Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond,
 205             NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i ),
 206             t.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") )) ));
 207     new_nodes.push_back( lemma );
 208     retNode = t;
 209     d_cache[t] = t;
 210   } else if( t.getKind() == kind::STRING_STRIDOF ) {
 211     if(options::stringExp()) {
 212       Node sk1 = NodeManager::currentNM()->mkSkolem( "io1", NodeManager::currentNM()->stringType(), "created for indexof" );
 213       Node sk2 = NodeManager::currentNM()->mkSkolem( "io2", NodeManager::currentNM()->stringType(), "created for indexof" );
 214       Node sk3 = NodeManager::currentNM()->mkSkolem( "io3", NodeManager::currentNM()->stringType(), "created for indexof" );
 215       Node sk4 = NodeManager::currentNM()->mkSkolem( "io4", NodeManager::currentNM()->stringType(), "created for indexof" );
 216       Node skk = NodeManager::currentNM()->mkSkolem( "iok", NodeManager::currentNM()->integerType(), "created for indexof" );
 217       Node eq = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3, sk4 ) );
 218       new_nodes.push_back( eq );
 219       Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
 220       Node krange = NodeManager::currentNM()->mkNode( kind::GEQ, skk, negone );
 221       new_nodes.push_back( krange );
 222       krange = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GT,
 223             NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ), skk) );
 224       new_nodes.push_back( krange );
 225       krange = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GT,
 226             NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[1] ), d_zero) );
 227       new_nodes.push_back( krange );
 228       krange = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GEQ,
 229             t[2], d_zero) );
 230       new_nodes.push_back( krange );
 231
 232       //str.len(s1) < y + str.len(s2)
 233       Node c1 = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::GT,
 234               NodeManager::currentNM()->mkNode( kind::PLUS, t[2], NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[1] )),
 235               NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] )));
 236       //str.len(t1) = y
 237       Node c2 = t[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
 238       //~contain(t234, s2)
 239       Node c3 = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::STRING_STRCTN,
 240             NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk2, sk3, sk4), t[1] ).negate());
 241       //left
 242       Node left = NodeManager::currentNM()->mkNode( kind::OR, c1, NodeManager::currentNM()->mkNode( kind::AND, c2, c3 ) );
 243       //t3 = s2
 244       Node c4 = t[1].eqNode( sk3 );
 245       //~contain(t2, s2)
 246       Node c5 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN,
 247                   NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sk2,
 248                     NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, t[1], d_zero,
 249                       NodeManager::currentNM()->mkNode(kind::MINUS,
 250                         NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, t[1]),
 251                         NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) )))),
 252                   t[1] ).negate();
 253       //k=str.len(s1, s2)
 254       Node c6 = skk.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH,
 255                   NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2 )));
 256       //right
 257       Node right = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::AND, c2, c4, c5, c6 ));
 258       Node cond = skk.eqNode( negone );
 259       Node rr = NodeManager::currentNM()->mkNode( kind::ITE, cond, left, right );
 260       new_nodes.push_back( rr );
 261       d_cache[t] = skk;
 262       retNode = skk;
 263     } else {
 264       throw LogicException("string indexof not supported in default mode, try --strings-exp");
 265     }
 266   } else if( t.getKind() == kind::STRING_ITOS || t.getKind() == kind::STRING_U16TOS || t.getKind() == kind::STRING_U32TOS ) {
 267     if(options::stringExp()) {
 268       //Node num = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE,
 269       //        NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero),
 270       //        t[0], NodeManager::currentNM()->mkNode(kind::UMINUS, t[0])));
 271       Node num = t[0];
 272       Node pret = NodeManager::currentNM()->mkNode(kind::STRING_ITOS, num);
 273       Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, pret);
 274
 275       Node nonneg = NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero);
 276       if(t.getKind()==kind::STRING_U16TOS) {
 277         nonneg = NodeManager::currentNM()->mkNode(kind::AND, nonneg, NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(UINT16_MAX) ), t[0]));
 278         Node lencond = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(5) ), lenp);
 279         new_nodes.push_back(lencond);
 280       } else if(t.getKind()==kind::STRING_U32TOS) {
 281         nonneg = NodeManager::currentNM()->mkNode(kind::AND, nonneg, NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(UINT32_MAX) ), t[0]));
 282         Node lencond = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) ), lenp);
 283         new_nodes.push_back(lencond);
 284       }
 285
 286       Node lem = NodeManager::currentNM()->mkNode(kind::IFF, nonneg.negate(),
 287         pret.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") ))//lenp.eqNode(d_zero)
 288         );
 289       new_nodes.push_back(lem);
 290
 291       //non-neg
 292       Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
 293       Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);
 294       Node g1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, b1, d_zero ),
 295             NodeManager::currentNM()->mkNode( kind::GT, lenp, b1 ) ) );
 296       Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
 297       Node nine = NodeManager::currentNM()->mkConst( ::CVC4::Rational(9) );
 298       Node ten = NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) );
 299
 300       std::vector< TypeNode > argTypes;
 301       argTypes.push_back(NodeManager::currentNM()->integerType());
 302       Node ufP = NodeManager::currentNM()->mkSkolem("ufP",
 303                 NodeManager::currentNM()->mkFunctionType(
 304                   argTypes, NodeManager::currentNM()->integerType()),
 305                 "uf type conv P");
 306       Node ufM = NodeManager::currentNM()->mkSkolem("ufM",
 307                 NodeManager::currentNM()->mkFunctionType(
 308                   argTypes, NodeManager::currentNM()->integerType()),
 309                 "uf type conv M");
 310
 311       lem = num.eqNode(NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero));
 312       new_nodes.push_back( lem );
 313
 314       Node ufx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, b1);
 315       Node ufx1 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, NodeManager::currentNM()->mkNode(kind::MINUS,b1,one));
 316       Node ufMx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, b1);
 317       Node b1gtz = NodeManager::currentNM()->mkNode(kind::GT, b1, d_zero);
 318       Node cc1 = ufx1.eqNode( NodeManager::currentNM()->mkNode(kind::PLUS,
 319               NodeManager::currentNM()->mkNode(kind::MULT, ufx, ten),
 320               NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, NodeManager::currentNM()->mkNode(kind::MINUS,b1,one)) ));
 321       cc1 = NodeManager::currentNM()->mkNode(kind::IMPLIES, b1gtz, cc1);
 322       Node lstx = lenp.eqNode(NodeManager::currentNM()->mkNode(kind::PLUS, b1, one));
 323       Node cc2 = ufx.eqNode(ufMx);
 324       cc2 = NodeManager::currentNM()->mkNode(kind::IMPLIES, lstx, cc2);
 325       // leading zero
 326       Node cl = NodeManager::currentNM()->mkNode(kind::AND, lstx, d_zero.eqNode(b1).negate());
 327       Node cc21 = NodeManager::currentNM()->mkNode(kind::IMPLIES, cl, NodeManager::currentNM()->mkNode(kind::GT, ufMx, d_zero));
 328       //cc3
 329       Node cc3 = NodeManager::currentNM()->mkNode(kind::GEQ, ufMx, d_zero);
 330       Node cc4 = NodeManager::currentNM()->mkNode(kind::GEQ, nine, ufMx);
 331
 332       Node b21 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
 333       Node b22 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
 334       Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b21, b22);
 335
 336       Node c21 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, b21).eqNode(
 337             NodeManager::currentNM()->mkNode(kind::MINUS, lenp, NodeManager::currentNM()->mkNode(kind::PLUS, b1, one) ));
 338       Node ch =
 339         NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(0))),
 340         NodeManager::currentNM()->mkConst(::CVC4::String("0")),
 341         NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(1))),
 342         NodeManager::currentNM()->mkConst(::CVC4::String("1")),
 343         NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(2))),
 344         NodeManager::currentNM()->mkConst(::CVC4::String("2")),
 345         NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(3))),
 346         NodeManager::currentNM()->mkConst(::CVC4::String("3")),
 347         NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(4))),
 348         NodeManager::currentNM()->mkConst(::CVC4::String("4")),
 349         NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(5))),
 350         NodeManager::currentNM()->mkConst(::CVC4::String("5")),
 351         NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(6))),
 352         NodeManager::currentNM()->mkConst(::CVC4::String("6")),
 353         NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(7))),
 354         NodeManager::currentNM()->mkConst(::CVC4::String("7")),
 355         NodeManager::currentNM()->mkNode(kind::ITE, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(8))),
 356         NodeManager::currentNM()->mkConst(::CVC4::String("8")),
 357         NodeManager::currentNM()->mkConst(::CVC4::String("9")))))))))));
 358       Node c22 = pret.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, b21, ch, b22) );
 359       Node cc5 = NodeManager::currentNM()->mkNode(kind::EXISTS, b2v, NodeManager::currentNM()->mkNode(kind::AND, c21, c22));
 360       std::vector< Node > svec;
 361       svec.push_back(cc1);svec.push_back(cc2);
 362       svec.push_back(cc21);
 363       svec.push_back(cc3);svec.push_back(cc4);svec.push_back(cc5);
 364       Node conc = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, svec) );
 365       conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, g1, conc );
 366       conc = NodeManager::currentNM()->mkNode( kind::FORALL, b1v, conc );
 367       conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, nonneg, conc );
 368       new_nodes.push_back( conc );
 369
 370       /*conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::IMPLIES,
 371               NodeManager::currentNM()->mkNode(kind::LT, t[0], d_zero),
 372               t.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT,
 373                 NodeManager::currentNM()->mkConst(::CVC4::String("-")), pret))));
 374       new_nodes.push_back( conc );*/
 375
 376       d_cache[t] = pret;
 377       if(t != pret) {
 378         d_cache[pret] = pret;
 379       }
 380       retNode = pret;
 381     } else {
 382       throw LogicException("string int.to.str not supported in default mode, try --strings-exp");
 383     }
 384   } else if( t.getKind() == kind::STRING_STOI || t.getKind() == kind::STRING_STOU16 || t.getKind() == kind::STRING_STOU32 ) {
 385     if(options::stringExp()) {
 386       Node str = t[0];
 387       Node pret = NodeManager::currentNM()->mkNode(kind::STRING_STOI, str);
 388       Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, str);
 389
 390       Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
 391       Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
 392       Node nine = NodeManager::currentNM()->mkConst( ::CVC4::Rational(9) );
 393       Node ten = NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) );
 394       std::vector< TypeNode > argTypes;
 395       argTypes.push_back(NodeManager::currentNM()->integerType());
 396       Node ufP = NodeManager::currentNM()->mkSkolem("ufP",
 397                 NodeManager::currentNM()->mkFunctionType(
 398                   argTypes, NodeManager::currentNM()->integerType()),
 399                 "uf type conv P");
 400       Node ufM = NodeManager::currentNM()->mkSkolem("ufM",
 401                 NodeManager::currentNM()->mkFunctionType(
 402                   argTypes, NodeManager::currentNM()->integerType()),
 403                 "uf type conv M");
 404
 405       //Node ufP0 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero);
 406       //new_nodes.push_back(pret.eqNode(ufP0));
 407       //lemma
 408       Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES,
 409         str.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(""))),
 410         pret.eqNode(negone));
 411       new_nodes.push_back(lem);
 412       /*lem = NodeManager::currentNM()->mkNode(kind::IFF,
 413         t[0].eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("0"))),
 414         t.eqNode(d_zero));
 415       new_nodes.push_back(lem);*/
 416       if(t.getKind()==kind::STRING_U16TOS) {
 417         lem = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst(::CVC4::String("5")), lenp);
 418         new_nodes.push_back(lem);
 419       } else if(t.getKind()==kind::STRING_U32TOS) {
 420         lem = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst(::CVC4::String("9")), lenp);
 421         new_nodes.push_back(lem);
 422       }
 423       //cc1
 424       Node cc1 = str.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("")));
 425       //cc1 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(negone), cc1);
 426       //cc2
 427       std::vector< Node > vec_n;
 428       Node p = NodeManager::currentNM()->mkSkolem("p", NodeManager::currentNM()->integerType());
 429       Node g = NodeManager::currentNM()->mkNode(kind::GEQ, p, d_zero);
 430       vec_n.push_back(g);
 431       g = NodeManager::currentNM()->mkNode(kind::GT, lenp, p);
 432       vec_n.push_back(g);
 433       Node z2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, str, p, one);
 434       char chtmp[2];
 435       chtmp[1] = '\0';
 436       for(unsigned i=0; i<=9; i++) {
 437         chtmp[0] = i + '0';
 438         std::string stmp(chtmp);
 439         g = z2.eqNode( NodeManager::currentNM()->mkConst(::CVC4::String(stmp)) ).negate();
 440         vec_n.push_back(g);
 441       }
 442       Node cc2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, vec_n));
 443       //cc3
 444       Node b2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
 445       Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2);
 446       Node g2 = NodeManager::currentNM()->mkNode(kind::AND,
 447             NodeManager::currentNM()->mkNode(kind::GEQ, b2, d_zero),
 448             NodeManager::currentNM()->mkNode(kind::GT, lenp, b2));
 449       Node ufx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, b2);
 450       Node ufx1 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, NodeManager::currentNM()->mkNode(kind::MINUS,b2,one));
 451       Node ufMx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, b2);
 452       std::vector< Node > vec_c3;
 453       std::vector< Node > vec_c3b;
 454       //qx between 0 and 9
 455       Node c3cc = NodeManager::currentNM()->mkNode(kind::GEQ, ufMx, d_zero);
 456       vec_c3b.push_back(c3cc);
 457       c3cc = NodeManager::currentNM()->mkNode(kind::GEQ, nine, ufMx);
 458       vec_c3b.push_back(c3cc);
 459       Node sx = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, str, b2, one);
 460       for(unsigned i=0; i<=9; i++) {
 461         chtmp[0] = i + '0';
 462         std::string stmp(chtmp);
 463         c3cc = NodeManager::currentNM()->mkNode(kind::IFF,
 464           ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(i))),
 465           sx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(stmp))));
 466         vec_c3b.push_back(c3cc);
 467       }
 468       //c312
 469       Node b2gtz = NodeManager::currentNM()->mkNode(kind::GT, b2, d_zero);
 470       c3cc = NodeManager::currentNM()->mkNode(kind::IMPLIES, b2gtz,
 471         ufx.eqNode(NodeManager::currentNM()->mkNode(kind::PLUS,
 472           NodeManager::currentNM()->mkNode(kind::MULT, ufx1, ten),
 473           ufMx)));
 474       vec_c3b.push_back(c3cc);
 475       c3cc = NodeManager::currentNM()->mkNode(kind::AND, vec_c3b);
 476       c3cc = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::IMPLIES, g2, c3cc) );
 477       c3cc = NodeManager::currentNM()->mkNode(kind::FORALL, b2v, c3cc);
 478       vec_c3.push_back(c3cc);
 479       //unbound
 480       c3cc = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero).eqNode(NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, d_zero));
 481       vec_c3.push_back(c3cc);
 482       Node lstx = NodeManager::currentNM()->mkNode(kind::MINUS, lenp, one);
 483       Node upflstx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, lstx);
 484       c3cc = upflstx.eqNode(pret);
 485       vec_c3.push_back(c3cc);
 486       Node cc3 = NodeManager::currentNM()->mkNode(kind::AND, vec_c3);
 487       Node conc = NodeManager::currentNM()->mkNode(kind::ITE, pret.eqNode(negone),
 488               NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2), cc3);
 489       new_nodes.push_back( conc );
 490
 491       d_cache[t] = pret;
 492       if(t != pret) {
 493         d_cache[pret] = pret;
 494       }
 495       retNode = pret;
 496     } else {
 497       throw LogicException("string int.to.str not supported in default mode, try --strings-exp");
 498     }
 499   } else if( t.getKind() == kind::STRING_STRREPL ) {
 500     if(options::stringExp()) {
 501       Node x = t[0];
 502       Node y = t[1];
 503       Node z = t[2];
 504       Node sk1 = NodeManager::currentNM()->mkSkolem( "rp1", t[0].getType(), "created for replace" );
 505       Node sk2 = NodeManager::currentNM()->mkSkolem( "rp2", t[0].getType(), "created for replace" );
 506       Node skw = NodeManager::currentNM()->mkSkolem( "rpw", t[0].getType(), "created for replace" );
 507       Node cond = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, x, y );
 508       Node c1 = x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, y, sk2 ) );
 509       Node c2 = skw.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, z, sk2 ) );
 510       Node c3 = NodeManager::currentNM()->mkNode(kind::STRING_STRCTN,
 511                   NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sk1,
 512                      NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, y, d_zero,
 513                         NodeManager::currentNM()->mkNode(kind::MINUS,
 514                           NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y),
 515                           NodeManager::currentNM()->mkConst(::CVC4::Rational(1))))), y).negate();
 516       Node rr = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond,
 517               NodeManager::currentNM()->mkNode( kind::AND, c1, c2, c3),
 518               skw.eqNode(x) ) );
 519       new_nodes.push_back( rr );
 520       rr = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y), d_zero) );
 521       new_nodes.push_back( rr );
 522
 523       d_cache[t] = skw;
 524       retNode = skw;
 525     } else {
 526       throw LogicException("string replace not supported in default mode, try --strings-exp");
 527     }
 528   } else{
 529     d_cache[t] = Node::null();
 530     retNode = t;
 531   }
 532
 533   /*if( t.getNumChildren()>0 ) {
 534     std::vector< Node > cc;
 535     if (t.getMetaKind() == kind::metakind::PARAMETERIZED) {
 536       cc.push_back(t.getOperator());
 537     }
 538     bool changed = false;
 539     for( unsigned i=0; i<t.getNumChildren(); i++ ){
 540       Node tn = simplify( t[i], new_nodes );
 541       cc.push_back( tn );
 542       changed = changed || tn!=t[i];
 543     }
 544     if(changed) {
 545       Node n = NodeManager::currentNM()->mkNode( t.getKind(), cc );
 546       d_cache[t] = n;
 547       retNode = n;
 548     } else {
 549       d_cache[t] = Node::null();
 550       retNode = t;
 551     }
 552   }*/
 553
 554   Trace("strings-preprocess") << "StringsPreprocess::simplify returns: " << retNode << std::endl;
 555   if(!new_nodes.empty()) {
 556     Trace("strings-preprocess") << " ... new nodes (" << new_nodes.size() << "):\n";
 557     for(unsigned int i=0; i<new_nodes.size(); ++i) {
 558       Trace("strings-preprocess") << "\t" << new_nodes[i] << "\n";
 559     }
 560   }
 561
 562   return retNode;
 563 }
 564
 565 Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes) {
 566   std::hash_map<TNode, Node, TNodeHashFunction>::const_iterator i = d_cache.find(t);
 567   if(i != d_cache.end()) {
 568     return (*i).second.isNull() ? t : (*i).second;
 569   }
 570
 571   unsigned num = t.getNumChildren();
 572   if(num == 0) {
 573     return simplify(t, new_nodes);
 574   } else {
 575     bool changed = false;
 576     std::vector< Node > cc;
 577     if (t.getMetaKind() == kind::metakind::PARAMETERIZED) {
 578       cc.push_back(t.getOperator());
 579     }
 580     for(unsigned i=0; i<t.getNumChildren(); i++) {
 581       Node s = decompose(t[i], new_nodes);
 582       cc.push_back( s );
 583       if(s != t[i]) {
 584         changed = true;
 585       }
 586     }
 587     if(changed) {
 588       Node tmp = NodeManager::currentNM()->mkNode( t.getKind(), cc );
 589       return simplify(tmp, new_nodes);
 590     } else {
 591       return simplify(t, new_nodes);
 592     }
 593   }
 594 }
 595
 596 void StringsPreprocess::simplify(std::vector< Node > &vec_node, std::vector< Node > &new_nodes) {
 597   for( unsigned i=0; i<vec_node.size(); i++ ){
 598     vec_node[i] = decompose( vec_node[i], new_nodes );
 599   }
 600 }
 601
 602 void StringsPreprocess::simplify(std::vector< Node > &vec_node) {
 603   std::vector< Node > new_nodes;
 604   simplify(vec_node, new_nodes);
 605   vec_node.insert( vec_node.end(), new_nodes.begin(), new_nodes.end() );
 606 }
 607
 608 }/* CVC4::theory::strings namespace */
 609 }/* CVC4::theory namespace */
 610 }/* CVC4 namespace */