195       : Formula(CNF) {}  in CNFFormulaBuilder()
232       Formula.KnownContradictory = true;  in addClause()
234       Formula.addClause(Literals[0]);  in addClause()
246     Formula.addClause(Simplified);  in addClause()
251   bool isKnownContradictory() { return Formula.KnownContradictory; }  in isKnownContradictory()
254   CNFFormula &Formula;  member
261 CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &Vals) {  in buildCNF()
269   llvm::DenseMap<const Formula *, Variable> SubValsToVar;  in buildCNF()
274     std::queue<const Formula *> UnprocessedSubVals;  in buildCNF()
275     for (const Formula *Val : Vals)  in buildCNF()
279       const Formula *Val = UnprocessedSubVals.front();  in buildCNF()
286       for (const Formula *F : Val->operands())  in buildCNF()
288       if (Val->kind() == Formula::AtomRef)  in buildCNF()
293   auto GetVar = [&SubValsToVar](const Formula *Val) {  in buildCNF()
305   for (const Formula *Val : Vals)  in buildCNF()
310   std::queue<const Formula *> UnprocessedSubVals;  in buildCNF()
311   for (const Formula *Val : Vals)  in buildCNF()
314     const Formula *Val = UnprocessedSubVals.front();  in buildCNF()
323     case Formula::AtomRef:  in buildCNF()
325     case Formula::Literal:  in buildCNF()
328     case Formula::And: {  in buildCNF()
348     case Formula::Or: {  in buildCNF()
368     case Formula::Not: {  in buildCNF()
378     case Formula::Implies: {  in buildCNF()
391     case Formula::Equal: {  in buildCNF()
418     for (const Formula *Child : Val->operands())  in buildCNF()
503       const llvm::ArrayRef<const Formula *> &Vals)  in WatchedLiteralsSolverImpl()
787 WatchedLiteralsSolver::solve(llvm::ArrayRef<const Formula *> Vals) {  in solve()