1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
|
/********************* */
/*! \file foreign_theory_rewrite.cpp
** \verbatim
** Top contributors (to current version):
** Yoni Zohar
** This file is part of the CVC4 project.
** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
** in the top-level source directory and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief The foreign_theory_rewrite preprocessing pass
**
** Simplifies nodes of one theory using rewrites from another.
**/
#include "preprocessing/passes/foreign_theory_rewrite.h"
#include "expr/node_traversal.h"
#include "preprocessing/assertion_pipeline.h"
#include "preprocessing/preprocessing_pass_context.h"
#include "theory/rewriter.h"
#include "theory/strings/arith_entail.h"
namespace cvc5 {
namespace preprocessing {
namespace passes {
using namespace cvc5::theory;
ForeignTheoryRewrite::ForeignTheoryRewrite(PreprocessingPassContext* preprocContext)
: PreprocessingPass(preprocContext, "foreign-theory-rewrite"),
d_cache(preprocContext->getUserContext()){};
Node ForeignTheoryRewrite::simplify(Node n)
{
std::vector<Node> toVisit;
n = Rewriter::rewrite(n);
toVisit.push_back(n);
// traverse n and rewrite until fixpoint
while (!toVisit.empty())
{
Node current = toVisit.back();
// split according to three cases:
// 1. We have not visited this node
// 2. We visited it but did not process it
// 3. We already processed and cached the node
if (d_cache.find(current) == d_cache.end())
{
// current is seen for the first time.
// mark it by assigning a null node
// and add its children to toVisit
d_cache[current] = Node();
toVisit.insert(toVisit.end(), current.begin(), current.end());
}
else if (d_cache[current].get().isNull())
{
// current was seen but was not processed.
// (a) remove from toVisit
toVisit.pop_back();
// (b) Reconstruct it with processed children
std::vector<Node> processedChildren;
for (Node child : current)
{
Assert(d_cache.find(child) != d_cache.end());
Assert(!d_cache[child].get().isNull());
processedChildren.push_back(d_cache[child]);
}
Node reconstruction = reconstructNode(current, processedChildren);
// (c) process the node and store the result in the cache
Node result = foreignRewrite(reconstruction);
d_cache[current] = result;
// (d) add the result to toVisit, unless it is the same as current
if (current != result)
{
toVisit.push_back(result);
}
}
else
{
// current was already processed
// remove from toVisit and skip
toVisit.pop_back();
}
}
return d_cache[n];
}
Node ForeignTheoryRewrite::foreignRewrite(Node n)
{
// n is a rewritten node, and so GT, LT, LEQ
// should have been eliminated
Assert(n.getKind() != kind::GT);
Assert(n.getKind() != kind::LT);
Assert(n.getKind() != kind::LEQ);
// apply rewrites according to the structure of n
if (n.getKind() == kind::GEQ)
{
return rewriteStringsGeq(n);
}
return n;
}
Node ForeignTheoryRewrite::rewriteStringsGeq(Node n)
{
// check if the node can be simplified to true
if (theory::strings::ArithEntail::check(n[0], n[1], false))
{
return NodeManager::currentNM()->mkConst(true);
}
return n;
}
Node ForeignTheoryRewrite::reconstructNode(Node originalNode,
std::vector<Node> newChildren)
{
// Nodes with no children are reconstructed to themselves
if (originalNode.getNumChildren() == 0)
{
Assert(newChildren.empty());
return originalNode;
}
// re-build the node with the same kind and new children
kind::Kind_t k = originalNode.getKind();
NodeBuilder<> builder(k);
// special case for parameterized nodes
if (originalNode.getMetaKind() == kind::metakind::PARAMETERIZED)
{
builder << originalNode.getOperator();
}
// reconstruction
for (Node child : newChildren)
{
builder << child;
}
return builder.constructNode();
}
PreprocessingPassResult ForeignTheoryRewrite::applyInternal(
AssertionPipeline* assertionsToPreprocess)
{
for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
{
assertionsToPreprocess->replace(
i, Rewriter::rewrite(simplify((*assertionsToPreprocess)[i])));
}
return PreprocessingPassResult::NO_CONFLICT;
}
} // namespace passes
} // namespace preprocessing
} // namespace cvc5
|
