GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/example_min_eval.cpp Lines: 30 30 100.0 %
Date: 2021-03-23 Branches: 46 108 42.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file example_min_eval.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-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 utility for minimizing the number of calls to
13
 ** evaluate a term on substitutions with a fixed domain.
14
 **/
15
16
#include "theory/quantifiers/sygus/example_min_eval.h"
17
18
#include "expr/node_algorithm.h"
19
#include "theory/quantifiers/sygus/term_database_sygus.h"
20
21
namespace CVC4 {
22
namespace theory {
23
namespace quantifiers {
24
25
26807
ExampleMinEval::ExampleMinEval(Node n,
26
                               const std::vector<Node>& vars,
27
26807
                               EmeEval* ece)
28
{
29
26807
  AlwaysAssert(d_evalNode.isNull());
30
26807
  d_evalNode = n;
31
26807
  d_vars.insert(d_vars.end(), vars.begin(), vars.end());
32
33
  // compute its free variables
34
53614
  std::unordered_set<Node, NodeHashFunction> fvs;
35
26807
  expr::getFreeVariables(n, fvs);
36
262235
  for (size_t i = 0, vsize = vars.size(); i < vsize; i++)
37
  {
38
235428
    if (fvs.find(vars[i]) != fvs.end())
39
    {
40
      // will use this index
41
49369
      d_indices.push_back(i);
42
    }
43
  }
44
53614
  Trace("example-cache") << "For " << n << ", " << d_indices.size() << " / "
45
53614
                         << d_vars.size() << " variables are relevant"
46
26807
                         << std::endl;
47
26807
  d_ece = ece;
48
26807
}
49
50
230002
Node ExampleMinEval::evaluate(const std::vector<Node>& subs)
51
{
52
230002
  Assert(d_vars.size() == subs.size());
53
54
230002
  if (d_indices.size() == d_vars.size())
55
  {
56
    // no sharing is possible since all variables are relevant, just evaluate
57
77873
    return d_ece->eval(d_evalNode, d_vars, subs);
58
  }
59
60
  // get the subsequence of subs that is relevant
61
304258
  std::vector<Node> relSubs;
62
448139
  for (unsigned i = 0, ssize = d_indices.size(); i < ssize; i++)
63
  {
64
296010
    relSubs.push_back(subs[d_indices[i]]);
65
  }
66
304258
  Node res = d_trie.existsTerm(relSubs);
67
152129
  if (res.isNull())
68
  {
69
    // not already cached, must evaluate
70
104278
    res = d_ece->eval(d_evalNode, d_vars, subs);
71
72
    // add to trie
73
104278
    d_trie.addTerm(res, relSubs);
74
  }
75
152129
  return res;
76
}
77
78
182151
Node EmeEvalTds::eval(TNode n,
79
                      const std::vector<Node>& args,
80
                      const std::vector<Node>& vals)
81
{
82
182151
  return d_tds->evaluateBuiltin(d_tn, n, vals);
83
}
84
85
}  // namespace quantifiers
86
}  // namespace theory
87
26685
} /* namespace CVC4 */