CNFFormula.cpp Source File (original) (raw)

14#include "llvm/ADT/DenseSet.h"

16#include

21namespace {

34struct CNFFormulaBuilder {

36 explicit CNFFormulaBuilder(CNFFormula &CNF) : Formula(CNF) {}

46 void addClause(ArrayRef Literals) {

48 assert(!Literals.empty() && Literals.size() <= 3);

50 llvm::SmallVector 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)) {

56 return;

57 else

58 continue;

59 }

60 if (falseVars.contains(X)) {

62 return;

63 else

64 continue;

65 }

66 Simplified.push_back(L);

67 }

68 if (Simplified.empty()) {

71 Formula.addClause(Simplified);

72 return;

73 }

74 if (Simplified.size() == 1) {

76 const Literal lit = Simplified.front();

79 trueVars.insert(v);

80 else

81 falseVars.insert(v);

82 }

83 Formula.addClause(Simplified);

84 }

88 bool isKnownContradictory() { return Formula.knownContradictory(); }

90private:

91 CNFFormula &Formula;

92 llvm::DenseSet trueVars;

93 llvm::DenseSet falseVars;

94};

96}

99 : LargestVar(LargestVar), KnownContradictory(false) {

100 Clauses.push_back(0);

101 ClauseStarts.push_back(0);

102}

103

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

116 llvm::DenseMap<Variable, Atom> &Atomics) {

117

118

119

120

121

122

123

124 llvm::DenseMap<const Formula *, Variable> FormulaToVar;

125

127 {

128 std::queue<const Formula *> UnprocessedFormulas;

129 for (const Formula *F : Formulas)

130 UnprocessedFormulas.push(F);

131 while (!UnprocessedFormulas.empty()) {

133 const Formula *F = UnprocessedFormulas.front();

134 UnprocessedFormulas.pop();

135

136 if (!FormulaToVar.try_emplace(F, Var).second)

137 continue;

138 ++NextVar;

139

141 UnprocessedFormulas.push(Op);

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

154 std::vector ProcessedSubVals(NextVar, false);

155 CNFFormulaBuilder builder(CNF);

156

157

158

159 for (const Formula *F : Formulas)

160 builder.addClause(posLit(GetVar(F)));

161

162

163

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()) {

178 break;

181 break;

185

186 if (LHS == RHS) {

187

188

189

190 builder.addClause({negLit(Var), posLit(LHS)});

191 builder.addClause({posLit(Var), negLit(LHS)});

192 } else {

193

194

195

196 builder.addClause({negLit(Var), posLit(LHS)});

197 builder.addClause({negLit(Var), posLit(RHS)});

199 }

200 break;

201 }

205

206 if (LHS == RHS) {

207

208

209

210 builder.addClause({negLit(Var), posLit(LHS)});

211 builder.addClause({posLit(Var), negLit(LHS)});

212 } else {

213

214

215

217 builder.addClause({posLit(Var), negLit(LHS)});

218 builder.addClause({posLit(Var), negLit(RHS)});

219 }

220 break;

221 }

224

225

226

227

228 builder.addClause({negLit(Var), negLit(Operand)});

229 builder.addClause({posLit(Var), posLit(Operand)});

230 break;

231 }

235

236

237

238

239

240 builder.addClause({posLit(Var), posLit(LHS)});

241 builder.addClause({posLit(Var), negLit(RHS)});

243 break;

244 }

248

249 if (LHS == RHS) {

250

251

252

253 builder.addClause(posLit(Var));

254

255

256 continue;

257 }

258

259

260

261

266 break;

267 }

268 }

269 if (builder.isKnownContradictory()) {

270 return CNF;

271 }

273 UnprocessedFormulas.push(Child);

274 }

275

276

277

278

280 CNFFormulaBuilder FinalBuilder(FinalCNF);

281

282

286 }

287 }

288

289

292 if (FinalBuilder.isKnownContradictory()) {

293 break;

294 }

295 }

296

297

298 return FinalCNF;

299}

300

301}

302}

A boolean formula in 3-CNF (conjunctive normal form with at most 3 literals per clause).

size_t clauseSize(ClauseID C) const

Returns the number of literals in clause C.

CNFFormula(Variable LargestVar)

Definition CNFFormula.cpp:98

llvm::ArrayRef< Literal > clauseLiterals(ClauseID C) const

Returns the literals of clause C.

ClauseID numClauses() const

Returns the number of clauses in the formula.

void addClause(ArrayRef< Literal > lits)

Adds the L1 v ... v Ln clause to the formula.

Definition CNFFormula.cpp:104

ArrayRef< const Formula * > operands() const

@ Equal

True if LHS is false or RHS is true.

@ Implies

True if either LHS or RHS is true.

@ AtomRef

A reference to an atomic boolean variable.

@ Literal

Constant true or false.

@ Or

True if LHS and RHS are both true.

@ And

True if its only operand is false.

Dataflow Directional Tag Classes.

uint32_t ClauseID

Clause identifiers are represented as positive integers.

constexpr Literal posLit(Variable V)

Returns the positive literal V.

constexpr bool isNegLit(Literal L)

Returns whether L is a negative literal.

uint32_t Literal

Literals are represented as positive integers.

uint32_t Variable

Boolean variables are represented as positive integers.

CNFFormula buildCNF(const llvm::ArrayRef< const Formula * > &Formulas, llvm::DenseMap< Variable, Atom > &Atomics)

Converts the conjunction of Vals into a formula in conjunctive normal form where each clause has at l...

Definition CNFFormula.cpp:115

constexpr Literal NullLit

A null literal is used as a placeholder in various data structures and algorithms.

constexpr Variable var(Literal L)

Returns the variable of L.

constexpr Literal negLit(Variable V)

Returns the negative literal !V.

constexpr bool isPosLit(Literal L)

Returns whether L is a positive literal.

The JSON file list parser is used to communicate input to InstallAPI.

const half4 lit(half NDotL, half NDotH, half M)