GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bags/bags_rewriter.h Lines: 2 2 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bags_rewriter.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mudathir Mohamed
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief Bags theory rewriter.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H
18
#define CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H
19
20
#include "theory/bags/rewrites.h"
21
#include "theory/theory_rewriter.h"
22
#include "util/statistics_registry.h"
23
#include "util/stats_histogram.h"
24
25
namespace CVC4 {
26
namespace theory {
27
namespace bags {
28
29
/** a class represents the result of rewriting bag nodes */
30
9246
struct BagsRewriteResponse
31
{
32
  BagsRewriteResponse();
33
  BagsRewriteResponse(Node n, Rewrite rewrite);
34
  BagsRewriteResponse(const BagsRewriteResponse& r);
35
  /** the rewritten node */
36
  Node d_node;
37
  /** type of rewrite used by bags */
38
  Rewrite d_rewrite;
39
40
}; /* struct BagsRewriteResponse */
41
42
9118
class BagsRewriter : public TheoryRewriter
43
{
44
 public:
45
  BagsRewriter(IntegralHistogramStat<Rewrite>* statistics = nullptr);
46
47
  /**
48
   * postRewrite nodes with kinds: MK_BAG, BAG_COUNT, UNION_MAX, UNION_DISJOINT,
49
   * INTERSECTION_MIN, DIFFERENCE_SUBTRACT, DIFFERENCE_REMOVE, BAG_CHOOSE,
50
   * BAG_CARD, BAG_IS_SINGLETON.
51
   * See the rewrite rules for these kinds below.
52
   */
53
  RewriteResponse postRewrite(TNode n) override;
54
  /**
55
   * preRewrite nodes with kinds: EQUAL, SUBBAG.
56
   * See the rewrite rules for these kinds below.
57
   */
58
  RewriteResponse preRewrite(TNode n) override;
59
60
 private:
61
  /**
62
   * rewrites for n include:
63
   * - (= A A) = true where A is a bag
64
   */
65
  BagsRewriteResponse preRewriteEqual(const TNode& n) const;
66
67
  /**
68
   * rewrites for n include:
69
   * - (bag.is_included A B) = ((difference_subtract A B) == emptybag)
70
   */
71
  BagsRewriteResponse rewriteSubBag(const TNode& n) const;
72
73
  /**
74
   * rewrites for n include:
75
   * - (bag x 0) = (emptybag T) where T is the type of x
76
   * - (bag x (-c)) = (emptybag T) where T is the type of x, and c > 0 is a
77
   *   constant
78
   * - otherwise = n
79
   */
80
  BagsRewriteResponse rewriteMakeBag(const TNode& n) const;
81
82
  /**
83
   * rewrites for n include:
84
   * - (bag.count x emptybag) = 0
85
   * - (bag.count x (bag x c) = c
86
   * - otherwise = n
87
   */
88
  BagsRewriteResponse rewriteBagCount(const TNode& n) const;
89
90
  /**
91
   *  rewrites for n include:
92
   *  - (duplicate_removal (bag x n)) = (bag x 1)
93
   *     where n is a positive constant
94
   */
95
  BagsRewriteResponse rewriteDuplicateRemoval(const TNode& n) const;
96
97
  /**
98
   * rewrites for n include:
99
   * - (union_max A emptybag) = A
100
   * - (union_max emptybag A) = A
101
   * - (union_max A A) = A
102
   * - (union_max A (union_max A B)) = (union_max A B)
103
   * - (union_max A (union_max B A)) = (union_max B A)
104
   * - (union_max (union_max A B) A) = (union_max A B)
105
   * - (union_max (union_max B A) A) = (union_max B A)
106
   * - (union_max A (union_disjoint A B)) = (union_disjoint A B)
107
   * - (union_max A (union_disjoint B A)) = (union_disjoint B A)
108
   * - (union_max (union_disjoint A B) A) = (union_disjoint A B)
109
   * - (union_max (union_disjoint B A) A) = (union_disjoint B A)
110
   * - otherwise = n
111
   */
112
  BagsRewriteResponse rewriteUnionMax(const TNode& n) const;
113
114
  /**
115
   * rewrites for n include:
116
   * - (union_disjoint A emptybag) = A
117
   * - (union_disjoint emptybag A) = A
118
   * - (union_disjoint (union_max A B) (intersection_min A B)) =
119
   *         (union_disjoint A B) // sum(a,b) = max(a,b) + min(a,b)
120
   * - other permutations of the above like swapping A and B, or swapping
121
   *   intersection_min and union_max
122
   * - otherwise = n
123
   */
124
  BagsRewriteResponse rewriteUnionDisjoint(const TNode& n) const;
125
126
  /**
127
   * rewrites for n include:
128
   * - (intersection_min A emptybag) = emptybag
129
   * - (intersection_min emptybag A) = emptybag
130
   * - (intersection_min A A) = A
131
   * - (intersection_min A (union_disjoint A B)) = A
132
   * - (intersection_min A (union_disjoint B A)) = A
133
   * - (intersection_min (union_disjoint A B) A) = A
134
   * - (intersection_min (union_disjoint B A) A) = A
135
   * - (intersection_min A (union_max A B)) = A
136
   * - (intersection_min A (union_max B A)) = A
137
   * - (intersection_min (union_max A B) A) = A
138
   * - (intersection_min (union_max B A) A) = A
139
   * - otherwise = n
140
   */
141
  BagsRewriteResponse rewriteIntersectionMin(const TNode& n) const;
142
143
  /**
144
   * rewrites for n include:
145
   * - (difference_subtract A emptybag) = A
146
   * - (difference_subtract emptybag A) = emptybag
147
   * - (difference_subtract A A) = emptybag
148
   * - (difference_subtract (union_disjoint A B) A) = B
149
   * - (difference_subtract (union_disjoint B A) A) = B
150
   * - (difference_subtract A (union_disjoint A B)) = emptybag
151
   * - (difference_subtract A (union_disjoint B A)) = emptybag
152
   * - (difference_subtract A (union_max A B)) = emptybag
153
   * - (difference_subtract A (union_max B A)) = emptybag
154
   * - (difference_subtract (intersection_min A B) A) = emptybag
155
   * - (difference_subtract (intersection_min B A) A) = emptybag
156
   * - otherwise = n
157
   */
158
  BagsRewriteResponse rewriteDifferenceSubtract(const TNode& n) const;
159
160
  /**
161
   * rewrites for n include:
162
   * - (difference_remove A emptybag) = A
163
   * - (difference_remove emptybag A) = emptybag
164
   * - (difference_remove A A) = emptybag
165
   * - (difference_remove A (union_disjoint A B)) = emptybag
166
   * - (difference_remove A (union_disjoint B A)) = emptybag
167
   * - (difference_remove A (union_max A B)) = emptybag
168
   * - (difference_remove A (union_max B A)) = emptybag
169
   * - (difference_remove (intersection_min A B) A) = emptybag
170
   * - (difference_remove (intersection_min B A) A) = emptybag
171
   * - otherwise = n
172
   */
173
  BagsRewriteResponse rewriteDifferenceRemove(const TNode& n) const;
174
  /**
175
   * rewrites for n include:
176
   * - (bag.choose (bag x c)) = x where c is a constant > 0
177
   * - otherwise = n
178
   */
179
  BagsRewriteResponse rewriteChoose(const TNode& n) const;
180
  /**
181
   * rewrites for n include:
182
   * - (bag.card (bag x c)) = c where c is a constant > 0
183
   * - (bag.card (union-disjoint A B)) = (+ (bag.card A) (bag.card B))
184
   * - otherwise = n
185
   */
186
  BagsRewriteResponse rewriteCard(const TNode& n) const;
187
188
  /**
189
   * rewrites for n include:
190
   * - (bag.is_singleton (bag x c)) = (c == 1)
191
   */
192
  BagsRewriteResponse rewriteIsSingleton(const TNode& n) const;
193
194
  /**
195
   *  rewrites for n include:
196
   *  - (bag.from_set (singleton (singleton_op Int) x)) = (bag x 1)
197
   */
198
  BagsRewriteResponse rewriteFromSet(const TNode& n) const;
199
200
  /**
201
   *  rewrites for n include:
202
   *  - (bag.to_set (bag x n)) = (singleton (singleton_op T) x)
203
   *     where n is a positive constant and T is the type of the bag's elements
204
   */
205
  BagsRewriteResponse rewriteToSet(const TNode& n) const;
206
207
  /**
208
   *  rewrites for n include:
209
   *  - (= A A) = true
210
   *  - (= A B) = false if A and B are different bag constants
211
   *  - (= B A) = (= A B) if A < B and at least one of A or B is not a constant
212
   */
213
  BagsRewriteResponse postRewriteEqual(const TNode& n) const;
214
215
 private:
216
  /** Reference to the rewriter statistics. */
217
  NodeManager* d_nm;
218
  Node d_zero;
219
  Node d_one;
220
  /** Reference to the rewriter statistics. */
221
  IntegralHistogramStat<Rewrite>* d_statistics;
222
}; /* class TheoryBagsRewriter */
223
224
}  // namespace bags
225
}  // namespace theory
226
}  // namespace CVC4
227
228
#endif /* CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H */