172     llvm::SetVector<const Formula *> Constraints) {  in querySolver()  argument
173   return S.solve(Constraints.getArrayRef());  in querySolver()
184   // to show that assuming `F` is false makes the constraints induced by the  in flowConditionImplies()
186   llvm::SetVector<const Formula *> Constraints;  in flowConditionImplies()  local
187   Constraints.insert(&arena().makeAtomRef(Token));  in flowConditionImplies()
188   Constraints.insert(&arena().makeNot(F));  in flowConditionImplies()
189   addTransitiveFlowConditionConstraints(Token, Constraints);  in flowConditionImplies()
190   return isUnsatisfiable(std::move(Constraints));  in flowConditionImplies()
198   llvm::SetVector<const Formula *> Constraints;  in flowConditionAllows()  local
199   Constraints.insert(&arena().makeAtomRef(Token));  in flowConditionAllows()
200   Constraints.insert(&F);  in flowConditionAllows()
201   addTransitiveFlowConditionConstraints(Token, Constraints);  in flowConditionAllows()
202   return isSatisfiable(std::move(Constraints));  in flowConditionAllows()
207   llvm::SetVector<const Formula *> Constraints;  in equivalentFormulas()  local
208   Constraints.insert(&arena().makeNot(arena().makeEquals(Val1, Val2)));  in equivalentFormulas()
209   return isUnsatisfiable(std::move(Constraints));  in equivalentFormulas()
213     Atom Token, llvm::SetVector<const Formula *> &Constraints) {  in addTransitiveFlowConditionConstraints()  argument
218     Constraints.insert(Invariant);  in addTransitiveFlowConditionConstraints()
219   // Define all the flow conditions that might be referenced in constraints.  in addTransitiveFlowConditionConstraints()
228       Constraints.insert(&arena().makeAtomRef(Token));  in addTransitiveFlowConditionConstraints()
230       // Bind flow condition token via `iff` to its set of constraints:  in addTransitiveFlowConditionConstraints()
231       // FC <=> (C1 ^ C2 ^ ...), where Ci are constraints  in addTransitiveFlowConditionConstraints()
232       Constraints.insert(&arena().makeEquals(arena().makeAtomRef(Token),  in addTransitiveFlowConditionConstraints()
256   llvm::SetVector<const Formula *> Constraints;  in dumpFlowCondition()  local
257   Constraints.insert(&arena().makeAtomRef(Token));  in dumpFlowCondition()
258   addTransitiveFlowConditionConstraints(Token, Constraints);  in dumpFlowCondition()
262   llvm::SetVector<const Formula *> OriginalConstraints = Constraints;  in dumpFlowCondition()
263   simplifyConstraints(Constraints, arena(), &Info);  in dumpFlowCondition()
264   if (!Constraints.empty()) {  in dumpFlowCondition()
265     OS << "Constraints:\n";  in dumpFlowCondition()
266     for (const auto *Constraint : Constraints) {  in dumpFlowCondition()
285   OS << "\nFlow condition constraints before simplification:\n";  in dumpFlowCondition()