Lines Matching refs:NotX
61 auto NotX = Ctx.neg(X); in TEST() local
65 solve({NotX}), in TEST()
72 auto NotX = Ctx.neg(X); in TEST() local
75 expectUnsatisfiable(solve({X, NotX})); in TEST()
94 auto NotX = Ctx.neg(X); in TEST() local
95 auto NotNotX = Ctx.neg(NotX); in TEST()
98 expectUnsatisfiable(solve({NotNotX, NotX})); in TEST()
126 auto NotX = Ctx.neg(X); in TEST() local
127 auto XOrNotX = Ctx.disj(X, NotX); in TEST()
145 auto NotX = Ctx.neg(X); in TEST() local
146 auto XAndNotX = Ctx.conj(X, NotX); in TEST()
165 auto NotX = Ctx.neg(X); in TEST() local
166 auto NotXOrY = Ctx.disj(NotX, Y); in TEST()
168 auto NotXOrNotY = Ctx.disj(NotX, NotY); in TEST()
182 auto NotX = Ctx.neg(X); in TEST() local
183 auto NotXOrY = Ctx.disj(NotX, Y); in TEST()
185 auto NotXOrNotY = Ctx.disj(NotX, NotY); in TEST()
199 auto NotX = Ctx.neg(X); in TEST() local
200 auto NotXOrY = Ctx.disj(NotX, Y); in TEST()
202 auto NotXOrNotY = Ctx.disj(NotX, NotY); in TEST()
213 auto NotX = Ctx.neg(X); in TEST() local
216 auto XIffYDNF = Ctx.disj(Ctx.conj(X, Y), Ctx.conj(NotX, NotY)); in TEST()
280 auto NotX = Ctx.neg(X); in TEST() local
283 expectUnsatisfiable(solve({XEqY, YEqZ, Z, NotX})); in TEST()