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 |
|
|
19 |
|
using namespace cvc5; |
20 |
|
using namespace cvc5::kind; |
21 |
|
|
22 |
|
namespace cvc5 { |
23 |
|
namespace theory { |
24 |
|
namespace quantifiers { |
25 |
|
|
26 |
128 |
ExampleEvalCache::ExampleEvalCache(TermDbSygus* tds, |
27 |
128 |
Node e) |
28 |
128 |
: d_tds(tds), d_stn(e.getType()) |
29 |
|
{ |
30 |
128 |
d_indexSearchVals = !d_tds->isVariableAgnosticEnumerator(e); |
31 |
128 |
} |
32 |
|
|
33 |
128 |
ExampleEvalCache::~ExampleEvalCache() {} |
34 |
|
|
35 |
570 |
void ExampleEvalCache::addExample(const std::vector<Node>& ex) |
36 |
|
{ |
37 |
570 |
d_examples.push_back(ex); |
38 |
570 |
} |
39 |
|
|
40 |
14444 |
Node ExampleEvalCache::addSearchVal(TypeNode tn, Node bv) |
41 |
|
{ |
42 |
14444 |
if (!d_indexSearchVals) |
43 |
|
{ |
44 |
|
// not indexing search values |
45 |
|
return Node::null(); |
46 |
|
} |
47 |
28888 |
std::vector<Node> vals; |
48 |
14444 |
evaluateVec(bv, vals, true); |
49 |
14444 |
Trace("sygus-pbe-debug") << "Add to trie..." << std::endl; |
50 |
28888 |
Node ret = d_trie[tn].addOrGetTerm(bv, vals); |
51 |
14444 |
Trace("sygus-pbe-debug") << "...got " << ret << std::endl; |
52 |
|
// Only save the cache data if necessary: if the enumerated term |
53 |
|
// is redundant, its cached data will not be used later and thus should |
54 |
|
// be discarded. This applies also to the case where the evaluation |
55 |
|
// was cached prior to this call. |
56 |
14444 |
if (ret != bv) |
57 |
|
{ |
58 |
8496 |
clearEvaluationCache(bv); |
59 |
|
} |
60 |
14444 |
Assert(ret.getType().isComparableTo(bv.getType())); |
61 |
14444 |
return ret; |
62 |
|
} |
63 |
|
|
64 |
17626 |
void ExampleEvalCache::evaluateVec(Node bv, |
65 |
|
std::vector<Node>& exOut, |
66 |
|
bool doCache) |
67 |
|
{ |
68 |
|
// is it in the cache? |
69 |
17626 |
std::map<Node, std::vector<Node>>::iterator it = d_exOutCache.find(bv); |
70 |
17626 |
if (it != d_exOutCache.end()) |
71 |
|
{ |
72 |
1831 |
exOut.insert(exOut.end(), it->second.begin(), it->second.end()); |
73 |
1831 |
return; |
74 |
|
} |
75 |
|
// get the evaluation |
76 |
15795 |
evaluateVecInternal(bv, exOut); |
77 |
|
// store in cache if necessary |
78 |
15795 |
if (doCache) |
79 |
|
{ |
80 |
14368 |
std::vector<Node>& eocv = d_exOutCache[bv]; |
81 |
14368 |
eocv.insert(eocv.end(), exOut.begin(), exOut.end()); |
82 |
|
} |
83 |
|
} |
84 |
|
|
85 |
15795 |
void ExampleEvalCache::evaluateVecInternal(Node bv, |
86 |
|
std::vector<Node>& exOut) const |
87 |
|
{ |
88 |
|
// use ExampleMinEval |
89 |
15795 |
SygusTypeInfo& ti = d_tds->getTypeInfo(d_stn); |
90 |
15795 |
const std::vector<Node>& varlist = ti.getVarList(); |
91 |
31590 |
EmeEvalTds emetds(d_tds, d_stn); |
92 |
31590 |
ExampleMinEval eme(bv, varlist, &emetds); |
93 |
154078 |
for (size_t j = 0, esize = d_examples.size(); j < esize; j++) |
94 |
|
{ |
95 |
276566 |
Node res = eme.evaluate(d_examples[j]); |
96 |
138283 |
exOut.push_back(res); |
97 |
|
} |
98 |
15795 |
} |
99 |
|
|
100 |
380 |
Node ExampleEvalCache::evaluate(Node bn, unsigned i) const |
101 |
|
{ |
102 |
380 |
Assert(i < d_examples.size()); |
103 |
380 |
return d_tds->evaluateBuiltin(d_stn, bn, d_examples[i]); |
104 |
|
} |
105 |
|
|
106 |
8496 |
void ExampleEvalCache::clearEvaluationCache(Node bv) |
107 |
|
{ |
108 |
8496 |
Assert(d_exOutCache.find(bv) != d_exOutCache.end()); |
109 |
8496 |
d_exOutCache.erase(bv); |
110 |
8496 |
} |
111 |
|
|
112 |
3387 |
void ExampleEvalCache::clearEvaluationAll() { d_exOutCache.clear(); } |
113 |
|
|
114 |
|
} // namespace quantifiers |
115 |
|
} // namespace theory |
116 |
29502 |
} // namespace cvc5 |