GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/example_eval_cache.cpp Lines: 50 51 98.0 %
Date: 2021-03-22 Branches: 70 182 38.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file example_eval_cache.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
13
 **
14
 **/
15
#include "theory/quantifiers/sygus/example_eval_cache.h"
16
17
#include "theory/quantifiers/sygus/example_min_eval.h"
18
#include "theory/quantifiers/sygus/synth_conjecture.h"
19
20
using namespace CVC4;
21
using namespace CVC4::kind;
22
23
namespace CVC4 {
24
namespace theory {
25
namespace quantifiers {
26
27
207
ExampleEvalCache::ExampleEvalCache(TermDbSygus* tds,
28
                                   SynthConjecture* p,
29
                                   Node f,
30
207
                                   Node e)
31
207
    : d_tds(tds), d_stn(e.getType())
32
{
33
207
  ExampleInfer* ei = p->getExampleInfer();
34
207
  Assert(ei->hasExamples(f));
35
1196
  for (unsigned i = 0, nex = ei->getNumExamples(f); i < nex; i++)
36
  {
37
1978
    std::vector<Node> input;
38
989
    ei->getExample(f, i, input);
39
989
    d_examples.push_back(input);
40
  }
41
207
  d_indexSearchVals = !d_tds->isVariableAgnosticEnumerator(e);
42
207
}
43
44
207
ExampleEvalCache::~ExampleEvalCache() {}
45
46
24754
Node ExampleEvalCache::addSearchVal(TypeNode tn, Node bv)
47
{
48
24754
  if (!d_indexSearchVals)
49
  {
50
    // not indexing search values
51
    return Node::null();
52
  }
53
49508
  std::vector<Node> vals;
54
24754
  evaluateVec(bv, vals, true);
55
24754
  Trace("sygus-pbe-debug") << "Add to trie..." << std::endl;
56
49508
  Node ret = d_trie[tn].addOrGetTerm(bv, vals);
57
24754
  Trace("sygus-pbe-debug") << "...got " << ret << std::endl;
58
  // Only save the cache data if necessary: if the enumerated term
59
  // is redundant, its cached data will not be used later and thus should
60
  // be discarded. This applies also to the case where the evaluation
61
  // was cached prior to this call.
62
24754
  if (ret != bv)
63
  {
64
14338
    clearEvaluationCache(bv);
65
  }
66
24754
  Assert(ret.getType().isComparableTo(bv.getType()));
67
24754
  return ret;
68
}
69
70
29759
void ExampleEvalCache::evaluateVec(Node bv,
71
                                   std::vector<Node>& exOut,
72
                                   bool doCache)
73
{
74
  // is it in the cache?
75
29759
  std::map<Node, std::vector<Node>>::iterator it = d_exOutCache.find(bv);
76
29759
  if (it != d_exOutCache.end())
77
  {
78
2952
    exOut.insert(exOut.end(), it->second.begin(), it->second.end());
79
2952
    return;
80
  }
81
  // get the evaluation
82
26807
  evaluateVecInternal(bv, exOut);
83
  // store in cache if necessary
84
26807
  if (doCache)
85
  {
86
24634
    std::vector<Node>& eocv = d_exOutCache[bv];
87
24634
    eocv.insert(eocv.end(), exOut.begin(), exOut.end());
88
  }
89
}
90
91
26807
void ExampleEvalCache::evaluateVecInternal(Node bv,
92
                                           std::vector<Node>& exOut) const
93
{
94
  // use ExampleMinEval
95
26807
  SygusTypeInfo& ti = d_tds->getTypeInfo(d_stn);
96
26807
  const std::vector<Node>& varlist = ti.getVarList();
97
53614
  EmeEvalTds emetds(d_tds, d_stn);
98
53614
  ExampleMinEval eme(bv, varlist, &emetds);
99
256809
  for (size_t j = 0, esize = d_examples.size(); j < esize; j++)
100
  {
101
460004
    Node res = eme.evaluate(d_examples[j]);
102
230002
    exOut.push_back(res);
103
  }
104
26807
}
105
106
660
Node ExampleEvalCache::evaluate(Node bn, unsigned i) const
107
{
108
660
  Assert(i < d_examples.size());
109
660
  return d_tds->evaluateBuiltin(d_stn, bn, d_examples[i]);
110
}
111
112
14338
void ExampleEvalCache::clearEvaluationCache(Node bv)
113
{
114
14338
  Assert(d_exOutCache.find(bv) != d_exOutCache.end());
115
14338
  d_exOutCache.erase(bv);
116
14338
}
117
118
5317
void ExampleEvalCache::clearEvaluationAll() { d_exOutCache.clear(); }
119
120
}  // namespace quantifiers
121
}  // namespace theory
122
26676
}  // namespace CVC4