Lines Matching defs:CNF
39 CNFFormula CNF;
110 : Atomics(), CNF(buildCNF(Vals, Atomics)),
111 LevelVars(CNF.largestVar() + 1), LevelStates(CNF.largestVar() + 1) {
115 if (CNF.knownContradictory())
120 const size_t NumLiterals = 2 * CNF.largestVar() + 1;
122 for (ClauseID C = 1; C <= CNF.numClauses(); ++C) {
124 Literal FirstLit = CNF.clauseLiterals(C).front();
135 VarAssignments.resize(CNF.largestVar() + 1, Assignment::Unassigned);
138 for (Variable Var = CNF.largestVar(); Var != NullVar; --Var) {
147 if (CNF.knownContradictory()) {
148 // Short-cut the solving process. We already found out at CNF
292 CNF.startOfClause(FalseLitWatcher);
324 llvm::ArrayRef<Literal> Clause = CNF.clauseLiterals(LitWatcher);