src/theory/quantifiers/skolemize.cpp

   1 /*********************                                                        */
   2 /*! \file skolemize.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 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 skolemization utility
  13  **/
  14
  15 #include "theory/quantifiers/skolemize.h"
  16
  17 #include "options/quantifiers_options.h"
  18 #include "theory/quantifiers/term_util.h"
  19 #include "theory/quantifiers_engine.h"
  20 #include "theory/sort_inference.h"
  21 #include "theory/theory_engine.h"
  22
  23 using namespace CVC4::kind;
  24
  25 namespace CVC4 {
  26 namespace theory {
  27 namespace quantifiers {
  28
  29 Skolemize::Skolemize(QuantifiersEngine* qe, context::UserContext* u)
  30     : d_quantEngine(qe), d_skolemized(u)
  31 {
  32 }
  33
  34 Node Skolemize::process(Node q)
  35 {
  36   // do skolemization
  37   if (d_skolemized.find(q) == d_skolemized.end())
  38   {
  39     Node body = getSkolemizedBody(q);
  40     NodeBuilder<> nb(kind::OR);
  41     nb << q << body.notNode();
  42     Node lem = nb;
  43     d_skolemized[q] = lem;
  44     return lem;
  45   }
  46   return Node::null();
  47 }
  48
  49 bool Skolemize::getSkolemConstants(Node q, std::vector<Node>& skolems)
  50 {
  51   std::unordered_map<Node, std::vector<Node>, NodeHashFunction>::iterator it =
  52       d_skolem_constants.find(q);
  53   if (it != d_skolem_constants.end())
  54   {
  55     skolems.insert(skolems.end(), it->second.begin(), it->second.end());
  56     return true;
  57   }
  58   return false;
  59 }
  60
  61 Node Skolemize::getSkolemConstant(Node q, unsigned i)
  62 {
  63   std::unordered_map<Node, std::vector<Node>, NodeHashFunction>::iterator it =
  64       d_skolem_constants.find(q);
  65   if (it != d_skolem_constants.end())
  66   {
  67     if (i < it->second.size())
  68     {
  69       return it->second[i];
  70     }
  71   }
  72   return Node::null();
  73 }
  74
  75 void Skolemize::getSelfSel(const Datatype& dt,
  76                            const DatatypeConstructor& dc,
  77                            Node n,
  78                            TypeNode ntn,
  79                            std::vector<Node>& selfSel)
  80 {
  81   TypeNode tspec;
  82   if (dt.isParametric())
  83   {
  84     tspec = TypeNode::fromType(
  85         dc.getSpecializedConstructorType(n.getType().toType()));
  86     Trace("sk-ind-debug") << "Specialized constructor type : " << tspec
  87                           << std::endl;
  88     Assert(tspec.getNumChildren() == dc.getNumArgs());
  89   }
  90   Trace("sk-ind-debug") << "Check self sel " << dc.getName() << " "
  91                         << dt.getName() << std::endl;
  92   for (unsigned j = 0; j < dc.getNumArgs(); j++)
  93   {
  94     std::vector<Node> ssc;
  95     if (dt.isParametric())
  96     {
  97       Trace("sk-ind-debug") << "Compare " << tspec[j] << " " << ntn
  98                             << std::endl;
  99       if (tspec[j] == ntn)
 100       {
 101         ssc.push_back(n);
 102       }
 103     }
 104     else
 105     {
 106       TypeNode tn = TypeNode::fromType(dc[j].getRangeType());
 107       Trace("sk-ind-debug") << "Compare " << tn << " " << ntn << std::endl;
 108       if (tn == ntn)
 109       {
 110         ssc.push_back(n);
 111       }
 112     }
 113     /* TODO: more than weak structural induction
 114     else if( tn.isDatatype() && std::find( visited.begin(), visited.end(), tn
 115     )==visited.end() ){
 116       visited.push_back( tn );
 117       const Datatype& dt =
 118     ((DatatypeType)(subs[0].getType()).toType()).getDatatype();
 119       std::vector< Node > disj;
 120       for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
 121         getSelfSel( dt[i], n, ntn, ssc );
 122       }
 123       visited.pop_back();
 124     }
 125     */
 126     for (unsigned k = 0; k < ssc.size(); k++)
 127     {
 128       Node ss = NodeManager::currentNM()->mkNode(
 129           APPLY_SELECTOR_TOTAL,
 130           dc.getSelectorInternal(n.getType().toType(), j),
 131           n);
 132       if (std::find(selfSel.begin(), selfSel.end(), ss) == selfSel.end())
 133       {
 134         selfSel.push_back(ss);
 135       }
 136     }
 137   }
 138 }
 139
 140 Node Skolemize::mkSkolemizedBody(Node f,
 141                                  Node n,
 142                                  std::vector<TypeNode>& argTypes,
 143                                  std::vector<TNode>& fvs,
 144                                  std::vector<Node>& sk,
 145                                  Node& sub,
 146                                  std::vector<unsigned>& sub_vars)
 147 {
 148   Assert(sk.empty() || sk.size() == f[0].getNumChildren());
 149   // calculate the variables and substitution
 150   std::vector<TNode> ind_vars;
 151   std::vector<unsigned> ind_var_indicies;
 152   std::vector<TNode> vars;
 153   std::vector<unsigned> var_indicies;
 154   for (unsigned i = 0; i < f[0].getNumChildren(); i++)
 155   {
 156     if (isInductionTerm(f[0][i]))
 157     {
 158       ind_vars.push_back(f[0][i]);
 159       ind_var_indicies.push_back(i);
 160     }
 161     else
 162     {
 163       vars.push_back(f[0][i]);
 164       var_indicies.push_back(i);
 165     }
 166     Node s;
 167     // make the new function symbol or use existing
 168     if (i >= sk.size())
 169     {
 170       if (argTypes.empty())
 171       {
 172         s = NodeManager::currentNM()->mkSkolem(
 173             "skv", f[0][i].getType(), "created during skolemization");
 174       }
 175       else
 176       {
 177         TypeNode typ = NodeManager::currentNM()->mkFunctionType(
 178             argTypes, f[0][i].getType());
 179         Node op = NodeManager::currentNM()->mkSkolem(
 180             "skop", typ, "op created during pre-skolemization");
 181         // DOTHIS: set attribute on op, marking that it should not be selected
 182         // as trigger
 183         std::vector<Node> funcArgs;
 184         funcArgs.push_back(op);
 185         funcArgs.insert(funcArgs.end(), fvs.begin(), fvs.end());
 186         s = NodeManager::currentNM()->mkNode(kind::APPLY_UF, funcArgs);
 187       }
 188       sk.push_back(s);
 189     }
 190     else
 191     {
 192       Assert(sk[i].getType() == f[0][i].getType());
 193     }
 194   }
 195   Node ret;
 196   if (vars.empty())
 197   {
 198     ret = n;
 199   }
 200   else
 201   {
 202     std::vector<Node> var_sk;
 203     for (unsigned i = 0; i < var_indicies.size(); i++)
 204     {
 205       var_sk.push_back(sk[var_indicies[i]]);
 206     }
 207     Assert(vars.size() == var_sk.size());
 208     ret = n.substitute(vars.begin(), vars.end(), var_sk.begin(), var_sk.end());
 209   }
 210   if (!ind_vars.empty())
 211   {
 212     Trace("sk-ind") << "Ind strengthen : (not " << f << ")" << std::endl;
 213     Trace("sk-ind") << "Skolemized is : " << ret << std::endl;
 214     Node n_str_ind;
 215     TypeNode tn = ind_vars[0].getType();
 216     Node k = sk[ind_var_indicies[0]];
 217     Node nret = ret.substitute(ind_vars[0], k);
 218     // note : everything is under a negation
 219     // the following constructs ~( R( x, k ) => ~P( x ) )
 220     if (options::dtStcInduction() && tn.isDatatype())
 221     {
 222       const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
 223       std::vector<Node> disj;
 224       for (unsigned i = 0; i < dt.getNumConstructors(); i++)
 225       {
 226         std::vector<Node> selfSel;
 227         getSelfSel(dt, dt[i], k, tn, selfSel);
 228         std::vector<Node> conj;
 229         conj.push_back(
 230             NodeManager::currentNM()
 231                 ->mkNode(APPLY_TESTER, Node::fromExpr(dt[i].getTester()), k)
 232                 .negate());
 233         for (unsigned j = 0; j < selfSel.size(); j++)
 234         {
 235           conj.push_back(ret.substitute(ind_vars[0], selfSel[j]).negate());
 236         }
 237         disj.push_back(conj.size() == 1
 238                            ? conj[0]
 239                            : NodeManager::currentNM()->mkNode(OR, conj));
 240       }
 241       Assert(!disj.empty());
 242       n_str_ind = disj.size() == 1
 243                       ? disj[0]
 244                       : NodeManager::currentNM()->mkNode(AND, disj);
 245     }
 246     else if (options::intWfInduction() && tn.isInteger())
 247     {
 248       Node icond = NodeManager::currentNM()->mkNode(
 249           GEQ, k, NodeManager::currentNM()->mkConst(Rational(0)));
 250       Node iret =
 251           ret.substitute(
 252                  ind_vars[0],
 253                  NodeManager::currentNM()->mkNode(
 254                      MINUS, k, NodeManager::currentNM()->mkConst(Rational(1))))
 255               .negate();
 256       n_str_ind = NodeManager::currentNM()->mkNode(OR, icond.negate(), iret);
 257       n_str_ind = NodeManager::currentNM()->mkNode(AND, icond, n_str_ind);
 258     }
 259     else
 260     {
 261       Trace("sk-ind") << "Unknown induction for term : " << ind_vars[0]
 262                       << ", type = " << tn << std::endl;
 263       Assert(false);
 264     }
 265     Trace("sk-ind") << "Strengthening is : " << n_str_ind << std::endl;
 266
 267     std::vector<Node> rem_ind_vars;
 268     rem_ind_vars.insert(
 269         rem_ind_vars.end(), ind_vars.begin() + 1, ind_vars.end());
 270     if (!rem_ind_vars.empty())
 271     {
 272       Node bvl = NodeManager::currentNM()->mkNode(BOUND_VAR_LIST, rem_ind_vars);
 273       nret = NodeManager::currentNM()->mkNode(FORALL, bvl, nret);
 274       nret = Rewriter::rewrite(nret);
 275       sub = nret;
 276       sub_vars.insert(
 277           sub_vars.end(), ind_var_indicies.begin() + 1, ind_var_indicies.end());
 278       n_str_ind = NodeManager::currentNM()
 279                       ->mkNode(FORALL, bvl, n_str_ind.negate())
 280                       .negate();
 281     }
 282     ret = NodeManager::currentNM()->mkNode(OR, nret, n_str_ind);
 283   }
 284   Trace("quantifiers-sk-debug") << "mkSkolem body for " << f
 285                                 << " returns : " << ret << std::endl;
 286   // if it has an instantiation level, set the skolemized body to that level
 287   if (f.hasAttribute(InstLevelAttribute()))
 288   {
 289     theory::QuantifiersEngine::setInstantiationLevelAttr(
 290         ret, f.getAttribute(InstLevelAttribute()));
 291   }
 292
 293   if (Trace.isOn("quantifiers-sk"))
 294   {
 295     Trace("quantifiers-sk") << "Skolemize : ";
 296     for (unsigned i = 0; i < sk.size(); i++)
 297     {
 298       Trace("quantifiers-sk") << sk[i] << " ";
 299     }
 300     Trace("quantifiers-sk") << "for " << std::endl;
 301     Trace("quantifiers-sk") << "   " << f << std::endl;
 302   }
 303
 304   return ret;
 305 }
 306
 307 Node Skolemize::getSkolemizedBody(Node f)
 308 {
 309   Assert(f.getKind() == FORALL);
 310   if (d_skolem_body.find(f) == d_skolem_body.end())
 311   {
 312     std::vector<TypeNode> fvTypes;
 313     std::vector<TNode> fvs;
 314     Node sub;
 315     std::vector<unsigned> sub_vars;
 316     d_skolem_body[f] = mkSkolemizedBody(
 317         f, f[1], fvTypes, fvs, d_skolem_constants[f], sub, sub_vars);
 318     // store sub quantifier information
 319     if (!sub.isNull())
 320     {
 321       // if we are skolemizing one at a time, we already know the skolem
 322       // constants of the sub-quantified formula, store them
 323       Assert(d_skolem_constants[sub].empty());
 324       for (unsigned i = 0; i < sub_vars.size(); i++)
 325       {
 326         d_skolem_constants[sub].push_back(d_skolem_constants[f][sub_vars[i]]);
 327       }
 328     }
 329     Assert(d_skolem_constants[f].size() == f[0].getNumChildren());
 330     if (options::sortInference())
 331     {
 332       for (unsigned i = 0; i < d_skolem_constants[f].size(); i++)
 333       {
 334         // carry information for sort inference
 335         d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar(
 336             f, f[0][i], d_skolem_constants[f][i]);
 337       }
 338     }
 339   }
 340   return d_skolem_body[f];
 341 }
 342
 343 bool Skolemize::isInductionTerm(Node n)
 344 {
 345   TypeNode tn = n.getType();
 346   if (options::dtStcInduction() && tn.isDatatype())
 347   {
 348     const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
 349     return !dt.isCodatatype();
 350   }
 351   if (options::intWfInduction() && n.getType().isInteger())
 352   {
 353     return true;
 354   }
 355   return false;
 356 }
 357
 358 bool Skolemize::printSkolemization(std::ostream& out)
 359 {
 360   bool printed = false;
 361   for (NodeNodeMap::iterator it = d_skolemized.begin();
 362        it != d_skolemized.end();
 363        ++it)
 364   {
 365     Node q = (*it).first;
 366     printed = true;
 367     out << "(skolem " << q << std::endl;
 368     out << "  ( ";
 369     for (unsigned i = 0; i < d_skolem_constants[q].size(); i++)
 370     {
 371       if (i > 0)
 372       {
 373         out << " ";
 374       }
 375       out << d_skolem_constants[q][i];
 376     }
 377     out << " )" << std::endl;
 378     out << ")" << std::endl;
 379   }
 380   return printed;
 381 }
 382
 383 } /* CVC4::theory::quantifiers namespace */
 384 } /* CVC4::theory namespace */
 385 } /* CVC4 namespace */