GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/fun_def_evaluator.cpp Lines: 129 143 90.2 %
Date: 2021-03-23 Branches: 321 764 42.0 %

Line Exec Source
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-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.\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
2190
FunDefEvaluator::FunDefEvaluator() {}
29
30
39
void FunDefEvaluator::assertDefinition(Node q)
31
{
32
39
  Trace("fd-eval") << "FunDefEvaluator: assertDefinition " << q << std::endl;
33
78
  Node h = QuantAttributes::getFunDefHead(q);
34
39
  if (h.isNull())
35
  {
36
    // not a function definition
37
    return;
38
  }
39
  // h possibly with zero arguments?
40
78
  Node f = h.hasOperator() ? h.getOperator() : h;
41
39
  Assert(d_funDefMap.find(f) == d_funDefMap.end())
42
      << "FunDefEvaluator::assertDefinition: function already defined";
43
39
  FunDefInfo& fdi = d_funDefMap[f];
44
39
  fdi.d_body = QuantAttributes::getFunDefBody(q);
45
39
  Assert(!fdi.d_body.isNull());
46
39
  fdi.d_args.insert(fdi.d_args.end(), q[0].begin(), q[0].end());
47
78
  Trace("fd-eval") << "FunDefEvaluator: function " << f << " is defined with "
48
39
                   << fdi.d_args << " / " << fdi.d_body << std::endl;
49
}
50
51
3664
Node FunDefEvaluator::evaluate(Node n) const
52
{
53
  // should do standard rewrite before this call
54
3664
  Assert(Rewriter::rewrite(n) == n);
55
3664
  Trace("fd-eval") << "FunDefEvaluator: evaluate " << n << std::endl;
56
3664
  NodeManager* nm = NodeManager::currentNM();
57
7328
  std::unordered_map<TNode, unsigned, TNodeHashFunction> funDefCount;
58
3664
  std::unordered_map<TNode, unsigned, TNodeHashFunction>::iterator itCount;
59
7328
  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
60
3664
  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
61
3664
  std::map<Node, FunDefInfo>::const_iterator itf;
62
7328
  std::vector<TNode> visit;
63
7328
  TNode cur;
64
7328
  TNode curEval;
65
7328
  Node f;
66
3664
  visit.push_back(n);
67
100792
  do
68
  {
69
104456
    cur = visit.back();
70
104456
    visit.pop_back();
71
104456
    it = visited.find(cur);
72
104456
    Trace("fd-eval-debug") << "evaluate subterm " << cur << std::endl;
73
74
104456
    if (it == visited.end())
75
    {
76
51724
      if (cur.isConst())
77
      {
78
17424
        Trace("fd-eval-debug") << "constant " << cur << std::endl;
79
17424
        visited[cur] = cur;
80
      }
81
34300
      else if (cur.getKind() == ITE)
82
      {
83
2200
        Trace("fd-eval-debug") << "ITE " << cur << std::endl;
84
2200
        visited[cur] = Node::null();
85
2200
        visit.push_back(cur);
86
2200
        visit.push_back(cur[0]);
87
      }
88
      else
89
      {
90
32100
        Trace("fd-eval-debug") << "recurse " << cur << std::endl;
91
32100
        visited[cur] = Node::null();
92
32100
        visit.push_back(cur);
93
94569
        for (const Node& cn : cur)
94
        {
95
62469
          visit.push_back(cn);
96
        }
97
      }
98
    }
99
    else
100
    {
101
52732
      curEval = it->second;
102
52732
      if (curEval.isNull())
103
      {
104
30744
        Trace("fd-eval-debug") << "from arguments " << cur << std::endl;
105
59571
        Node ret = cur;
106
30744
        bool childChanged = false;
107
59571
        std::vector<Node> children;
108
30744
        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
30744
        if (ck != APPLY_UF && cur.getMetaKind() == metakind::PARAMETERIZED)
112
        {
113
5406
          children.push_back(cur.getOperator());
114
        }
115
25338
        else if (ck == ITE)
116
        {
117
          // get evaluation of condition
118
1917
          it = visited.find(cur[0]);
119
1917
          Assert(it != visited.end());
120
1917
          Assert(!it->second.isNull());
121
1917
          if (!it->second.isConst())
122
          {
123
939
            Trace("fd-eval") << "FunDefEvaluator: couldn't reduce condition of "
124
                                "ITE to const, FAIL\n";
125
939
            return Node::null();
126
          }
127
          // pick child to evaluate depending on condition eval
128
978
          unsigned childIdxToEval = it->second.getConst<bool>() ? 1 : 2;
129
1956
          Trace("fd-eval-debug2")
130
978
              << "FunDefEvaluator: result of ITE condition : "
131
978
              << it->second.getConst<bool>() << "\n";
132
          // the result will be the result of evaluation the child
133
978
          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
978
          visit.push_back(cur);
137
978
          visit.push_back(cur[childIdxToEval]);
138
1956
          Trace("fd-eval-debug2") << "FunDefEvaluator: result will be from : "
139
978
                                  << cur[childIdxToEval] << "\n";
140
978
          continue;
141
        }
142
28827
        unsigned child CVC4_UNUSED = 0;
143
84457
        for (const Node& cn : cur)
144
        {
145
55630
          it = visited.find(cn);
146
55630
          Assert(it != visited.end());
147
55630
          Assert(!it->second.isNull());
148
55630
          childChanged = childChanged || cn != it->second;
149
55630
          children.push_back(it->second);
150
111260
          Trace("fd-eval-debug2") << "argument " << child++
151
55630
                                  << " eval : " << it->second << std::endl;
152
        }
153
28827
        if (cur.getKind() == APPLY_UF)
154
        {
155
          // need to evaluate it
156
6420
          f = cur.getOperator();
157
12840
          Trace("fd-eval-debug2")
158
6420
              << "FunDefEvaluator: need to eval " << f << "\n";
159
6420
          itf = d_funDefMap.find(f);
160
6420
          itCount = funDefCount.find(f);
161
6420
          if (itCount == funDefCount.end())
162
          {
163
3559
            funDefCount[f] = 0;
164
3559
            itCount = funDefCount.find(f);
165
          }
166
12840
          if (itf == d_funDefMap.end()
167
12840
              || 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
6420
          ++funDefCount[f];
177
          // get the function definition
178
12840
          Node sbody = itf->second.d_body;
179
12840
          Trace("fd-eval-debug2")
180
6420
              << "FunDefEvaluator: definition: " << sbody << "\n";
181
6420
          const std::vector<Node>& args = itf->second.d_args;
182
6420
          if (!args.empty())
183
          {
184
            // invoke it on arguments using the evaluator
185
6420
            sbody = d_eval.eval(sbody, args, children);
186
6420
            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
6420
            Assert(!sbody.isNull());
198
          }
199
          // our result is the result of the body
200
6420
          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
6420
          if (!sbody.isConst())
205
          {
206
8768
            Trace("fd-eval-debug2") << "FunDefEvaluator: will map " << cur
207
4384
                                    << " from body " << sbody << "\n";
208
4384
            visit.push_back(cur);
209
4384
            visit.push_back(sbody);
210
          }
211
        }
212
        else
213
        {
214
22407
          if (childChanged)
215
          {
216
4776
            ret = nm->mkNode(cur.getKind(), children);
217
4776
            ret = Rewriter::rewrite(ret);
218
          }
219
22407
          Trace("fd-eval-debug2") << "built from arguments " << ret << "\n";
220
22407
          visited[cur] = ret;
221
        }
222
      }
223
21988
      else if (cur != curEval && !curEval.isConst())
224
      {
225
3316
        Trace("fd-eval-debug") << "from body " << cur << std::endl;
226
3316
        Trace("fd-eval-debug") << "and eval  " << curEval << std::endl;
227
        // we had to evaluate our body, which should have a definition now
228
3316
        it = visited.find(curEval);
229
3316
        if (it == visited.end())
230
        {
231
2
          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
2
          visited[cur] = curEval;
235
        }
236
        else
237
        {
238
6628
          Trace("fd-eval-debug2")
239
3314
              << "eval with definition " << it->second << "\n";
240
3314
          visited[cur] = it->second;
241
      }
242
    }
243
    }
244
103517
  } while (!visit.empty());
245
2725
  Trace("fd-eval") << "FunDefEvaluator: return " << visited[n] << ", SUCCESS\n";
246
2725
  Assert(visited.find(n) != visited.end());
247
2725
  Assert(!visited.find(n)->second.isNull());
248
2725
  return visited[n];
249
}
250
251
223393
bool FunDefEvaluator::hasDefinitions() const { return !d_funDefMap.empty(); }
252
253
}  // namespace quantifiers
254
}  // namespace theory
255
33105
}  // namespace CVC4