src/theory/quantifiers/dynamic_rewrite.cpp

   1 /*********************                                                        */
   2 /*! \file dynamic_rewrite.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Andres Noetzli
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2018 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 dynamic_rewriter
  13  **/
  14
  15 #include "theory/quantifiers/dynamic_rewrite.h"
  16
  17 #include "theory/rewriter.h"
  18
  19 using namespace std;
  20 using namespace CVC4::kind;
  21
  22 namespace CVC4 {
  23 namespace theory {
  24 namespace quantifiers {
  25
  26 DynamicRewriter::DynamicRewriter(const std::string& name,
  27                                  context::UserContext* u)
  28     : d_equalityEngine(u, "DynamicRewriter::" + name, true), d_rewrites(u)
  29 {
  30   d_equalityEngine.addFunctionKind(kind::APPLY_UF);
  31 }
  32
  33 void DynamicRewriter::addRewrite(Node a, Node b)
  34 {
  35   Trace("dyn-rewrite") << "Dyn-Rewriter : " << a << " == " << b << std::endl;
  36   if (a == b)
  37   {
  38     Trace("dyn-rewrite") << "...equal." << std::endl;
  39     return;
  40   }
  41
  42   // add to the equality engine
  43   Node ai = toInternal(a);
  44   Node bi = toInternal(b);
  45   if (ai.isNull() || bi.isNull())
  46   {
  47     Trace("dyn-rewrite") << "...not internalizable." << std::endl;
  48     return;
  49   }
  50   Trace("dyn-rewrite-debug") << "Internal : " << ai << " " << bi << std::endl;
  51
  52   Trace("dyn-rewrite-debug") << "assert eq..." << std::endl;
  53   Node eq = ai.eqNode(bi);
  54   d_rewrites.push_back(eq);
  55   d_equalityEngine.assertEquality(eq, true, eq);
  56   Assert(d_equalityEngine.consistent());
  57   Trace("dyn-rewrite-debug") << "Finished" << std::endl;
  58 }
  59
  60 bool DynamicRewriter::areEqual(Node a, Node b)
  61 {
  62   if (a == b)
  63   {
  64     return true;
  65   }
  66   Trace("dyn-rewrite-debug") << "areEqual? : " << a << " " << b << std::endl;
  67   // add to the equality engine
  68   Node ai = toInternal(a);
  69   Node bi = toInternal(b);
  70   if (ai.isNull() || bi.isNull())
  71   {
  72     Trace("dyn-rewrite") << "...not internalizable." << std::endl;
  73     return false;
  74   }
  75   Trace("dyn-rewrite-debug") << "internal : " << ai << " " << bi << std::endl;
  76   d_equalityEngine.addTerm(ai);
  77   d_equalityEngine.addTerm(bi);
  78   Trace("dyn-rewrite-debug") << "...added terms" << std::endl;
  79   return d_equalityEngine.areEqual(ai, bi);
  80 }
  81
  82 Node DynamicRewriter::toInternal(Node a)
  83 {
  84   std::map<Node, Node>::iterator it = d_term_to_internal.find(a);
  85   if (it != d_term_to_internal.end())
  86   {
  87     return it->second;
  88   }
  89   Node ret = a;
  90
  91   if (!a.isVar())
  92   {
  93     std::vector<Node> children;
  94     if (a.hasOperator())
  95     {
  96       Node op = a.getOperator();
  97       if (a.getKind() != APPLY_UF)
  98       {
  99         op = d_ois_trie[op].getSymbol(a);
 100         // if this term involves an argument that is not of first class type,
 101         // we cannot reason about it. This includes operators like str.in-re.
 102         if (op.isNull())
 103         {
 104           return Node::null();
 105         }
 106       }
 107       children.push_back(op);
 108     }
 109     for (const Node& ca : a)
 110     {
 111       Node cai = toInternal(ca);
 112       if (cai.isNull())
 113       {
 114         return Node::null();
 115       }
 116       children.push_back(cai);
 117     }
 118     if (!children.empty())
 119     {
 120       if (children.size() == 1)
 121       {
 122         ret = children[0];
 123       }
 124       else
 125       {
 126         ret = NodeManager::currentNM()->mkNode(APPLY_UF, children);
 127       }
 128     }
 129   }
 130   d_term_to_internal[a] = ret;
 131   d_internal_to_term[ret] = a;
 132   return ret;
 133 }
 134
 135 Node DynamicRewriter::toExternal(Node ai)
 136 {
 137   std::map<Node, Node>::iterator it = d_internal_to_term.find(ai);
 138   if (it != d_internal_to_term.end())
 139   {
 140     return it->second;
 141   }
 142   return Node::null();
 143 }
 144
 145 Node DynamicRewriter::OpInternalSymTrie::getSymbol(Node n)
 146 {
 147   std::vector<TypeNode> ctypes;
 148   for (const Node& cn : n)
 149   {
 150     ctypes.push_back(cn.getType());
 151   }
 152   ctypes.push_back(n.getType());
 153
 154   OpInternalSymTrie* curr = this;
 155   for (unsigned i = 0, size = ctypes.size(); i < size; i++)
 156   {
 157     // cannot handle certain types (e.g. regular expressions or functions)
 158     if (!ctypes[i].isFirstClass())
 159     {
 160       return Node::null();
 161     }
 162     curr = &(curr->d_children[ctypes[i]]);
 163   }
 164   if (!curr->d_sym.isNull())
 165   {
 166     return curr->d_sym;
 167   }
 168   // make UF operator
 169   TypeNode utype;
 170   if (ctypes.size() == 1)
 171   {
 172     utype = ctypes[0];
 173   }
 174   else
 175   {
 176     utype = NodeManager::currentNM()->mkFunctionType(ctypes);
 177   }
 178   Node f = NodeManager::currentNM()->mkSkolem(
 179       "ufd", utype, "internal op for dynamic_rewriter");
 180   curr->d_sym = f;
 181   return f;
 182 }
 183
 184 } /* CVC4::theory::quantifiers namespace */
 185 } /* CVC4::theory namespace */
 186 } /* CVC4 namespace */