src/theory/quantifiers/quantifiers_rewriter.cpp

   1 /*********************                                                        */
   2 /*! \file quantifiers_rewriter.cpp
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: Andrew Reynolds
   6  ** Minor contributors (to current version): Tim King
   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 Implementation of QuantifiersRewriter class
  13  **/
  14
  15 #include "theory/quantifiers/quantifiers_rewriter.h"
  16 #include "theory/quantifiers/options.h"
  17 #include "theory/quantifiers/term_database.h"
  18 #include "theory/datatypes/datatypes_rewriter.h"
  19
  20 using namespace std;
  21 using namespace CVC4;
  22 using namespace CVC4::kind;
  23 using namespace CVC4::context;
  24 using namespace CVC4::theory;
  25 using namespace CVC4::theory::quantifiers;
  26
  27 bool QuantifiersRewriter::isClause( Node n ){
  28   if( isLiteral( n ) ){
  29     return true;
  30   }else if( n.getKind()==NOT ){
  31     return isCube( n[0] );
  32   }else if( n.getKind()==OR ){
  33     for( int i=0; i<(int)n.getNumChildren(); i++ ){
  34       if( !isClause( n[i] ) ){
  35         return false;
  36       }
  37     }
  38     return true;
  39   }else if( n.getKind()==IMPLIES ){
  40     return isCube( n[0] ) && isClause( n[1] );
  41   }else{
  42     return false;
  43   }
  44 }
  45
  46 bool QuantifiersRewriter::isLiteral( Node n ){
  47   switch( n.getKind() ){
  48   case NOT:
  49     return isLiteral( n[0] );
  50     break;
  51   case OR:
  52   case AND:
  53   case IMPLIES:
  54   case XOR:
  55   case ITE:
  56   case IFF:
  57     return false;
  58     break;
  59   case EQUAL:
  60     return n[0].getType()!=NodeManager::currentNM()->booleanType();
  61     break;
  62   default:
  63     break;
  64   }
  65   return true;
  66 }
  67
  68 bool QuantifiersRewriter::isCube( Node n ){
  69   if( isLiteral( n ) ){
  70     return true;
  71   }else if( n.getKind()==NOT ){
  72     return isClause( n[0] );
  73   }else if( n.getKind()==AND ){
  74     for( int i=0; i<(int)n.getNumChildren(); i++ ){
  75       if( !isCube( n[i] ) ){
  76         return false;
  77       }
  78     }
  79     return true;
  80   }else{
  81     return false;
  82   }
  83 }
  84
  85 void QuantifiersRewriter::addNodeToOrBuilder( Node n, NodeBuilder<>& t ){
  86   if( n.getKind()==OR ){
  87     for( int i=0; i<(int)n.getNumChildren(); i++ ){
  88       t << n[i];
  89     }
  90   }else{
  91     t << n;
  92   }
  93 }
  94
  95 void QuantifiersRewriter::computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n ){
  96   if( n.getKind()==BOUND_VARIABLE ){
  97     if( std::find( args.begin(), args.end(), n )!=args.end() ){
  98       activeMap[ n ] = true;
  99     }
 100   }else{
 101     for( int i=0; i<(int)n.getNumChildren(); i++ ){
 102       computeArgs( args, activeMap, n[i] );
 103     }
 104   }
 105 }
 106
 107 void QuantifiersRewriter::computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ) {
 108   std::map< Node, bool > activeMap;
 109   computeArgs( args, activeMap, n );
 110   for( unsigned i=0; i<args.size(); i++ ){
 111     if( activeMap[args[i]] ){
 112       activeArgs.push_back( args[i] );
 113     }
 114   }
 115 }
 116
 117
 118 bool QuantifiersRewriter::hasArg( std::vector< Node >& args, Node n ){
 119   if( std::find( args.begin(), args.end(), n )!=args.end() ){
 120     return true;
 121   }else{
 122     for( int i=0; i<(int)n.getNumChildren(); i++ ){
 123       if( hasArg( args, n[i] ) ){
 124         return true;
 125       }
 126     }
 127     return false;
 128   }
 129 }
 130
 131 void QuantifiersRewriter::setNestedQuantifiers( Node n, Node q ){
 132   std::vector< Node > processed;
 133   setNestedQuantifiers2( n, q, processed );
 134 }
 135
 136 void QuantifiersRewriter::setNestedQuantifiers2( Node n, Node q, std::vector< Node >& processed ) {
 137   if( std::find( processed.begin(), processed.end(), n )==processed.end() ){
 138     processed.push_back( n );
 139     if( n.getKind()==FORALL || n.getKind()==EXISTS ){
 140       Trace("quantifiers-rewrite-debug") << "Set nested quant attribute " << n << std::endl;
 141       NestedQuantAttribute nqai;
 142       n[0].setAttribute(nqai,q);
 143     }
 144     for( int i=0; i<(int)n.getNumChildren(); i++ ){
 145       setNestedQuantifiers2( n[i], q, processed );
 146     }
 147   }
 148 }
 149
 150 RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
 151   if( in.getKind()==kind::EXISTS || in.getKind()==kind::FORALL ){
 152     Trace("quantifiers-rewrite-debug") << "pre-rewriting " << in << " " << in[0].hasAttribute(NestedQuantAttribute()) << std::endl;
 153     if( !in.hasAttribute(NestedQuantAttribute()) ){
 154       setNestedQuantifiers( in[ 1 ], in );
 155     }
 156     std::vector< Node > args;
 157     for( int i=0; i<(int)in[0].getNumChildren(); i++ ){
 158       args.push_back( in[0][i] );
 159     }
 160     Node body = in[1];
 161     bool doRewrite = false;
 162     std::vector< Node > ipl;
 163     while( body.getNumChildren()>=2 && body.getKind()==in.getKind() ){
 164       if( body.getNumChildren()==3 ){
 165         for( unsigned i=0; i<body[2].getNumChildren(); i++ ){
 166           ipl.push_back( body[2][i] );
 167         }
 168       }
 169       for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
 170         args.push_back( body[0][i] );
 171       }
 172       body = body[1];
 173       doRewrite = true;
 174     }
 175     if( doRewrite ){
 176       std::vector< Node > children;
 177       children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST,args) );
 178       children.push_back( body );
 179       if( in.getNumChildren()==3 ){
 180         for( unsigned i=0; i<in[2].getNumChildren(); i++ ){
 181           ipl.push_back( in[2][i] );
 182         }
 183       }
 184       if( !ipl.empty() ){
 185         children.push_back( NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, ipl ) );
 186       }
 187       Node n = NodeManager::currentNM()->mkNode( in.getKind(), children );
 188       if( in!=n ){
 189         setAttributes( in, n );
 190         Trace("quantifiers-pre-rewrite") << "*** pre-rewrite " << in << std::endl;
 191         Trace("quantifiers-pre-rewrite") << " to " << std::endl;
 192         Trace("quantifiers-pre-rewrite") << n << std::endl;
 193       }
 194       return RewriteResponse(REWRITE_DONE, n);
 195     }
 196   }
 197   return RewriteResponse(REWRITE_DONE, in);
 198 }
 199
 200 RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
 201   Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << std::endl;
 202   Trace("quantifiers-rewrite-debug") << "Attributes : " << in[0].hasAttribute(NestedQuantAttribute())  << std::endl;
 203   if( !options::quantRewriteRules() || !TermDb::isRewriteRule( in ) ){
 204     RewriteStatus status = REWRITE_DONE;
 205     Node ret = in;
 206     //get the arguments
 207     std::vector< Node > args;
 208     for( int i=0; i<(int)in[0].getNumChildren(); i++ ){
 209       args.push_back( in[0][i] );
 210     }
 211     //get the instantiation pattern list
 212     Node ipl;
 213     if( in.getNumChildren()==3 ){
 214       ipl = in[2];
 215     }
 216     //get the body
 217     if( in.getKind()==EXISTS ){
 218       std::vector< Node > children;
 219       children.push_back( in[0] );
 220       children.push_back( in[1].negate() );
 221       if( in.getNumChildren()==3 ){
 222         children.push_back( in[2] );
 223       }
 224       ret = NodeManager::currentNM()->mkNode( FORALL, children );
 225       ret = ret.negate();
 226       status = REWRITE_AGAIN_FULL;
 227     }else{
 228       bool isNested = in[0].hasAttribute(NestedQuantAttribute());
 229       for( int op=0; op<COMPUTE_LAST; op++ ){
 230         if( doOperation( in, isNested, op ) ){
 231           ret = computeOperation( in, isNested, op );
 232           if( ret!=in ){
 233             status = REWRITE_AGAIN_FULL;
 234             break;
 235           }
 236         }
 237       }
 238     }
 239     //print if changed
 240     if( in!=ret ){
 241       setAttributes( in, ret );
 242       Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl;
 243       Trace("quantifiers-rewrite") << " to " << std::endl;
 244       Trace("quantifiers-rewrite") << ret << std::endl;
 245       //Trace("quantifiers-rewrite-debug") << "Attributes : " << ret[0].hasAttribute(NestedQuantAttribute()) << std::endl;
 246     }
 247     return RewriteResponse( status, ret );
 248   }
 249   return RewriteResponse(REWRITE_DONE, in);
 250 }
 251
 252 Node QuantifiersRewriter::computeElimSymbols( Node body ) {
 253   if( isLiteral( body ) ){
 254     return body;
 255   }else{
 256     bool childrenChanged = false;
 257     std::vector< Node > children;
 258     for( unsigned i=0; i<body.getNumChildren(); i++ ){
 259       Node c = computeElimSymbols( body[i] );
 260       if( i==0 && ( body.getKind()==IMPLIES || body.getKind()==XOR ) ){
 261         c = c.negate();
 262       }
 263       children.push_back( c );
 264       childrenChanged = childrenChanged || c!=body[i];
 265     }
 266     if( body.getKind()==IMPLIES ){
 267       return NodeManager::currentNM()->mkNode( OR, children );
 268     }else if( body.getKind()==XOR ){
 269       return NodeManager::currentNM()->mkNode( IFF, children );
 270     }else if( childrenChanged ){
 271       return NodeManager::currentNM()->mkNode( body.getKind(), children );
 272     }else{
 273       return body;
 274     }
 275   }
 276 }
 277
 278 Node QuantifiersRewriter::computeNNF( Node body ){
 279   if( body.getKind()==NOT ){
 280     if( body[0].getKind()==NOT ){
 281       return computeNNF( body[0][0] );
 282     }else if( isLiteral( body[0] ) ){
 283       return body;
 284     }else{
 285       std::vector< Node > children;
 286       Kind k = body[0].getKind();
 287       if( body[0].getKind()==OR || body[0].getKind()==AND ){
 288         for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
 289           children.push_back( computeNNF( body[0][i].notNode() ) );
 290         }
 291         k = body[0].getKind()==AND ? OR : AND;
 292       }else if( body[0].getKind()==IFF ){
 293         for( int i=0; i<2; i++ ){
 294           Node nn = i==0 ? body[0][i] : body[0][i].notNode();
 295           children.push_back( computeNNF( nn ) );
 296         }
 297       }else if( body[0].getKind()==ITE ){
 298         for( int i=0; i<3; i++ ){
 299           Node nn = i==0 ? body[0][i] : body[0][i].notNode();
 300           children.push_back( computeNNF( nn ) );
 301         }
 302       }else{
 303         Notice() << "Unhandled Quantifiers NNF: " << body << std::endl;
 304         return body;
 305       }
 306       return NodeManager::currentNM()->mkNode( k, children );
 307     }
 308   }else if( isLiteral( body ) ){
 309     return body;
 310   }else{
 311     std::vector< Node > children;
 312     bool childrenChanged = false;
 313     for( int i=0; i<(int)body.getNumChildren(); i++ ){
 314       Node nc = computeNNF( body[i] );
 315       children.push_back( nc );
 316       childrenChanged = childrenChanged || nc!=body[i];
 317     }
 318     if( childrenChanged ){
 319       return NodeManager::currentNM()->mkNode( body.getKind(), children );
 320     }else{
 321       return body;
 322     }
 323   }
 324 }
 325
 326 Node QuantifiersRewriter::computeSimpleIteLift( Node body ) {
 327   if( body.getKind()==EQUAL ){
 328     for( size_t i=0; i<2; i++ ){
 329       if( body[i].getKind()==ITE ){
 330         Node no = i==0 ? body[1] : body[0];
 331         bool doRewrite = false;
 332         std::vector< Node > children;
 333         children.push_back( body[i][0] );
 334         for( size_t j=1; j<=2; j++ ){
 335           //check if it rewrites to a constant
 336           Node nn = NodeManager::currentNM()->mkNode( EQUAL, no, body[i][j] );
 337           nn = Rewriter::rewrite( nn );
 338           children.push_back( nn );
 339           if( nn.isConst() ){
 340             doRewrite = true;
 341           }
 342         }
 343         if( doRewrite ){
 344           return NodeManager::currentNM()->mkNode( ITE, children );
 345         }
 346       }
 347     }
 348   }else if( body.getKind()!=APPLY_UF && body.getType()==NodeManager::currentNM()->booleanType() ){
 349     bool changed = false;
 350     std::vector< Node > children;
 351     for( size_t i=0; i<body.getNumChildren(); i++ ){
 352       Node nn = computeSimpleIteLift( body[i] );
 353       children.push_back( nn );
 354       changed = changed || nn!=body[i];
 355     }
 356     if( changed ){
 357       return NodeManager::currentNM()->mkNode( body.getKind(), children );
 358     }
 359   }
 360   return body;
 361 }
 362
 363 Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){
 364   Trace("var-elim-quant-debug") << "Compute var elimination for " << body << std::endl;
 365   QuantPhaseReq qpr( body );
 366   std::vector< Node > vars;
 367   std::vector< Node > subs;
 368   for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){
 369     //Notice() << "   " << it->first << " -> " << ( it->second ? "true" : "false" ) << std::endl;
 370     if( it->first.getKind()==EQUAL ){
 371       if( it->second && options::varElimQuant() ){
 372         for( int i=0; i<2; i++ ){
 373           int j = i==0 ? 1 : 0;
 374           std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[i] );
 375           if( ita!=args.end() ){
 376             std::vector< Node > temp;
 377             temp.push_back( it->first[i] );
 378             if( !hasArg( temp, it->first[j] ) ){
 379               vars.push_back( it->first[i] );
 380               subs.push_back( it->first[j] );
 381               args.erase( ita );
 382               break;
 383             }
 384           }
 385         }
 386         if( !vars.empty() ){
 387           break;
 388         }
 389       }
 390     }
 391     else if( it->first.getKind()==APPLY_TESTER ){
 392       if( options::dtVarExpandQuant() && it->second && it->first[0].getKind()==BOUND_VARIABLE ){
 393         Trace("dt-var-expand") << "Expand datatype variable based on : " << it->first << std::endl;
 394         std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[0] );
 395         if( ita!=args.end() ){
 396           vars.push_back( it->first[0] );
 397           Expr testerExpr = it->first.getOperator().toExpr();
 398           int index = Datatype::indexOf( testerExpr );
 399           const Datatype& dt = Datatype::datatypeOf(testerExpr);
 400           const DatatypeConstructor& c = dt[index];
 401           std::vector< Node > newChildren;
 402           newChildren.push_back( Node::fromExpr( c.getConstructor() ) );
 403           std::vector< Node > newVars;
 404           for( unsigned j=0; j<c.getNumArgs(); j++ ){
 405             TypeNode tn = TypeNode::fromType( c[j].getSelector().getType() );
 406             tn = tn[1];
 407             Node v = NodeManager::currentNM()->mkBoundVar( tn );
 408             newChildren.push_back( v );
 409             newVars.push_back( v );
 410           }
 411           subs.push_back( NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, newChildren ) );
 412           Trace("dt-var-expand") << "...apply substitution " << subs[0] << "/" << vars[0] << std::endl;
 413           args.erase( ita );
 414           args.insert( args.end(), newVars.begin(), newVars.end() );
 415         }
 416       }
 417     }
 418   }
 419   if( !vars.empty() ){
 420     Trace("var-elim-quant") << "VE " << vars.size() << "/" << args.size() << std::endl;
 421     //remake with eliminated nodes
 422     body = body.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
 423     body = Rewriter::rewrite( body );
 424     if( !ipl.isNull() ){
 425       ipl = ipl.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
 426     }
 427     Trace("var-elim-quant") << "Return " << body << std::endl;
 428   }
 429   return body;
 430 }
 431
 432 Node QuantifiersRewriter::computeClause( Node n ){
 433   Assert( isClause( n ) );
 434   if( isLiteral( n ) ){
 435     return n;
 436   }else{
 437     NodeBuilder<> t(OR);
 438     if( n.getKind()==NOT ){
 439       if( n[0].getKind()==NOT ){
 440         return computeClause( n[0][0] );
 441       }else{
 442         //De-Morgan's law
 443         Assert( n[0].getKind()==AND );
 444         for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
 445           Node nn = computeClause( n[0][i].notNode() );
 446           addNodeToOrBuilder( nn, t );
 447         }
 448       }
 449     }else{
 450       for( int i=0; i<(int)n.getNumChildren(); i++ ){
 451         Node nn = computeClause( n[i] );
 452         addNodeToOrBuilder( nn, t );
 453       }
 454     }
 455     return t.constructNode();
 456   }
 457 }
 458
 459 void QuantifiersRewriter::setAttributes( Node in, Node n ) {
 460   if( n.getKind()==FORALL && in.getKind()==FORALL ){
 461     if( in[0].hasAttribute(NestedQuantAttribute()) ){
 462       setNestedQuantifiers( n[0], in[0].getAttribute(NestedQuantAttribute()) );
 463     }
 464   }
 465 }
 466
 467 Node QuantifiersRewriter::computeCNF( Node n, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred ){
 468   if( isLiteral( n ) ){
 469     return n;
 470   }else if( !forcePred && isClause( n ) ){
 471     return computeClause( n );
 472   }else{
 473     Kind k = n.getKind();
 474     NodeBuilder<> t(k);
 475     for( int i=0; i<(int)n.getNumChildren(); i++ ){
 476       Node nc = n[i];
 477       Node ncnf = computeCNF( nc, args, defs, k!=OR );
 478       if( k==OR ){
 479         addNodeToOrBuilder( ncnf, t );
 480       }else{
 481         t << ncnf;
 482       }
 483     }
 484     if( !forcePred && k==OR ){
 485       return t.constructNode();
 486     }else{
 487       //compute the free variables
 488       Node nt = t;
 489       std::vector< Node > activeArgs;
 490       computeArgVec( args, activeArgs, nt );
 491       std::vector< TypeNode > argTypes;
 492       for( int i=0; i<(int)activeArgs.size(); i++ ){
 493         argTypes.push_back( activeArgs[i].getType() );
 494       }
 495       //create the predicate
 496       Assert( argTypes.size()>0 );
 497       TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, NodeManager::currentNM()->booleanType() );
 498       std::stringstream ss;
 499       ss << "cnf_" << n.getKind() << "_" << n.getId();
 500       Node op = NodeManager::currentNM()->mkSkolem( ss.str(), typ, "was created by the quantifiers rewriter" );
 501       std::vector< Node > predArgs;
 502       predArgs.push_back( op );
 503       predArgs.insert( predArgs.end(), activeArgs.begin(), activeArgs.end() );
 504       Node pred = NodeManager::currentNM()->mkNode( APPLY_UF, predArgs );
 505       Trace("quantifiers-rewrite-cnf-debug") << "Made predicate " << pred << " for " << nt << std::endl;
 506       //create the bound var list
 507       Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, activeArgs );
 508       //now, look at the structure of nt
 509       if( nt.getKind()==NOT ){
 510         //case for NOT
 511         for( int i=0; i<2; i++ ){
 512           NodeBuilder<> tt(OR);
 513           tt << ( i==0 ? nt[0].notNode() : nt[0] );
 514           tt << ( i==0 ? pred.notNode() : pred );
 515           defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
 516         }
 517       }else if( nt.getKind()==OR ){
 518         //case for OR
 519         for( int i=0; i<(int)nt.getNumChildren(); i++ ){
 520           NodeBuilder<> tt(OR);
 521           tt << nt[i].notNode() << pred;
 522           defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
 523         }
 524         NodeBuilder<> tt(OR);
 525         for( int i=0; i<(int)nt.getNumChildren(); i++ ){
 526           tt << nt[i];
 527         }
 528         tt << pred.notNode();
 529         defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
 530       }else if( nt.getKind()==AND ){
 531         //case for AND
 532         for( int i=0; i<(int)nt.getNumChildren(); i++ ){
 533           NodeBuilder<> tt(OR);
 534           tt << nt[i] << pred.notNode();
 535           defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
 536         }
 537         NodeBuilder<> tt(OR);
 538         for( int i=0; i<(int)nt.getNumChildren(); i++ ){
 539           tt << nt[i].notNode();
 540         }
 541         tt << pred;
 542         defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
 543       }else if( nt.getKind()==IFF ){
 544         //case for IFF
 545         for( int i=0; i<4; i++ ){
 546           NodeBuilder<> tt(OR);
 547           tt << ( ( i==0 || i==3 ) ? nt[0].notNode() : nt[0] );
 548           tt << ( ( i==1 || i==3 ) ? nt[1].notNode() : nt[1] );
 549           tt << ( ( i==0 || i==1 ) ? pred.notNode() : pred );
 550           defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
 551         }
 552       }else if( nt.getKind()==ITE ){
 553         //case for ITE
 554         for( int j=1; j<=2; j++ ){
 555           for( int i=0; i<2; i++ ){
 556             NodeBuilder<> tt(OR);
 557             tt << ( ( j==1 ) ? nt[0].notNode() : nt[0] );
 558             tt << ( ( i==1 ) ? nt[j].notNode() : nt[j] );
 559             tt << ( ( i==0 ) ? pred.notNode() : pred );
 560             defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
 561           }
 562         }
 563         for( int i=0; i<2; i++ ){
 564           NodeBuilder<> tt(OR);
 565           tt << ( i==0 ? nt[1].notNode() : nt[1] );
 566           tt << ( i==0 ? nt[2].notNode() : nt[2] );
 567           tt << ( i==1 ? pred.notNode() : pred );
 568           defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() );
 569         }
 570       }else{
 571         Notice() << "Unhandled Quantifiers CNF: " << nt << std::endl;
 572       }
 573       return pred;
 574     }
 575   }
 576 }
 577
 578 Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, bool pol ){
 579   if( body.getKind()==FORALL ){
 580     if( pol ){
 581       std::vector< Node > terms;
 582       std::vector< Node > subs;
 583       //for doing prenexing of same-signed quantifiers
 584       //must rename each variable that already exists
 585       for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
 586         //if( std::find( args.begin(), args.end(), body[0][i] )!=args.end() ){
 587         terms.push_back( body[0][i] );
 588         subs.push_back( NodeManager::currentNM()->mkBoundVar( body[0][i].getType() ) );
 589       }
 590       args.insert( args.end(), subs.begin(), subs.end() );
 591       Node newBody = body[1];
 592       newBody = newBody.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
 593       Debug("quantifiers-substitute-debug") << "Did substitute have an effect" << (body[1] != newBody) << body[1] << " became " << newBody << endl;
 594       return newBody;
 595     }else{
 596       return body;
 597     }
 598   }else if( body.getKind()==ITE || body.getKind()==XOR || body.getKind()==IFF ){
 599     return body;
 600   }else{
 601     Assert( body.getKind()!=EXISTS );
 602     bool childrenChanged = false;
 603     std::vector< Node > newChildren;
 604     for( int i=0; i<(int)body.getNumChildren(); i++ ){
 605       bool newPol = body.getKind()==NOT  ? !pol : pol;
 606       Node n = computePrenex( body[i], args, newPol );
 607       newChildren.push_back( n );
 608       if( n!=body[i] ){
 609         childrenChanged = true;
 610       }
 611     }
 612     if( childrenChanged ){
 613       if( body.getKind()==NOT && newChildren[0].getKind()==NOT ){
 614         return newChildren[0][0];
 615       }else{
 616         return NodeManager::currentNM()->mkNode( body.getKind(), newChildren );
 617       }
 618     }else{
 619       return body;
 620     }
 621   }
 622 }
 623
 624 Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >& vars ) {
 625   if( body.getKind()==OR ){
 626     size_t var_found_count = 0;
 627     size_t eqc_count = 0;
 628     size_t eqc_active = 0;
 629     std::map< Node, int > var_to_eqc;
 630     std::map< int, std::vector< Node > > eqc_to_var;
 631     std::map< int, std::vector< Node > > eqc_to_lit;
 632
 633     std::vector<Node> lits;
 634
 635     for( size_t i=0; i<body.getNumChildren(); i++ ){
 636       //get variables contained in the literal
 637       Node n = body[i];
 638       std::vector<Node> lit_vars;
 639       computeArgVec( vars, lit_vars, n);
 640       //collectVars( n, vars, lit_vars );
 641       if (lit_vars.empty()) {
 642         lits.push_back(n);
 643       }else {
 644         std::vector<int> eqcs;
 645         std::vector<Node> lit_new_vars;
 646         //for each variable in literal
 647         for( size_t j=0; j<lit_vars.size(); j++) {
 648           //see if the variable has already been found
 649           if (var_to_eqc.find(lit_vars[j])!=var_to_eqc.end()) {
 650             int eqc = var_to_eqc[lit_vars[j]];
 651             if (std::find(eqcs.begin(), eqcs.end(), eqc)==eqcs.end()) {
 652               eqcs.push_back(eqc);
 653             }
 654           }
 655           else {
 656             var_found_count++;
 657             lit_new_vars.push_back(lit_vars[j]);
 658           }
 659         }
 660         if (eqcs.empty()) {
 661           eqcs.push_back(eqc_count);
 662           eqc_count++;
 663           eqc_active++;
 664         }
 665
 666         int eqcz = eqcs[0];
 667         //merge equivalence classes with eqcz
 668         for (unsigned j=1; j<eqcs.size(); j++) {
 669           int eqc = eqcs[j];
 670           //move all variables from equivalence class
 671           for (unsigned k=0; k<eqc_to_var[eqc].size(); k++) {
 672             Node v = eqc_to_var[eqc][k];
 673             var_to_eqc[v] = eqcz;
 674             eqc_to_var[eqcz].push_back(v);
 675           }
 676           eqc_to_var.erase(eqc);
 677           //move all literals from equivalence class
 678           for (unsigned k=0; k<eqc_to_lit[eqc].size(); k++) {
 679             Node l = eqc_to_lit[eqc][k];
 680             eqc_to_lit[eqcz].push_back(l);
 681           }
 682           eqc_to_lit.erase(eqc);
 683           eqc_active--;
 684         }
 685         if (eqc_active==1 && var_found_count==vars.size()) {
 686           return f;
 687         }
 688         //add variables to equivalence class
 689         for (size_t j=0; j<lit_new_vars.size(); j++) {
 690           var_to_eqc[lit_new_vars[j]] = eqcz;
 691           eqc_to_var[eqcz].push_back(lit_new_vars[j]);
 692         }
 693         //add literal to equivalence class
 694         eqc_to_lit[eqcz].push_back(n);
 695       }
 696     }
 697     if (eqc_active>1) {
 698       Trace("clause-split-debug") << "Split clause " << f << std::endl;
 699       Trace("clause-split-debug") << "   Ground literals: " << std::endl;
 700       for( size_t i=0; i<lits.size(); i++) {
 701         Trace("clause-split-debug") << "      " << lits[i] << std::endl;
 702       }
 703       Trace("clause-split-debug") << std::endl;
 704       Trace("clause-split-debug") << "Equivalence classes: " << std::endl;
 705       for (std::map< int, std::vector< Node > >::iterator it = eqc_to_lit.begin(); it != eqc_to_lit.end(); ++it ){
 706         Trace("clause-split-debug") << "   Literals: " << std::endl;
 707         for (size_t i=0; i<it->second.size(); i++) {
 708           Trace("clause-split-debug") << "      " << it->second[i] << std::endl;
 709         }
 710         int eqc = it->first;
 711         Trace("clause-split-debug") << "   Variables: " << std::endl;
 712         for (size_t i=0; i<eqc_to_var[eqc].size(); i++) {
 713           Trace("clause-split-debug") << "      " << eqc_to_var[eqc][i] << std::endl;
 714         }
 715         Trace("clause-split-debug") << std::endl;
 716         Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, eqc_to_var[eqc]);
 717         Node body = it->second.size()==1 ? it->second[0] : NodeManager::currentNM()->mkNode(OR,it->second);
 718         Node fa = NodeManager::currentNM()->mkNode( FORALL, bvl, body );
 719         lits.push_back(fa);
 720       }
 721       Node nf = NodeManager::currentNM()->mkNode(OR,lits);
 722       Trace("clause-split-debug") << "Made node : " << nf << std::endl;
 723       return nf;
 724     }
 725   }
 726   return f;
 727 }
 728
 729 Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node ipl ){
 730   std::vector< Node > activeArgs;
 731   computeArgVec( args, activeArgs, body );
 732   if( activeArgs.empty() ){
 733     return body;
 734   }else{
 735     std::vector< Node > children;
 736     children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, activeArgs ) );
 737     children.push_back( body );
 738     if( !ipl.isNull() ){
 739       children.push_back( ipl );
 740     }
 741     return NodeManager::currentNM()->mkNode( kind::FORALL, children );
 742   }
 743 }
 744
 745 Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl, bool isNested ){
 746   //Notice() << "rewrite quant " << body << std::endl;
 747   if( body.getKind()==FORALL ){
 748     //combine arguments
 749     std::vector< Node > newArgs;
 750     for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
 751       newArgs.push_back( body[0][i] );
 752     }
 753     newArgs.insert( newArgs.end(), args.begin(), args.end() );
 754     return mkForAll( newArgs, body[ 1 ], ipl );
 755   }else if( !isNested ){
 756     if( body.getKind()==NOT ){
 757       //push not downwards
 758       if( body[0].getKind()==NOT ){
 759         return computeMiniscoping( f, args, body[0][0], ipl );
 760       }else if( body[0].getKind()==AND ){
 761         if( doMiniscopingNoFreeVar() ){
 762           NodeBuilder<> t(kind::OR);
 763           for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
 764             t <<  ( body[0][i].getKind()==NOT ? body[0][i][0] : body[0][i].notNode() );
 765           }
 766           return computeMiniscoping( f, args, t.constructNode(), ipl );
 767         }
 768       }else if( body[0].getKind()==OR ){
 769         if( doMiniscopingAnd() ){
 770           NodeBuilder<> t(kind::AND);
 771           for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
 772             Node trm = body[0][i].negate();
 773             t << computeMiniscoping( f, args, trm, ipl );
 774           }
 775           return t.constructNode();
 776         }
 777       }
 778     }else if( body.getKind()==AND ){
 779       if( doMiniscopingAnd() ){
 780         //break apart
 781         NodeBuilder<> t(kind::AND);
 782         for( int i=0; i<(int)body.getNumChildren(); i++ ){
 783           t << computeMiniscoping( f, args, body[i], ipl );
 784         }
 785         Node retVal = t;
 786         return retVal;
 787       }
 788     }else if( body.getKind()==OR ){
 789       if( doMiniscopingNoFreeVar() ){
 790         Node newBody = body;
 791         NodeBuilder<> body_split(kind::OR);
 792         NodeBuilder<> tb(kind::OR);
 793         for( int i=0; i<(int)body.getNumChildren(); i++ ){
 794           Node trm = body[i];
 795           if( hasArg( args, body[i] ) ){
 796             tb << trm;
 797           }else{
 798             body_split << trm;
 799           }
 800         }
 801         if( tb.getNumChildren()==0 ){
 802           return body_split;
 803         }else if( body_split.getNumChildren()>0 ){
 804           newBody = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb;
 805           body_split << mkForAll( args, newBody, ipl );
 806           return body_split.getNumChildren()==1 ? body_split.getChild( 0 ) : body_split;
 807         }
 808       }
 809     }
 810   }
 811   //if( body==f[1] ){
 812   //  return f;
 813   //}else{
 814   return mkForAll( args, body, ipl );
 815   //}
 816 }
 817
 818 Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& args, Node body, bool isNested ){
 819   if( !isNested ){
 820     std::map< Node, std::vector< Node > > varLits;
 821     std::map< Node, std::vector< Node > > litVars;
 822     if( body.getKind()==OR ){
 823       Trace("ag-miniscope") << "compute aggressive miniscoping on " << body << std::endl;
 824       for( size_t i=0; i<body.getNumChildren(); i++ ){
 825         std::vector< Node > activeArgs;
 826         computeArgVec( args, activeArgs, body[i] );
 827         for (unsigned j=0; j<activeArgs.size(); j++ ){
 828           varLits[activeArgs[j]].push_back( body[i] );
 829         }
 830         litVars[body[i]].insert( litVars[body[i]].begin(), activeArgs.begin(), activeArgs.end() );
 831       }
 832       //find the variable in the least number of literals
 833       Node bestVar;
 834       for( std::map< Node, std::vector< Node > >::iterator it = varLits.begin(); it != varLits.end(); ++it ){
 835         if( bestVar.isNull() || varLits[bestVar].size()>it->second.size() ){
 836           bestVar = it->first;
 837         }
 838       }
 839       Trace("ag-miniscope-debug") << "Best variable " << bestVar << " occurs in " << varLits[bestVar].size() << "/ " << body.getNumChildren() << " literals." << std::endl;
 840       if( !bestVar.isNull() && varLits[bestVar].size()<body.getNumChildren() ){
 841         //we can miniscope
 842         Trace("ag-miniscope") << "Miniscope on " << bestVar << std::endl;
 843         //make the bodies
 844         std::vector< Node > qlit1;
 845         qlit1.insert( qlit1.begin(), varLits[bestVar].begin(), varLits[bestVar].end() );
 846         std::vector< Node > qlitt;
 847         //for all literals not containing bestVar
 848         for( size_t i=0; i<body.getNumChildren(); i++ ){
 849           if( std::find( qlit1.begin(), qlit1.end(), body[i] )==qlit1.end() ){
 850             qlitt.push_back( body[i] );
 851           }
 852         }
 853         //make the variable lists
 854         std::vector< Node > qvl1;
 855         std::vector< Node > qvl2;
 856         std::vector< Node > qvsh;
 857         for( unsigned i=0; i<args.size(); i++ ){
 858           bool found1 = false;
 859           bool found2 = false;
 860           for( size_t j=0; j<varLits[args[i]].size(); j++ ){
 861             if( !found1 && std::find( qlit1.begin(), qlit1.end(), varLits[args[i]][j] )!=qlit1.end() ){
 862               found1 = true;
 863             }else if( !found2 && std::find( qlitt.begin(), qlitt.end(), varLits[args[i]][j] )!=qlitt.end() ){
 864               found2 = true;
 865             }
 866             if( found1 && found2 ){
 867               break;
 868             }
 869           }
 870           if( found1 ){
 871             if( found2 ){
 872               qvsh.push_back( args[i] );
 873             }else{
 874               qvl1.push_back( args[i] );
 875             }
 876           }else{
 877             Assert(found2);
 878             qvl2.push_back( args[i] );
 879           }
 880         }
 881         Assert( !qvl1.empty() );
 882         Assert( !qvl2.empty() || !qvsh.empty() );
 883         //check for literals that only contain shared variables
 884         std::vector< Node > qlitsh;
 885         std::vector< Node > qlit2;
 886         for( size_t i=0; i<qlitt.size(); i++ ){
 887           bool hasVar2 = false;
 888           for( size_t j=0; j<litVars[qlitt[i]].size(); j++ ){
 889             if( std::find( qvl2.begin(), qvl2.end(), litVars[qlitt[i]][j] )!=qvl2.end() ){
 890               hasVar2 = true;
 891               break;
 892             }
 893           }
 894           if( hasVar2 ){
 895             qlit2.push_back( qlitt[i] );
 896           }else{
 897             qlitsh.push_back( qlitt[i] );
 898           }
 899         }
 900         varLits.clear();
 901         litVars.clear();
 902         Trace("ag-miniscope-debug") << "Split into literals : " << qlit1.size() << " / " << qlit2.size() << " / " << qlitsh.size();
 903         Trace("ag-miniscope-debug") << ", variables : " << qvl1.size() << " / " << qvl2.size() << " / " << qvsh.size() << std::endl;
 904         Node n1 = qlit1.size()==1 ? qlit1[0] : NodeManager::currentNM()->mkNode( OR, qlit1 );
 905         n1 = computeAggressiveMiniscoping( qvl1, n1 );
 906         qlitsh.push_back( n1 );
 907         if( !qlit2.empty() ){
 908           Node n2 = qlit2.size()==1 ? qlit2[0] : NodeManager::currentNM()->mkNode( OR, qlit2 );
 909           n2 = computeAggressiveMiniscoping( qvl2, n2 );
 910           qlitsh.push_back( n2 );
 911         }
 912         Node n = NodeManager::currentNM()->mkNode( OR, qlitsh );
 913         if( !qvsh.empty() ){
 914           Node bvl = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, qvsh);
 915           n = NodeManager::currentNM()->mkNode( FORALL, bvl, n );
 916         }
 917         Trace("ag-miniscope") << "Return " << n << " for " << body << std::endl;
 918         return n;
 919       }
 920     }
 921   }
 922   return mkForAll( args, body, Node::null() );
 923 }
 924
 925 bool QuantifiersRewriter::doMiniscopingNoFreeVar(){
 926   return options::miniscopeQuantFreeVar();
 927 }
 928
 929 bool QuantifiersRewriter::doMiniscopingAnd(){
 930   if( options::miniscopeQuant() ){
 931     return true;
 932   }else{
 933     if( options::cbqi() ){
 934       return true;
 935     }else{
 936       return false;
 937     }
 938   }
 939 }
 940
 941 bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption ){
 942   if( computeOption==COMPUTE_ELIM_SYMBOLS ){
 943     return true;
 944   }else if( computeOption==COMPUTE_MINISCOPING ){
 945     return true;
 946   }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
 947     return options::aggressiveMiniscopeQuant();
 948   }else if( computeOption==COMPUTE_NNF ){
 949     return options::nnfQuant();
 950   }else if( computeOption==COMPUTE_SIMPLE_ITE_LIFT ){
 951     return options::simpleIteLiftQuant();
 952   }else if( computeOption==COMPUTE_PRENEX ){
 953     return options::prenexQuant() && !options::aggressiveMiniscopeQuant();
 954   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
 955     return options::varElimQuant() || options::dtVarExpandQuant();
 956   }else if( computeOption==COMPUTE_CNF ){
 957     return false;//return options::cnfQuant() ; FIXME
 958   }else if( computeOption==COMPUTE_SPLIT ){
 959     return options::clauseSplit();
 960   }else{
 961     return false;
 962   }
 963 }
 964
 965 //general method for computing various rewrites
 966 Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOption ){
 967   if( f.getKind()==FORALL ){
 968     Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << ", nested = " << isNested << std::endl;
 969     std::vector< Node > args;
 970     for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
 971       args.push_back( f[0][i] );
 972     }
 973     NodeBuilder<> defs(kind::AND);
 974     Node n = f[1];
 975     Node ipl;
 976     if( f.getNumChildren()==3 ){
 977       ipl = f[2];
 978     }
 979     if( computeOption==COMPUTE_ELIM_SYMBOLS ){
 980       n = computeElimSymbols( n );
 981     }else if( computeOption==COMPUTE_MINISCOPING ){
 982       //return directly
 983       return computeMiniscoping( f, args, n, ipl, isNested );
 984     }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
 985       return computeAggressiveMiniscoping( args, n, isNested );
 986     }else if( computeOption==COMPUTE_NNF ){
 987       n = computeNNF( n );
 988     }else if( computeOption==COMPUTE_SIMPLE_ITE_LIFT ){
 989       n = computeSimpleIteLift( n );
 990     }else if( computeOption==COMPUTE_PRENEX ){
 991       n = computePrenex( n, args, true );
 992     }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
 993       Node prev;
 994       do{
 995         prev = n;
 996         n = computeVarElimination( n, args, ipl );
 997       }while( prev!=n && !args.empty() );
 998     }else if( computeOption==COMPUTE_CNF ){
 999       //n = computeNNF( n );
1000       n = computeCNF( n, args, defs, false );
1001       ipl = Node::null();
1002     }else if( computeOption==COMPUTE_SPLIT ) {
1003       return computeSplit(f, n, args );
1004     }
1005     Trace("quantifiers-rewrite-debug") << "Compute Operation: return " << n << ", " << args.size() << std::endl;
1006     if( f[1]==n && args.size()==f[0].getNumChildren() ){
1007       return f;
1008     }else{
1009       if( args.empty() ){
1010         defs << n;
1011       }else{
1012         std::vector< Node > children;
1013         children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) );
1014         children.push_back( n );
1015         if( !ipl.isNull() ){
1016           children.push_back( ipl );
1017         }
1018         defs << NodeManager::currentNM()->mkNode(kind::FORALL, children );
1019       }
1020       return defs.getNumChildren()==1 ? defs.getChild( 0 ) : defs.constructNode();
1021     }
1022   }else{
1023     return f;
1024   }
1025 }
1026
1027
1028 Node QuantifiersRewriter::rewriteRewriteRule( Node r ) {
1029   Kind rrkind = r[2].getKind();
1030
1031   //guards, pattern, body
1032
1033   //   Replace variables by Inst_* variable and tag the terms that contain them
1034   std::vector<Node> vars;
1035   vars.reserve(r[0].getNumChildren());
1036   for( Node::const_iterator v = r[0].begin(); v != r[0].end(); ++v ){
1037     vars.push_back(*v);
1038   };
1039
1040   // Body/Remove_term/Guards/Triggers
1041   Node body = r[2][1];
1042   TNode new_terms = r[2][1];
1043   std::vector<Node> guards;
1044   std::vector<Node> pattern;
1045   Node true_node = NodeManager::currentNM()->mkConst(true);
1046   // shortcut
1047   TNode head = r[2][0];
1048   switch(rrkind){
1049   case kind::RR_REWRITE:
1050     // Equality
1051     pattern.push_back( head );
1052     if( head.getType().isBoolean() ){
1053       body = head.iffNode(body);
1054     }else{
1055       body = head.eqNode(body);
1056     }
1057     break;
1058   case kind::RR_REDUCTION:
1059   case kind::RR_DEDUCTION:
1060     // Add head to guards and pattern
1061     switch(head.getKind()){
1062     case kind::AND:
1063       for( unsigned i = 0; i<head.getNumChildren(); i++ ){
1064         guards.push_back(head[i]);
1065         pattern.push_back(head[i]);
1066       }
1067       break;
1068     default:
1069       if( head!=true_node ){
1070         guards.push_back(head);
1071         pattern.push_back( head );
1072       }
1073       break;
1074     }
1075     break;
1076   default:
1077     Unreachable("RewriteRules can be of only three kinds");
1078     break;
1079   }
1080   // Add the other guards
1081   TNode g = r[1];
1082   switch(g.getKind()){
1083   case kind::AND:
1084     for( unsigned i = 0; i<g.getNumChildren(); i++ ){
1085       guards.push_back(g[i]);
1086     }
1087     break;
1088   default:
1089     if( g != true_node ){
1090       guards.push_back( g );
1091     }
1092     break;
1093   }
1094   // Add the other triggers
1095   if( r[2].getNumChildren() >= 3 ){
1096     for( unsigned i=0; i<r[2][2][0].getNumChildren(); i++ ) {
1097       pattern.push_back( r[2][2][0][i] );
1098     }
1099   }
1100
1101   Trace("rr-rewrite") << "Rule is " << r << std::endl;
1102   Trace("rr-rewrite") << "Head is " << head << std::endl;
1103   Trace("rr-rewrite") << "Patterns are ";
1104   for( unsigned i=0; i<pattern.size(); i++ ){
1105     Trace("rr-rewrite") << pattern[i] << " ";
1106   }
1107   Trace("rr-rewrite") << std::endl;
1108
1109   NodeBuilder<> forallB(kind::FORALL);
1110   forallB << r[0];
1111   Node gg = guards.size()==0 ? true_node : ( guards.size()==1 ? guards[0] : NodeManager::currentNM()->mkNode( AND, guards ) );
1112   gg = NodeManager::currentNM()->mkNode( OR, gg.negate(), body );
1113   gg = Rewriter::rewrite( gg );
1114   forallB << gg;
1115   NodeBuilder<> patternB(kind::INST_PATTERN);
1116   patternB.append(pattern);
1117   NodeBuilder<> patternListB(kind::INST_PATTERN_LIST);
1118   //the entire rewrite rule is the first pattern
1119   if( options::quantRewriteRules() ){
1120     patternListB << NodeManager::currentNM()->mkNode( INST_PATTERN, r );
1121   }
1122   patternListB << static_cast<Node>(patternB);
1123   forallB << static_cast<Node>(patternListB);
1124   Node rn = (Node) forallB;
1125
1126   return rn;
1127 }
1128
1129 struct ContainsQuantAttributeId {};
1130 typedef expr::Attribute<ContainsQuantAttributeId, uint64_t> ContainsQuantAttribute;
1131
1132 // check if the given node contains a universal quantifier
1133 bool QuantifiersRewriter::containsQuantifiers(Node n) {
1134   if( n.hasAttribute(ContainsQuantAttribute()) ){
1135     return n.getAttribute(ContainsQuantAttribute())==1;
1136   } else if(n.getKind() == kind::FORALL) {
1137     return true;
1138   } else {
1139     bool cq = false;
1140     for( unsigned i = 0; i < n.getNumChildren(); ++i ){
1141       if( containsQuantifiers(n[i]) ){
1142         cq = true;
1143         break;
1144       }
1145     }
1146     ContainsQuantAttribute cqa;
1147     n.setAttribute(cqa, cq ? 1 : 0);
1148     return cq;
1149   }
1150 }
1151
1152 Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector< TNode >& fvs ){
1153   Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << endl;
1154   if( n.getKind()==kind::NOT ){
1155     Node nn = preSkolemizeQuantifiers( n[0], !polarity, fvTypes, fvs );
1156     return nn.negate();
1157   }else if( n.getKind()==kind::FORALL ){
1158     if( polarity ){
1159       if( options::preSkolemQuant() ){
1160         vector< Node > children;
1161         children.push_back( n[0] );
1162         //add children to current scope
1163         std::vector< TypeNode > fvt;
1164         std::vector< TNode > fvss;
1165         fvt.insert( fvt.begin(), fvTypes.begin(), fvTypes.end() );
1166         fvss.insert( fvss.begin(), fvs.begin(), fvs.end() );
1167         for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
1168           fvt.push_back( n[0][i].getType() );
1169           fvss.push_back( n[0][i] );
1170         }
1171         //process body
1172         children.push_back( preSkolemizeQuantifiers( n[1], polarity, fvt, fvss ) );
1173         if( n.getNumChildren()==3 ){
1174           children.push_back( n[2] );
1175         }
1176         //return processed quantifier
1177         return NodeManager::currentNM()->mkNode( kind::FORALL, children );
1178       }
1179     }else{
1180       //process body
1181       Node nn = preSkolemizeQuantifiers( n[1], polarity, fvTypes, fvs );
1182       std::vector< Node > sk;
1183       Node sub;
1184       std::vector< unsigned > sub_vars;
1185       //return skolemized body
1186       return TermDb::mkSkolemizedBody( n, nn, fvTypes, fvs, sk, sub, sub_vars );
1187     }
1188   }else{
1189     //check if it contains a quantifier as a subterm
1190     //if so, we will write this node
1191     if( containsQuantifiers( n ) ){
1192       if( n.getType().isBoolean() ){
1193         if( n.getKind()==kind::ITE || n.getKind()==kind::IFF || n.getKind()==kind::XOR || n.getKind()==kind::IMPLIES ){
1194           Node nn;
1195           //must remove structure
1196           if( n.getKind()==kind::ITE ){
1197             nn = NodeManager::currentNM()->mkNode( kind::AND,
1198                    NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ),
1199                    NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) );
1200           }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){
1201             nn = NodeManager::currentNM()->mkNode( kind::AND,
1202                    NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ),
1203                    NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) );
1204           }else if( n.getKind()==kind::IMPLIES ){
1205             nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] );
1206           }
1207           return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs );
1208         }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){
1209           vector< Node > children;
1210           for( int i=0; i<(int)n.getNumChildren(); i++ ){
1211             children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvTypes, fvs ) );
1212           }
1213           return NodeManager::currentNM()->mkNode( n.getKind(), children );
1214         }
1215       }
1216     }
1217   }
1218   return n;
1219 }
1220
1221 bool QuantifiersRewriter::isDtStrInductionQuantifier( Node q ){
1222   Assert( q.getKind()==FORALL );
1223   return q[0].getNumChildren()==1 && datatypes::DatatypesRewriter::isTermDatatype( q[0][0] );
1224 }