303 lines · cpp
1//===- CNFFormula.cpp -------------------------------------------*- C++ -*-===//2//3// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.4// See https://llvm.org/LICENSE.txt for license information.5// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception6//7//===----------------------------------------------------------------------===//8//9// A representation of a boolean formula in 3-CNF.10//11//===----------------------------------------------------------------------===//12 13#include "clang/Analysis/FlowSensitive/CNFFormula.h"14#include "llvm/ADT/DenseSet.h"15 16#include <queue>17 18namespace clang {19namespace dataflow {20 21namespace {22 23/// Applies simplifications while building up a BooleanFormula.24/// We keep track of unit clauses, which tell us variables that must be25/// true/false in any model that satisfies the overall formula.26/// Such variables can be dropped from subsequently-added clauses, which27/// may in turn yield more unit clauses or even a contradiction.28/// The total added complexity of this preprocessing is O(N) where we29/// for every clause, we do a lookup for each unit clauses.30/// The lookup is O(1) on average. This method won't catch all31/// contradictory formulas, more passes can in principle catch32/// more cases but we leave all these and the general case to the33/// proper SAT solver.34struct CNFFormulaBuilder {35 // Formula should outlive CNFFormulaBuilder.36 explicit CNFFormulaBuilder(CNFFormula &CNF) : Formula(CNF) {}37 38 /// Adds the `L1 v ... v Ln` clause to the formula. Applies39 /// simplifications, based on single-literal clauses.40 ///41 /// Requirements:42 ///43 /// `Li` must not be `NullLit`.44 ///45 /// All literals must be distinct.46 void addClause(ArrayRef<Literal> Literals) {47 // We generate clauses with up to 3 literals in this file.48 assert(!Literals.empty() && Literals.size() <= 3);49 // Contains literals of the simplified clause.50 llvm::SmallVector<Literal> Simplified;51 for (auto L : Literals) {52 assert(L != NullLit && !llvm::is_contained(Simplified, L));53 auto X = var(L);54 if (trueVars.contains(X)) { // X must be true55 if (isPosLit(L))56 return; // Omit clause `(... v X v ...)`, it is `true`.57 else58 continue; // Omit `!X` from `(... v !X v ...)`.59 }60 if (falseVars.contains(X)) { // X must be false61 if (isNegLit(L))62 return; // Omit clause `(... v !X v ...)`, it is `true`.63 else64 continue; // Omit `X` from `(... v X v ...)`.65 }66 Simplified.push_back(L);67 }68 if (Simplified.empty()) {69 // Simplification made the clause empty, which is equivalent to `false`.70 // We already know that this formula is unsatisfiable.71 Formula.addClause(Simplified);72 return;73 }74 if (Simplified.size() == 1) {75 // We have new unit clause.76 const Literal lit = Simplified.front();77 const Variable v = var(lit);78 if (isPosLit(lit))79 trueVars.insert(v);80 else81 falseVars.insert(v);82 }83 Formula.addClause(Simplified);84 }85 86 /// Returns true if we observed a contradiction while adding clauses.87 /// In this case then the formula is already known to be unsatisfiable.88 bool isKnownContradictory() { return Formula.knownContradictory(); }89 90private:91 CNFFormula &Formula;92 llvm::DenseSet<Variable> trueVars;93 llvm::DenseSet<Variable> falseVars;94};95 96} // namespace97 98CNFFormula::CNFFormula(Variable LargestVar)99 : LargestVar(LargestVar), KnownContradictory(false) {100 Clauses.push_back(0);101 ClauseStarts.push_back(0);102}103 104void CNFFormula::addClause(ArrayRef<Literal> lits) {105 assert(!llvm::is_contained(lits, NullLit));106 107 if (lits.empty())108 KnownContradictory = true;109 110 const size_t S = Clauses.size();111 ClauseStarts.push_back(S);112 llvm::append_range(Clauses, lits);113}114 115CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &Formulas,116 llvm::DenseMap<Variable, Atom> &Atomics) {117 // The general strategy of the algorithm implemented below is to map each118 // of the sub-values in `Vals` to a unique variable and use these variables in119 // the resulting CNF expression to avoid exponential blow up. The number of120 // literals in the resulting formula is guaranteed to be linear in the number121 // of sub-formulas in `Vals`.122 123 // Map each sub-formula in `Vals` to a unique variable.124 llvm::DenseMap<const Formula *, Variable> FormulaToVar;125 // Store variable identifiers and Atom of atomic booleans.126 Variable NextVar = 1;127 {128 std::queue<const Formula *> UnprocessedFormulas;129 for (const Formula *F : Formulas)130 UnprocessedFormulas.push(F);131 while (!UnprocessedFormulas.empty()) {132 Variable Var = NextVar;133 const Formula *F = UnprocessedFormulas.front();134 UnprocessedFormulas.pop();135 136 if (!FormulaToVar.try_emplace(F, Var).second)137 continue;138 ++NextVar;139 140 for (const Formula *Op : F->operands())141 UnprocessedFormulas.push(Op);142 if (F->kind() == Formula::AtomRef)143 Atomics[Var] = F->getAtom();144 }145 }146 147 auto GetVar = [&FormulaToVar](const Formula *F) {148 auto ValIt = FormulaToVar.find(F);149 assert(ValIt != FormulaToVar.end());150 return ValIt->second;151 };152 153 CNFFormula CNF(NextVar - 1);154 std::vector<bool> ProcessedSubVals(NextVar, false);155 CNFFormulaBuilder builder(CNF);156 157 // Add a conjunct for each variable that represents a top-level conjunction158 // value in `Vals`.159 for (const Formula *F : Formulas)160 builder.addClause(posLit(GetVar(F)));161 162 // Add conjuncts that represent the mapping between newly-created variables163 // and their corresponding sub-formulas.164 std::queue<const Formula *> UnprocessedFormulas;165 for (const Formula *F : Formulas)166 UnprocessedFormulas.push(F);167 while (!UnprocessedFormulas.empty()) {168 const Formula *F = UnprocessedFormulas.front();169 UnprocessedFormulas.pop();170 const Variable Var = GetVar(F);171 172 if (ProcessedSubVals[Var])173 continue;174 ProcessedSubVals[Var] = true;175 176 switch (F->kind()) {177 case Formula::AtomRef:178 break;179 case Formula::Literal:180 CNF.addClause(F->literal() ? posLit(Var) : negLit(Var));181 break;182 case Formula::And: {183 const Variable LHS = GetVar(F->operands()[0]);184 const Variable RHS = GetVar(F->operands()[1]);185 186 if (LHS == RHS) {187 // `X <=> (A ^ A)` is equivalent to `(!X v A) ^ (X v !A)` which is188 // already in conjunctive normal form. Below we add each of the189 // conjuncts of the latter expression to the result.190 builder.addClause({negLit(Var), posLit(LHS)});191 builder.addClause({posLit(Var), negLit(LHS)});192 } else {193 // `X <=> (A ^ B)` is equivalent to `(!X v A) ^ (!X v B) ^ (X v !A v194 // !B)` which is already in conjunctive normal form. Below we add each195 // of the conjuncts of the latter expression to the result.196 builder.addClause({negLit(Var), posLit(LHS)});197 builder.addClause({negLit(Var), posLit(RHS)});198 builder.addClause({posLit(Var), negLit(LHS), negLit(RHS)});199 }200 break;201 }202 case Formula::Or: {203 const Variable LHS = GetVar(F->operands()[0]);204 const Variable RHS = GetVar(F->operands()[1]);205 206 if (LHS == RHS) {207 // `X <=> (A v A)` is equivalent to `(!X v A) ^ (X v !A)` which is208 // already in conjunctive normal form. Below we add each of the209 // conjuncts of the latter expression to the result.210 builder.addClause({negLit(Var), posLit(LHS)});211 builder.addClause({posLit(Var), negLit(LHS)});212 } else {213 // `X <=> (A v B)` is equivalent to `(!X v A v B) ^ (X v !A) ^ (X v214 // !B)` which is already in conjunctive normal form. Below we add each215 // of the conjuncts of the latter expression to the result.216 builder.addClause({negLit(Var), posLit(LHS), posLit(RHS)});217 builder.addClause({posLit(Var), negLit(LHS)});218 builder.addClause({posLit(Var), negLit(RHS)});219 }220 break;221 }222 case Formula::Not: {223 const Variable Operand = GetVar(F->operands()[0]);224 225 // `X <=> !Y` is equivalent to `(!X v !Y) ^ (X v Y)` which is226 // already in conjunctive normal form. Below we add each of the227 // conjuncts of the latter expression to the result.228 builder.addClause({negLit(Var), negLit(Operand)});229 builder.addClause({posLit(Var), posLit(Operand)});230 break;231 }232 case Formula::Implies: {233 const Variable LHS = GetVar(F->operands()[0]);234 const Variable RHS = GetVar(F->operands()[1]);235 236 // `X <=> (A => B)` is equivalent to237 // `(X v A) ^ (X v !B) ^ (!X v !A v B)` which is already in238 // conjunctive normal form. Below we add each of the conjuncts of239 // the latter expression to the result.240 builder.addClause({posLit(Var), posLit(LHS)});241 builder.addClause({posLit(Var), negLit(RHS)});242 builder.addClause({negLit(Var), negLit(LHS), posLit(RHS)});243 break;244 }245 case Formula::Equal: {246 const Variable LHS = GetVar(F->operands()[0]);247 const Variable RHS = GetVar(F->operands()[1]);248 249 if (LHS == RHS) {250 // `X <=> (A <=> A)` is equivalent to `X` which is already in251 // conjunctive normal form. Below we add each of the conjuncts of the252 // latter expression to the result.253 builder.addClause(posLit(Var));254 255 // No need to visit the sub-values of `Val`.256 continue;257 }258 // `X <=> (A <=> B)` is equivalent to259 // `(X v A v B) ^ (X v !A v !B) ^ (!X v A v !B) ^ (!X v !A v B)` which260 // is already in conjunctive normal form. Below we add each of the261 // conjuncts of the latter expression to the result.262 builder.addClause({posLit(Var), posLit(LHS), posLit(RHS)});263 builder.addClause({posLit(Var), negLit(LHS), negLit(RHS)});264 builder.addClause({negLit(Var), posLit(LHS), negLit(RHS)});265 builder.addClause({negLit(Var), negLit(LHS), posLit(RHS)});266 break;267 }268 }269 if (builder.isKnownContradictory()) {270 return CNF;271 }272 for (const Formula *Child : F->operands())273 UnprocessedFormulas.push(Child);274 }275 276 // Unit clauses that were added later were not277 // considered for the simplification of earlier clauses. Do a final278 // pass to find more opportunities for simplification.279 CNFFormula FinalCNF(NextVar - 1);280 CNFFormulaBuilder FinalBuilder(FinalCNF);281 282 // Collect unit clauses.283 for (ClauseID C = 1; C <= CNF.numClauses(); ++C) {284 if (CNF.clauseSize(C) == 1) {285 FinalBuilder.addClause(CNF.clauseLiterals(C)[0]);286 }287 }288 289 // Add all clauses that were added previously, preserving the order.290 for (ClauseID C = 1; C <= CNF.numClauses(); ++C) {291 FinalBuilder.addClause(CNF.clauseLiterals(C));292 if (FinalBuilder.isKnownContradictory()) {293 break;294 }295 }296 // It is possible there were new unit clauses again, but297 // we stop here and leave the rest to the solver algorithm.298 return FinalCNF;299}300 301} // namespace dataflow302} // namespace clang303