17 static const Formula &
18 substitute(const Formula &F,  in substitute()
19            const llvm::DenseMap<Atom, const Formula *> &Substitutions,  in substitute()
22   case Formula::AtomRef:  in substitute()
27   case Formula::Literal:  in substitute()
29   case Formula::Not:  in substitute()
31   case Formula::And:  in substitute()
34   case Formula::Or:  in substitute()
37   case Formula::Implies:  in substitute()
41   case Formula::Equal:  in substitute()
75 void simplifyConstraints(llvm::SetVector<const Formula *> &Constraints,  in simplifyConstraints()
89       case Formula::AtomRef:  in simplifyConstraints()
92       case Formula::Not:  in simplifyConstraints()
93         if (Constraint->operands()[0]->kind() == Formula::AtomRef)  in simplifyConstraints()
96       case Formula::Equal: {  in simplifyConstraints()
97         ArrayRef<const Formula *> operands = Constraint->operands();  in simplifyConstraints()
98         if (operands[0]->kind() == Formula::AtomRef &&  in simplifyConstraints()
99             operands[1]->kind() == Formula::AtomRef) {  in simplifyConstraints()
113     llvm::DenseMap<Atom, const Formula *> Substitutions;  in simplifyConstraints()
130     llvm::SetVector<const Formula *> NewConstraints;  in simplifyConstraints()
132       const Formula &NewConstraint =  in simplifyConstraints()
140       if (NewConstraint.kind() == Formula::And) {  in simplifyConstraints()