1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Yoni Zohar, Gereon Kremer, Andrew Reynolds |
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 |
|
* The static learning preprocessing pass. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "preprocessing/passes/static_learning.h" |
17 |
|
|
18 |
|
#include <string> |
19 |
|
|
20 |
|
#include "expr/node.h" |
21 |
|
#include "preprocessing/assertion_pipeline.h" |
22 |
|
#include "preprocessing/preprocessing_pass_context.h" |
23 |
|
#include "theory/rewriter.h" |
24 |
|
#include "theory/theory_engine.h" |
25 |
|
|
26 |
|
namespace cvc5 { |
27 |
|
namespace preprocessing { |
28 |
|
namespace passes { |
29 |
|
|
30 |
15340 |
StaticLearning::StaticLearning(PreprocessingPassContext* preprocContext) |
31 |
|
: PreprocessingPass(preprocContext, "static-learning"), |
32 |
15340 |
d_cache(userContext()){}; |
33 |
|
|
34 |
19107 |
PreprocessingPassResult StaticLearning::applyInternal( |
35 |
|
AssertionPipeline* assertionsToPreprocess) |
36 |
|
{ |
37 |
19107 |
d_preprocContext->spendResource(Resource::PreprocessStep); |
38 |
|
|
39 |
38214 |
std::vector<TNode> toProcess; |
40 |
|
|
41 |
136423 |
for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) |
42 |
|
{ |
43 |
117316 |
const Node& n = (*assertionsToPreprocess)[i]; |
44 |
|
|
45 |
|
/* Already processed in this context. */ |
46 |
117316 |
if (d_cache.find(n) != d_cache.end()) |
47 |
|
{ |
48 |
32367 |
continue; |
49 |
|
} |
50 |
|
|
51 |
169898 |
NodeBuilder learned(kind::AND); |
52 |
84949 |
learned << n; |
53 |
|
|
54 |
|
/* Process all assertions in nested AND terms. */ |
55 |
169898 |
std::vector<TNode> assertions; |
56 |
84949 |
flattenAnd(n, assertions); |
57 |
335927 |
for (TNode a : assertions) |
58 |
|
{ |
59 |
250978 |
d_preprocContext->getTheoryEngine()->ppStaticLearn(a, learned); |
60 |
|
} |
61 |
|
|
62 |
84949 |
if (learned.getNumChildren() == 1) |
63 |
|
{ |
64 |
84579 |
learned.clear(); |
65 |
|
} |
66 |
|
else |
67 |
|
{ |
68 |
370 |
assertionsToPreprocess->replace(i, rewrite(learned.constructNode())); |
69 |
|
} |
70 |
|
} |
71 |
38214 |
return PreprocessingPassResult::NO_CONFLICT; |
72 |
|
} |
73 |
|
|
74 |
84949 |
void StaticLearning::flattenAnd(TNode node, std::vector<TNode>& children) |
75 |
|
{ |
76 |
169898 |
std::vector<TNode> visit = {node}; |
77 |
202899 |
do |
78 |
|
{ |
79 |
546198 |
TNode cur = visit.back(); |
80 |
287848 |
visit.pop_back(); |
81 |
|
|
82 |
287848 |
if (d_cache.find(cur) != d_cache.end()) |
83 |
|
{ |
84 |
29498 |
continue; |
85 |
|
} |
86 |
258350 |
d_cache.insert(cur); |
87 |
|
|
88 |
258350 |
if (cur.getKind() == kind::AND) |
89 |
|
{ |
90 |
7372 |
visit.insert(visit.end(), cur.begin(), cur.end()); |
91 |
|
} |
92 |
|
else |
93 |
|
{ |
94 |
250978 |
children.push_back(cur); |
95 |
|
} |
96 |
287848 |
} while (!visit.empty()); |
97 |
84949 |
} |
98 |
|
|
99 |
|
} // namespace passes |
100 |
|
} // namespace preprocessing |
101 |
31137 |
} // namespace cvc5 |