src/theory/quantifiers/fun_def_evaluator.cpp

   1 /*********************                                                        */
   2 /*! \file fun_def_evaluator.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-2019 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 techniques for evaluating terms with recursively
  13  ** defined functions.
  14  **/
  15
  16 #include "theory/quantifiers/fun_def_evaluator.h"
  17
  18 #include "options/quantifiers_options.h"
  19 #include "theory/quantifiers/quantifiers_attributes.h"
  20 #include "theory/rewriter.h"
  21
  22 using namespace CVC4::kind;
  23
  24 namespace CVC4 {
  25 namespace theory {
  26 namespace quantifiers {
  27
  28 FunDefEvaluator::FunDefEvaluator() {}
  29
  30 void FunDefEvaluator::assertDefinition(Node q)
  31 {
  32   Trace("fd-eval") << "FunDefEvaluator: assertDefinition " << q << std::endl;
  33   Node h = QuantAttributes::getFunDefHead(q);
  34   if (h.isNull())
  35   {
  36     // not a function definition
  37     return;
  38   }
  39   // h possibly with zero arguments?
  40   Node f = h.hasOperator() ? h.getOperator() : h;
  41   Assert(d_funDefMap.find(f) == d_funDefMap.end())
  42       << "FunDefEvaluator::assertDefinition: function already defined";
  43   FunDefInfo& fdi = d_funDefMap[f];
  44   fdi.d_body = QuantAttributes::getFunDefBody(q);
  45   Assert(!fdi.d_body.isNull());
  46   fdi.d_args.insert(fdi.d_args.end(), q[0].begin(), q[0].end());
  47   Trace("fd-eval") << "FunDefEvaluator: function " << f << " is defined with "
  48                    << fdi.d_args << " / " << fdi.d_body << std::endl;
  49 }
  50
  51 Node FunDefEvaluator::evaluate(Node n) const
  52 {
  53   // should do standard rewrite before this call
  54   Assert(Rewriter::rewrite(n) == n);
  55   Trace("fd-eval") << "FunDefEvaluator: evaluate " << n << std::endl;
  56   NodeManager* nm = NodeManager::currentNM();
  57   std::unordered_map<TNode, unsigned, TNodeHashFunction> funDefCount;
  58   std::unordered_map<TNode, unsigned, TNodeHashFunction>::iterator itCount;
  59   std::unordered_map<TNode, Node, TNodeHashFunction> visited;
  60   std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
  61   std::map<Node, FunDefInfo>::const_iterator itf;
  62   std::vector<TNode> visit;
  63   TNode cur;
  64   TNode curEval;
  65   Node f;
  66   visit.push_back(n);
  67   do
  68   {
  69     cur = visit.back();
  70     visit.pop_back();
  71     it = visited.find(cur);
  72     Trace("fd-eval-debug") << "evaluate subterm " << cur << std::endl;
  73
  74     if (it == visited.end())
  75     {
  76       if (cur.isConst())
  77       {
  78         Trace("fd-eval-debug") << "constant " << cur << std::endl;
  79         visited[cur] = cur;
  80       }
  81       else if (cur.getKind() == ITE)
  82       {
  83         Trace("fd-eval-debug") << "ITE " << cur << std::endl;
  84         visited[cur] = Node::null();
  85         visit.push_back(cur);
  86         visit.push_back(cur[0]);
  87       }
  88       else
  89       {
  90         Trace("fd-eval-debug") << "recurse " << cur << std::endl;
  91         visited[cur] = Node::null();
  92         visit.push_back(cur);
  93         for (const Node& cn : cur)
  94         {
  95           visit.push_back(cn);
  96         }
  97       }
  98     }
  99     else
 100     {
 101       curEval = it->second;
 102       if (curEval.isNull())
 103       {
 104         Trace("fd-eval-debug") << "from arguments " << cur << std::endl;
 105         Node ret = cur;
 106         bool childChanged = false;
 107         std::vector<Node> children;
 108         Kind ck = cur.getKind();
 109         // If a parameterized node that is not APPLY_UF (which is handled below,
 110         // we add it to the children vector.
 111         if (ck != APPLY_UF && cur.getMetaKind() == metakind::PARAMETERIZED)
 112         {
 113           children.push_back(cur.getOperator());
 114         }
 115         else if (ck == ITE)
 116         {
 117           // get evaluation of condition
 118           it = visited.find(cur[0]);
 119           Assert(it != visited.end());
 120           Assert(!it->second.isNull());
 121           if (!it->second.isConst())
 122           {
 123             Trace("fd-eval") << "FunDefEvaluator: couldn't reduce condition of "
 124                                 "ITE to const, FAIL\n";
 125             return Node::null();
 126           }
 127           // pick child to evaluate depending on condition eval
 128           unsigned childIdxToEval = it->second.getConst<bool>() ? 1 : 2;
 129           Trace("fd-eval-debug2")
 130               << "FunDefEvaluator: result of ITE condition : "
 131               << it->second.getConst<bool>() << "\n";
 132           // the result will be the result of evaluation the child
 133           visited[cur] = cur[childIdxToEval];
 134           // push back self and child. The child will be evaluated first and
 135           // result will be the result of evaluation child
 136           visit.push_back(cur);
 137           visit.push_back(cur[childIdxToEval]);
 138           Trace("fd-eval-debug2") << "FunDefEvaluator: result will be from : "
 139                                   << cur[childIdxToEval] << "\n";
 140           continue;
 141         }
 142         unsigned child CVC4_UNUSED = 0;
 143         for (const Node& cn : cur)
 144         {
 145           it = visited.find(cn);
 146           Assert(it != visited.end());
 147           Assert(!it->second.isNull());
 148           childChanged = childChanged || cn != it->second;
 149           children.push_back(it->second);
 150           Trace("fd-eval-debug2") << "argument " << child++
 151                                   << " eval : " << it->second << std::endl;
 152         }
 153         if (cur.getKind() == APPLY_UF)
 154         {
 155           // need to evaluate it
 156           f = cur.getOperator();
 157           Trace("fd-eval-debug2")
 158               << "FunDefEvaluator: need to eval " << f << "\n";
 159           itf = d_funDefMap.find(f);
 160           itCount = funDefCount.find(f);
 161           if (itCount == funDefCount.end())
 162           {
 163             funDefCount[f] = 0;
 164             itCount = funDefCount.find(f);
 165           }
 166           if (itf == d_funDefMap.end()
 167               || itCount->second > options::sygusRecFunEvalLimit())
 168           {
 169             Trace("fd-eval")
 170                 << "FunDefEvaluator: "
 171                 << (itf == d_funDefMap.end() ? "no definition for "
 172                                              : "too many evals for ")
 173                 << f << ", FAIL" << std::endl;
 174             return Node::null();
 175           }
 176           ++funDefCount[f];
 177           // get the function definition
 178           Node sbody = itf->second.d_body;
 179           Trace("fd-eval-debug2")
 180               << "FunDefEvaluator: definition: " << sbody << "\n";
 181           const std::vector<Node>& args = itf->second.d_args;
 182           if (!args.empty())
 183           {
 184             // invoke it on arguments
 185             sbody = sbody.substitute(
 186                 args.begin(), args.end(), children.begin(), children.end());
 187             // rewrite it
 188             sbody = Rewriter::rewrite(sbody);
 189             if (Trace.isOn("fd-eval-debug2"))
 190             {
 191               Trace("fd-eval-debug2")
 192                   << "FunDefEvaluator: evaluation with args:\n";
 193               for (const Node& child : children)
 194               {
 195                 Trace("fd-eval-debug2") << "..." << child << "\n";
 196               }
 197               Trace("fd-eval-debug2")
 198                   << "FunDefEvaluator: results in " << sbody << "\n";
 199             }
 200           }
 201           // our result is the result of the body
 202           visited[cur] = sbody;
 203           // If its not constant, we push back self and the substituted body.
 204           // Thus, we evaluate the body first; our result will be the result of
 205           // evaluating the body.
 206           if (!sbody.isConst())
 207           {
 208             Trace("fd-eval-debug2") << "FunDefEvaluator: will map " << cur
 209                                     << " from body " << sbody << "\n";
 210             visit.push_back(cur);
 211             visit.push_back(sbody);
 212           }
 213         }
 214         else
 215         {
 216           if (childChanged)
 217           {
 218             ret = nm->mkNode(cur.getKind(), children);
 219             ret = Rewriter::rewrite(ret);
 220           }
 221           Trace("fd-eval-debug2") << "built from arguments " << ret << "\n";
 222           visited[cur] = ret;
 223         }
 224       }
 225       else if (cur != curEval && !curEval.isConst())
 226       {
 227         Trace("fd-eval-debug") << "from body " << cur << std::endl;
 228         Trace("fd-eval-debug") << "and eval  " << curEval << std::endl;
 229         // we had to evaluate our body, which should have a definition now
 230         it = visited.find(curEval);
 231         if (it == visited.end())
 232         {
 233           Trace("fd-eval-debug2") << "eval without definition\n";
 234           // this is the case where curEval was not a constant but it was
 235           // irreducible, for example (DT_SYGUS_EVAL e args)
 236           visited[cur] = curEval;
 237         }
 238         else
 239         {
 240           Trace("fd-eval-debug2")
 241               << "eval with definition " << it->second << "\n";
 242           visited[cur] = it->second;
 243       }
 244     }
 245     }
 246   } while (!visit.empty());
 247   Trace("fd-eval") << "FunDefEvaluator: return " << visited[n] << ", SUCCESS\n";
 248   Assert(visited.find(n) != visited.end());
 249   Assert(!visited.find(n)->second.isNull());
 250   return visited[n];
 251 }
 252
 253 bool FunDefEvaluator::hasDefinitions() const { return !d_funDefMap.empty(); }
 254
 255 }  // namespace quantifiers
 256 }  // namespace theory
 257 }  // namespace CVC4