src/expr/skolem_manager.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 skolem manager class.
  14  */
  15
  16 #include "expr/skolem_manager.h"
  17
  18 #include <sstream>
  19
  20 #include "expr/attribute.h"
  21 #include "expr/bound_var_manager.h"
  22 #include "expr/node_algorithm.h"
  23
  24 using namespace cvc5::kind;
  25
  26 namespace cvc5 {
  27
  28 // Attributes are global maps from Nodes to data. Thus, note that these could
  29 // be implemented as internal maps in SkolemManager.
  30 struct WitnessFormAttributeId
  31 {
  32 };
  33 typedef expr::Attribute<WitnessFormAttributeId, Node> WitnessFormAttribute;
  34
  35 struct SkolemFormAttributeId
  36 {
  37 };
  38 typedef expr::Attribute<SkolemFormAttributeId, Node> SkolemFormAttribute;
  39
  40 struct OriginalFormAttributeId
  41 {
  42 };
  43 typedef expr::Attribute<OriginalFormAttributeId, Node> OriginalFormAttribute;
  44
  45 const char* toString(SkolemFunId id)
  46 {
  47   switch (id)
  48   {
  49     case SkolemFunId::DIV_BY_ZERO: return "DIV_BY_ZERO";
  50     case SkolemFunId::INT_DIV_BY_ZERO: return "INT_DIV_BY_ZERO";
  51     case SkolemFunId::MOD_BY_ZERO: return "MOD_BY_ZERO";
  52     case SkolemFunId::SQRT: return "SQRT";
  53     case SkolemFunId::SELECTOR_WRONG: return "SELECTOR_WRONG";
  54     case SkolemFunId::SHARED_SELECTOR: return "SHARED_SELECTOR";
  55     case SkolemFunId::SEQ_NTH_OOB: return "SEQ_NTH_OOB";
  56     case SkolemFunId::RE_UNFOLD_POS_COMPONENT: return "RE_UNFOLD_POS_COMPONENT";
  57     default: return "?";
  58   }
  59 }
  60
  61 std::ostream& operator<<(std::ostream& out, SkolemFunId id)
  62 {
  63   out << toString(id);
  64   return out;
  65 }
  66
  67 Node SkolemManager::mkSkolem(Node v,
  68                              Node pred,
  69                              const std::string& prefix,
  70                              const std::string& comment,
  71                              int flags,
  72                              ProofGenerator* pg)
  73 {
  74   // We do not currently insist that pred does not contain witness terms
  75   Assert(v.getKind() == BOUND_VARIABLE);
  76   // make the witness term
  77   NodeManager* nm = NodeManager::currentNM();
  78   Node bvl = nm->mkNode(BOUND_VAR_LIST, v);
  79   // Make the witness term, where notice that pred may contain skolems. We do
  80   // not recursively convert pred to witness form, since witness terms should
  81   // be treated as opaque. Moreover, the use of witness forms leads to
  82   // variable shadowing issues in e.g. skolemization.
  83   Node w = nm->mkNode(WITNESS, bvl, pred);
  84   // store the mapping to proof generator if it exists
  85   if (pg != nullptr)
  86   {
  87     // We cache based on the existential of the original predicate
  88     Node q = nm->mkNode(EXISTS, bvl, pred);
  89     // Notice this may overwrite an existing proof generator. This does not
  90     // matter since either should be able to prove q.
  91     d_gens[q] = pg;
  92   }
  93   Node k = mkSkolemInternal(w, prefix, comment, flags);
  94   // set witness form attribute for k
  95   WitnessFormAttribute wfa;
  96   k.setAttribute(wfa, w);
  97   Trace("sk-manager-skolem")
  98       << "skolem: " << k << " witness " << w << std::endl;
  99   return k;
 100 }
 101
 102 Node SkolemManager::mkSkolemize(Node q,
 103                                 std::vector<Node>& skolems,
 104                                 const std::string& prefix,
 105                                 const std::string& comment,
 106                                 int flags,
 107                                 ProofGenerator* pg)
 108 {
 109   Trace("sk-manager-debug") << "mkSkolemize " << q << std::endl;
 110   Assert(q.getKind() == EXISTS);
 111   Node currQ = q;
 112   for (const Node& av : q[0])
 113   {
 114     Assert(currQ.getKind() == EXISTS && av == currQ[0][0]);
 115     // currQ is updated to the result of skolemizing its first variable in
 116     // the method below.
 117     Node sk = skolemize(currQ, currQ, prefix, comment, flags);
 118     Trace("sk-manager-debug")
 119         << "made skolem " << sk << " for " << av << std::endl;
 120     skolems.push_back(sk);
 121   }
 122   if (pg != nullptr)
 123   {
 124     // Same as above, this may overwrite an existing proof generator
 125     d_gens[q] = pg;
 126   }
 127   Trace("sk-manager-debug") << "...mkSkolemize returns " << currQ << std::endl;
 128   return currQ;
 129 }
 130
 131 Node SkolemManager::skolemize(Node q,
 132                               Node& qskolem,
 133                               const std::string& prefix,
 134                               const std::string& comment,
 135                               int flags)
 136 {
 137   Assert(q.getKind() == EXISTS);
 138   Node v;
 139   std::vector<Node> ovars;
 140   Trace("sk-manager-debug") << "mkSkolemize..." << std::endl;
 141   NodeManager* nm = NodeManager::currentNM();
 142   for (const Node& av : q[0])
 143   {
 144     if (v.isNull())
 145     {
 146       v = av;
 147       continue;
 148     }
 149     ovars.push_back(av);
 150   }
 151   Assert(!v.isNull());
 152   // make the predicate with one variable stripped off
 153   Node pred = q[1];
 154   Trace("sk-manager-debug") << "make exists predicate" << std::endl;
 155   if (!ovars.empty())
 156   {
 157     // keeps the same variables
 158     Node bvl = nm->mkNode(BOUND_VAR_LIST, ovars);
 159     // update the predicate
 160     pred = nm->mkNode(EXISTS, bvl, pred);
 161   }
 162   Trace("sk-manager-debug") << "call sub mkSkolem" << std::endl;
 163   // don't use a proof generator, since this may be an intermediate, partially
 164   // skolemized formula.
 165   Node k = mkSkolem(v, pred, prefix, comment, flags, nullptr);
 166   Assert(k.getType() == v.getType());
 167   TNode tv = v;
 168   TNode tk = k;
 169   Trace("sk-manager-debug")
 170       << "qskolem apply " << tv << " -> " << tk << " to " << pred << std::endl;
 171   // the quantified formula with one step of skolemization
 172   qskolem = pred.substitute(tv, tk);
 173   Trace("sk-manager-debug") << "qskolem done substitution" << std::endl;
 174   return k;
 175 }
 176
 177 Node SkolemManager::mkPurifySkolem(Node t,
 178                                    const std::string& prefix,
 179                                    const std::string& comment,
 180                                    int flags)
 181 {
 182   Node to = getOriginalForm(t);
 183   // We do not currently insist that to does not contain witness terms
 184
 185   Node k = mkSkolemInternal(to, prefix, comment, flags);
 186   // set original form attribute for k
 187   OriginalFormAttribute ofa;
 188   k.setAttribute(ofa, to);
 189
 190   Trace("sk-manager-skolem")
 191       << "skolem: " << k << " purify " << to << std::endl;
 192   return k;
 193 }
 194
 195 Node SkolemManager::mkSkolemFunction(SkolemFunId id,
 196                                      TypeNode tn,
 197                                      Node cacheVal,
 198                                      int flags)
 199 {
 200   std::tuple<SkolemFunId, TypeNode, Node> key(id, tn, cacheVal);
 201   std::map<std::tuple<SkolemFunId, TypeNode, Node>, Node>::iterator it =
 202       d_skolemFuns.find(key);
 203   if (it == d_skolemFuns.end())
 204   {
 205     NodeManager* nm = NodeManager::currentNM();
 206     std::stringstream ss;
 207     ss << "SKOLEM_FUN_" << id;
 208     Node k = nm->mkSkolem(ss.str(), tn, "an internal skolem function", flags);
 209     d_skolemFuns[key] = k;
 210     d_skolemFunMap[k] = key;
 211     return k;
 212   }
 213   return it->second;
 214 }
 215
 216 Node SkolemManager::mkSkolemFunction(SkolemFunId id,
 217                                      TypeNode tn,
 218                                      const std::vector<Node>& cacheVals,
 219                                      int flags)
 220 {
 221   Assert(cacheVals.size() > 1);
 222   Node cacheVal = NodeManager::currentNM()->mkNode(SEXPR, cacheVals);
 223   return mkSkolemFunction(id, tn, cacheVal, flags);
 224 }
 225
 226 bool SkolemManager::isSkolemFunction(Node k,
 227                                      SkolemFunId& id,
 228                                      Node& cacheVal) const
 229 {
 230   std::map<Node, std::tuple<SkolemFunId, TypeNode, Node>>::const_iterator it =
 231       d_skolemFunMap.find(k);
 232   if (it == d_skolemFunMap.end())
 233   {
 234     return false;
 235   }
 236   id = std::get<0>(it->second);
 237   cacheVal = std::get<2>(it->second);
 238   return true;
 239 }
 240
 241 Node SkolemManager::mkDummySkolem(const std::string& prefix,
 242                                   const TypeNode& type,
 243                                   const std::string& comment,
 244                                   int flags)
 245 {
 246   return NodeManager::currentNM()->mkSkolem(prefix, type, comment, flags);
 247 }
 248
 249 ProofGenerator* SkolemManager::getProofGenerator(Node t) const
 250 {
 251   std::map<Node, ProofGenerator*>::const_iterator it = d_gens.find(t);
 252   if (it != d_gens.end())
 253   {
 254     return it->second;
 255   }
 256   return nullptr;
 257 }
 258
 259 Node SkolemManager::getWitnessForm(Node k)
 260 {
 261   Assert(k.getKind() == SKOLEM);
 262   // simply look up the witness form for k via an attribute
 263   WitnessFormAttribute wfa;
 264   return k.getAttribute(wfa);
 265 }
 266
 267 Node SkolemManager::getOriginalForm(Node n)
 268 {
 269   if (n.isNull())
 270   {
 271     return n;
 272   }
 273   Trace("sk-manager-debug")
 274       << "SkolemManager::getOriginalForm " << n << std::endl;
 275   OriginalFormAttribute ofa;
 276   NodeManager* nm = NodeManager::currentNM();
 277   std::unordered_map<TNode, Node> visited;
 278   std::unordered_map<TNode, Node>::iterator it;
 279   std::vector<TNode> visit;
 280   TNode cur;
 281   visit.push_back(n);
 282   do
 283   {
 284     cur = visit.back();
 285     visit.pop_back();
 286     it = visited.find(cur);
 287
 288     if (it == visited.end())
 289     {
 290       if (cur.hasAttribute(ofa))
 291       {
 292         visited[cur] = cur.getAttribute(ofa);
 293       }
 294       else
 295       {
 296         visited[cur] = Node::null();
 297         visit.push_back(cur);
 298         if (cur.getMetaKind() == metakind::PARAMETERIZED)
 299         {
 300           visit.push_back(cur.getOperator());
 301         }
 302         for (const Node& cn : cur)
 303         {
 304           visit.push_back(cn);
 305         }
 306       }
 307     }
 308     else if (it->second.isNull())
 309     {
 310       Node ret = cur;
 311       bool childChanged = false;
 312       std::vector<Node> children;
 313       if (cur.getMetaKind() == metakind::PARAMETERIZED)
 314       {
 315         it = visited.find(cur.getOperator());
 316         Assert(it != visited.end());
 317         Assert(!it->second.isNull());
 318         childChanged = childChanged || cur.getOperator() != it->second;
 319         children.push_back(it->second);
 320       }
 321       for (const Node& cn : cur)
 322       {
 323         it = visited.find(cn);
 324         Assert(it != visited.end());
 325         Assert(!it->second.isNull());
 326         childChanged = childChanged || cn != it->second;
 327         children.push_back(it->second);
 328       }
 329       if (childChanged)
 330       {
 331         ret = nm->mkNode(cur.getKind(), children);
 332       }
 333       cur.setAttribute(ofa, ret);
 334       visited[cur] = ret;
 335     }
 336   } while (!visit.empty());
 337   Assert(visited.find(n) != visited.end());
 338   Assert(!visited.find(n)->second.isNull());
 339   Trace("sk-manager-debug") << "..return " << visited[n] << std::endl;
 340   return visited[n];
 341 }
 342
 343 Node SkolemManager::mkSkolemInternal(Node w,
 344                                      const std::string& prefix,
 345                                      const std::string& comment,
 346                                      int flags)
 347 {
 348   // note that witness, original forms are independent, but share skolems
 349   NodeManager* nm = NodeManager::currentNM();
 350   // w is not necessarily a witness term
 351   SkolemFormAttribute sfa;
 352   Node k;
 353   // could already have a skolem if we used w already
 354   if (w.hasAttribute(sfa))
 355   {
 356     return w.getAttribute(sfa);
 357   }
 358   // make the new skolem
 359   if (flags & NodeManager::SKOLEM_BOOL_TERM_VAR)
 360   {
 361     Assert (w.getType().isBoolean());
 362     k = nm->mkBooleanTermVariable();
 363   }
 364   else
 365   {
 366     k = nm->mkSkolem(prefix, w.getType(), comment, flags);
 367   }
 368   // set skolem form attribute for w
 369   w.setAttribute(sfa, k);
 370   Trace("sk-manager") << "SkolemManager::mkSkolem: " << k << " : " << w
 371                       << std::endl;
 372   return k;
 373 }
 374
 375 }  // namespace cvc5