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

Line Exec Source
1
/*********************                                                        */
2
/*! \file inference_generator.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mudathir Mohamed, Andrew Reynolds
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 Inference generator utility
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__BAGS__INFERENCE_GENERATOR_H
18
#define CVC4__THEORY__BAGS__INFERENCE_GENERATOR_H
19
20
#include "expr/node.h"
21
#include "infer_info.h"
22
23
namespace CVC4 {
24
namespace theory {
25
namespace bags {
26
27
class InferenceManager;
28
class SolverState;
29
30
/**
31
 * An inference generator class. This class is used by the core solver to
32
 * generate lemmas
33
 */
34
17988
class InferenceGenerator
35
{
36
 public:
37
  InferenceGenerator(SolverState* state, InferenceManager* im);
38
39
  /**
40
   * @param A is a bag of type (Bag E)
41
   * @param e is a node of type E
42
   * @return an inference that represents the following implication
43
   * (=>
44
   *   true
45
   *   (>= (bag.count e A) 0)
46
   */
47
  InferInfo nonNegativeCount(Node n, Node e);
48
49
  /**
50
   * @param n is (bag x c) of type (Bag E)
51
   * @param e is a node of type E
52
   * @return an inference that represents the following implication
53
   * (=>
54
   *   true
55
   *   (= (bag.count e skolem) c))
56
   *   if e is exactly node x. Node skolem is a fresh variable equals (bag x c).
57
   *   Otherwise the following inference is returned
58
   * (=>
59
   *   true
60
   *   (= (bag.count e skolem) (ite (= e x) c 0)))
61
   */
62
  InferInfo mkBag(Node n, Node e);
63
  /**
64
   * @param n is (= A B) where A, B are bags of type (Bag E), and
65
   * (not (= A B)) is an assertion in the equality engine
66
   * @return an inference that represents the following implication
67
   * (=>
68
   *   (not (= A B))
69
   *   (not (= (count e A) (count e B))))
70
   *   where e is a fresh skolem of type E.
71
   */
72
  InferInfo bagDisequality(Node n);
73
  /**
74
   * @param n is (as emptybag (Bag E))
75
   * @param e is a node of Type E
76
   * @return an inference that represents the following implication
77
   * (=>
78
   *   true
79
   *   (= 0 (count e skolem)))
80
   *   where skolem = (as emptybag (Bag String))
81
   */
82
  InferInfo empty(Node n, Node e);
83
  /**
84
   * @param n is (union_disjoint A B) where A, B are bags of type (Bag E)
85
   * @param e is a node of Type E
86
   * @return an inference that represents the following implication
87
   * (=>
88
   *   true
89
   *   (= (count e skolem)
90
   *      (+ (count e A) (count e B))))
91
   *  where skolem is a fresh variable equals (union_disjoint A B)
92
   */
93
  InferInfo unionDisjoint(Node n, Node e);
94
  /**
95
   * @param n is (union_disjoint A B) where A, B are bags of type (Bag E)
96
   * @param e is a node of Type E
97
   * @return an inference that represents the following implication
98
   * (=>
99
   *   true
100
   *   (=
101
   *     (count e skolem)
102
   *     (ite
103
   *       (> (count e A) (count e B))
104
   *       (count e A)
105
   *       (count e B)))))
106
   * where skolem is a fresh variable equals (union_max A B)
107
   */
108
  InferInfo unionMax(Node n, Node e);
109
  /**
110
   * @param n is (intersection_min A B) where A, B are bags of type (Bag E)
111
   * @param e is a node of Type E
112
   * @return an inference that represents the following implication
113
   * (=>
114
   *   true
115
   *   (=
116
   *     (count e skolem)
117
   *     (ite(
118
   *       (< (count e A) (count e B))
119
   *       (count e A)
120
   *       (count e B)))))
121
   * where skolem is a fresh variable equals (intersection_min A B)
122
   */
123
  InferInfo intersection(Node n, Node e);
124
  /**
125
   * @param n is (difference_subtract A B) where A, B are bags of type (Bag E)
126
   * @param e is a node of Type E
127
   * @return an inference that represents the following implication
128
   * (=>
129
   *   true
130
   *   (=
131
   *     (count e skolem)
132
   *     (ite
133
   *       (>= (count e A) (count e B))
134
   *       (- (count e A) (count e B))
135
   *       0))))
136
   * where skolem is a fresh variable equals (difference_subtract A B)
137
   */
138
  InferInfo differenceSubtract(Node n, Node e);
139
  /**
140
   * @param n is (difference_remove A B) where A, B are bags of type (Bag E)
141
   * @param e is a node of Type E
142
   * @return an inference that represents the following implication
143
   * (=>
144
   *   true
145
   *   (=
146
   *     (count e skolem)
147
   *     (ite
148
   *       (= (count e B) 0)
149
   *       (count e A)
150
   *       0))))
151
   * where skolem is a fresh variable equals (difference_remove A B)
152
   */
153
  InferInfo differenceRemove(Node n, Node e);
154
  /**
155
   * @param n is (duplicate_removal A) where A is a bag of type (Bag E)
156
   * @param e is a node of Type E
157
   * @return an inference that represents the following implication
158
   * (=>
159
   *   true
160
   *   (=
161
   *    (count e skolem)
162
   *    (ite (>= (count e A) 1) 1 0))))
163
   * where skolem is a fresh variable equals (duplicate_removal A)
164
   */
165
  InferInfo duplicateRemoval(Node n, Node e);
166
167
  /**
168
   * @param element of type T
169
   * @param bag of type (bag T)
170
   * @return  a count term (bag.count element bag)
171
   */
172
  Node getMultiplicityTerm(Node element, Node bag);
173
174
 private:
175
  /** generate skolem variable for node n and add it to inferInfo */
176
  Node getSkolem(Node& n, InferInfo& inferInfo);
177
178
  NodeManager* d_nm;
179
  SkolemManager* d_sm;
180
  SolverState* d_state;
181
  /** Pointer to the inference manager */
182
  InferenceManager* d_im;
183
  /** Commonly used constants */
184
  Node d_true;
185
  Node d_zero;
186
  Node d_one;
187
};
188
189
}  // namespace bags
190
}  // namespace theory
191
}  // namespace CVC4
192
193
#endif /* CVC4__THEORY__BAGS__INFERENCE_GENERATOR_H */