ea396e32cec361c9523df9be60ace022c6ad97e0
3 #include "cvc4_private.h"
4 #include "theory/theory.h"
5 #include "context/context.h"
11 struct CoreRewriteRules
{
14 static inline Node
apply(Node node
) { return node
; }
15 static inline bool applies(Node node
) { return false; }
18 struct ConcatFlatten
{
19 static Node
apply(Node node
);
20 static bool applies(Node node
);
23 struct ConcatExtractMerge
{
24 static Node
apply(Node node
);
25 static bool applies(Node node
);
28 struct ConcatConstantMerge
{
29 static Node
apply(Node node
);
30 static bool applies(Node node
);
33 struct ExtractExtract
{
34 static Node
apply(Node node
);
35 static bool applies(Node node
);
39 static Node
apply(Node node
);
40 static bool applies(Node node
);
43 struct ExtractConcat
{
44 static Node
apply(Node node
);
45 static bool applies(Node node
);
48 struct ExtractConstant
{
49 static Node
apply(Node node
);
50 static bool applies(Node node
);
54 static Node
apply(Node node
);
55 static bool applies(Node node
);
59 static Node
apply(Node node
);
60 static bool applies(Node node
);
65 template<Kind kind
, typename Rule
>
66 struct ApplyRuleToChildren
{
68 static Node
apply(Node node
) {
69 if (node
.getKind() != kind
) {
70 if (Rule::applies(node
)) return Rule::apply(node
);
73 NodeBuilder
<> result(kind
);
74 for (unsigned i
= 0, end
= node
.getNumChildren(); i
< end
; ++ i
) {
75 if (Rule::applies(node
[i
])) result
<< Rule::apply(node
[i
]);
76 else result
<< node
[i
];
81 static bool applies(Node node
) {
82 if (node
.getKind() == kind
) return true;
83 return Rule::applies(node
);
92 typename R3
= CoreRewriteRules::EmptyRule
,
93 typename R4
= CoreRewriteRules::EmptyRule
,
94 typename R5
= CoreRewriteRules::EmptyRule
,
95 typename R6
= CoreRewriteRules::EmptyRule
,
96 typename R7
= CoreRewriteRules::EmptyRule
98 struct LinearRewriteStrategy
{
99 static Node
apply(Node node
) {
101 if (R1::applies(current
)) current
= R1::apply(current
);
102 if (R2::applies(current
)) current
= R2::apply(current
);
103 if (R3::applies(current
)) current
= R3::apply(current
);
104 if (R4::applies(current
)) current
= R4::apply(current
);
105 if (R5::applies(current
)) current
= R5::apply(current
);
106 if (R6::applies(current
)) current
= R6::apply(current
);
107 if (R7::applies(current
)) current
= R7::apply(current
);
112 } // End namespace bv
113 } // End namespace theory
114 } // End namespace CVC4