9 //  A representation of a boolean formula in 3-CNF.
25 /// true/false in any model that satisfies the overall formula.
35   // Formula should outlive CNFFormulaBuilder.
36   explicit CNFFormulaBuilder(CNFFormula &CNF) : Formula(CNF) {}  in CNFFormulaBuilder()
38   /// Adds the `L1 v ... v Ln` clause to the formula. Applies
71       // We already know that this formula is unsatisfiable.  in addClause()
72       Formula.addClause(Simplified);  in addClause()
84     Formula.addClause(Simplified);  in addClause()
88   /// In this case then the formula is already known to be unsatisfiable.
89   bool isKnownContradictory() { return Formula.knownContradictory(); }  in isKnownContradictory()
92   CNFFormula &Formula;  member
116 CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &Formulas,  in buildCNF()
121   // literals in the resulting formula is guaranteed to be linear in the number  in buildCNF()
124   // Map each sub-formula in `Vals` to a unique variable.  in buildCNF()
125   llvm::DenseMap<const Formula *, Variable> FormulaToVar;  in buildCNF()
129     std::queue<const Formula *> UnprocessedFormulas;  in buildCNF()
130     for (const Formula *F : Formulas)  in buildCNF()
134       const Formula *F = UnprocessedFormulas.front();  in buildCNF()
141       for (const Formula *Op : F->operands())  in buildCNF()
143       if (F->kind() == Formula::AtomRef)  in buildCNF()
148   auto GetVar = [&FormulaToVar](const Formula *F) {  in buildCNF()
160   for (const Formula *F : Formulas)  in buildCNF()
165   std::queue<const Formula *> UnprocessedFormulas;  in buildCNF()
166   for (const Formula *F : Formulas)  in buildCNF()
169     const Formula *F = UnprocessedFormulas.front();  in buildCNF()
178     case Formula::AtomRef:  in buildCNF()
180     case Formula::Literal:  in buildCNF()
183     case Formula::And: {  in buildCNF()
203     case Formula::Or: {  in buildCNF()
223     case Formula::Not: {  in buildCNF()
233     case Formula::Implies: {  in buildCNF()
246     case Formula::Equal: {  in buildCNF()
273     for (const Formula *Child : F->operands())  in buildCNF()