1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Aina Niemetz |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* This class caches the evaluation of nodes on a fixed list of examples. |
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 cvc5; |
21 |
|
using namespace cvc5::kind; |
22 |
|
|
23 |
|
namespace cvc5 { |
24 |
|
namespace theory { |
25 |
|
namespace quantifiers { |
26 |
|
|
27 |
128 |
ExampleEvalCache::ExampleEvalCache(TermDbSygus* tds, |
28 |
|
SynthConjecture* p, |
29 |
|
Node f, |
30 |
128 |
Node e) |
31 |
128 |
: d_tds(tds), d_stn(e.getType()) |
32 |
|
{ |
33 |
128 |
ExampleInfer* ei = p->getExampleInfer(); |
34 |
128 |
Assert(ei->hasExamples(f)); |
35 |
698 |
for (unsigned i = 0, nex = ei->getNumExamples(f); i < nex; i++) |
36 |
|
{ |
37 |
1140 |
std::vector<Node> input; |
38 |
570 |
ei->getExample(f, i, input); |
39 |
570 |
d_examples.push_back(input); |
40 |
|
} |
41 |
128 |
d_indexSearchVals = !d_tds->isVariableAgnosticEnumerator(e); |
42 |
128 |
} |
43 |
|
|
44 |
128 |
ExampleEvalCache::~ExampleEvalCache() {} |
45 |
|
|
46 |
14363 |
Node ExampleEvalCache::addSearchVal(TypeNode tn, Node bv) |
47 |
|
{ |
48 |
14363 |
if (!d_indexSearchVals) |
49 |
|
{ |
50 |
|
// not indexing search values |
51 |
|
return Node::null(); |
52 |
|
} |
53 |
28726 |
std::vector<Node> vals; |
54 |
14363 |
evaluateVec(bv, vals, true); |
55 |
14363 |
Trace("sygus-pbe-debug") << "Add to trie..." << std::endl; |
56 |
28726 |
Node ret = d_trie[tn].addOrGetTerm(bv, vals); |
57 |
14363 |
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 |
14363 |
if (ret != bv) |
63 |
|
{ |
64 |
8498 |
clearEvaluationCache(bv); |
65 |
|
} |
66 |
14363 |
Assert(ret.getType().isComparableTo(bv.getType())); |
67 |
14363 |
return ret; |
68 |
|
} |
69 |
|
|
70 |
17506 |
void ExampleEvalCache::evaluateVec(Node bv, |
71 |
|
std::vector<Node>& exOut, |
72 |
|
bool doCache) |
73 |
|
{ |
74 |
|
// is it in the cache? |
75 |
17506 |
std::map<Node, std::vector<Node>>::iterator it = d_exOutCache.find(bv); |
76 |
17506 |
if (it != d_exOutCache.end()) |
77 |
|
{ |
78 |
1793 |
exOut.insert(exOut.end(), it->second.begin(), it->second.end()); |
79 |
1793 |
return; |
80 |
|
} |
81 |
|
// get the evaluation |
82 |
15713 |
evaluateVecInternal(bv, exOut); |
83 |
|
// store in cache if necessary |
84 |
15713 |
if (doCache) |
85 |
|
{ |
86 |
14286 |
std::vector<Node>& eocv = d_exOutCache[bv]; |
87 |
14286 |
eocv.insert(eocv.end(), exOut.begin(), exOut.end()); |
88 |
|
} |
89 |
|
} |
90 |
|
|
91 |
15713 |
void ExampleEvalCache::evaluateVecInternal(Node bv, |
92 |
|
std::vector<Node>& exOut) const |
93 |
|
{ |
94 |
|
// use ExampleMinEval |
95 |
15713 |
SygusTypeInfo& ti = d_tds->getTypeInfo(d_stn); |
96 |
15713 |
const std::vector<Node>& varlist = ti.getVarList(); |
97 |
31426 |
EmeEvalTds emetds(d_tds, d_stn); |
98 |
31426 |
ExampleMinEval eme(bv, varlist, &emetds); |
99 |
153766 |
for (size_t j = 0, esize = d_examples.size(); j < esize; j++) |
100 |
|
{ |
101 |
276106 |
Node res = eme.evaluate(d_examples[j]); |
102 |
138053 |
exOut.push_back(res); |
103 |
|
} |
104 |
15713 |
} |
105 |
|
|
106 |
380 |
Node ExampleEvalCache::evaluate(Node bn, unsigned i) const |
107 |
|
{ |
108 |
380 |
Assert(i < d_examples.size()); |
109 |
380 |
return d_tds->evaluateBuiltin(d_stn, bn, d_examples[i]); |
110 |
|
} |
111 |
|
|
112 |
8498 |
void ExampleEvalCache::clearEvaluationCache(Node bv) |
113 |
|
{ |
114 |
8498 |
Assert(d_exOutCache.find(bv) != d_exOutCache.end()); |
115 |
8498 |
d_exOutCache.erase(bv); |
116 |
8498 |
} |
117 |
|
|
118 |
3330 |
void ExampleEvalCache::clearEvaluationAll() { d_exOutCache.clear(); } |
119 |
|
|
120 |
|
} // namespace quantifiers |
121 |
|
} // namespace theory |
122 |
29337 |
} // namespace cvc5 |