src/expr/term_canonize.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Aina Niemetz
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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.
  11  * ****************************************************************************
  12  *
  13  * Implementation of term canonize.
  14  */
  15
  16 #include "expr/term_canonize.h"
  17
  18 #include <sstream>
  19
  20 // TODO #1216: move the code in this include
  21 #include "theory/quantifiers/term_util.h"
  22
  23 using namespace cvc5::kind;
  24
  25 namespace cvc5 {
  26 namespace expr {
  27
  28 TermCanonize::TermCanonize(TypeClassCallback* tcc)
  29     : d_tcc(tcc), d_op_id_count(0), d_typ_id_count(0)
  30 {
  31 }
  32
  33 int TermCanonize::getIdForOperator(Node op)
  34 {
  35   std::map<Node, int>::iterator it = d_op_id.find(op);
  36   if (it == d_op_id.end())
  37   {
  38     d_op_id[op] = d_op_id_count;
  39     d_op_id_count++;
  40     return d_op_id[op];
  41   }
  42   return it->second;
  43 }
  44
  45 int TermCanonize::getIdForType(TypeNode t)
  46 {
  47   std::map<TypeNode, int>::iterator it = d_typ_id.find(t);
  48   if (it == d_typ_id.end())
  49   {
  50     d_typ_id[t] = d_typ_id_count;
  51     d_typ_id_count++;
  52     return d_typ_id[t];
  53   }
  54   return it->second;
  55 }
  56
  57 bool TermCanonize::getTermOrder(Node a, Node b)
  58 {
  59   if (a.getKind() == BOUND_VARIABLE)
  60   {
  61     if (b.getKind() == BOUND_VARIABLE)
  62     {
  63       return getIndexForFreeVariable(a) < getIndexForFreeVariable(b);
  64     }
  65     return true;
  66   }
  67   if (b.getKind() != BOUND_VARIABLE)
  68   {
  69     Node aop = a.hasOperator() ? a.getOperator() : a;
  70     Node bop = b.hasOperator() ? b.getOperator() : b;
  71     Trace("aeq-debug2") << a << "...op..." << aop << std::endl;
  72     Trace("aeq-debug2") << b << "...op..." << bop << std::endl;
  73     if (aop == bop)
  74     {
  75       if (a.getNumChildren() == b.getNumChildren())
  76       {
  77         for (unsigned i = 0, size = a.getNumChildren(); i < size; i++)
  78         {
  79           if (a[i] != b[i])
  80           {
  81             // first distinct child determines the ordering
  82             return getTermOrder(a[i], b[i]);
  83           }
  84         }
  85       }
  86       else
  87       {
  88         return aop.getNumChildren() < bop.getNumChildren();
  89       }
  90     }
  91     else
  92     {
  93       return getIdForOperator(aop) < getIdForOperator(bop);
  94     }
  95   }
  96   return false;
  97 }
  98
  99 Node TermCanonize::getCanonicalFreeVar(TypeNode tn, unsigned i, uint32_t tc)
 100 {
 101   Assert(!tn.isNull());
 102   NodeManager* nm = NodeManager::currentNM();
 103   std::pair<TypeNode, uint32_t> key(tn, tc);
 104   std::vector<Node>& tvars = d_cn_free_var[key];
 105   while (tvars.size() <= i)
 106   {
 107     std::stringstream oss;
 108     oss << tn;
 109     std::string typ_name = oss.str();
 110     while (typ_name[0] == '(')
 111     {
 112       typ_name.erase(typ_name.begin());
 113     }
 114     std::stringstream os;
 115     os << typ_name[0] << i;
 116     Node x = nm->mkBoundVar(os.str().c_str(), tn);
 117     d_fvIndex[x] = tvars.size();
 118     tvars.push_back(x);
 119   }
 120   return tvars[i];
 121 }
 122
 123 uint32_t TermCanonize::getTypeClass(TNode v)
 124 {
 125   return d_tcc == nullptr ? 0 : d_tcc->getTypeClass(v);
 126 }
 127
 128 size_t TermCanonize::getIndexForFreeVariable(Node v) const
 129 {
 130   std::map<Node, size_t>::const_iterator it = d_fvIndex.find(v);
 131   if (it == d_fvIndex.end())
 132   {
 133     return 0;
 134   }
 135   return it->second;
 136 }
 137
 138 struct sortTermOrder
 139 {
 140   TermCanonize* d_tu;
 141   bool operator()(Node i, Node j) { return d_tu->getTermOrder(i, j); }
 142 };
 143
 144 Node TermCanonize::getCanonicalTerm(
 145     TNode n,
 146     bool apply_torder,
 147     bool doHoVar,
 148     std::map<std::pair<TypeNode, uint32_t>, unsigned>& var_count,
 149     std::map<TNode, Node>& visited)
 150 {
 151   std::map<TNode, Node>::iterator it = visited.find(n);
 152   if (it != visited.end())
 153   {
 154     return it->second;
 155   }
 156
 157   Trace("canon-term-debug") << "Get canonical term for " << n << std::endl;
 158   if (n.getKind() == BOUND_VARIABLE)
 159   {
 160     uint32_t tc = getTypeClass(n);
 161     TypeNode tn = n.getType();
 162     std::pair<TypeNode, uint32_t> key(tn, tc);
 163     // allocate variable
 164     unsigned vn = var_count[key];
 165     var_count[key]++;
 166     Node fv = getCanonicalFreeVar(tn, vn, tc);
 167     visited[n] = fv;
 168     Trace("canon-term-debug") << "...allocate variable." << std::endl;
 169     return fv;
 170   }
 171   else if (n.getNumChildren() > 0)
 172   {
 173     // collect children
 174     Trace("canon-term-debug") << "Collect children" << std::endl;
 175     std::vector<Node> cchildren;
 176     for (const Node& cn : n)
 177     {
 178       cchildren.push_back(cn);
 179     }
 180     // if applicable, first sort by term order
 181     if (apply_torder && theory::quantifiers::TermUtil::isComm(n.getKind()))
 182     {
 183       Trace("canon-term-debug")
 184           << "Sort based on commutative operator " << n.getKind() << std::endl;
 185       sortTermOrder sto;
 186       sto.d_tu = this;
 187       std::sort(cchildren.begin(), cchildren.end(), sto);
 188     }
 189     // now make canonical
 190     Trace("canon-term-debug") << "Make canonical children" << std::endl;
 191     for (unsigned i = 0, size = cchildren.size(); i < size; i++)
 192     {
 193       cchildren[i] = getCanonicalTerm(
 194           cchildren[i], apply_torder, doHoVar, var_count, visited);
 195     }
 196     if (n.getMetaKind() == metakind::PARAMETERIZED)
 197     {
 198       Node op = n.getOperator();
 199       if (doHoVar)
 200       {
 201         op = getCanonicalTerm(op, apply_torder, doHoVar, var_count, visited);
 202       }
 203       Trace("canon-term-debug") << "Insert operator " << op << std::endl;
 204       cchildren.insert(cchildren.begin(), op);
 205     }
 206     Trace("canon-term-debug")
 207         << "...constructing for " << n << "." << std::endl;
 208     Node ret = NodeManager::currentNM()->mkNode(n.getKind(), cchildren);
 209     Trace("canon-term-debug")
 210         << "...constructed " << ret << " for " << n << "." << std::endl;
 211     visited[n] = ret;
 212     return ret;
 213   }
 214   Trace("canon-term-debug") << "...return 0-child term." << std::endl;
 215   return n;
 216 }
 217
 218 Node TermCanonize::getCanonicalTerm(TNode n, bool apply_torder, bool doHoVar)
 219 {
 220   std::map<std::pair<TypeNode, uint32_t>, unsigned> var_count;
 221   std::map<TNode, Node> visited;
 222   return getCanonicalTerm(n, apply_torder, doHoVar, var_count, visited);
 223 }
 224
 225 Node TermCanonize::getCanonicalTerm(TNode n,
 226                                     std::map<TNode, Node>& visited,
 227                                     bool apply_torder,
 228                                     bool doHoVar)
 229 {
 230   std::map<std::pair<TypeNode, uint32_t>, unsigned> var_count;
 231   return getCanonicalTerm(n, apply_torder, doHoVar, var_count, visited);
 232 }
 233
 234 }  // namespace expr
 235 }  // namespace cvc5