src/theory/quantifiers/quantifiers_attributes.cpp

   1 /*********************                                                        */
   2 /*! \file quantifiers_attributes.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Paul Meng
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 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 QuantifiersAttributes class
  13  **/
  14
  15 #include "theory/quantifiers/quantifiers_attributes.h"
  16
  17 #include "options/quantifiers_options.h"
  18 #include "theory/arith/arith_msum.h"
  19 #include "theory/quantifiers/fun_def_engine.h"
  20 #include "theory/quantifiers/rewrite_engine.h"
  21 #include "theory/quantifiers/sygus/ce_guided_instantiation.h"
  22 #include "theory/quantifiers/term_util.h"
  23 #include "theory/quantifiers_engine.h"
  24
  25 using namespace std;
  26 using namespace CVC4::kind;
  27 using namespace CVC4::context;
  28
  29 namespace CVC4 {
  30 namespace theory {
  31 namespace quantifiers {
  32
  33 QuantAttributes::QuantAttributes( QuantifiersEngine * qe ) :
  34 d_quantEngine(qe) {
  35
  36 }
  37
  38 void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::vector< Node >& node_values, std::string str_value ){
  39   Trace("quant-attr-debug") << "Set " << attr << " " << n << std::endl;
  40   if( attr=="axiom" ){
  41     Trace("quant-attr-debug") << "Set axiom " << n << std::endl;
  42     AxiomAttribute aa;
  43     n.setAttribute( aa, true );
  44   }else if( attr=="conjecture" ){
  45     Trace("quant-attr-debug") << "Set conjecture " << n << std::endl;
  46     ConjectureAttribute ca;
  47     n.setAttribute( ca, true );
  48   }else if( attr=="fun-def" ){
  49     Trace("quant-attr-debug") << "Set function definition " << n << std::endl;
  50     FunDefAttribute fda;
  51     n.setAttribute( fda, true );
  52   }else if( attr=="sygus" ){
  53     Trace("quant-attr-debug") << "Set sygus " << n << std::endl;
  54     SygusAttribute ca;
  55     n.setAttribute( ca, true );
  56   } else if (attr == "sygus-synth-grammar") {
  57     Assert( node_values.size()==1 );
  58     Trace("quant-attr-debug") << "Set sygus synth grammar " << n << " to "
  59                               << node_values[0] << std::endl;
  60     SygusSynthGrammarAttribute ssg;
  61     n.setAttribute(ssg, node_values[0]);
  62   }else if( attr=="sygus-synth-fun-var-list" ){
  63     Assert( node_values.size()==1 );
  64     Trace("quant-attr-debug") << "Set sygus synth fun var list to " << n << " to "  << node_values[0] << std::endl;
  65     SygusSynthFunVarListAttribute ssfvla;
  66     n.setAttribute( ssfvla, node_values[0] );
  67   }else if( attr=="synthesis" ){
  68     Trace("quant-attr-debug") << "Set synthesis " << n << std::endl;
  69     SynthesisAttribute ca;
  70     n.setAttribute( ca, true );
  71   }else if( attr=="quant-inst-max-level" ){
  72     Assert( node_values.size()==1 );
  73     uint64_t lvl = node_values[0].getConst<Rational>().getNumerator().getLong();
  74     Trace("quant-attr-debug") << "Set instantiation level " << n << " to " << lvl << std::endl;
  75     QuantInstLevelAttribute qila;
  76     n.setAttribute( qila, lvl );
  77   }else if( attr=="rr-priority" ){
  78     Assert( node_values.size()==1 );
  79     uint64_t lvl = node_values[0].getConst<Rational>().getNumerator().getLong();
  80     Trace("quant-attr-debug") << "Set rewrite rule priority " << n << " to " << lvl << std::endl;
  81     RrPriorityAttribute rrpa;
  82     n.setAttribute( rrpa, lvl );
  83   }else if( attr=="quant-elim" ){
  84     Trace("quant-attr-debug") << "Set quantifier elimination " << n << std::endl;
  85     QuantElimAttribute qea;
  86     n.setAttribute( qea, true );
  87   }else if( attr=="quant-elim-partial" ){
  88     Trace("quant-attr-debug") << "Set partial quantifier elimination " << n << std::endl;
  89     QuantElimPartialAttribute qepa;
  90     n.setAttribute( qepa, true );
  91   }
  92 }
  93
  94 bool QuantAttributes::checkRewriteRule( Node q ) {
  95   return !getRewriteRule( q ).isNull();
  96 }
  97
  98 Node QuantAttributes::getRewriteRule( Node q ) {
  99   if (q.getKind() == FORALL && q.getNumChildren() == 3
 100       && q[2][0].getNumChildren() > 0
 101       && q[2][0][0].getKind() == REWRITE_RULE)
 102   {
 103     return q[2][0][0];
 104   }else{
 105     return Node::null();
 106   }
 107 }
 108
 109 bool QuantAttributes::checkFunDef( Node q ) {
 110   return !getFunDefHead( q ).isNull();
 111 }
 112
 113 bool QuantAttributes::checkFunDefAnnotation( Node ipl ) {
 114   if( !ipl.isNull() ){
 115     for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
 116       if( ipl[i].getKind()==INST_ATTRIBUTE ){
 117         if( ipl[i][0].getAttribute(FunDefAttribute()) ){
 118           return true;
 119         }
 120       }
 121     }
 122   }
 123   return false;
 124 }
 125
 126 Node QuantAttributes::getFunDefHead( Node q ) {
 127   //&& q[1].getKind()==EQUAL && q[1][0].getKind()==APPLY_UF &&
 128   if( q.getKind()==FORALL && q.getNumChildren()==3 ){
 129     Node ipl = q[2];
 130     for (unsigned i = 0; i < ipl.getNumChildren(); i++)
 131     {
 132       if (ipl[i].getKind() == INST_ATTRIBUTE
 133           && ipl[i][0].getAttribute(FunDefAttribute()))
 134       {
 135         return ipl[i][0];
 136       }
 137     }
 138   }
 139   return Node::null();
 140 }
 141 Node QuantAttributes::getFunDefBody( Node q ) {
 142   Node h = getFunDefHead( q );
 143   if( !h.isNull() ){
 144     if( q[1].getKind()==EQUAL ){
 145       if( q[1][0]==h ){
 146         return q[1][1];
 147       }else if( q[1][1]==h ){
 148         return q[1][0];
 149       }
 150       else if (q[1][0].getType().isReal())
 151       {
 152         // solve for h in the equality
 153         std::map<Node, Node> msum;
 154         if (ArithMSum::getMonomialSum(q[1], msum))
 155         {
 156           Node veq;
 157           int res = ArithMSum::isolate(h, msum, veq, EQUAL);
 158           if (res != 0)
 159           {
 160             Assert(veq.getKind() == EQUAL);
 161             return res == 1 ? veq[0] : veq[1];
 162           }
 163         }
 164       }
 165     }else{
 166       Node atom = q[1].getKind()==NOT ? q[1][0] : q[1];
 167       bool pol = q[1].getKind()!=NOT;
 168       if( atom==h ){
 169         return NodeManager::currentNM()->mkConst( pol );
 170       }
 171     }
 172   }
 173   return Node::null();
 174 }
 175
 176 bool QuantAttributes::checkSygusConjecture( Node q ) {
 177   return ( q.getKind()==FORALL && q.getNumChildren()==3 ) ? checkSygusConjectureAnnotation( q[2] ) : false;
 178 }
 179
 180 bool QuantAttributes::checkSygusConjectureAnnotation( Node ipl ){
 181   if( !ipl.isNull() ){
 182     for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
 183       if( ipl[i].getKind()==INST_ATTRIBUTE ){
 184         Node avar = ipl[i][0];
 185         if( avar.getAttribute(SygusAttribute()) ){
 186           return true;
 187         }
 188       }
 189     }
 190   }
 191   return false;
 192 }
 193
 194 bool QuantAttributes::checkQuantElimAnnotation( Node ipl ) {
 195   if( !ipl.isNull() ){
 196     for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
 197       if( ipl[i].getKind()==INST_ATTRIBUTE ){
 198         Node avar = ipl[i][0];
 199         if( avar.getAttribute(QuantElimAttribute()) ){
 200           return true;
 201         }
 202       }
 203     }
 204   }
 205   return false;
 206 }
 207
 208 void QuantAttributes::computeAttributes( Node q ) {
 209   computeQuantAttributes( q, d_qattr[q] );
 210   if( !d_qattr[q].d_rr.isNull() ){
 211     if( d_quantEngine->getRewriteEngine()==NULL ){
 212       Trace("quant-warn") << "WARNING : rewrite engine is null, and we have : " << q << std::endl;
 213     }
 214     //set rewrite engine as owner
 215     d_quantEngine->setOwner( q, d_quantEngine->getRewriteEngine(), 2 );
 216   }
 217   if( d_qattr[q].isFunDef() ){
 218     Node f = d_qattr[q].d_fundef_f;
 219     if( d_fun_defs.find( f )!=d_fun_defs.end() ){
 220       Message() << "Cannot define function " << f << " more than once." << std::endl;
 221       AlwaysAssert(false);
 222     }
 223     d_fun_defs[f] = true;
 224     d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine(), 2 );
 225   }
 226   if( d_qattr[q].d_sygus ){
 227     if( d_quantEngine->getCegInstantiation()==NULL ){
 228       Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl;
 229     }
 230     d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation(), 2 );
 231   }
 232   if( d_qattr[q].d_synthesis ){
 233     if( d_quantEngine->getCegInstantiation()==NULL ){
 234       Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl;
 235     }
 236     d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation(), 2 );
 237   }
 238 }
 239
 240 void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){
 241   Trace("quant-attr-debug") << "Compute attributes for " << q << std::endl;
 242   if( q.getNumChildren()==3 ){
 243     qa.d_ipl = q[2];
 244     for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
 245       Trace("quant-attr-debug") << "Check : " << q[2][i] << " " << q[2][i].getKind() << std::endl;
 246       if( q[2][i].getKind()==INST_PATTERN || q[2][i].getKind()==INST_NO_PATTERN ){
 247         qa.d_hasPattern = true;
 248       }else if( q[2][i].getKind()==INST_ATTRIBUTE ){
 249         Node avar = q[2][i][0];
 250         if( avar.getAttribute(AxiomAttribute()) ){
 251           Trace("quant-attr") << "Attribute : axiom : " << q << std::endl;
 252           qa.d_axiom = true;
 253         }
 254         if( avar.getAttribute(ConjectureAttribute()) ){
 255           Trace("quant-attr") << "Attribute : conjecture : " << q << std::endl;
 256           qa.d_conjecture = true;
 257         }
 258         if( avar.getAttribute(FunDefAttribute()) ){
 259           Trace("quant-attr") << "Attribute : function definition : " << q << std::endl;
 260           //get operator directly from pattern
 261           qa.d_fundef_f = q[2][i][0].getOperator();
 262         }
 263         if( avar.getAttribute(SygusAttribute()) ){
 264           //not necessarily nested existential
 265           //Assert( q[1].getKind()==NOT );
 266           //Assert( q[1][0].getKind()==FORALL );
 267           Trace("quant-attr") << "Attribute : sygus : " << q << std::endl;
 268           qa.d_sygus = true;
 269         }
 270         if( avar.getAttribute(SynthesisAttribute()) ){
 271           Trace("quant-attr") << "Attribute : synthesis : " << q << std::endl;
 272           qa.d_synthesis = true;
 273         }
 274         if( avar.hasAttribute(QuantInstLevelAttribute()) ){
 275           qa.d_qinstLevel = avar.getAttribute(QuantInstLevelAttribute());
 276           Trace("quant-attr") << "Attribute : quant inst level " << qa.d_qinstLevel << " : " << q << std::endl;
 277         }
 278         if( avar.hasAttribute(RrPriorityAttribute()) ){
 279           qa.d_rr_priority = avar.getAttribute(RrPriorityAttribute());
 280           Trace("quant-attr") << "Attribute : rr priority " << qa.d_rr_priority << " : " << q << std::endl;
 281         }
 282         if( avar.getAttribute(QuantElimAttribute()) ){
 283           Trace("quant-attr") << "Attribute : quantifier elimination : " << q << std::endl;
 284           qa.d_quant_elim = true;
 285           //don't set owner, should happen naturally
 286         }
 287         if( avar.getAttribute(QuantElimPartialAttribute()) ){
 288           Trace("quant-attr") << "Attribute : quantifier elimination partial : " << q << std::endl;
 289           qa.d_quant_elim = true;
 290           qa.d_quant_elim_partial = true;
 291           //don't set owner, should happen naturally
 292         }
 293         if( avar.hasAttribute(QuantIdNumAttribute()) ){
 294           qa.d_qid_num = avar;
 295           Trace("quant-attr") << "Attribute : id number " << qa.d_qid_num.getAttribute(QuantIdNumAttribute()) << " : " << q << std::endl;
 296         }
 297         if( avar.getKind()==REWRITE_RULE ){
 298           Trace("quant-attr") << "Attribute : rewrite rule : " << q << std::endl;
 299           Assert( i==0 );
 300           qa.d_rr = avar;
 301         }
 302       }
 303     }
 304   }
 305 }
 306
 307 bool QuantAttributes::isConjecture( Node q ) {
 308   std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
 309   if( it==d_qattr.end() ){
 310     return false;
 311   }else{
 312     return it->second.d_conjecture;
 313   }
 314 }
 315
 316 bool QuantAttributes::isAxiom( Node q ) {
 317   std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
 318   if( it==d_qattr.end() ){
 319     return false;
 320   }else{
 321     return it->second.d_axiom;
 322   }
 323 }
 324
 325 bool QuantAttributes::isFunDef( Node q ) {
 326   std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
 327   if( it==d_qattr.end() ){
 328     return false;
 329   }else{
 330     return it->second.isFunDef();
 331   }
 332 }
 333
 334 bool QuantAttributes::isSygus( Node q ) {
 335   std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
 336   if( it==d_qattr.end() ){
 337     return false;
 338   }else{
 339     return it->second.d_sygus;
 340   }
 341 }
 342
 343 bool QuantAttributes::isSynthesis( Node q ) {
 344   std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
 345   if( it==d_qattr.end() ){
 346     return false;
 347   }else{
 348     return it->second.d_synthesis;
 349   }
 350 }
 351
 352 int QuantAttributes::getQuantInstLevel( Node q ) {
 353   std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
 354   if( it==d_qattr.end() ){
 355     return -1;
 356   }else{
 357     return it->second.d_qinstLevel;
 358   }
 359 }
 360
 361 int QuantAttributes::getRewriteRulePriority( Node q ) {
 362   std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
 363   if( it==d_qattr.end() ){
 364     return -1;
 365   }else{
 366     return it->second.d_rr_priority;
 367   }
 368 }
 369
 370 bool QuantAttributes::isQuantElim( Node q ) {
 371   std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
 372   if( it==d_qattr.end() ){
 373     return false;
 374   }else{
 375     return it->second.d_quant_elim;
 376   }
 377 }
 378
 379 bool QuantAttributes::isQuantElimPartial( Node q ) {
 380   std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
 381   if( it==d_qattr.end() ){
 382     return false;
 383   }else{
 384     return it->second.d_quant_elim_partial;
 385   }
 386 }
 387
 388 int QuantAttributes::getQuantIdNum( Node q ) {
 389   std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
 390   if( it!=d_qattr.end() ){
 391     if( !it->second.d_qid_num.isNull() ){
 392       return it->second.d_qid_num.getAttribute(QuantIdNumAttribute());
 393     }
 394   }
 395   return -1;
 396 }
 397
 398 Node QuantAttributes::getQuantIdNumNode( Node q ) {
 399   std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
 400   if( it==d_qattr.end() ){
 401     return Node::null();
 402   }else{
 403     return it->second.d_qid_num;
 404   }
 405 }
 406
 407 void QuantAttributes::setInstantiationLevelAttr(Node n, Node qn, uint64_t level)
 408 {
 409   Trace("inst-level-debug2") << "IL : " << n << " " << qn << " " << level
 410                              << std::endl;
 411   // if not from the vector of terms we instantiatied
 412   if (qn.getKind() != BOUND_VARIABLE && n != qn)
 413   {
 414     // if this is a new term, without an instantiation level
 415     if (!n.hasAttribute(InstLevelAttribute()))
 416     {
 417       InstLevelAttribute ila;
 418       n.setAttribute(ila, level);
 419       Trace("inst-level-debug") << "Set instantiation level " << n << " to "
 420                                 << level << std::endl;
 421       Assert(n.getNumChildren() == qn.getNumChildren());
 422       for (unsigned i = 0; i < n.getNumChildren(); i++)
 423       {
 424         setInstantiationLevelAttr(n[i], qn[i], level);
 425       }
 426     }
 427   }
 428 }
 429
 430 void QuantAttributes::setInstantiationLevelAttr(Node n, uint64_t level)
 431 {
 432   if (!n.hasAttribute(InstLevelAttribute()))
 433   {
 434     InstLevelAttribute ila;
 435     n.setAttribute(ila, level);
 436     Trace("inst-level-debug") << "Set instantiation level " << n << " to "
 437                               << level << std::endl;
 438     for (unsigned i = 0; i < n.getNumChildren(); i++)
 439     {
 440       setInstantiationLevelAttr(n[i], level);
 441     }
 442   }
 443 }
 444
 445 } /* CVC4::theory::quantifiers namespace */
 446 } /* CVC4::theory namespace */
 447 } /* CVC4 namespace */