CNF

Undocumented in source.

struct CNF {

size_t variableNum;

size_t clauseNum;

Clause[Clause.ID] allClauses;

Clause[Clause.ID] normalClauses;

Clause[Clause.ID] unitClauses;

Clause[Clause.ID] emptyClauses;

Literal[][Clause.ID] literalsInClause;

Clause.ID[][Literal] clausesContainingLiteral;

this(Clause[] clauses, Preamble preamble);

void removeLiterals(Literal literal);

void removeClauseById(Clause.ID clauseId);

void removeClauseContainingLiteral(Literal literal);

void simplify(Literal literal);

string toString();

string debugString();

}

Constructors

this this(Clause[] clauses, Preamble preamble): Undocumented in source.
this this(CNF rhs): Undocumented in source.

Members

Functions

debugString string debugString(): Undocumented in source. Be warned that the author may not have intended to support it.
removeClauseById void removeClauseById(Clause.ID clauseId): Undocumented in source. Be warned that the author may not have intended to support it.
removeClauseContainingLiteral void removeClauseContainingLiteral(Literal literal): Undocumented in source. Be warned that the author may not have intended to support it.
removeLiterals void removeLiterals(Literal literal): Undocumented in source. Be warned that the author may not have intended to support it.
simplify void simplify(Literal literal): Undocumented in source. Be warned that the author may not have intended to support it.
toString string toString(): Undocumented in source. Be warned that the author may not have intended to support it.

Variables

allClauses Clause[Clause.ID] allClauses;
clauseNum size_t clauseNum;: Undocumented in source.
clausesContainingLiteral Clause.ID[][Literal] clausesContainingLiteral;: Undocumented in source.
emptyClauses Clause[Clause.ID] emptyClauses;: Undocumented in source.
literalsInClause Literal[][Clause.ID] literalsInClause;: Undocumented in source.
normalClauses Clause[Clause.ID] normalClauses;: Undocumented in source.
unitClauses Clause[Clause.ID] unitClauses;: Undocumented in source.
variableNum size_t variableNum;: Undocumented in source.

Meta

Source

See Implementation

satd cnf aliases

functions

negate

structs