src/theory/quantifiers/quant_util.cpp

   1 /*********************                                                        */
   2 /*! \file quant_util.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Tim King
   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 Implementation of quantifier utilities
  13  **/
  14
  15 #include "theory/quantifiers/quant_util.h"
  16 #include "theory/quantifiers/inst_match.h"
  17 #include "theory/quantifiers/term_database.h"
  18 #include "theory/quantifiers_engine.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
  26
  27 unsigned QuantifiersModule::needsModel( Theory::Effort e ) {
  28   return QuantifiersEngine::QEFFORT_NONE;
  29 }
  30
  31 eq::EqualityEngine * QuantifiersModule::getEqualityEngine() {
  32   return d_quantEngine->getMasterEqualityEngine();
  33 }
  34
  35 bool QuantifiersModule::areEqual( TNode n1, TNode n2 ) {
  36   return d_quantEngine->getEqualityQuery()->areEqual( n1, n2 );
  37 }
  38
  39 bool QuantifiersModule::areDisequal( TNode n1, TNode n2 ) {
  40   return d_quantEngine->getEqualityQuery()->areDisequal( n1, n2 );
  41 }
  42
  43 TNode QuantifiersModule::getRepresentative( TNode n ) {
  44   return d_quantEngine->getEqualityQuery()->getRepresentative( n );
  45 }
  46
  47 quantifiers::TermDb * QuantifiersModule::getTermDatabase() {
  48   return d_quantEngine->getTermDatabase();
  49 }
  50
  51 bool QuantArith::getMonomial( Node n, Node& c, Node& v ){
  52   if( n.getKind()==MULT && n.getNumChildren()==2 && n[0].isConst() ){
  53     c = n[0];
  54     v = n[1];
  55     return true;
  56   }else{
  57     return false;
  58   }
  59 }
  60 bool QuantArith::getMonomial( Node n, std::map< Node, Node >& msum ) {
  61   if( n.isConst() ){
  62     if( msum.find(Node::null())==msum.end() ){
  63       msum[Node::null()] = n;
  64       return true;
  65     }
  66   }else if( n.getKind()==MULT && n.getNumChildren()==2 && n[0].isConst() ){
  67     if( msum.find(n[1])==msum.end() ){
  68       msum[n[1]] = n[0];
  69       return true;
  70     }
  71   }else{
  72     if( msum.find(n)==msum.end() ){
  73       msum[n] = Node::null();
  74       return true;
  75     }
  76   }
  77   return false;
  78 }
  79
  80 bool QuantArith::getMonomialSum( Node n, std::map< Node, Node >& msum ) {
  81   if ( n.getKind()==PLUS ){
  82     for( unsigned i=0; i<n.getNumChildren(); i++) {
  83       if (!getMonomial( n[i], msum )){
  84         return false;
  85       }
  86     }
  87     return true;
  88   }else{
  89     return getMonomial( n, msum );
  90   }
  91 }
  92
  93 bool QuantArith::getMonomialSumLit( Node lit, std::map< Node, Node >& msum ) {
  94   if( lit.getKind()==GEQ || lit.getKind()==EQUAL ){
  95     if( getMonomialSum( lit[0], msum ) ){
  96       if( lit[1].isConst() && lit[1].getConst<Rational>().isZero() ){
  97         return true;
  98       }else{
  99         //subtract the other side
 100         std::map< Node, Node > msum2;
 101         if( getMonomialSum( lit[1], msum2 ) ){
 102           for( std::map< Node, Node >::iterator it = msum2.begin(); it != msum2.end(); ++it ){
 103             std::map< Node, Node >::iterator it2 = msum.find( it->first );
 104             if( it2!=msum.end() ){
 105               Node r = NodeManager::currentNM()->mkNode( MINUS, it2->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(1) ) : it2->second,
 106                                                                 it->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(1) ) : it->second );
 107               msum[it->first] = Rewriter::rewrite( r );
 108             }else{
 109               msum[it->first] = it->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(-1) ) : negate( it->second );
 110             }
 111           }
 112           return true;
 113         }
 114       }
 115     }
 116   }
 117   return false;
 118 }
 119
 120 Node QuantArith::mkNode( std::map< Node, Node >& msum ) {
 121   std::vector< Node > children;
 122   for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
 123     Node m;
 124     if( !it->first.isNull() ){
 125       if( !it->second.isNull() ){
 126         m = NodeManager::currentNM()->mkNode( MULT, it->second, it->first );
 127       }else{
 128         m = it->first;
 129       }
 130     }else{
 131       Assert( !it->second.isNull() );
 132       m = it->second;
 133     }
 134     children.push_back(m);
 135   }
 136   return children.size()>1 ? NodeManager::currentNM()->mkNode( PLUS, children ) : (children.size()==1 ? children[0] : NodeManager::currentNM()->mkConst( Rational(0) ));
 137 }
 138
 139 // given (msum <k> 0), solve (veq_c * v <k> val) or (val <k> veq_c * v), where:
 140 // veq_c is either null (meaning 1), or positive.
 141 // return value 1: veq_c*v is RHS, -1: veq_c*v is LHS, 0: failed.
 142 int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k ) {
 143   std::map< Node, Node >::iterator itv = msum.find( v );
 144   if( itv!=msum.end() ){
 145     std::vector< Node > children;
 146     Rational r = itv->second.isNull() ? Rational(1) : itv->second.getConst<Rational>();
 147     if ( r.sgn()!=0 ){
 148       for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
 149         if( it->first!=v ){
 150           Node m;
 151           if( !it->first.isNull() ){
 152             if ( !it->second.isNull() ){
 153               m = NodeManager::currentNM()->mkNode( MULT, it->second, it->first );
 154             }else{
 155               m = it->first;
 156             }
 157           }else{
 158             m = it->second;
 159           }
 160           children.push_back(m);
 161         }
 162       }
 163       val = children.size()>1 ? NodeManager::currentNM()->mkNode( PLUS, children ) :
 164                                 (children.size()==1 ? children[0] : NodeManager::currentNM()->mkConst( Rational(0) ));
 165       if( !r.isOne() && !r.isNegativeOne() ){
 166         if( v.getType().isInteger() ){
 167           veq_c = NodeManager::currentNM()->mkConst( r.abs() );
 168         }else{
 169           val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / r.abs() ) );
 170         }
 171       }
 172       if( r.sgn()==1 ){
 173         val = negate(val);
 174       }else{
 175         val = Rewriter::rewrite( val );
 176       }
 177       return ( r.sgn()==1 || k==EQUAL ) ? 1 : -1;
 178     }
 179   }
 180   return 0;
 181 }
 182
 183 int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k, bool doCoeff ) {
 184   Node veq_c;
 185   Node val;
 186   //isolate v in the (in)equality
 187   int ires = isolate( v, msum, veq_c, val, k );
 188   if( ires!=0 ){
 189     Node vc = v;
 190     if( !veq_c.isNull() ){
 191       if( doCoeff ){
 192         vc = NodeManager::currentNM()->mkNode( MULT, veq_c, vc );
 193       }else{
 194         return 0;
 195       }
 196     }
 197     bool inOrder = ires==1;
 198     veq = NodeManager::currentNM()->mkNode( k, inOrder ? vc : val, inOrder ? val : vc );
 199   }
 200   return ires;
 201 }
 202
 203 Node QuantArith::solveEqualityFor( Node lit, Node v ) {
 204   Assert( lit.getKind()==EQUAL || lit.getKind()==IFF );
 205   //first look directly at sides
 206   TypeNode tn = lit[0].getType();
 207   for( unsigned r=0; r<2; r++ ){
 208     if( lit[r]==v ){
 209       return lit[1-r];
 210     }
 211   }
 212   if( tn.isReal() ){
 213     if( quantifiers::TermDb::containsTerm( lit, v ) ){
 214       std::map< Node, Node > msum;
 215       if( QuantArith::getMonomialSumLit( lit, msum ) ){
 216         Node val, veqc;
 217         if( QuantArith::isolate( v, msum, veqc, val, EQUAL )!=0 ){
 218           if( veqc.isNull() ){
 219             return val;
 220           }
 221         }
 222       }
 223     }
 224   }
 225   return Node::null();
 226 }
 227
 228 Node QuantArith::negate( Node t ) {
 229   Node tt = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) ), t );
 230   tt = Rewriter::rewrite( tt );
 231   return tt;
 232 }
 233
 234 Node QuantArith::offset( Node t, int i ) {
 235   Node tt = NodeManager::currentNM()->mkNode( PLUS, NodeManager::currentNM()->mkConst( Rational(i) ), t );
 236   tt = Rewriter::rewrite( tt );
 237   return tt;
 238 }
 239
 240 void QuantArith::debugPrintMonomialSum( std::map< Node, Node >& msum, const char * c ) {
 241   for(std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
 242     Trace(c) << "  ";
 243     if( !it->second.isNull() ){
 244       Trace(c) << it->second;
 245       if( !it->first.isNull() ){
 246         Trace(c) << " * ";
 247       }
 248     }
 249     if( !it->first.isNull() ){
 250       Trace(c) << it->first;
 251     }
 252     Trace(c) << std::endl;
 253   }
 254   Trace(c) << std::endl;
 255 }
 256
 257
 258 void QuantRelevance::registerQuantifier( Node f ){
 259   //compute symbols in f
 260   std::vector< Node > syms;
 261   computeSymbols( f[1], syms );
 262   d_syms[f].insert( d_syms[f].begin(), syms.begin(), syms.end() );
 263   //set initial relevance
 264   int minRelevance = -1;
 265   for( int i=0; i<(int)syms.size(); i++ ){
 266     d_syms_quants[ syms[i] ].push_back( f );
 267     int r = getRelevance( syms[i] );
 268     if( r!=-1 && ( minRelevance==-1 || r<minRelevance ) ){
 269       minRelevance = r;
 270     }
 271   }
 272   if( minRelevance!=-1 ){
 273     setRelevance( f, minRelevance+1 );
 274   }
 275 }
 276
 277
 278 /** compute symbols */
 279 void QuantRelevance::computeSymbols( Node n, std::vector< Node >& syms ){
 280   if( n.getKind()==APPLY_UF ){
 281     Node op = n.getOperator();
 282     if( std::find( syms.begin(), syms.end(), op )==syms.end() ){
 283       syms.push_back( op );
 284     }
 285   }
 286   if( n.getKind()!=FORALL ){
 287     for( int i=0; i<(int)n.getNumChildren(); i++ ){
 288       computeSymbols( n[i], syms );
 289     }
 290   }
 291 }
 292
 293 /** set relevance */
 294 void QuantRelevance::setRelevance( Node s, int r ){
 295   if( d_computeRel ){
 296     int rOld = getRelevance( s );
 297     if( rOld==-1 || r<rOld ){
 298       d_relevance[s] = r;
 299       if( s.getKind()==FORALL ){
 300         for( int i=0; i<(int)d_syms[s].size(); i++ ){
 301           setRelevance( d_syms[s][i], r );
 302         }
 303       }else{
 304         for( int i=0; i<(int)d_syms_quants[s].size(); i++ ){
 305           setRelevance( d_syms_quants[s][i], r+1 );
 306         }
 307       }
 308     }
 309   }
 310 }
 311
 312
 313 QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){
 314   initialize( n, computeEq );
 315 }
 316
 317 void QuantPhaseReq::initialize( Node n, bool computeEq ){
 318   std::map< Node, int > phaseReqs2;
 319   computePhaseReqs( n, false, phaseReqs2 );
 320   for( std::map< Node, int >::iterator it = phaseReqs2.begin(); it != phaseReqs2.end(); ++it ){
 321     if( it->second==1 ){
 322       d_phase_reqs[ it->first ] = true;
 323     }else if( it->second==-1 ){
 324       d_phase_reqs[ it->first ] = false;
 325     }
 326   }
 327   Debug("inst-engine-phase-req") << "Phase requirements for " << n << ":" << std::endl;
 328   //now, compute if any patterns are equality required
 329   if( computeEq ){
 330     for( std::map< Node, bool >::iterator it = d_phase_reqs.begin(); it != d_phase_reqs.end(); ++it ){
 331       Debug("inst-engine-phase-req") << "   " << it->first << " -> " << it->second << std::endl;
 332       if( it->first.getKind()==EQUAL ){
 333         if( quantifiers::TermDb::hasInstConstAttr(it->first[0]) ){
 334           if( !quantifiers::TermDb::hasInstConstAttr(it->first[1]) ){
 335             d_phase_reqs_equality_term[ it->first[0] ] = it->first[1];
 336             d_phase_reqs_equality[ it->first[0] ] = it->second;
 337             Debug("inst-engine-phase-req") << "      " << it->first[0] << ( it->second ? " == " : " != " ) << it->first[1] << std::endl;
 338           }
 339         }else if( quantifiers::TermDb::hasInstConstAttr(it->first[1]) ){
 340           d_phase_reqs_equality_term[ it->first[1] ] = it->first[0];
 341           d_phase_reqs_equality[ it->first[1] ] = it->second;
 342           Debug("inst-engine-phase-req") << "      " << it->first[1] << ( it->second ? " == " : " != " ) << it->first[0] << std::endl;
 343         }
 344       }
 345     }
 346   }
 347 }
 348
 349 void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs ){
 350   bool newReqPol = false;
 351   bool newPolarity;
 352   if( n.getKind()==NOT ){
 353     newReqPol = true;
 354     newPolarity = !polarity;
 355   }else if( n.getKind()==OR || n.getKind()==IMPLIES ){
 356     if( !polarity ){
 357       newReqPol = true;
 358       newPolarity = false;
 359     }
 360   }else if( n.getKind()==AND ){
 361     if( polarity ){
 362       newReqPol = true;
 363       newPolarity = true;
 364     }
 365   }else{
 366     int val = polarity ? 1 : -1;
 367     if( phaseReqs.find( n )==phaseReqs.end() ){
 368       phaseReqs[n] = val;
 369     }else if( val!=phaseReqs[n] ){
 370       phaseReqs[n] = 0;
 371     }
 372   }
 373   if( newReqPol ){
 374     for( int i=0; i<(int)n.getNumChildren(); i++ ){
 375       if( n.getKind()==IMPLIES && i==0 ){
 376         computePhaseReqs( n[i], !newPolarity, phaseReqs );
 377       }else{
 378         computePhaseReqs( n[i], newPolarity, phaseReqs );
 379       }
 380     }
 381   }
 382 }
 383
 384 void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) {
 385   if( n.getKind()==AND || n.getKind()==OR || n.getKind()==SEP_STAR ){
 386     newHasPol = hasPol;
 387     newPol = pol;
 388   }else if( n.getKind()==IMPLIES ){
 389     newHasPol = hasPol;
 390     newPol = child==0 ? !pol : pol;
 391   }else if( n.getKind()==NOT ){
 392     newHasPol = hasPol;
 393     newPol = !pol;
 394   }else if( n.getKind()==ITE ){
 395     newHasPol = (child!=0) && hasPol;
 396     newPol = pol;
 397   }else if( n.getKind()==FORALL ){
 398     newHasPol = (child==1) && hasPol;
 399     newPol = pol;
 400   }else{
 401     newHasPol = false;
 402     newPol = pol;
 403   }
 404 }
 405
 406 void QuantPhaseReq::getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) {
 407   if( n.getKind()==AND || n.getKind()==OR ){
 408     newHasPol = hasPol && pol==( n.getKind()==AND );
 409     newPol = pol;
 410   }else if( n.getKind()==IMPLIES ){
 411     newHasPol = hasPol && !pol;
 412     newPol = child==0 ? !pol : pol;
 413   }else if( n.getKind()==NOT ){
 414     newHasPol = hasPol;
 415     newPol = !pol;
 416   }else{
 417     newHasPol = false;
 418     newPol = pol;
 419   }
 420 }
 421
 422 void QuantEPR::registerNode( Node n, std::map< int, std::map< Node, bool > >& visited, bool beneathQuant, bool hasPol, bool pol ) {
 423   int vindex = hasPol ? ( pol ? 1 : -1 ) : 0;
 424   if( visited[vindex].find( n )==visited[vindex].end() ){
 425     visited[vindex][n] = true;
 426     Trace("quant-epr-debug") << "QuantEPR::registerNode " << n << std::endl;
 427     if( n.getKind()==FORALL ){
 428       if( beneathQuant || !hasPol || !pol ){
 429         for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
 430           TypeNode tn = n[0][i].getType();
 431           if( d_non_epr.find( tn )==d_non_epr.end() ){
 432             Trace("quant-epr") << "Sort " << tn << " is non-EPR because of nested quantification." << std::endl;
 433             d_non_epr[tn] = true;
 434           }
 435         }
 436       }else{
 437         beneathQuant = true;
 438       }
 439     }
 440     TypeNode tn = n.getType();
 441
 442     if( n.getNumChildren()>0 ){
 443       if( tn.isSort() ){
 444         if( d_non_epr.find( tn )==d_non_epr.end() ){
 445           Trace("quant-epr") << "Sort " << tn << " is non-EPR because of " << n << std::endl;
 446           d_non_epr[tn] = true;
 447         }
 448       }
 449       for( unsigned i=0; i<n.getNumChildren(); i++ ){
 450         bool newHasPol;
 451         bool newPol;
 452         QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
 453         registerNode( n[i], visited, beneathQuant, newHasPol, newPol );
 454       }
 455     }else if( tn.isSort() ){
 456       if( n.getKind()==BOUND_VARIABLE ){
 457         if( d_consts.find( tn )==d_consts.end() ){
 458           //mark that at least one constant must occur
 459           d_consts[tn].clear();
 460         }
 461       }else if( std::find( d_consts[tn].begin(), d_consts[tn].end(), n )==d_consts[tn].end() ){
 462         d_consts[tn].push_back( n );
 463         Trace("quant-epr") << "...constant of type " << tn << " : " << n << std::endl;
 464       }
 465     }
 466   }
 467 }
 468
 469 void QuantEPR::registerAssertion( Node assertion ) {
 470   std::map< int, std::map< Node, bool > > visited;
 471   registerNode( assertion, visited, false, true, true );
 472 }
 473
 474 void QuantEPR::finishInit() {
 475   Trace("quant-epr-debug") << "QuantEPR::finishInit" << std::endl;
 476   for( std::map< TypeNode, std::vector< Node > >::iterator it = d_consts.begin(); it != d_consts.end(); ++it ){
 477     Assert( d_epr_axiom.find( it->first )==d_epr_axiom.end() );
 478     Trace("quant-epr-debug") << "process " << it->first << std::endl;
 479     if( d_non_epr.find( it->first )!=d_non_epr.end() ){
 480       Trace("quant-epr-debug") << "...non-epr" << std::endl;
 481       it->second.clear();
 482     }else{
 483       Trace("quant-epr-debug") << "...epr, #consts = " << it->second.size() << std::endl;
 484       if( it->second.empty() ){
 485         it->second.push_back( NodeManager::currentNM()->mkSkolem( "e", it->first, "EPR base constant" ) );
 486       }
 487       if( Trace.isOn("quant-epr") ){
 488         Trace("quant-epr") << "Type " << it->first << " is EPR, with constants : " << std::endl;
 489         for( unsigned i=0; i<it->second.size(); i++ ){
 490           Trace("quant-epr") << "  " << it->second[i] << std::endl;
 491         }
 492       }
 493     }
 494   }
 495 }
 496
 497 bool QuantEPR::isEPRConstant( TypeNode tn, Node k ) {
 498   return std::find( d_consts[tn].begin(), d_consts[tn].end(), k )!=d_consts[tn].end();
 499 }
 500
 501 void QuantEPR::addEPRConstant( TypeNode tn, Node k ) {
 502   Assert( isEPR( tn ) );
 503   Assert( d_epr_axiom.find( tn )==d_epr_axiom.end() );
 504   if( !isEPRConstant( tn, k ) ){
 505     d_consts[tn].push_back( k );
 506   }
 507 }
 508
 509 Node QuantEPR::mkEPRAxiom( TypeNode tn ) {
 510   Assert( isEPR( tn ) );
 511   std::map< TypeNode, Node >::iterator ita = d_epr_axiom.find( tn );
 512   if( ita==d_epr_axiom.end() ){
 513     std::vector< Node > disj;
 514     Node x = NodeManager::currentNM()->mkBoundVar( tn );
 515     for( unsigned i=0; i<d_consts[tn].size(); i++ ){
 516       disj.push_back( NodeManager::currentNM()->mkNode( tn.isBoolean() ? IFF : EQUAL, x, d_consts[tn][i] ) );
 517     }
 518     Assert( !disj.empty() );
 519     d_epr_axiom[tn] = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, x ), disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj ) );
 520     return d_epr_axiom[tn];
 521   }else{
 522     return ita->second;
 523   }
 524 }
 525