19            const llvm::DenseMap<Atom, const Formula *> &Substitutions,  in substitute()  argument
23     if (auto iter = Substitutions.find(F.getAtom());  in substitute()
24         iter != Substitutions.end())  in substitute()
30     return arena.makeNot(substitute(*F.operands()[0], Substitutions, arena));  in substitute()
32     return arena.makeAnd(substitute(*F.operands()[0], Substitutions, arena),  in substitute()
33                          substitute(*F.operands()[1], Substitutions, arena));  in substitute()
35     return arena.makeOr(substitute(*F.operands()[0], Substitutions, arena),  in substitute()
36                         substitute(*F.operands()[1], Substitutions, arena));  in substitute()
39         substitute(*F.operands()[0], Substitutions, arena),  in substitute()
40         substitute(*F.operands()[1], Substitutions, arena));  in substitute()
42     return arena.makeEquals(substitute(*F.operands()[0], Substitutions, arena),  in substitute()
43                             substitute(*F.operands()[1], Substitutions, arena));  in substitute()
113     llvm::DenseMap<Atom, const Formula *> Substitutions;  in simplifyConstraints()  local
122         Substitutions.insert({TheAtom, &arena.makeLiteral(true)});  in simplifyConstraints()
124         Substitutions.insert({TheAtom, &arena.makeLiteral(false)});  in simplifyConstraints()
126         Substitutions.insert({TheAtom, &arena.makeAtomRef(Leader)});  in simplifyConstraints()
133           substitute(*Constraint, Substitutions, arena);  in simplifyConstraints()