src/theory/datatypes/theory_datatypes_utils.cpp

   1 /*********************                                                        */
   2 /*! \file theory_datatypes_utils.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, 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 rewriter for the theory of (co)inductive datatypes.
  13  **
  14  ** Implementation of rewriter for the theory of (co)inductive datatypes.
  15  **/
  16
  17 #include "theory/datatypes/theory_datatypes_utils.h"
  18
  19 #include "expr/dtype.h"
  20
  21 using namespace CVC4;
  22 using namespace CVC4::kind;
  23
  24 namespace CVC4 {
  25 namespace theory {
  26 namespace datatypes {
  27 namespace utils {
  28
  29 /** get instantiate cons */
  30 Node getInstCons(Node n, const DType& dt, int index)
  31 {
  32   Assert(index >= 0 && index < (int)dt.getNumConstructors());
  33   std::vector<Node> children;
  34   NodeManager* nm = NodeManager::currentNM();
  35   children.push_back(dt[index].getConstructor());
  36   TypeNode tn = n.getType();
  37   for (unsigned i = 0, nargs = dt[index].getNumArgs(); i < nargs; i++)
  38   {
  39     Node nc = nm->mkNode(
  40         APPLY_SELECTOR_TOTAL, dt[index].getSelectorInternal(tn, i), n);
  41     children.push_back(nc);
  42   }
  43   Node n_ic = nm->mkNode(APPLY_CONSTRUCTOR, children);
  44   if (dt.isParametric())
  45   {
  46     // add type ascription for ambiguous constructor types
  47     if (!n_ic.getType().isComparableTo(tn))
  48     {
  49       Debug("datatypes-parametric")
  50           << "DtInstantiate: ambiguous type for " << n_ic << ", ascribe to "
  51           << n.getType() << std::endl;
  52       Debug("datatypes-parametric")
  53           << "Constructor is " << dt[index] << std::endl;
  54       TypeNode tspec = dt[index].getSpecializedConstructorType(n.getType());
  55       Debug("datatypes-parametric")
  56           << "Type specification is " << tspec << std::endl;
  57       children[0] = nm->mkNode(APPLY_TYPE_ASCRIPTION,
  58                                nm->mkConst(AscriptionType(tspec)),
  59                                children[0]);
  60       n_ic = nm->mkNode(APPLY_CONSTRUCTOR, children);
  61       Assert(n_ic.getType() == tn);
  62     }
  63   }
  64   Assert(isInstCons(n, n_ic, dt) == index);
  65   // n_ic = Rewriter::rewrite( n_ic );
  66   return n_ic;
  67 }
  68
  69 int isInstCons(Node t, Node n, const DType& dt)
  70 {
  71   if (n.getKind() == APPLY_CONSTRUCTOR)
  72   {
  73     int index = indexOf(n.getOperator());
  74     const DTypeConstructor& c = dt[index];
  75     TypeNode tn = n.getType();
  76     for (unsigned i = 0, size = n.getNumChildren(); i < size; i++)
  77     {
  78       if (n[i].getKind() != APPLY_SELECTOR_TOTAL
  79           || n[i].getOperator() != c.getSelectorInternal(tn, i) || n[i][0] != t)
  80       {
  81         return -1;
  82       }
  83     }
  84     return index;
  85   }
  86   return -1;
  87 }
  88
  89 int isTester(Node n, Node& a)
  90 {
  91   if (n.getKind() == APPLY_TESTER)
  92   {
  93     a = n[0];
  94     return indexOf(n.getOperator());
  95   }
  96   return -1;
  97 }
  98
  99 int isTester(Node n)
 100 {
 101   if (n.getKind() == APPLY_TESTER)
 102   {
 103     return indexOf(n.getOperator());
 104   }
 105   return -1;
 106 }
 107
 108 size_t indexOf(Node n) { return DType::indexOf(n); }
 109
 110 size_t cindexOf(Node n) { return DType::cindexOf(n); }
 111
 112 const DType& datatypeOf(Node n)
 113 {
 114   TypeNode t = n.getType();
 115   switch (t.getKind())
 116   {
 117     case CONSTRUCTOR_TYPE: return t[t.getNumChildren() - 1].getDType();
 118     case SELECTOR_TYPE:
 119     case TESTER_TYPE: return t[0].getDType();
 120     default:
 121       Unhandled() << "arg must be a datatype constructor, selector, or tester";
 122   }
 123 }
 124
 125 Node mkTester(Node n, int i, const DType& dt)
 126 {
 127   return NodeManager::currentNM()->mkNode(APPLY_TESTER, dt[i].getTester(), n);
 128 }
 129
 130 Node mkSplit(Node n, const DType& dt)
 131 {
 132   std::vector<Node> splits;
 133   for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
 134   {
 135     Node test = mkTester(n, i, dt);
 136     splits.push_back(test);
 137   }
 138   NodeManager* nm = NodeManager::currentNM();
 139   return splits.size() == 1 ? splits[0] : nm->mkNode(OR, splits);
 140 }
 141
 142 bool isNullaryApplyConstructor(Node n)
 143 {
 144   Assert(n.getKind() == APPLY_CONSTRUCTOR);
 145   for (const Node& nc : n)
 146   {
 147     if (nc.getType().isDatatype())
 148     {
 149       return false;
 150     }
 151   }
 152   return true;
 153 }
 154
 155 bool isNullaryConstructor(const DTypeConstructor& c)
 156 {
 157   for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++)
 158   {
 159     if (c[j].getType().getRangeType().isDatatype())
 160     {
 161       return false;
 162     }
 163   }
 164   return true;
 165 }
 166
 167 bool checkClash(Node n1, Node n2, std::vector<Node>& rew)
 168 {
 169   Trace("datatypes-rewrite-debug")
 170       << "Check clash : " << n1 << " " << n2 << std::endl;
 171   if (n1.getKind() == APPLY_CONSTRUCTOR && n2.getKind() == APPLY_CONSTRUCTOR)
 172   {
 173     if (n1.getOperator() != n2.getOperator())
 174     {
 175       Trace("datatypes-rewrite-debug")
 176           << "Clash operators : " << n1 << " " << n2 << " " << n1.getOperator()
 177           << " " << n2.getOperator() << std::endl;
 178       return true;
 179     }
 180     Assert(n1.getNumChildren() == n2.getNumChildren());
 181     for (unsigned i = 0, size = n1.getNumChildren(); i < size; i++)
 182     {
 183       if (checkClash(n1[i], n2[i], rew))
 184       {
 185         return true;
 186       }
 187     }
 188   }
 189   else if (n1 != n2)
 190   {
 191     if (n1.isConst() && n2.isConst())
 192     {
 193       Trace("datatypes-rewrite-debug")
 194           << "Clash constants : " << n1 << " " << n2 << std::endl;
 195       return true;
 196     }
 197     else
 198     {
 199       Node eq = NodeManager::currentNM()->mkNode(EQUAL, n1, n2);
 200       rew.push_back(eq);
 201     }
 202   }
 203   return false;
 204 }
 205
 206 }  // namespace utils
 207 }  // namespace datatypes
 208 }  // namespace theory
 209 }  // namespace CVC4