Lines Matching refs:Atom
19 const llvm::DenseMap<Atom, const Formula *> &Substitutions, in substitute() argument
52 static llvm::DenseSet<Atom>
53 projectToLeaders(const llvm::DenseSet<Atom> &Atoms, in projectToLeaders()
54 llvm::EquivalenceClasses<Atom> &EquivalentAtoms) { in projectToLeaders()
55 llvm::DenseSet<Atom> Result; in projectToLeaders()
57 for (Atom Atom : Atoms) in projectToLeaders() local
58 Result.insert(EquivalentAtoms.getOrInsertLeaderValue(Atom)); in projectToLeaders()
65 static llvm::SmallVector<Atom>
66 atomsInEquivalenceClass(const llvm::EquivalenceClasses<Atom> &EquivalentAtoms, in atomsInEquivalenceClass()
67 llvm::EquivalenceClasses<Atom>::iterator LeaderIt) { in atomsInEquivalenceClass()
68 llvm::SmallVector<Atom> Result; in atomsInEquivalenceClass()
82 llvm::EquivalenceClasses<Atom> EquivalentAtoms; in simplifyConstraints()
83 llvm::DenseSet<Atom> TrueAtoms; in simplifyConstraints()
84 llvm::DenseSet<Atom> FalseAtoms; in simplifyConstraints()
113 llvm::DenseMap<Atom, const Formula *> Substitutions; in simplifyConstraints()
115 Atom TheAtom = It->getData(); in simplifyConstraints()
116 Atom Leader = EquivalentAtoms.getLeaderValue(TheAtom); in simplifyConstraints()
158 Atom At = *EquivalentAtoms.findLeader(It); in simplifyConstraints()
161 llvm::SmallVector<Atom> Atoms = in simplifyConstraints()
168 for (Atom At : TrueAtoms) in simplifyConstraints()
172 for (Atom At : FalseAtoms) in simplifyConstraints()