src/theory/quantifiers/quantifiers_attributes.cpp

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