clause_graph
Clg_Conj(
clause_graph left,
clause_graph right
)
- Create a CLG representing a conjunction of two CLGs
clause_graph
Clg_Disj(
clause_graph left,
clause_graph right
)
- Create a CLG representing a disjunction of two CLGs
void
Clg_Extract(
clause_graph head,
int type,
Clg_Commit commit,
void * data
)
- Calls commit with each extracted clause as an argument.
type indicates the style of clause (eg, ZChaff
all-positive integer format); *data is passed to commit
as an extra argument.
Clauses have duplicated literals suppressed and
clauses with both positive and negative
occurrences of the same literal are skipped.
void
Clg_Free(
clause_graph graph
)
- Free all CLGs
clause_graph
Clg_Lit(
int literal
)
- Create a CLG representing a single literal
int
Clg_Size(
clause_graph graph
)
- Return the number of clauses stored in the CLG