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, Haniel Barbosa, 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 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 using the evaluator
 185             sbody = d_eval.eval(sbody, args, children);
 186             if (Trace.isOn("fd-eval-debug2"))
 187             {
 188               Trace("fd-eval-debug2")
 189                   << "FunDefEvaluator: evaluation with args:\n";
 190               for (const Node& ch : children)
 191               {
 192                 Trace("fd-eval-debug2") << "..." << ch << "\n";
 193               }
 194               Trace("fd-eval-debug2")
 195                   << "FunDefEvaluator: results in " << sbody << "\n";
 196             }
 197             Assert(!sbody.isNull());
 198           }
 199           // our result is the result of the body
 200           visited[cur] = sbody;
 201           // If its not constant, we push back self and the substituted body.
 202           // Thus, we evaluate the body first; our result will be the result of
 203           // evaluating the body.
 204           if (!sbody.isConst())
 205           {
 206             Trace("fd-eval-debug2") << "FunDefEvaluator: will map " << cur
 207                                     << " from body " << sbody << "\n";
 208             visit.push_back(cur);
 209             visit.push_back(sbody);
 210           }
 211         }
 212         else
 213         {
 214           if (childChanged)
 215           {
 216             ret = nm->mkNode(cur.getKind(), children);
 217             ret = Rewriter::rewrite(ret);
 218           }
 219           Trace("fd-eval-debug2") << "built from arguments " << ret << "\n";
 220           visited[cur] = ret;
 221         }
 222       }
 223       else if (cur != curEval && !curEval.isConst())
 224       {
 225         Trace("fd-eval-debug") << "from body " << cur << std::endl;
 226         Trace("fd-eval-debug") << "and eval  " << curEval << std::endl;
 227         // we had to evaluate our body, which should have a definition now
 228         it = visited.find(curEval);
 229         if (it == visited.end())
 230         {
 231           Trace("fd-eval-debug2") << "eval without definition\n";
 232           // this is the case where curEval was not a constant but it was
 233           // irreducible, for example (DT_SYGUS_EVAL e args)
 234           visited[cur] = curEval;
 235         }
 236         else
 237         {
 238           Trace("fd-eval-debug2")
 239               << "eval with definition " << it->second << "\n";
 240           visited[cur] = it->second;
 241       }
 242     }
 243     }
 244   } while (!visit.empty());
 245   Trace("fd-eval") << "FunDefEvaluator: return " << visited[n] << ", SUCCESS\n";
 246   Assert(visited.find(n) != visited.end());
 247   Assert(!visited.find(n)->second.isNull());
 248   return visited[n];
 249 }
 250
 251 bool FunDefEvaluator::hasDefinitions() const { return !d_funDefMap.empty(); }
 252
 253 }  // namespace quantifiers
 254 }  // namespace theory
 255 }  // namespace CVC4