Lines Matching refs:conj

47   auto B = Ctx.conj(Ctx.atom(), Ctx.atom());  in TEST()
93   auto B = Ctx.disj(Ctx.conj(B0, Ctx.neg(B1)), Ctx.conj(Ctx.neg(B0), B1));  in TEST()
110   auto B = Ctx.conj(  in TEST()
113                Ctx.conj(Ctx.atom(), Ctx.disj(Ctx.atom(), Ctx.atom()))));  in TEST()
143   auto B = Ctx.disj(Ctx.conj(Cond, Ctx.conj(Then, Ctx.neg(Else))),  in TEST()
144                     Ctx.conj(Ctx.neg(Cond), Ctx.conj(Ctx.neg(Then), Else)));  in TEST()
169   auto B = Ctx.disj(Ctx.conj(False, Ctx.atom()), Ctx.disj(True, Ctx.atom()));  in TEST()
305   auto Iff = Ctx.conj(Ctx.disj(Ctx.neg(B0), B1), Ctx.disj(B0, Ctx.neg(B1)));  in TEST()
337   auto XOR = Ctx.disj(Ctx.conj(B0, Ctx.neg(B1)), Ctx.conj(Ctx.neg(B0), B1));  in TEST()
370   auto B = Ctx.disj(Ctx.conj(Cond, Ctx.conj(Then, Ctx.neg(Else))),  in TEST()
371                     Ctx.conj(Ctx.neg(Cond), Ctx.conj(Ctx.neg(Then), Else)));  in TEST()
413       Ctx.disj(Ctx.neg(Ctx.conj(ThisIntEqZero, OtherIntEqZero)), IntsAreEq);  in TEST()