Lines Matching full:constraints

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