src/theory/quantifiers/sygus/sygus_grammar_norm.cpp

   1 /*********************                                                        */
   2 /*! \file sygus_grammar_norm.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Haniel Barbosa
   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 class for for simplifying SyGuS grammars after they
  13  ** are encoded into datatypes.
  14  **/
  15
  16 #include "theory/quantifiers/sygus/sygus_grammar_norm.h"
  17
  18 #include "expr/datatype.h"
  19 #include "options/quantifiers_options.h"
  20 #include "printer/sygus_print_callback.h"
  21 #include "smt/smt_engine.h"
  22 #include "smt/smt_engine_scope.h"
  23 #include "theory/quantifiers/sygus/ce_guided_conjecture.h"
  24 #include "theory/quantifiers/sygus/sygus_grammar_red.h"
  25 #include "theory/quantifiers/sygus/term_database_sygus.h"
  26 #include "theory/quantifiers/term_util.h"
  27
  28 #include <numeric>  // for std::iota
  29
  30 using namespace CVC4::kind;
  31
  32 namespace CVC4 {
  33 namespace theory {
  34 namespace quantifiers {
  35
  36 bool OpPosTrie::getOrMakeType(TypeNode tn,
  37                               TypeNode& unres_tn,
  38                               const std::vector<unsigned>& op_pos,
  39                               unsigned ind)
  40 {
  41   if (ind == op_pos.size())
  42   {
  43     /* Found type */
  44     if (!d_unres_tn.isNull())
  45     {
  46       Trace("sygus-grammar-normalize-trie")
  47           << "\tFound type " << d_unres_tn << "\n";
  48       unres_tn = d_unres_tn;
  49       return true;
  50     }
  51     /* Creating unresolved type */
  52     std::stringstream ss;
  53     ss << tn << "_";
  54     for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
  55     {
  56       ss << "_" << std::to_string(op_pos[i]);
  57     }
  58     d_unres_tn = NodeManager::currentNM()->mkSort(
  59         ss.str(), ExprManager::SORT_FLAG_PLACEHOLDER);
  60     Trace("sygus-grammar-normalize-trie")
  61         << "\tCreating type " << d_unres_tn << "\n";
  62     unres_tn = d_unres_tn;
  63     return false;
  64   }
  65   /* Go to next node */
  66   return d_children[op_pos[ind]].getOrMakeType(tn, unres_tn, op_pos, ind + 1);
  67 }
  68
  69 void SygusGrammarNorm::TypeObject::addConsInfo(SygusGrammarNorm* sygus_norm,
  70                                                const DatatypeConstructor& cons)
  71 {
  72   Trace("sygus-grammar-normalize") << "...for " << cons.getName() << "\n";
  73   /* Recover the sygus operator to not lose reference to the original
  74    * operator (NOT, ITE, etc) */
  75   Node exp_sop_n = Node::fromExpr(
  76       smt::currentSmtEngine()->expandDefinitions(cons.getSygusOp()));
  77   d_ops.push_back(Rewriter::rewrite(exp_sop_n));
  78   Trace("sygus-grammar-normalize-defs")
  79       << "\tOriginal op: " << cons.getSygusOp()
  80       << "\n\tExpanded one: " << exp_sop_n
  81       << "\n\tRewritten one: " << d_ops.back() << "\n\n";
  82   d_cons_names.push_back(cons.getName());
  83   d_pc.push_back(cons.getSygusPrintCallback());
  84   d_weight.push_back(cons.getWeight());
  85   d_cons_args_t.push_back(std::vector<Type>());
  86   for (const DatatypeConstructorArg& arg : cons)
  87   {
  88     /* Collect unresolved type nodes corresponding to the typenode of the
  89      * arguments */
  90     d_cons_args_t.back().push_back(
  91         sygus_norm
  92             ->normalizeSygusRec(TypeNode::fromType(
  93                 static_cast<SelectorType>(arg.getType()).getRangeType()))
  94             .toType());
  95   }
  96 }
  97
  98 void SygusGrammarNorm::TypeObject::buildDatatype(SygusGrammarNorm* sygus_norm,
  99                                                  const Datatype& dt)
 100 {
 101   /* Use the sygus type to not lose reference to the original types (Bool,
 102    * Int, etc) */
 103   d_dt.setSygus(dt.getSygusType(),
 104                 sygus_norm->d_sygus_vars.toExpr(),
 105                 dt.getSygusAllowConst(),
 106                 dt.getSygusAllowAll());
 107   for (unsigned i = 0, size_d_ops = d_ops.size(); i < size_d_ops; ++i)
 108   {
 109     d_dt.addSygusConstructor(d_ops[i].toExpr(),
 110                              d_cons_names[i],
 111                              d_cons_args_t[i],
 112                              d_pc[i],
 113                              d_weight[i]);
 114   }
 115   Trace("sygus-grammar-normalize") << "...built datatype " << d_dt << " ";
 116   /* Add to global accumulators */
 117   sygus_norm->d_dt_all.push_back(d_dt);
 118   sygus_norm->d_unres_t_all.insert(d_unres_tn.toType());
 119   Trace("sygus-grammar-normalize") << "---------------------------------\n";
 120 }
 121
 122 void SygusGrammarNorm::TransfDrop::buildType(SygusGrammarNorm* sygus_norm,
 123                                              TypeObject& to,
 124                                              const Datatype& dt,
 125                                              std::vector<unsigned>& op_pos)
 126 {
 127   std::vector<unsigned> difference;
 128   std::set_difference(op_pos.begin(),
 129                       op_pos.end(),
 130                       d_drop_indices.begin(),
 131                       d_drop_indices.end(),
 132                       std::back_inserter(difference));
 133   op_pos = difference;
 134 }
 135
 136 /* TODO #1304: have more operators and types. Moreover, have more general ways
 137    of finding kind of operator, e.g. if op is (\lambda xy. x + y) this
 138    function should realize that it is chainable for integers */
 139 bool SygusGrammarNorm::TransfChain::isChainable(TypeNode tn, Node op)
 140 {
 141   /* Checks whether operator occurs chainable for its type */
 142   if (tn.isInteger() && NodeManager::currentNM()->operatorToKind(op) == PLUS)
 143   {
 144     return true;
 145   }
 146   return false;
 147 }
 148
 149 /* TODO #1304: have more operators and types. Moreover, have more general ways
 150    of finding kind of operator, e.g. if op is (\lambda xy. x + y) this
 151    function should realize that it is chainable for integers */
 152 bool SygusGrammarNorm::TransfChain::isId(TypeNode tn, Node op, Node n)
 153 {
 154   if (tn.isInteger() && NodeManager::currentNM()->operatorToKind(op) == PLUS
 155       && n == TermUtil::mkTypeValue(tn, 0))
 156   {
 157     return true;
 158   }
 159   return false;
 160 }
 161
 162 void SygusGrammarNorm::TransfChain::buildType(SygusGrammarNorm* sygus_norm,
 163                                               TypeObject& to,
 164                                               const Datatype& dt,
 165                                               std::vector<unsigned>& op_pos)
 166 {
 167   NodeManager* nm = NodeManager::currentNM();
 168   std::vector<unsigned> claimed(d_elem_pos);
 169   claimed.push_back(d_chain_op_pos);
 170   unsigned nb_op_pos = op_pos.size();
 171   /* TODO do this properly */
 172   /* Remove from op_pos the positions claimed by the transformation */
 173   std::sort(op_pos.begin(), op_pos.end());
 174   std::sort(claimed.begin(), claimed.end());
 175   std::vector<unsigned> difference;
 176   std::set_difference(op_pos.begin(),
 177                       op_pos.end(),
 178                       claimed.begin(),
 179                       claimed.end(),
 180                       std::back_inserter(difference));
 181   op_pos = difference;
 182   if (Trace.isOn("sygus-grammar-normalize-chain"))
 183   {
 184     Trace("sygus-grammar-normalize-chain")
 185         << "OP at " << d_chain_op_pos << "\n"
 186         << d_elem_pos.size() << " d_elem_pos: ";
 187     for (unsigned i = 0, size = d_elem_pos.size(); i < size; ++i)
 188     {
 189       Trace("sygus-grammar-normalize-chain") << d_elem_pos[i] << " ";
 190     }
 191     Trace("sygus-grammar-normalize-chain")
 192         << "\n"
 193         << op_pos.size() << " remaining op_pos: ";
 194     for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
 195     {
 196       Trace("sygus-grammar-normalize-chain") << op_pos[i] << " ";
 197     }
 198     Trace("sygus-grammar-normalize-chain") << "\n";
 199   }
 200   /* Build identity operator and empty callback */
 201   Node iden_op =
 202       SygusGrammarNorm::getIdOp(TypeNode::fromType(dt.getSygusType()));
 203   /* If all operators are claimed, create a monomial */
 204   if (nb_op_pos == d_elem_pos.size() + 1)
 205   {
 206     Trace("sygus-grammar-normalize-chain")
 207         << "\tCreating id type for " << d_elem_pos.back() << "\n";
 208     /* creates type for element */
 209     std::vector<unsigned> tmp;
 210     tmp.push_back(d_elem_pos.back());
 211     Type t = sygus_norm->normalizeSygusRec(to.d_tn, dt, tmp).toType();
 212     /* consumes element */
 213     d_elem_pos.pop_back();
 214     /* adds to Root: "type" */
 215     to.d_ops.push_back(iden_op);
 216     to.d_cons_names.push_back("id");
 217     to.d_pc.push_back(printer::SygusEmptyPrintCallback::getEmptyPC());
 218     /* Identity operators should not increase the size of terms */
 219     to.d_weight.push_back(0);
 220     to.d_cons_args_t.push_back(std::vector<Type>());
 221     to.d_cons_args_t.back().push_back(t);
 222     Trace("sygus-grammar-normalize-chain")
 223         << "\tAdding  " << t << " to " << to.d_unres_tn << "\n";
 224     /* adds to Root: "type + Root" */
 225     to.d_ops.push_back(nm->operatorOf(PLUS));
 226     to.d_cons_names.push_back(kindToString(PLUS));
 227     to.d_pc.push_back(nullptr);
 228     to.d_weight.push_back(-1);
 229     to.d_cons_args_t.push_back(std::vector<Type>());
 230     to.d_cons_args_t.back().push_back(t);
 231     to.d_cons_args_t.back().push_back(to.d_unres_tn.toType());
 232     Trace("sygus-grammar-normalize-chain")
 233         << "\tAdding PLUS to " << to.d_unres_tn << " with arg types "
 234         << to.d_unres_tn << " and " << t << "\n";
 235   }
 236   /* In the initial case if not all operators claimed always creates a next */
 237   Assert(nb_op_pos != d_elem_pos.size() + 1 || d_elem_pos.size() > 1);
 238   /* TODO #1304: consider case in which CHAIN op has different types than
 239      to.d_tn */
 240   /* If no more elements to chain, finish */
 241   if (d_elem_pos.size() == 0)
 242   {
 243     return;
 244   }
 245   /* Creates a type do be added to root representing next step in the chain */
 246   /* Add + to elems */
 247   d_elem_pos.push_back(d_chain_op_pos);
 248   if (Trace.isOn("sygus-grammar-normalize-chain"))
 249   {
 250     Trace("sygus-grammar-normalize-chain")
 251         << "\tCreating type for next entry with sygus_ops ";
 252     for (unsigned i = 0, size = d_elem_pos.size(); i < size; ++i)
 253     {
 254       Trace("sygus-grammar-normalize-chain")
 255           << dt[d_elem_pos[i]].getSygusOp() << " ";
 256     }
 257     Trace("sygus-grammar-normalize-chain") << "\n";
 258   }
 259   /* adds to Root: (\lambda x. x ) Next */
 260   to.d_ops.push_back(iden_op);
 261   to.d_cons_names.push_back("id_next");
 262   to.d_pc.push_back(printer::SygusEmptyPrintCallback::getEmptyPC());
 263   to.d_weight.push_back(0);
 264   to.d_cons_args_t.push_back(std::vector<Type>());
 265   to.d_cons_args_t.back().push_back(
 266       sygus_norm->normalizeSygusRec(to.d_tn, dt, d_elem_pos).toType());
 267 }
 268
 269 std::map<TypeNode, Node> SygusGrammarNorm::d_tn_to_id = {};
 270
 271 /* Traverse the constructors of dt according to the positions in op_pos. Collect
 272  * those that fit the kinds established by to_collect. Remove collected operator
 273  * positions from op_pos. Accumulate collected positions in collected
 274  *
 275  * returns true if collected anything
 276  */
 277 std::unique_ptr<SygusGrammarNorm::Transf> SygusGrammarNorm::inferTransf(
 278     TypeNode tn, const Datatype& dt, const std::vector<unsigned>& op_pos)
 279 {
 280   NodeManager* nm = NodeManager::currentNM();
 281   TypeNode sygus_tn = TypeNode::fromType(dt.getSygusType());
 282   Trace("sygus-gnorm") << "Infer transf for " << dt.getName() << "..."
 283                        << std::endl;
 284   Trace("sygus-gnorm") << "  #cons = " << op_pos.size() << " / "
 285                        << dt.getNumConstructors() << std::endl;
 286   // look for redundant constructors to drop
 287   if (options::sygusMinGrammar() && dt.getNumConstructors() == op_pos.size())
 288   {
 289     SygusRedundantCons src;
 290     src.initialize(d_qe, tn);
 291     std::vector<unsigned> rindices;
 292     src.getRedundant(rindices);
 293     if (!rindices.empty())
 294     {
 295       Trace("sygus-gnorm") << "...drop transf, " << rindices.size() << "/"
 296                            << op_pos.size() << " constructors." << std::endl;
 297       Assert(rindices.size() < op_pos.size());
 298       return std::unique_ptr<Transf>(new TransfDrop(rindices));
 299     }
 300   }
 301
 302   // if normalization option is not enabled, we do not infer the transformations
 303   // below
 304   if (!options::sygusGrammarNorm())
 305   {
 306     return nullptr;
 307   }
 308
 309   /* TODO #1304: step 1: look for singleton */
 310   /* step 2: look for chain */
 311   unsigned chain_op_pos = dt.getNumConstructors();
 312   std::vector<unsigned> elem_pos;
 313   for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
 314   {
 315     Assert(op_pos[i] < dt.getNumConstructors());
 316     Expr sop = dt[op_pos[i]].getSygusOp();
 317     /* Collects a chainable operator such as PLUS */
 318     if (sop.getKind() == BUILTIN
 319         && TransfChain::isChainable(sygus_tn, Node::fromExpr(sop)))
 320     {
 321       Assert(nm->operatorToKind(Node::fromExpr(sop)) == PLUS);
 322       /* TODO #1304: be robust for this case */
 323       /* For now only transforms applications whose arguments have the same type
 324        * as the root */
 325       bool same_type_plus = true;
 326       for (const DatatypeConstructorArg& arg : dt[op_pos[i]])
 327       {
 328         if (TypeNode::fromType(
 329                 static_cast<SelectorType>(arg.getType()).getRangeType())
 330             != tn)
 331         {
 332           same_type_plus = false;
 333           break;
 334         }
 335       }
 336       if (!same_type_plus)
 337       {
 338         Trace("sygus-grammar-normalize-infer")
 339             << "\tFor OP " << PLUS << " did not collecting sop " << sop
 340             << " in position " << op_pos[i] << "\n";
 341         continue;
 342       }
 343       Assert(chain_op_pos == dt.getNumConstructors());
 344       Trace("sygus-grammar-normalize-infer")
 345           << "\tCollecting chainable OP " << sop << " in position " << op_pos[i]
 346           << "\n";
 347       chain_op_pos = op_pos[i];
 348       continue;
 349     }
 350     /* TODO #1304: check this for each operator */
 351     /* Collects elements that are not the identity (e.g. 0 is the id of PLUS) */
 352     if (!TransfChain::isId(sygus_tn, nm->operatorOf(PLUS), Node::fromExpr(sop)))
 353     {
 354       Trace("sygus-grammar-normalize-infer")
 355           << "\tCollecting for NON_ID_ELEMS the sop " << sop
 356           << " in position " << op_pos[i] << "\n";
 357       elem_pos.push_back(op_pos[i]);
 358     }
 359   }
 360   /* Typenode admits a chain transformation for normalization */
 361   if (chain_op_pos != dt.getNumConstructors() && !elem_pos.empty())
 362   {
 363     Trace("sygus-gnorm") << "...chain transf." << std::endl;
 364     Trace("sygus-grammar-normalize-infer")
 365         << "\tInfering chain transformation\n";
 366     return std::unique_ptr<Transf>(new TransfChain(chain_op_pos, elem_pos));
 367   }
 368   return nullptr;
 369 }
 370
 371 TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn,
 372                                              const Datatype& dt,
 373                                              std::vector<unsigned>& op_pos)
 374 {
 375   /* Corresponding type node to tn with the given operator positions. To be
 376    * retrieved (if cached) or defined (otherwise) */
 377   TypeNode unres_tn;
 378   if (Trace.isOn("sygus-grammar-normalize-trie"))
 379   {
 380     Trace("sygus-grammar-normalize-trie")
 381         << "\tRecursing on " << tn << " with op_positions ";
 382     for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
 383     {
 384       Trace("sygus-grammar-normalize-trie") << op_pos[i] << " ";
 385     }
 386     Trace("sygus-grammar-normalize-trie") << "\n";
 387   }
 388   /* Checks if unresolved type already created (and returns) or creates it
 389    * (and then proceeds to definition) */
 390   std::sort(op_pos.begin(), op_pos.end());
 391   if (d_tries[tn].getOrMakeType(tn, unres_tn, op_pos))
 392   {
 393     if (Trace.isOn("sygus-grammar-normalize-trie"))
 394     {
 395       Trace("sygus-grammar-normalize-trie")
 396           << "\tTypenode " << tn << " has already been normalized with op_pos ";
 397       for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
 398       {
 399         Trace("sygus-grammar-normalize-trie") << op_pos[i] << " ";
 400       }
 401       Trace("sygus-grammar-normalize-trie") << " with tn " << unres_tn << "\n";
 402     }
 403     return unres_tn;
 404   }
 405   if (Trace.isOn("sygus-grammar-normalize-trie"))
 406   {
 407     Trace("sygus-grammar-normalize-trie")
 408         << "\tTypenode " << tn << " not yet normalized with op_pos ";
 409     for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
 410     {
 411       Trace("sygus-grammar-normalize-trie") << op_pos[i] << " ";
 412     }
 413     Trace("sygus-grammar-normalize-trie") << "\n";
 414   }
 415   /* Creates type object for normalization */
 416   TypeObject to(tn, unres_tn);
 417
 418   /* Determine normalization transformation based on sygus type and given
 419     * operators */
 420   std::unique_ptr<Transf> transformation = inferTransf(tn, dt, op_pos);
 421   /* If a transformation was selected, apply it */
 422   if (transformation != nullptr)
 423   {
 424     transformation->buildType(this, to, dt, op_pos);
 425   }
 426
 427   /* Remaining operators are rebuilt as they are */
 428   for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
 429   {
 430     Assert(op_pos[i] < dt.getNumConstructors());
 431     to.addConsInfo(this, dt[op_pos[i]]);
 432   }
 433   /* Build normalize datatype */
 434   if (Trace.isOn("sygus-grammar-normalize"))
 435   {
 436     Trace("sygus-grammar-normalize") << "\nFor positions ";
 437     for (unsigned i = 0, size = op_pos.size(); i < size; ++i)
 438     {
 439       Trace("sygus-grammar-normalize") << op_pos[i] << " ";
 440     }
 441     Trace("sygus-grammar-normalize") << " and datatype " << dt << " \n";
 442   }
 443   to.buildDatatype(this, dt);
 444   return to.d_unres_tn;
 445 }
 446
 447 TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn)
 448 {
 449   /* Collect all operators for normalization */
 450   const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
 451   std::vector<unsigned> op_pos(dt.getNumConstructors());
 452   std::iota(op_pos.begin(), op_pos.end(), 0);
 453   return normalizeSygusRec(tn, dt, op_pos);
 454 }
 455
 456 TypeNode SygusGrammarNorm::normalizeSygusType(TypeNode tn, Node sygus_vars)
 457 {
 458   /* Normalize all types in tn */
 459   d_sygus_vars = sygus_vars;
 460   normalizeSygusRec(tn);
 461   /* Resolve created types */
 462   Assert(!d_dt_all.empty() && !d_unres_t_all.empty());
 463   if (Trace.isOn("sygus-grammar-normalize-build"))
 464   {
 465     Trace("sygus-grammar-normalize-build")
 466         << "making mutual datatyes with datatypes \n";
 467     for (unsigned i = 0, size = d_dt_all.size(); i < size; ++i)
 468     {
 469       Trace("sygus-grammar-normalize-build") << d_dt_all[i];
 470     }
 471     Trace("sygus-grammar-normalize-build") << " and unresolved types\n";
 472     for (const Type& unres_t : d_unres_t_all)
 473     {
 474       Trace("sygus-grammar-normalize-build") << unres_t << " ";
 475     }
 476     Trace("sygus-grammar-normalize-build") << "\n";
 477   }
 478   Assert(d_dt_all.size() == d_unres_t_all.size());
 479   std::vector<DatatypeType> types =
 480       NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(
 481           d_dt_all, d_unres_t_all);
 482   Assert(types.size() == d_dt_all.size());
 483   /* Clear accumulators */
 484   d_dt_all.clear();
 485   d_unres_t_all.clear();
 486   /* By construction the normalized type node will be the last one considered */
 487   return TypeNode::fromType(types.back());
 488 }
 489
 490 }  // namespace quantifiers
 491 }  // namespace theory
 492 }  // namespace CVC4