183   llvm::DenseSet<BoolValue *> Constraints;  in TEST()  local
184   EXPECT_THAT(debugString(Constraints), StrEq(""));  in TEST()
189   llvm::DenseSet<BoolValue *> Constraints;  in TEST()  local
192   Constraints.insert(Ctx.disj(X, Y));  in TEST()
193   Constraints.insert(Ctx.disj(X, Ctx.neg(Y)));  in TEST()
203   EXPECT_THAT(debugString(Constraints, {{X, "X"}, {Y, "Y"}}),  in TEST()
207 Solver::Result CheckSAT(std::vector<BoolValue *> Constraints) {  in CheckSAT()  argument
208   llvm::DenseSet<BoolValue *> ConstraintsSet(Constraints.begin(),  in CheckSAT()
209                                              Constraints.end());  in CheckSAT()
216   std::vector<BoolValue *> Constraints({Ctx.atom()});  in TEST()  local
217   auto Result = CheckSAT(Constraints);  in TEST()
228   EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));  in TEST()
235   std::vector<BoolValue *> Constraints({B0, Ctx.neg(B0)});  in TEST()  local
236   auto Result = CheckSAT(Constraints);  in TEST()
249   EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));  in TEST()
255   std::vector<BoolValue *> Constraints({Ctx.atom(), Ctx.atom()});  in TEST()  local
256   auto Result = CheckSAT(Constraints);  in TEST()
270   EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));  in TEST()
279   std::vector<BoolValue *> Constraints({B0, Impl});  in TEST()  local
280   auto Result = CheckSAT(Constraints);  in TEST()
297   EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));  in TEST()
306   std::vector<BoolValue *> Constraints({B0, Iff});  in TEST()  local
307   auto Result = CheckSAT(Constraints);  in TEST()
329   EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));  in TEST()
338   std::vector<BoolValue *> Constraints({B0, XOR});  in TEST()  local
339   auto Result = CheckSAT(Constraints);  in TEST()
361   EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));  in TEST()
372   std::vector<BoolValue *> Constraints({Cond, B});  in TEST()  local
373   auto Result = CheckSAT(Constraints);  in TEST()
401   EXPECT_THAT(debugString(Constraints, Result,  in TEST()
414   std::vector<BoolValue *> Constraints(  in TEST()  local
416   auto Result = CheckSAT(Constraints);  in TEST()
439   EXPECT_THAT(debugString(Constraints, Result,  in TEST()