26   ConstraintContext Ctx;  in TEST()  local
27   auto B = Ctx.atom();  in TEST()
34   ConstraintContext Ctx;  in TEST()  local
35   EXPECT_EQ("true", llvm::to_string(*Ctx.literal(true)));  in TEST()
36   EXPECT_EQ("false", llvm::to_string(*Ctx.literal(false)));  in TEST()
40   ConstraintContext Ctx;  in TEST()  local
41   auto B = Ctx.neg(Ctx.atom());  in TEST()
48   ConstraintContext Ctx;  in TEST()  local
49   auto *V0 = Ctx.atom();  in TEST()
50   auto *V1 = Ctx.atom();  in TEST()
51   EXPECT_EQ("(V0 & V1)", llvm::to_string(*Ctx.conj(V0, V1)));  in TEST()
55   ConstraintContext Ctx;  in TEST()  local
56   auto *V0 = Ctx.atom();  in TEST()
57   auto *V1 = Ctx.atom();  in TEST()
58   EXPECT_EQ("(V0 | V1)", llvm::to_string(*Ctx.disj(V0, V1)));  in TEST()
62   ConstraintContext Ctx;  in TEST()  local
63   auto *V0 = Ctx.atom();  in TEST()
64   auto *V1 = Ctx.atom();  in TEST()
65   EXPECT_EQ("(V0 => V1)", llvm::to_string(*Ctx.impl(V0, V1)));  in TEST()
69   ConstraintContext Ctx;  in TEST()  local
70   auto *V0 = Ctx.atom();  in TEST()
71   auto *V1 = Ctx.atom();  in TEST()
72   EXPECT_EQ("(V0 = V1)", llvm::to_string(*Ctx.iff(V0, V1)));  in TEST()
76   ConstraintContext Ctx;  in TEST()  local
77   auto V0 = Ctx.atom();  in TEST()
78   auto V1 = Ctx.atom();  in TEST()
79   auto B = Ctx.disj(Ctx.conj(V0, Ctx.neg(V1)), Ctx.conj(Ctx.neg(V0), V1));  in TEST()
86   ConstraintContext Ctx;  in TEST()  local
87   auto V0 = Ctx.atom();  in TEST()
88   auto V1 = Ctx.atom();  in TEST()
89   auto V2 = Ctx.atom();  in TEST()
90   auto V3 = Ctx.atom();  in TEST()
91   auto V4 = Ctx.atom();  in TEST()
92   auto B = Ctx.conj(V0, Ctx.disj(V1, Ctx.conj(V2, Ctx.disj(V3, V4))));  in TEST()
99   ConstraintContext Ctx;  in TEST()  local
100   auto X = Ctx.atom();  in TEST()
101   auto Y = Ctx.atom();  in TEST()
105   auto V2 = Ctx.atom();  in TEST()
106   auto V3 = Ctx.atom();  in TEST()
107   auto B = Ctx.disj(Ctx.conj(Y, V2), Ctx.disj(X, V3));  in TEST()