src/theory/uf/ho_extension.cpp

   1 /*********************                                                        */
   2 /*! \file ho_extension.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, 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 the higher-order extension of TheoryUF.
  13  **
  14  **/
  15
  16 #include "theory/uf/ho_extension.h"
  17
  18 #include "expr/node_algorithm.h"
  19 #include "options/uf_options.h"
  20 #include "theory/theory_model.h"
  21 #include "theory/uf/theory_uf_rewriter.h"
  22
  23 using namespace std;
  24 using namespace CVC4::kind;
  25
  26 namespace CVC4 {
  27 namespace theory {
  28 namespace uf {
  29
  30 HoExtension::HoExtension(TheoryState& state, TheoryInferenceManager& im)
  31     : d_state(state),
  32       d_im(im),
  33       d_extensionality(state.getUserContext()),
  34       d_uf_std_skolem(state.getUserContext())
  35 {
  36   d_true = NodeManager::currentNM()->mkConst(true);
  37 }
  38
  39 Node HoExtension::ppRewrite(Node node)
  40 {
  41   // convert HO_APPLY to APPLY_UF if fully applied
  42   if (node[0].getType().getNumChildren() == 2)
  43   {
  44     Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl;
  45     Node ret = getApplyUfForHoApply(node);
  46     Trace("uf-ho") << "uf-ho : ppRewrite : " << node << " to " << ret
  47                    << std::endl;
  48     return ret;
  49   }
  50   return node;
  51 }
  52
  53 Node HoExtension::getExtensionalityDeq(TNode deq, bool isCached)
  54 {
  55   Assert(deq.getKind() == NOT && deq[0].getKind() == EQUAL);
  56   Assert(deq[0][0].getType().isFunction());
  57   if (isCached)
  58   {
  59     std::map<Node, Node>::iterator it = d_extensionality_deq.find(deq);
  60     if (it != d_extensionality_deq.end())
  61     {
  62       return it->second;
  63     }
  64   }
  65   TypeNode tn = deq[0][0].getType();
  66   std::vector<TypeNode> argTypes = tn.getArgTypes();
  67   std::vector<Node> skolems;
  68   NodeManager* nm = NodeManager::currentNM();
  69   for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++)
  70   {
  71     Node k =
  72         nm->mkSkolem("k", argTypes[i], "skolem created for extensionality.");
  73     skolems.push_back(k);
  74   }
  75   Node t[2];
  76   for (unsigned i = 0; i < 2; i++)
  77   {
  78     std::vector<Node> children;
  79     Node curr = deq[0][i];
  80     while (curr.getKind() == HO_APPLY)
  81     {
  82       children.push_back(curr[1]);
  83       curr = curr[0];
  84     }
  85     children.push_back(curr);
  86     std::reverse(children.begin(), children.end());
  87     children.insert(children.end(), skolems.begin(), skolems.end());
  88     t[i] = nm->mkNode(APPLY_UF, children);
  89   }
  90   Node conc = t[0].eqNode(t[1]).negate();
  91   if (isCached)
  92   {
  93     d_extensionality_deq[deq] = conc;
  94   }
  95   return conc;
  96 }
  97
  98 unsigned HoExtension::applyExtensionality(TNode deq)
  99 {
 100   Assert(deq.getKind() == NOT && deq[0].getKind() == EQUAL);
 101   Assert(deq[0][0].getType().isFunction());
 102   // apply extensionality
 103   if (d_extensionality.find(deq) == d_extensionality.end())
 104   {
 105     d_extensionality.insert(deq);
 106     Node conc = getExtensionalityDeq(deq);
 107     Node lem = NodeManager::currentNM()->mkNode(OR, deq[0], conc);
 108     Trace("uf-ho-lemma") << "uf-ho-lemma : extensionality : " << lem
 109                          << std::endl;
 110     d_im.lemma(lem);
 111     return 1;
 112   }
 113   return 0;
 114 }
 115
 116 Node HoExtension::getApplyUfForHoApply(Node node)
 117 {
 118   Assert(node[0].getType().getNumChildren() == 2);
 119   std::vector<TNode> args;
 120   Node f = TheoryUfRewriter::decomposeHoApply(node, args, true);
 121   Node new_f = f;
 122   NodeManager* nm = NodeManager::currentNM();
 123   if (!TheoryUfRewriter::canUseAsApplyUfOperator(f))
 124   {
 125     NodeNodeMap::const_iterator itus = d_uf_std_skolem.find(f);
 126     if (itus == d_uf_std_skolem.end())
 127     {
 128       std::unordered_set<Node, NodeHashFunction> fvs;
 129       expr::getFreeVariables(f, fvs);
 130       Node lem;
 131       if (!fvs.empty())
 132       {
 133         std::vector<TypeNode> newTypes;
 134         std::vector<Node> vs;
 135         std::vector<Node> nvs;
 136         for (const Node& v : fvs)
 137         {
 138           TypeNode vt = v.getType();
 139           newTypes.push_back(vt);
 140           Node nv = nm->mkBoundVar(vt);
 141           vs.push_back(v);
 142           nvs.push_back(nv);
 143         }
 144         TypeNode ft = f.getType();
 145         std::vector<TypeNode> argTypes = ft.getArgTypes();
 146         TypeNode rangeType = ft.getRangeType();
 147
 148         newTypes.insert(newTypes.end(), argTypes.begin(), argTypes.end());
 149         TypeNode nft = nm->mkFunctionType(newTypes, rangeType);
 150         new_f = nm->mkSkolem("app_uf", nft);
 151         for (const Node& v : vs)
 152         {
 153           new_f = nm->mkNode(HO_APPLY, new_f, v);
 154         }
 155         Assert(new_f.getType() == f.getType());
 156         Node eq = new_f.eqNode(f);
 157         Node seq = eq.substitute(vs.begin(), vs.end(), nvs.begin(), nvs.end());
 158         lem = nm->mkNode(
 159             FORALL, nm->mkNode(BOUND_VAR_LIST, nvs), seq);
 160       }
 161       else
 162       {
 163         // introduce skolem to make a standard APPLY_UF
 164         new_f = nm->mkSkolem("app_uf", f.getType());
 165         lem = new_f.eqNode(f);
 166       }
 167       Trace("uf-ho-lemma")
 168           << "uf-ho-lemma : Skolem definition for apply-conversion : " << lem
 169           << std::endl;
 170       d_im.lemma(lem);
 171       d_uf_std_skolem[f] = new_f;
 172     }
 173     else
 174     {
 175       new_f = (*itus).second;
 176     }
 177     // unroll the HO_APPLY, adding to the first argument position
 178     // Note arguments in the vector args begin at position 1.
 179     while (new_f.getKind() == HO_APPLY)
 180     {
 181       args.insert(args.begin() + 1, new_f[1]);
 182       new_f = new_f[0];
 183     }
 184   }
 185   Assert(TheoryUfRewriter::canUseAsApplyUfOperator(new_f));
 186   args[0] = new_f;
 187   Node ret = nm->mkNode(APPLY_UF, args);
 188   Assert(ret.getType() == node.getType());
 189   return ret;
 190 }
 191
 192 unsigned HoExtension::checkExtensionality(TheoryModel* m)
 193 {
 194   eq::EqualityEngine* ee = d_state.getEqualityEngine();
 195   NodeManager* nm = NodeManager::currentNM();
 196   unsigned num_lemmas = 0;
 197   bool isCollectModel = (m != nullptr);
 198   Trace("uf-ho") << "HoExtension::checkExtensionality, collectModel="
 199                  << isCollectModel << "..." << std::endl;
 200   std::map<TypeNode, std::vector<Node> > func_eqcs;
 201   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
 202   while (!eqcs_i.isFinished())
 203   {
 204     Node eqc = (*eqcs_i);
 205     TypeNode tn = eqc.getType();
 206     if (tn.isFunction())
 207     {
 208       // if during collect model, must have an infinite type
 209       // if not during collect model, must have a finite type
 210       if (tn.isInterpretedFinite() != isCollectModel)
 211       {
 212         func_eqcs[tn].push_back(eqc);
 213         Trace("uf-ho-debug")
 214             << "  func eqc : " << tn << " : " << eqc << std::endl;
 215       }
 216     }
 217     ++eqcs_i;
 218   }
 219
 220   for (std::map<TypeNode, std::vector<Node> >::iterator itf = func_eqcs.begin();
 221        itf != func_eqcs.end();
 222        ++itf)
 223   {
 224     for (unsigned j = 0, sizej = itf->second.size(); j < sizej; j++)
 225     {
 226       for (unsigned k = (j + 1), sizek = itf->second.size(); k < sizek; k++)
 227       {
 228         // if these equivalence classes are not explicitly disequal, do
 229         // extensionality to ensure distinctness
 230         if (!ee->areDisequal(itf->second[j], itf->second[k], false))
 231         {
 232           Node deq =
 233               Rewriter::rewrite(itf->second[j].eqNode(itf->second[k]).negate());
 234           // either add to model, or add lemma
 235           if (isCollectModel)
 236           {
 237             // Add extentionality disequality to the model.
 238             // It is important that we construct new (unconstrained) variables
 239             // k here, so that we do not generate any inconsistencies.
 240             Node edeq = getExtensionalityDeq(deq, false);
 241             Assert(edeq.getKind() == NOT && edeq[0].getKind() == EQUAL);
 242             // introducing terms, must add required constraints, e.g. to
 243             // force equalities between APPLY_UF and HO_APPLY terms
 244             for (unsigned r = 0; r < 2; r++)
 245             {
 246               if (!collectModelInfoHoTerm(edeq[0][r], m))
 247               {
 248                 return 1;
 249               }
 250             }
 251             Trace("uf-ho-debug")
 252                 << "Add extensionality deq to model : " << edeq << std::endl;
 253             if (!m->assertEquality(edeq[0][0], edeq[0][1], false))
 254             {
 255               Node eq = edeq[0][0].eqNode(edeq[0][1]);
 256               Node lem = nm->mkNode(OR, deq.negate(), eq);
 257               Trace("uf-ho") << "HoExtension: cmi extensionality lemma " << lem
 258                              << std::endl;
 259               d_im.lemma(lem);
 260               return 1;
 261             }
 262           }
 263           else
 264           {
 265             // apply extensionality lemma
 266             num_lemmas += applyExtensionality(deq);
 267           }
 268         }
 269       }
 270     }
 271   }
 272   return num_lemmas;
 273 }
 274
 275 unsigned HoExtension::applyAppCompletion(TNode n)
 276 {
 277   Assert(n.getKind() == APPLY_UF);
 278
 279   eq::EqualityEngine* ee = d_state.getEqualityEngine();
 280   // must expand into APPLY_HO version if not there already
 281   Node ret = TheoryUfRewriter::getHoApplyForApplyUf(n);
 282   if (!ee->hasTerm(ret) || !ee->areEqual(ret, n))
 283   {
 284     Node eq = n.eqNode(ret);
 285     Trace("uf-ho-lemma") << "uf-ho-lemma : infer, by apply-expand : " << eq
 286                          << std::endl;
 287     d_im.assertInternalFact(eq, true, PfRule::HO_APP_ENCODE, {}, {n});
 288     return 1;
 289   }
 290   Trace("uf-ho-debug") << "    ...already have " << ret << " == " << n << "."
 291                        << std::endl;
 292   return 0;
 293 }
 294
 295 unsigned HoExtension::checkAppCompletion()
 296 {
 297   Trace("uf-ho") << "HoExtension::checkApplyCompletion..." << std::endl;
 298   // compute the operators that are relevant (those for which an HO_APPLY exist)
 299   std::set<TNode> rlvOp;
 300   eq::EqualityEngine* ee = d_state.getEqualityEngine();
 301   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
 302   std::map<TNode, std::vector<Node> > apply_uf;
 303   while (!eqcs_i.isFinished())
 304   {
 305     Node eqc = (*eqcs_i);
 306     Trace("uf-ho-debug") << "  apply completion : visit eqc " << eqc
 307                          << std::endl;
 308     eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
 309     while (!eqc_i.isFinished())
 310     {
 311       Node n = *eqc_i;
 312       if (n.getKind() == APPLY_UF || n.getKind() == HO_APPLY)
 313       {
 314         int curr_sum = 0;
 315         std::map<TNode, bool> curr_rops;
 316         if (n.getKind() == APPLY_UF)
 317         {
 318           TNode rop = ee->getRepresentative(n.getOperator());
 319           if (rlvOp.find(rop) != rlvOp.end())
 320           {
 321             // try if its operator is relevant
 322             curr_sum = applyAppCompletion(n);
 323             if (curr_sum > 0)
 324             {
 325               return curr_sum;
 326             }
 327           }
 328           else
 329           {
 330             // add to pending list
 331             apply_uf[rop].push_back(n);
 332           }
 333           // Arguments are also relevant operators.
 334           // It might be possible include fewer terms here, see #1115.
 335           for (unsigned k = 0; k < n.getNumChildren(); k++)
 336           {
 337             if (n[k].getType().isFunction())
 338             {
 339               TNode rop2 = ee->getRepresentative(n[k]);
 340               curr_rops[rop2] = true;
 341             }
 342           }
 343         }
 344         else
 345         {
 346           Assert(n.getKind() == HO_APPLY);
 347           TNode rop = ee->getRepresentative(n[0]);
 348           curr_rops[rop] = true;
 349         }
 350         for (std::map<TNode, bool>::iterator itc = curr_rops.begin();
 351              itc != curr_rops.end();
 352              ++itc)
 353         {
 354           TNode rop = itc->first;
 355           if (rlvOp.find(rop) == rlvOp.end())
 356           {
 357             rlvOp.insert(rop);
 358             // now, try each pending APPLY_UF for this operator
 359             std::map<TNode, std::vector<Node> >::iterator itu =
 360                 apply_uf.find(rop);
 361             if (itu != apply_uf.end())
 362             {
 363               for (unsigned j = 0, size = itu->second.size(); j < size; j++)
 364               {
 365                 curr_sum = applyAppCompletion(itu->second[j]);
 366                 if (curr_sum > 0)
 367                 {
 368                   return curr_sum;
 369                 }
 370               }
 371             }
 372           }
 373         }
 374       }
 375       ++eqc_i;
 376     }
 377     ++eqcs_i;
 378   }
 379   return 0;
 380 }
 381
 382 unsigned HoExtension::check()
 383 {
 384   Trace("uf-ho") << "HoExtension::checkHigherOrder..." << std::endl;
 385
 386   // infer new facts based on apply completion until fixed point
 387   unsigned num_facts;
 388   do
 389   {
 390     num_facts = checkAppCompletion();
 391     if (d_state.isInConflict())
 392     {
 393       Trace("uf-ho") << "...conflict during app-completion." << std::endl;
 394       return 1;
 395     }
 396   } while (num_facts > 0);
 397
 398   if (options::ufHoExt())
 399   {
 400     unsigned num_lemmas = 0;
 401
 402     num_lemmas = checkExtensionality();
 403     if (num_lemmas > 0)
 404     {
 405       Trace("uf-ho") << "...extensionality returned " << num_lemmas
 406                      << " lemmas." << std::endl;
 407       return num_lemmas;
 408     }
 409   }
 410
 411   Trace("uf-ho") << "...finished check higher order." << std::endl;
 412
 413   return 0;
 414 }
 415
 416 bool HoExtension::collectModelInfoHo(TheoryModel* m,
 417                                      const std::set<Node>& termSet)
 418 {
 419   for (std::set<Node>::iterator it = termSet.begin(); it != termSet.end(); ++it)
 420   {
 421     Node n = *it;
 422     // For model-building with ufHo, we require that APPLY_UF is always
 423     // expanded to HO_APPLY. That is, we always expand to a fully applicative
 424     // encoding during model construction.
 425     if (!collectModelInfoHoTerm(n, m))
 426     {
 427       return false;
 428     }
 429   }
 430   int addedLemmas = checkExtensionality(m);
 431   return addedLemmas == 0;
 432 }
 433
 434 bool HoExtension::collectModelInfoHoTerm(Node n, TheoryModel* m)
 435 {
 436   if (n.getKind() == APPLY_UF)
 437   {
 438     Node hn = TheoryUfRewriter::getHoApplyForApplyUf(n);
 439     if (!m->assertEquality(n, hn, true))
 440     {
 441       Node eq = n.eqNode(hn);
 442       Trace("uf-ho") << "HoExtension: cmi app completion lemma " << eq
 443                      << std::endl;
 444       d_im.lemma(eq);
 445       return false;
 446     }
 447   }
 448   return true;
 449 }
 450
 451 }  // namespace uf
 452 }  // namespace theory
 453 }  // namespace CVC4