33 Solver::Result solve(llvm::DenseSet<BoolValue *> Vals) {  in solve()  function
34   return WatchedLiteralsSolver().solve(std::move(Vals));  in solve()
54       solve({X}),  in TEST()
65       solve({NotX}),  in TEST()
75   expectUnsatisfiable(solve({X, NotX}));  in TEST()
86       solve({X, NotY}),  in TEST()
98   expectUnsatisfiable(solve({NotNotX, NotX}));  in TEST()
109   expectUnsatisfiable(solve({NotXOrY, XOrY}));  in TEST()
120   expectUnsatisfiable(solve({NotXAndY, XAndY}));  in TEST()
130   expectSatisfiable(solve({XOrNotX}), _);  in TEST()
139   expectSatisfiable(solve({XOrX}), _);  in TEST()
149   expectUnsatisfiable(solve({XAndNotX}));  in TEST()
158   expectSatisfiable(solve({XAndX}), _);  in TEST()
172       solve({NotXOrY, NotXOrNotY}),  in TEST()
189       solve({XOrY, NotXOrY, NotXOrNotY}),  in TEST()
206   expectUnsatisfiable(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}));  in TEST()
220   expectUnsatisfiable(solve({NotEquivalent}));  in TEST()
229   expectSatisfiable(solve({XEqX}), _);  in TEST()
240       solve({XEqY}),  in TEST()
257       solve({XEqY, X, Y}),  in TEST()
270   expectUnsatisfiable(solve({XEqY, X, NotY}));  in TEST()
283   expectUnsatisfiable(solve({XEqY, YEqZ, Z, NotX}));  in TEST()
300   expectSatisfiable(solve({A, B}), _);  in TEST()
311   expectUnsatisfiable(solve({XEqY, X, NotY}));  in TEST()
323   expectUnsatisfiable(solve({NotEquivalent}));  in TEST()
334   expectUnsatisfiable(solve({XImplY, XAndNotY}));  in TEST()