src/theory/strings/theory_strings_preprocess.cpp

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