Lines Matching refs:Ctx
49 ConstraintContext Ctx; in TEST() local
50 auto X = Ctx.atom(); in TEST()
59 ConstraintContext Ctx; in TEST() local
60 auto X = Ctx.atom(); in TEST()
61 auto NotX = Ctx.neg(X); in TEST()
70 ConstraintContext Ctx; in TEST() local
71 auto X = Ctx.atom(); in TEST()
72 auto NotX = Ctx.neg(X); in TEST()
79 ConstraintContext Ctx; in TEST() local
80 auto X = Ctx.atom(); in TEST()
81 auto Y = Ctx.atom(); in TEST()
82 auto NotY = Ctx.neg(Y); in TEST()
92 ConstraintContext Ctx; in TEST() local
93 auto X = Ctx.atom(); in TEST()
94 auto NotX = Ctx.neg(X); in TEST()
95 auto NotNotX = Ctx.neg(NotX); in TEST()
102 ConstraintContext Ctx; in TEST() local
103 auto X = Ctx.atom(); in TEST()
104 auto Y = Ctx.atom(); in TEST()
105 auto XOrY = Ctx.disj(X, Y); in TEST()
106 auto NotXOrY = Ctx.neg(XOrY); in TEST()
113 ConstraintContext Ctx; in TEST() local
114 auto X = Ctx.atom(); in TEST()
115 auto Y = Ctx.atom(); in TEST()
116 auto XAndY = Ctx.conj(X, Y); in TEST()
117 auto NotXAndY = Ctx.neg(XAndY); in TEST()
124 ConstraintContext Ctx; in TEST() local
125 auto X = Ctx.atom(); in TEST()
126 auto NotX = Ctx.neg(X); in TEST()
127 auto XOrNotX = Ctx.disj(X, NotX); in TEST()
134 ConstraintContext Ctx; in TEST() local
135 auto X = Ctx.atom(); in TEST()
136 auto XOrX = Ctx.disj(X, X); in TEST()
143 ConstraintContext Ctx; in TEST() local
144 auto X = Ctx.atom(); in TEST()
145 auto NotX = Ctx.neg(X); in TEST()
146 auto XAndNotX = Ctx.conj(X, NotX); in TEST()
153 ConstraintContext Ctx; in TEST() local
154 auto X = Ctx.atom(); in TEST()
155 auto XAndX = Ctx.conj(X, X); in TEST()
162 ConstraintContext Ctx; in TEST() local
163 auto X = Ctx.atom(); in TEST()
164 auto Y = Ctx.atom(); in TEST()
165 auto NotX = Ctx.neg(X); in TEST()
166 auto NotXOrY = Ctx.disj(NotX, Y); in TEST()
167 auto NotY = Ctx.neg(Y); in TEST()
168 auto NotXOrNotY = Ctx.disj(NotX, NotY); in TEST()
178 ConstraintContext Ctx; in TEST() local
179 auto X = Ctx.atom(); in TEST()
180 auto Y = Ctx.atom(); in TEST()
181 auto XOrY = Ctx.disj(X, Y); in TEST()
182 auto NotX = Ctx.neg(X); in TEST()
183 auto NotXOrY = Ctx.disj(NotX, Y); in TEST()
184 auto NotY = Ctx.neg(Y); in TEST()
185 auto NotXOrNotY = Ctx.disj(NotX, NotY); in TEST()
195 ConstraintContext Ctx; in TEST() local
196 auto X = Ctx.atom(); in TEST()
197 auto Y = Ctx.atom(); in TEST()
198 auto XOrY = Ctx.disj(X, Y); in TEST()
199 auto NotX = Ctx.neg(X); in TEST()
200 auto NotXOrY = Ctx.disj(NotX, Y); in TEST()
201 auto NotY = Ctx.neg(Y); in TEST()
202 auto NotXOrNotY = Ctx.disj(NotX, NotY); in TEST()
203 auto XOrNotY = Ctx.disj(X, NotY); in TEST()
210 ConstraintContext Ctx; in TEST() local
211 auto X = Ctx.atom(); in TEST()
212 auto Y = Ctx.atom(); in TEST()
213 auto NotX = Ctx.neg(X); in TEST()
214 auto NotY = Ctx.neg(Y); in TEST()
215 auto XIffY = Ctx.iff(X, Y); in TEST()
216 auto XIffYDNF = Ctx.disj(Ctx.conj(X, Y), Ctx.conj(NotX, NotY)); in TEST()
217 auto NotEquivalent = Ctx.neg(Ctx.iff(XIffY, XIffYDNF)); in TEST()
224 ConstraintContext Ctx; in TEST() local
225 auto X = Ctx.atom(); in TEST()
226 auto XEqX = Ctx.iff(X, X); in TEST()
233 ConstraintContext Ctx; in TEST() local
234 auto X = Ctx.atom(); in TEST()
235 auto Y = Ctx.atom(); in TEST()
236 auto XEqY = Ctx.iff(X, Y); in TEST()
250 ConstraintContext Ctx; in TEST() local
251 auto X = Ctx.atom(); in TEST()
252 auto Y = Ctx.atom(); in TEST()
253 auto XEqY = Ctx.iff(X, Y); in TEST()
263 ConstraintContext Ctx; in TEST() local
264 auto X = Ctx.atom(); in TEST()
265 auto Y = Ctx.atom(); in TEST()
266 auto XEqY = Ctx.iff(X, Y); in TEST()
267 auto NotY = Ctx.neg(Y); in TEST()
274 ConstraintContext Ctx; in TEST() local
275 auto X = Ctx.atom(); in TEST()
276 auto Y = Ctx.atom(); in TEST()
277 auto Z = Ctx.atom(); in TEST()
278 auto XEqY = Ctx.iff(X, Y); in TEST()
279 auto YEqZ = Ctx.iff(Y, Z); in TEST()
280 auto NotX = Ctx.neg(X); in TEST()
287 ConstraintContext Ctx; in TEST() local
288 auto X = Ctx.atom(); in TEST()
289 auto Y = Ctx.atom(); in TEST()
290 auto Z = Ctx.atom(); in TEST()
291 auto W = Ctx.atom(); in TEST()
294 auto A = Ctx.iff(Ctx.neg(Ctx.disj(X, Y)), Ctx.conj(Ctx.neg(X), Ctx.neg(Y))); in TEST()
297 auto B = Ctx.iff(Ctx.neg(Ctx.conj(Z, W)), Ctx.disj(Ctx.neg(Z), Ctx.neg(W))); in TEST()
304 ConstraintContext Ctx; in TEST() local
305 auto X = Ctx.atom(); in TEST()
306 auto Y = Ctx.atom(); in TEST()
307 auto XEqY = Ctx.iff(X, Y); in TEST()
308 auto NotY = Ctx.neg(Y); in TEST()
315 ConstraintContext Ctx; in TEST() local
316 auto X = Ctx.atom(); in TEST()
317 auto Y = Ctx.atom(); in TEST()
318 auto XImpliesY = Ctx.impl(X, Y); in TEST()
319 auto XImpliesYDNF = Ctx.disj(Ctx.neg(X), Y); in TEST()
320 auto NotEquivalent = Ctx.neg(Ctx.iff(XImpliesY, XImpliesYDNF)); in TEST()
327 ConstraintContext Ctx; in TEST() local
328 auto X = Ctx.atom(); in TEST()
329 auto Y = Ctx.atom(); in TEST()
330 auto *XImplY = Ctx.impl(X, Y); in TEST()
331 auto *XAndNotY = Ctx.conj(X, Ctx.neg(Y)); in TEST()