Lines Matching refs:NotY
82 auto NotY = Ctx.neg(Y); in TEST() local
86 solve({X, NotY}), in TEST()
167 auto NotY = Ctx.neg(Y); in TEST() local
168 auto NotXOrNotY = Ctx.disj(NotX, NotY); in TEST()
184 auto NotY = Ctx.neg(Y); in TEST() local
185 auto NotXOrNotY = Ctx.disj(NotX, NotY); in TEST()
201 auto NotY = Ctx.neg(Y); in TEST() local
202 auto NotXOrNotY = Ctx.disj(NotX, NotY); in TEST()
203 auto XOrNotY = Ctx.disj(X, NotY); in TEST()
214 auto NotY = Ctx.neg(Y); in TEST() local
216 auto XIffYDNF = Ctx.disj(Ctx.conj(X, Y), Ctx.conj(NotX, NotY)); in TEST()
267 auto NotY = Ctx.neg(Y); in TEST() local
270 expectUnsatisfiable(solve({XEqY, X, NotY})); in TEST()
308 auto NotY = Ctx.neg(Y); in TEST() local
311 expectUnsatisfiable(solve({XEqY, X, NotY})); in TEST()