26   ConstraintContext Ctx;  in TEST()  local
27   auto B = Ctx.atom();  in TEST()
36   ConstraintContext Ctx;  in TEST()  local
37   auto B = Ctx.neg(Ctx.atom());  in TEST()
46   ConstraintContext Ctx;  in TEST()  local
47   auto B = Ctx.conj(Ctx.atom(), Ctx.atom());  in TEST()
57   ConstraintContext Ctx;  in TEST()  local
58   auto B = Ctx.disj(Ctx.atom(), Ctx.atom());  in TEST()
68   ConstraintContext Ctx;  in TEST()  local
69   auto B = Ctx.impl(Ctx.atom(), Ctx.atom());  in TEST()
79   ConstraintContext Ctx;  in TEST()  local
80   auto B = Ctx.iff(Ctx.atom(), Ctx.atom());  in TEST()
90   ConstraintContext Ctx;  in TEST()  local
91   auto B0 = Ctx.atom();  in TEST()
92   auto B1 = Ctx.atom();  in TEST()
93   auto B = Ctx.disj(Ctx.conj(B0, Ctx.neg(B1)), Ctx.conj(Ctx.neg(B0), B1));  in TEST()
109   ConstraintContext Ctx;  in TEST()  local
110   auto B = Ctx.conj(  in TEST()
111       Ctx.atom(),  in TEST()
112       Ctx.disj(Ctx.atom(),  in TEST()
113                Ctx.conj(Ctx.atom(), Ctx.disj(Ctx.atom(), Ctx.atom()))));  in TEST()
129   ConstraintContext Ctx;  in TEST()  local
130   auto True = cast<AtomicBoolValue>(Ctx.atom());  in TEST()
139   ConstraintContext Ctx;  in TEST()  local
140   auto Cond = cast<AtomicBoolValue>(Ctx.atom());  in TEST()
141   auto Then = cast<AtomicBoolValue>(Ctx.atom());  in TEST()
142   auto Else = cast<AtomicBoolValue>(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()
166   ConstraintContext Ctx;  in TEST()  local
167   auto True = cast<AtomicBoolValue>(Ctx.atom());  in TEST()
168   auto False = cast<AtomicBoolValue>(Ctx.atom());  in TEST()
169   auto B = Ctx.disj(Ctx.conj(False, Ctx.atom()), Ctx.disj(True, Ctx.atom()));  in TEST()
188   ConstraintContext Ctx;  in TEST()  local
190   auto X = cast<AtomicBoolValue>(Ctx.atom());  in TEST()
191   auto Y = cast<AtomicBoolValue>(Ctx.atom());  in TEST()
192   Constraints.insert(Ctx.disj(X, Y));  in TEST()
193   Constraints.insert(Ctx.disj(X, Ctx.neg(Y)));  in TEST()
215   ConstraintContext Ctx;  in TEST()  local
216   std::vector<BoolValue *> Constraints({Ctx.atom()});  in TEST()
233   ConstraintContext Ctx;  in TEST()  local
234   auto B0 = Ctx.atom();  in TEST()
235   std::vector<BoolValue *> Constraints({B0, Ctx.neg(B0)});  in TEST()
254   ConstraintContext Ctx;  in TEST()  local
255   std::vector<BoolValue *> Constraints({Ctx.atom(), Ctx.atom()});  in TEST()
275   ConstraintContext Ctx;  in TEST()  local
276   auto B0 = Ctx.atom();  in TEST()
277   auto B1 = Ctx.atom();  in TEST()
278   auto Impl = Ctx.disj(Ctx.neg(B0), B1);  in TEST()
302   ConstraintContext Ctx;  in TEST()  local
303   auto B0 = Ctx.atom();  in TEST()
304   auto B1 = Ctx.atom();  in TEST()
305   auto Iff = Ctx.conj(Ctx.disj(Ctx.neg(B0), B1), Ctx.disj(B0, Ctx.neg(B1)));  in TEST()
334   ConstraintContext Ctx;  in TEST()  local
335   auto B0 = Ctx.atom();  in TEST()
336   auto B1 = Ctx.atom();  in TEST()
337   auto XOR = Ctx.disj(Ctx.conj(B0, Ctx.neg(B1)), Ctx.conj(Ctx.neg(B0), B1));  in TEST()
366   ConstraintContext Ctx;  in TEST()  local
367   auto Cond = cast<AtomicBoolValue>(Ctx.atom());  in TEST()
368   auto Then = cast<AtomicBoolValue>(Ctx.atom());  in TEST()
369   auto Else = cast<AtomicBoolValue>(Ctx.atom());  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()
408   ConstraintContext Ctx;  in TEST()  local
409   auto IntsAreEq = cast<AtomicBoolValue>(Ctx.atom());  in TEST()
410   auto ThisIntEqZero = cast<AtomicBoolValue>(Ctx.atom());  in TEST()
411   auto OtherIntEqZero = cast<AtomicBoolValue>(Ctx.atom());  in TEST()
413       Ctx.disj(Ctx.neg(Ctx.conj(ThisIntEqZero, OtherIntEqZero)), IntsAreEq);  in TEST()
415       {ThisIntEqZero, Ctx.neg(IntsAreEq), BothZeroImpliesEQ});  in TEST()