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()
93         if (Constraint->operands()[0]->kind() == Formula::AtomRef)  in simplifyConstraints()
94           FalseAtoms.insert(Constraint->operands()[0]->getAtom());  in simplifyConstraints()
97         ArrayRef<const Formula *> operands = Constraint->operands();  in simplifyConstraints()  local
98         if (operands[0]->kind() == Formula::AtomRef &&  in simplifyConstraints()
99             operands[1]->kind() == Formula::AtomRef) {  in simplifyConstraints()
100           EquivalentAtoms.unionSets(operands[0]->getAtom(),  in simplifyConstraints()
101                                     operands[1]->getAtom());  in simplifyConstraints()
141         NewConstraints.insert(NewConstraint.operands()[0]);  in simplifyConstraints()
142         NewConstraints.insert(NewConstraint.operands()[1]);  in simplifyConstraints()