src/theory/datatypes/sygus_simple_sym.cpp

   1 /*********************                                                        */
   2 /*! \file sygus_simple_sym.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Haniel Barbosa, Mathias Preiner
   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 simple symmetry breaking for sygus
  13  **/
  14
  15 #include "theory/datatypes/sygus_simple_sym.h"
  16
  17 #include "theory/quantifiers_engine.h"
  18
  19 using namespace std;
  20 using namespace CVC4::kind;
  21
  22 namespace CVC4 {
  23 namespace theory {
  24 namespace datatypes {
  25
  26 SygusSimpleSymBreak::SygusSimpleSymBreak(QuantifiersEngine* qe)
  27     : d_tds(qe->getTermDatabaseSygus()), d_tutil(qe->getTermUtil())
  28 {
  29 }
  30
  31 /** Requirement trie
  32  *
  33  * This class is used to make queries about sygus grammars, including what
  34  * constructors they contain, and their types.
  35  *
  36  * As a simple example, consider the trie:
  37  * root:
  38  *   d_req_kind = PLUS
  39  *   d_children[0]:
  40  *     d_req_type = A
  41  *   d_children[1]:
  42  *     d_req_type = A
  43  * This trie is satisfied by sygus types that have a constructor whose builtin
  44  * kind is PLUS and whose argument types are both A.
  45  */
  46 class ReqTrie
  47 {
  48  public:
  49   ReqTrie() : d_req_kind(UNDEFINED_KIND) {}
  50   /** the children of this node */
  51   std::map<unsigned, ReqTrie> d_children;
  52   /** the (builtin) kind required by this node */
  53   Kind d_req_kind;
  54   /** the type that this node is required to be */
  55   TypeNode d_req_type;
  56   /** the constant required by this node */
  57   Node d_req_const;
  58   /** print this trie */
  59   void print(const char* c, int indent = 0)
  60   {
  61     if (d_req_kind != UNDEFINED_KIND)
  62     {
  63       Trace(c) << d_req_kind << " ";
  64     }
  65     else if (!d_req_type.isNull())
  66     {
  67       Trace(c) << d_req_type;
  68     }
  69     else if (!d_req_const.isNull())
  70     {
  71       Trace(c) << d_req_const;
  72     }
  73     else
  74     {
  75       Trace(c) << "_";
  76     }
  77     Trace(c) << std::endl;
  78     for (std::map<unsigned, ReqTrie>::iterator it = d_children.begin();
  79          it != d_children.end();
  80          ++it)
  81     {
  82       for (int i = 0; i <= indent; i++)
  83       {
  84         Trace(c) << "  ";
  85       }
  86       Trace(c) << it->first << " : ";
  87       it->second.print(c, indent + 1);
  88     }
  89   }
  90   /**
  91    * Are the requirements of this trie satisfied by sygus type tn?
  92    * tdb is a reference to the sygus term database.
  93    */
  94   bool satisfiedBy(quantifiers::TermDbSygus* tdb, TypeNode tn)
  95   {
  96     if (!d_req_const.isNull())
  97     {
  98       quantifiers::SygusTypeInfo& sti = tdb->getTypeInfo(tn);
  99       if (!sti.hasConst(d_req_const))
 100       {
 101         return false;
 102       }
 103     }
 104     if (!d_req_type.isNull())
 105     {
 106       Trace("sygus-sb-debug")
 107           << "- check if " << tn << " is type " << d_req_type << std::endl;
 108       if (tn != d_req_type)
 109       {
 110         return false;
 111       }
 112     }
 113     if (d_req_kind != UNDEFINED_KIND)
 114     {
 115       Trace("sygus-sb-debug")
 116           << "- check if " << tn << " has " << d_req_kind << std::endl;
 117       std::vector<TypeNode> argts;
 118       if (tdb->canConstructKind(tn, d_req_kind, argts))
 119       {
 120         for (std::map<unsigned, ReqTrie>::iterator it = d_children.begin();
 121              it != d_children.end();
 122              ++it)
 123         {
 124           if (it->first < argts.size())
 125           {
 126             TypeNode tnc = argts[it->first];
 127             if (!it->second.satisfiedBy(tdb, tnc))
 128             {
 129               return false;
 130             }
 131           }
 132           else
 133           {
 134             return false;
 135           }
 136         }
 137       }
 138       else
 139       {
 140         return false;
 141       }
 142     }
 143     return true;
 144   }
 145   /** is this the empty (trivially satisfied) trie? */
 146   bool empty()
 147   {
 148     return d_req_kind == UNDEFINED_KIND && d_req_const.isNull()
 149            && d_req_type.isNull() && d_children.empty();
 150   }
 151 };
 152
 153 bool SygusSimpleSymBreak::considerArgKind(
 154     TypeNode tn, TypeNode tnp, Kind k, Kind pk, int arg)
 155 {
 156   const DType& pdt = tnp.getDType();
 157   const DType& dt = tn.getDType();
 158   quantifiers::SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
 159   quantifiers::SygusTypeInfo& pti = d_tds->getTypeInfo(tnp);
 160   Assert(ti.hasKind(k));
 161   Assert(pti.hasKind(pk));
 162   Trace("sygus-sb-debug") << "Consider sygus arg kind " << k << ", pk = " << pk
 163                           << ", arg = " << arg << " in " << tnp << "?"
 164                           << std::endl;
 165   int c = ti.getKindConsNum(k);
 166   int pc = pti.getKindConsNum(pk);
 167   // check for associativity
 168   if (k == pk && quantifiers::TermUtil::isAssoc(k))
 169   {
 170     // if the operator is associative, then a repeated occurrence should only
 171     // occur in the leftmost argument position
 172     int firstArg = getFirstArgOccurrence(pdt[pc], tn);
 173     Assert(firstArg != -1);
 174     if (arg == firstArg)
 175     {
 176       return true;
 177     }
 178     // the argument types of the child must be the parent's type
 179     for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++)
 180     {
 181       TypeNode type = dt[c].getArgType(i);
 182       if (type != tnp)
 183       {
 184         return true;
 185       }
 186     }
 187     Trace("sygus-sb-simple")
 188         << "  sb-simple : do not consider " << k << " at child arg " << arg
 189         << " of " << k
 190         << " since it is associative, with first arg = " << firstArg
 191         << std::endl;
 192     return false;
 193   }
 194   // describes the shape of an alternate term to construct
 195   //  we check whether this term is in the sygus grammar below
 196   ReqTrie rt;
 197   Assert(rt.empty());
 198
 199   // construct rt by cases
 200   if (pk == NOT || pk == BITVECTOR_NOT || pk == UMINUS || pk == BITVECTOR_NEG)
 201   {
 202     // negation normal form
 203     if (pk == k)
 204     {
 205       rt.d_req_type = dt[c].getArgType(0);
 206     }
 207     else
 208     {
 209       Kind reqk = UNDEFINED_KIND;      // required kind for all children
 210       std::map<unsigned, Kind> reqkc;  // required kind for some children
 211       if (pk == NOT)
 212       {
 213         if (k == AND)
 214         {
 215           rt.d_req_kind = OR;
 216           reqk = NOT;
 217         }
 218         else if (k == OR)
 219         {
 220           rt.d_req_kind = AND;
 221           reqk = NOT;
 222         }
 223         else if (k == EQUAL)
 224         {
 225           rt.d_req_kind = XOR;
 226         }
 227         else if (k == XOR)
 228         {
 229           rt.d_req_kind = EQUAL;
 230         }
 231         else if (k == ITE)
 232         {
 233           rt.d_req_kind = ITE;
 234           reqkc[1] = NOT;
 235           reqkc[2] = NOT;
 236           rt.d_children[0].d_req_type = dt[c].getArgType(0);
 237         }
 238         else if (k == LEQ || k == GT)
 239         {
 240           //  (not (~ x y)) ----->  (~ (+ y 1) x)
 241           rt.d_req_kind = k;
 242           rt.d_children[0].d_req_kind = PLUS;
 243           rt.d_children[0].d_children[0].d_req_type = dt[c].getArgType(1);
 244           rt.d_children[0].d_children[1].d_req_const =
 245               NodeManager::currentNM()->mkConst(Rational(1));
 246           rt.d_children[1].d_req_type = dt[c].getArgType(0);
 247         }
 248         else if (k == LT || k == GEQ)
 249         {
 250           //  (not (~ x y)) ----->  (~ y (+ x 1))
 251           rt.d_req_kind = k;
 252           rt.d_children[0].d_req_type = dt[c].getArgType(1);
 253           rt.d_children[1].d_req_kind = PLUS;
 254           rt.d_children[1].d_children[0].d_req_type = dt[c].getArgType(0);
 255           rt.d_children[1].d_children[1].d_req_const =
 256               NodeManager::currentNM()->mkConst(Rational(1));
 257         }
 258       }
 259       else if (pk == BITVECTOR_NOT)
 260       {
 261         if (k == BITVECTOR_AND)
 262         {
 263           rt.d_req_kind = BITVECTOR_OR;
 264           reqk = BITVECTOR_NOT;
 265         }
 266         else if (k == BITVECTOR_OR)
 267         {
 268           rt.d_req_kind = BITVECTOR_AND;
 269           reqk = BITVECTOR_NOT;
 270         }
 271         else if (k == BITVECTOR_XNOR)
 272         {
 273           rt.d_req_kind = BITVECTOR_XOR;
 274         }
 275         else if (k == BITVECTOR_XOR)
 276         {
 277           rt.d_req_kind = BITVECTOR_XNOR;
 278         }
 279       }
 280       else if (pk == UMINUS)
 281       {
 282         if (k == PLUS)
 283         {
 284           rt.d_req_kind = PLUS;
 285           reqk = UMINUS;
 286         }
 287       }
 288       else if (pk == BITVECTOR_NEG)
 289       {
 290         if (k == PLUS)
 291         {
 292           rt.d_req_kind = PLUS;
 293           reqk = BITVECTOR_NEG;
 294         }
 295       }
 296       if (!rt.empty() && (reqk != UNDEFINED_KIND || !reqkc.empty()))
 297       {
 298         int pcr = pti.getKindConsNum(rt.d_req_kind);
 299         if (pcr != -1)
 300         {
 301           Assert(pcr < static_cast<int>(pdt.getNumConstructors()));
 302           // must have same number of arguments
 303           if (pdt[pcr].getNumArgs() == dt[c].getNumArgs())
 304           {
 305             for (unsigned i = 0, nargs = pdt[pcr].getNumArgs(); i < nargs; i++)
 306             {
 307               Kind rk = reqk;
 308               if (reqk == UNDEFINED_KIND)
 309               {
 310                 std::map<unsigned, Kind>::iterator itr = reqkc.find(i);
 311                 if (itr != reqkc.end())
 312                 {
 313                   rk = itr->second;
 314                 }
 315               }
 316               if (rk != UNDEFINED_KIND)
 317               {
 318                 rt.d_children[i].d_req_kind = rk;
 319                 rt.d_children[i].d_children[0].d_req_type = dt[c].getArgType(i);
 320               }
 321             }
 322           }
 323         }
 324       }
 325     }
 326   }
 327   else if (k == MINUS || k == BITVECTOR_SUB)
 328   {
 329     if (pk == EQUAL || pk == MINUS || pk == BITVECTOR_SUB || pk == LEQ
 330         || pk == LT || pk == GEQ || pk == GT)
 331     {
 332       int oarg = arg == 0 ? 1 : 0;
 333       //  (~ x (- y z))  ---->  (~ (+ x z) y)
 334       //  (~ (- y z) x)  ---->  (~ y (+ x z))
 335       rt.d_req_kind = pk;
 336       rt.d_children[arg].d_req_type = dt[c].getArgType(0);
 337       rt.d_children[oarg].d_req_kind = k == MINUS ? PLUS : BITVECTOR_PLUS;
 338       rt.d_children[oarg].d_children[0].d_req_type = pdt[pc].getArgType(oarg);
 339       rt.d_children[oarg].d_children[1].d_req_type = dt[c].getArgType(1);
 340     }
 341     else if (pk == PLUS || pk == BITVECTOR_PLUS)
 342     {
 343       //  (+ x (- y z))  -----> (- (+ x y) z)
 344       //  (+ (- y z) x)  -----> (- (+ x y) z)
 345       rt.d_req_kind = pk == PLUS ? MINUS : BITVECTOR_SUB;
 346       int oarg = arg == 0 ? 1 : 0;
 347       rt.d_children[0].d_req_kind = pk;
 348       rt.d_children[0].d_children[0].d_req_type = pdt[pc].getArgType(oarg);
 349       rt.d_children[0].d_children[1].d_req_type = dt[c].getArgType(0);
 350       rt.d_children[1].d_req_type = dt[c].getArgType(1);
 351     }
 352   }
 353   else if (k == ITE)
 354   {
 355     if (pk != ITE)
 356     {
 357       //  (o X (ite y z w) X')  -----> (ite y (o X z X') (o X w X'))
 358       rt.d_req_kind = ITE;
 359       rt.d_children[0].d_req_type = dt[c].getArgType(0);
 360       unsigned n_args = pdt[pc].getNumArgs();
 361       for (unsigned r = 1; r <= 2; r++)
 362       {
 363         rt.d_children[r].d_req_kind = pk;
 364         for (unsigned q = 0; q < n_args; q++)
 365         {
 366           if ((int)q == arg)
 367           {
 368             rt.d_children[r].d_children[q].d_req_type = dt[c].getArgType(r);
 369           }
 370           else
 371           {
 372             rt.d_children[r].d_children[q].d_req_type = pdt[pc].getArgType(q);
 373           }
 374         }
 375       }
 376       // this increases term size but is probably a good idea
 377     }
 378   }
 379   else if (k == NOT)
 380   {
 381     if (pk == ITE)
 382     {
 383       //  (ite (not y) z w)  -----> (ite y w z)
 384       rt.d_req_kind = ITE;
 385       rt.d_children[0].d_req_type = dt[c].getArgType(0);
 386       rt.d_children[1].d_req_type = pdt[pc].getArgType(2);
 387       rt.d_children[2].d_req_type = pdt[pc].getArgType(1);
 388     }
 389   }
 390   Trace("sygus-sb-debug") << "Consider sygus arg kind " << k << ", pk = " << pk
 391                           << ", arg = " << arg << "?" << std::endl;
 392   if (!rt.empty())
 393   {
 394     rt.print("sygus-sb-debug");
 395     // check if it meets the requirements
 396     if (rt.satisfiedBy(d_tds, tnp))
 397     {
 398       Trace("sygus-sb-debug") << "...success!" << std::endl;
 399       Trace("sygus-sb-simple")
 400           << "  sb-simple : do not consider " << k << " as arg " << arg
 401           << " of " << pk << std::endl;
 402       // do not need to consider the kind in the search since there are ways to
 403       // construct equivalent terms
 404       return false;
 405     }
 406     else
 407     {
 408       Trace("sygus-sb-debug") << "...failed." << std::endl;
 409     }
 410     Trace("sygus-sb-debug") << std::endl;
 411   }
 412   // must consider this kind in the search
 413   return true;
 414 }
 415
 416 bool SygusSimpleSymBreak::considerConst(
 417     TypeNode tn, TypeNode tnp, Node c, Kind pk, int arg)
 418 {
 419   const DType& pdt = tnp.getDType();
 420   // child grammar-independent
 421   if (!considerConst(pdt, tnp, c, pk, arg))
 422   {
 423     return false;
 424   }
 425   // this can probably be made child grammar independent
 426   quantifiers::SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
 427   quantifiers::SygusTypeInfo& pti = d_tds->getTypeInfo(tnp);
 428   int pc = pti.getKindConsNum(pk);
 429   if (pdt[pc].getNumArgs() == 2)
 430   {
 431     Kind ok;
 432     int offset;
 433     if (d_tutil->hasOffsetArg(pk, arg, offset, ok))
 434     {
 435       Trace("sygus-sb-simple-debug")
 436           << pk << " has offset arg " << ok << " " << offset << std::endl;
 437       int ok_arg = pti.getKindConsNum(ok);
 438       if (ok_arg != -1)
 439       {
 440         Trace("sygus-sb-simple-debug")
 441             << "...at argument " << ok_arg << std::endl;
 442         // other operator be the same type
 443         if (d_tds->isTypeMatch(pdt[ok_arg], pdt[arg]))
 444         {
 445           int status;
 446           Node co = d_tutil->getTypeValueOffset(c.getType(), c, offset, status);
 447           Trace("sygus-sb-simple-debug")
 448               << c << " with offset " << offset << " is " << co
 449               << ", status=" << status << std::endl;
 450           if (status == 0 && !co.isNull())
 451           {
 452             if (ti.hasConst(co))
 453             {
 454               Trace("sygus-sb-simple")
 455                   << "  sb-simple : by offset reasoning, do not consider const "
 456                   << c;
 457               Trace("sygus-sb-simple")
 458                   << " as arg " << arg << " of " << pk << " since we can use "
 459                   << co << " under " << ok << " " << std::endl;
 460               return false;
 461             }
 462           }
 463         }
 464       }
 465     }
 466   }
 467   return true;
 468 }
 469
 470 bool SygusSimpleSymBreak::considerConst(
 471     const DType& pdt, TypeNode tnp, Node c, Kind pk, int arg)
 472 {
 473   quantifiers::SygusTypeInfo& pti = d_tds->getTypeInfo(tnp);
 474   Assert(pti.hasKind(pk));
 475   int pc = pti.getKindConsNum(pk);
 476   bool ret = true;
 477   Trace("sygus-sb-debug") << "Consider sygus const " << c << ", parent = " << pk
 478                           << ", arg = " << arg << "?" << std::endl;
 479   if (d_tutil->isIdempotentArg(c, pk, arg))
 480   {
 481     if (pdt[pc].getNumArgs() == 2)
 482     {
 483       int oarg = arg == 0 ? 1 : 0;
 484       TypeNode otn = pdt[pc].getArgType(oarg);
 485       if (otn == tnp)
 486       {
 487         Trace("sygus-sb-simple")
 488             << "  sb-simple : " << c << " is idempotent arg " << arg << " of "
 489             << pk << "..." << std::endl;
 490         ret = false;
 491       }
 492     }
 493   }
 494   else
 495   {
 496     Node sc = d_tutil->isSingularArg(c, pk, arg);
 497     if (!sc.isNull())
 498     {
 499       if (pti.hasConst(sc))
 500       {
 501         Trace("sygus-sb-simple")
 502             << "  sb-simple : " << c << " is singular arg " << arg << " of "
 503             << pk << ", evaluating to " << sc << "..." << std::endl;
 504         ret = false;
 505       }
 506     }
 507   }
 508   if (ret)
 509   {
 510     ReqTrie rt;
 511     Assert(rt.empty());
 512     Node max_c = d_tutil->getTypeMaxValue(c.getType());
 513     Node zero_c = d_tutil->getTypeValue(c.getType(), 0);
 514     Node one_c = d_tutil->getTypeValue(c.getType(), 1);
 515     if (pk == XOR || pk == BITVECTOR_XOR)
 516     {
 517       if (c == max_c)
 518       {
 519         rt.d_req_kind = pk == XOR ? NOT : BITVECTOR_NOT;
 520       }
 521     }
 522     else if (pk == ITE)
 523     {
 524       if (arg == 0)
 525       {
 526         if (c == max_c)
 527         {
 528           rt.d_children[1].d_req_type = tnp;
 529         }
 530         else if (c == zero_c)
 531         {
 532           rt.d_children[2].d_req_type = tnp;
 533         }
 534       }
 535     }
 536     else if (pk == STRING_SUBSTR)
 537     {
 538       if (c == one_c && arg == 2)
 539       {
 540         rt.d_req_kind = STRING_CHARAT;
 541         rt.d_children[0].d_req_type = pdt[pc].getArgType(0);
 542         rt.d_children[1].d_req_type = pdt[pc].getArgType(1);
 543       }
 544     }
 545     if (!rt.empty())
 546     {
 547       // check if satisfied
 548       if (rt.satisfiedBy(d_tds, tnp))
 549       {
 550         Trace("sygus-sb-simple") << "  sb-simple : do not consider const " << c
 551                                  << " as arg " << arg << " of " << pk;
 552         Trace("sygus-sb-simple") << " in " << pdt.getName() << std::endl;
 553         // do not need to consider the constant in the search since there are
 554         // ways to construct equivalent terms
 555         ret = false;
 556       }
 557     }
 558   }
 559   return ret;
 560 }
 561
 562 int SygusSimpleSymBreak::solveForArgument(TypeNode tn,
 563                                           unsigned cindex,
 564                                           unsigned arg)
 565 {
 566   // we currently do not solve for arguments
 567   return -1;
 568 }
 569
 570 int SygusSimpleSymBreak::getFirstArgOccurrence(const DTypeConstructor& c,
 571                                                TypeNode tn)
 572 {
 573   for (unsigned i = 0, nargs = c.getNumArgs(); i < nargs; i++)
 574   {
 575     if (c.getArgType(i) == tn)
 576     {
 577       return i;
 578     }
 579   }
 580   return -1;
 581 }
 582
 583 }  // namespace datatypes
 584 }  // namespace theory
 585 }  // namespace CVC4